The conditional operator for propositions (now with a reference)

[Benoit]

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
 

[Alexander van der Vekens]

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

[Benoit]

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