Description: Definition of the
conditional operator for propositions. The value of
if-(𝜑,
𝜓, 𝜒) is 𝜓 if 𝜑 is true and 𝜒 if 𝜑
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 [𝜓, 𝜑, 𝜒] 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.) |