On Saturday, October 5, 2019 at 6:53:27 AM UTC-4, Benoit wrote: > > 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 agree it is more fundamental. My main concern is how useful would it be. Unlike the present df-if, where the need arises frequently, I don't think we have encountered much need for a predicate version. Does anyone know what existing theorems or proofs would benefit from it? In any case, I wouldn't like to see the present df-if defined in terms of it. I find bj-df-ifc somewhat confusing at first, at least for me, requiring that I unwrap a couple of layers of abstraction in my head to understand the otherwise simple idea. At a minimum it requires unnecessarily learning an extra definition that the reader probably won't encounter otherwise. > > * 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 agree they would make these easier to understand. However, these theorems are just for illustration and used for anything, so it wouldn't make much difference to set.mm as a whole. Even the more useful class versions (~elimhyp, ~dedth) are falling out of favor and used less and less. > * I just noticed that it appears in Mario's latest slides, among the first > definitions in peano.mm0. > Mario, do you use it much, and in what situations? > > 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. > If we do adopt it, I think bj-dfif5 is better (classically at least), for the same reason that the present df-if is more intuitive than dfif2 even though df-if has one more symbol. I would have to think hard and maybe even write down a truth table to figure out what bj-dfif2 is saying. The negation is important for the intuitive "alternation" idea: when ph is true it is this, or when ph is not true it is that. While df-bj-if is closer to the intuitive idea, we still have that if ph is false then (ph -> ps) is true, yet the final result is ch, a kind of counter-intuitive inversion. To me, the pure ANDs and ORs of bj-dfif5 are clearer. Let us hear what others think before deciding. Norm -- 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/7a215d32-31ba-4c14-8ed0-587f2ef1f1a4%40googlegroups.com.
