Description: Definition of the
conditional operator for propositions. The value of
if-(𝜑,
𝜓, 𝜒) is 𝜓 if 𝜑 is true and 𝜒 if 𝜑
false. See dfifp2 1008, dfifp3 1009, dfifp4 1010, dfifp5 1011, dfifp6 1012 and
dfifp7 1013 for alternate definitions.
This definition (in the form of dfifp2 1008) 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.) |