Definition df-ifp 1079

Description: Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1080, dfifp3 1081, dfifp4 1082, dfifp5 1083, dfifp6 1084 and dfifp7 1085 for alternate definitions.

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

This form was chosen as the definition rather than dfifp2 1080 for compatibility with intuitionistic logic development: with this form, it is clear that if-(𝜑, 𝜓, 𝜒) implies decidability of 𝜑, which is most often what is wanted.

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 formula of n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a formula of n variables, so by the induction hypothesis it is equivalent to a formula using only the connectives if-, ⊤, ⊥, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) is equivalent to the initial formula of n+1 variables. Now, since { → , ¬ } and similar systems suffice to express the connectives if-, ⊤, ⊥, they are also complete.

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

Assertion

Ref	Expression
df-ifp	⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))

Detailed syntax breakdown of Definition df-ifp

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	wif 1078	. 2 wff if-(𝜑, 𝜓, 𝜒)
5	1, 2	wa 400	. . 3 wff (𝜑 ∧ 𝜓)
6	1	wn 3	. . . 4 wff ¬ 𝜑
7	6, 3	wa 400	. . 3 wff (¬ 𝜑 ∧ 𝜒)
8	5, 7	wo 860	. 2 wff ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))
9	4, 8	wb 209	1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))

This definition is referenced by:  dfifp2  1080  dfifp6  1084  ifpdfbi  1086  ifpor  1089  casesifp  1094  1fpid3  1098  wlk1walk  29969  upgriswlk  29971  bj-df-ifc  37154  bj-dfif  37155  bj-ififc  37156  wl-ifp-ncond1  38091  wl-ifpimpr  38093  ifpdfan  44175  ifpnot23  44187  upgrwlkupwlk  48888