Axiom ax-luk1 35517

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 1659 and imim1 83, but introduced as an axiom. It focuses on a basic property of a valid implication, namely that the consequent has to be true whenever the antecedent is. So if 𝜑 and 𝜓 are somehow parametrized expressions, then 𝜑 → 𝜓 states that 𝜑 strengthen 𝜓, in that 𝜑 holds only for a (often proper) subset of those parameters making 𝜓 true. We easily accept, that when 𝜓 is stronger than 𝜒 and, at the same time 𝜑 is stronger than 𝜓, then 𝜑 must be stronger than 𝜒. This transitivity is expressed in this axiom.

A particular result of this strengthening property comes into play if the antecedent holds unconditionally. Then the consequent must hold unconditionally as well. This specialization is the foundational idea behind logical conclusion. Such conclusion is best expressed in so-called immediate versions of this axiom like imim1i 63 or syl 17. Note that these forms are weaker replacements (i.e. just frequent specialization) of the closed form presented here, hence a mere convenience.

We can identify in this axiom up to three antecedents, followed by a consequent. The number of antecedents is not really fixed; the fewer we are willing to "see", the more complex the consequent grows. On the other side, since 𝜒 is a variable capable of assuming an implication itself, we might find even more antecedents after some substitution of 𝜒. This shows that the ideas of antecedent and consequent in expressions like this depends on, and can adapt to, our current interpretation of the whole expression.

In this axiom, up to two antecedents happen to be of complex nature themselves, i.e. are an embedded implication. Logically, this axiom is a compact notion of simpler expressions, which I will later coin implication chains. Herein all antecedents and the consequent appear as simple variables, or their negation. Any propositional expression is equivalent to a set of such chains. This axiom, for example, is dissected into following chains, from which it can be recovered losslessly:

(𝜓 → (𝜒 → (𝜑 → 𝜒))); (¬ 𝜑 → (𝜒 → (𝜑 → 𝜒))); (𝜓 → (¬ 𝜓 → (𝜑 → 𝜒))); (¬ 𝜑 → (¬ 𝜓 → (𝜑 → 𝜒))). (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-luk1	⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Detailed syntax breakdown of Axiom ax-luk1

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. 2 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 3	wi 4	. . 3 wff (𝜑 → 𝜒)
5	2, 3, 4	bj-0 34649	. 2 wff ((𝜓 → 𝜒) → (𝜑 → 𝜒))
6	1, 2, 5	bj-0 34649	1 wff ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

This axiom is referenced by:  wl-luk-imim1i  35521  wl-luk-imim2i  35529  wl-luk-ax3  35531  wl-luk-pm2.27  35533  wl-luk-imim2  35538