Hi Benoît, that's really interesting - I wonder why we hadn't Church's book in our Bibliography until now (I hope you will add it...). Church is (only) mentioned in the section comment of "Propositional calculus".
Also his proof of completeness is very impressive. Can we formalize it in Metamath? I think, however, we need a definition of "completeness" first - or is there already something in this direction? Regards, Alexander On Friday, May 1, 2020 at 5:23:28 PM UTC+2, Benoit wrote: > > 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 > <https://www.google.com/url?q=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FConditioned_disjunction&sa=D&sntz=1&usg=AFQjCNGlwqLBWhBQSwwSUvMnkw5xZxr18w> > > 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/a8453c50-41d4-430d-8f42-26f5b3a83bd7%40googlegroups.com.
