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

Definition df-ifp 1063
Description: Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1064, dfifp3 1065, dfifp4 1066, dfifp5 1067, dfifp6 1068 and dfifp7 1069 for alternate definitions.

This definition (in the form of dfifp2 1064) 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 1064 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
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3wif 1062 . 2 wff if-(𝜑, 𝜓, 𝜒)
51, 2wa 397 . . 3 wff (𝜑𝜓)
61wn 3 . . . 4 wff ¬ 𝜑
76, 3wa 397 . . 3 wff 𝜑𝜒)
85, 7wo 846 . 2 wff ((𝜑𝜓) ∨ (¬ 𝜑𝜒))
94, 8wb 205 1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
This definition is referenced by:  dfifp2  1064  dfifp6  1068  ifpor  1072  casesifp  1078  ifpbi123dOLD  1080  1fpid3  1083  wlk1walk  28896  upgriswlk  28898  bj-df-ifc  35457  bj-dfif  35458  bj-ififc  35459  wl-ifp-ncond1  36345  wl-ifpimpr  36347  ifpdfan  42217  ifpnot23  42229  upgrwlkupwlk  46518
  Copyright terms: Public domain W3C validator