**Description: **Definition of the
conditional operator for propositions. The expression
if-(𝜑,
𝜓, 𝜒) is read "if 𝜑 then
𝜓
else 𝜒".
See dfifp2 1060, dfifp3 1061, dfifp4 1062, dfifp5 1063, dfifp6 1064 and dfifp7 1065 for
alternate definitions.
This definition (in the form of dfifp2 1060) 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 1060 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.) |