Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-section-impchain Structured version   Visualization version   GIF version

Theorem wl-section-impchain 32275
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.)

Hypothesis
Ref Expression
wl-section-impchain.hyp 𝜑
Assertion
Ref Expression
wl-section-impchain 𝜑

Proof of Theorem wl-section-impchain
StepHypRef Expression
1 wl-section-impchain.hyp 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator