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

Definition df-ifp 1422
Description: Definition of the conditional operator for propositions. The value of if- ( ph ,  ps ,  ch ) is  ps if  ph is true and  ch if  ph false. See dfifp2 1423, dfifp3 1424, dfifp4 1425, dfifp5 1426, dfifp6 1427 and dfifp7 1428 for alternate definitions.

This definition (in the form of dfifp2 1423) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's 
[ ps ,  ph ,  ch ] corresponds to our if- ( ph ,  ps ,  ch ) (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- , 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.  , F., they are also complete.

(Contributed by BJ, 22-Jun-2019.)

Assertion
Ref Expression
df-ifp  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )

Detailed syntax breakdown of Definition df-ifp
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3wif 1421 . 2  wff if- ( ph ,  ps ,  ch )
51, 2wa 371 . . 3  wff  ( ph  /\ 
ps )
61wn 3 . . . 4  wff  -.  ph
76, 3wa 371 . . 3  wff  ( -. 
ph  /\  ch )
85, 7wo 370 . 2  wff  ( (
ph  /\  ps )  \/  ( -.  ph  /\  ch ) )
94, 8wb 188 1  wff  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
Colors of variables: wff setvar class
This definition is referenced by:  dfifp2  1423  dfifp6  1427  ifpor  1430  casesifp  1435  bj-df-ifc  31158  ifpdfan  36073  ifpnot23  36086
  Copyright terms: Public domain W3C validator