**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).
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.) |