Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ifp Structured version   Visualization version   Unicode version

Definition df-ifp 1426
 Description: Definition of the conditional operator for propositions. The value of if- is if is true and if false. See dfifp2 1427, dfifp3 1428, dfifp4 1429, dfifp5 1430, dfifp6 1431 and dfifp7 1432 for alternate definitions. This definition (in the form of dfifp2 1427) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's corresponds to our if- (note the permutation of the first two variables). Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system if- is complete: for the induction step, consider a wff with n+1 variables; single out one variable, say ; when one sets 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- , say (resp. ); therefore, the formula if- represents the initial wff. Now, since and similar systems suffice to express if- , they are also complete. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
df-ifp if-

Detailed syntax breakdown of Definition df-ifp
StepHypRef Expression
1 wph . . 3
2 wps . . 3
3 wch . . 3
41, 2, 3wif 1425 . 2 if-
51, 2wa 371 . . 3
61wn 3 . . . 4
76, 3wa 371 . . 3
85, 7wo 370 . 2
94, 8wb 188 1 if-
 Colors of variables: wff setvar class This definition is referenced by:  dfifp2  1427  dfifp6  1431  ifpor  1434  casesifp  1439  ifpbi123d  1440  bj-df-ifc  31159  ifpdfan  36109  ifpnot23  36122  1wlkvtxiedg  39638  1wlk1walk  39648  upgr1wlkwlk  39651
 Copyright terms: Public domain W3C validator