Definition df-ifp 1013

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 1014, dfifp3 1015, dfifp4 1016, dfifp5 1017, dfifp6 1018 and dfifp7 1019 for alternate definitions.

This definition (in the form of dfifp2 1014) 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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	wif 1012	. 2 wff if- ( ph , ps , ch )
5	1, 2	wa 384	. . 3 wff ( ph /\ ps )
6	1	wn 3	. . . 4 wff -. ph
7	6, 3	wa 384	. . 3 wff ( -. ph /\ ch )
8	5, 7	wo 383	. 2 wff ( ( ph /\ ps ) \/ ( -. ph /\ ch ) )
9	4, 8	wb 196	1 wff (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )

This definition is referenced by:  dfifp2  1014  dfifp6  1018  ifpor  1021  casesifp  1026  ifpbi123d  1027  1fpid3  1029  wlk1walk  26535  upgriswlk  26537  bj-df-ifc  32565  ifpdfan  37810  ifpnot23  37823  upgrwlkupwlk  41721