**Description: **Definition of the
conditional operator for propositions. The value of
if-
is if is true and if
false. See dfifp2 1423, dfifp3 1424, dfifp4 1425, dfifp5 1426, dfifp6 1427 and
dfifp7 1428 for alternate definitions.
This definition (in the form of dfifp2 1423) 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.) |