| Description: An implication like (𝜓 → 𝜑) with one antecedent can
easily be
extended by prepending more and more antecedents, as in
(𝜒
→ (𝜓 → 𝜑)) or (𝜃 → (𝜒 → (𝜓 → 𝜑))). I
call these expressions implication chains, and the number of antecedents
(number of nodes minus one) denotes their length. A given length often
marks just a required minimum value, since the consequent 𝜑 itself
may represent an implication, or even an implication chain, such hiding
part of the whole chain. As an extension, it is useful to consider a
single variable 𝜑 as a degenerate implication chain of
length zero.
Implication chains play a particular role in logic, as all propositional
expressions turn out to be convertible to one or more implication
chains, their nodes as simple as a variable, or its negation.
So there is good reason to focus on implication chains as a sort of
normalized expressions, and build some general theorems around them,
with proofs using recursive patterns. This allows for theorems
referring to longer and longer implication chains in an automated way.
The theorem names in this section contain the text fragment 'impchain'
to point out their relevance to implication chains, followed by a number
indicating the (minimal) length of the longest chain involved.
(Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.)
(Proof modification is discouraged.) |
