Hi all, A few months ago, I added the "conditional operator for propositions" to my mathbox (currently Section 21.29.1.6, beginning at http://us2.metamath.org/mpeuni/wif.html). I propose to move it to the main part for the following reasons: * it is a pretty natural operator * it is analogous to the conditional operator for classes, which is already in the main part (see ~df-if) * it is actually more fundamental than the conditional operator for classes, and the latter could be defined from it (~bj-df-ifc) in a way which is in line with the treatment of classes in set.mm (i.e. as extensions of predicates), and is similar to ~df-csb in terms of ~df-sbc and ~df-nfc in terms of ~df-nf; this would improve consistency of set.mm * I recently noticed that it is implicitly used in theorems related to the weak deduction theorem (~elimh, ~dedt), and I added the corresponding theorems expressed using "if" (~bj-elimhyp, ~bj-dedthm); I think that this makes them easier to understand * I just noticed that it appears in Mario's latest slides, among the first definitions in peano.mm0.
In a first step, I would only move the staple theorems (i.e., not the theorems related to the weak deduction theorem, and not the new definition of the conditional operator for classes), by creating a subsection just before "1.2.8 Abbreviated conjunction and disjunction of three wff's". For the labeling/token/symbol: I would like to parallel the conventions for df-sb/~df-csb or df-nf/df-nfc, that is: * tokens: ` if ` and ` if_ ` * symbol: "if" and "underlined if" * inside labels: "if" (e.g., wif, df-if, iftru, ifor...) and "ifc" (e.g., cifc, df-ifc, ifctru...). Finally, there are several possible definitions (~df-bj-if, ~bj-dfif2 through ~bj-dfif7). Which one to take as *the* definition ? The current one might be the easiest to understand. On the other hand, I think that one should take one for which the two theorems ~bj-iftru and ~bj-iffal still hold intuitionistically. I haven't checked all variants, but I think this works for ~bj-dfif2, which furthermore has no negation in it. This would favor that one. Thanks for any remarks and suggestions. Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/02c6c02e-d844-4dde-84a9-e62854e312fa%40googlegroups.com.
