Following the recent move of the conditional operator on propositions ~df-ifp (https://groups.google.com/d/topic/metamath/zq_oZ15SFc8/discussion) to the main part of set.mm and the related work of Richard Penner, I searched a bit and finally found a reference (it should not come as a surprise that such a fundamental connective had already been studied). The reference is
Alonzo Church, Introduction to Mathematical Logic, Princeton University Press, 1956. In Section II.24 page 129, he introduces what he calls the "conditioned disjunction", with the notation [ps, ph, ch] which corresponds to our if- ( ph , ps , ch ) (note the permutation of the first two variables). Interestingly, his definition (Definition D12 page 132) is the one I originally proposed and which is now ~dfifp2. I'll add this reference to set.mm. See also https://en.wikipedia.org/wiki/Conditioned_disjunction He uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. It's pretty clever and it makes every step very easy. The first result is that the system {if-, T., F.} is complete: for the induction step, consider a wff with n+1 variables. Single out one variable, say ph. When one sets ph to True (resp. False), then what remains is a wff of n variables, so by the induction hypothesis it corresponds to a formula using only {if-, T., F.}, say ps (resp. ch). Therefore, the formula if- ( ph , ps , ch ) represents the initial wff. Now, since {->, -.} and similar systems suffice to express if-, T. and F., they are also complete. 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/00619ac2-f1e1-4471-b91d-d806e44d93c9%40googlegroups.com.
