Description: Definition of the
conditional operator for propositions. The expression
if-(𝜑,
𝜓, 𝜒) is read "if 𝜑 then
𝜓
else 𝜒".
See dfifp2 1048, dfifp3 1049, dfifp4 1050, dfifp5 1051, dfifp6 1052 and dfifp7 1053 for
alternate definitions.
This definition (in the form of dfifp2 1048) 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 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.) |