The reference and the above explanations have been added to http://us2.metamath.org/mpeuni/df-ifp.html and http://us2.metamath.org/mpeuni/dfifp2.html
On Saturday, May 2, 2020 at 9:18:03 AM UTC+2 Alexander van der Vekens wrote: > 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? > To formalize this completeness proof in Metamath, one needs to formalize the Metamath language, at least the propositional calculus part. This is the object of "Metamath in Metamath", which was started by Mario and is now dormant, since his priority switched to "Metamath Zero in Metamath Zero", the latter language being adapted to this purpose. Benoit 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/08b95496-b31a-43ef-ac32-5889e5d65253n%40googlegroups.com.
