Axiom ax-luk1

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 and imim1 , 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 ph and ps are somehow parametrized expressions, then ph -> ps states that ph strengthen ps , in that ph holds only for a (often proper) subset of those parameters making ps true. We easily accept, that when ps is stronger than ch and, at the same time ph is stronger than ps , then ph must be stronger than ch . 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 or syl . 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 ch is a variable capable of assuming an implication itself, we might find even more antecedents after some substitution of ch . 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:

( ps -> ( ch -> ( ph -> ch ) ) ) ; ( -. ph -> ( ch -> ( ph -> ch ) ) ) ; ( ps -> ( -. ps -> ( ph -> ch ) ) ) ; ( -. ph -> ( -. ps -> ( ph -> ch ) ) ) . (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-luk1	$$⊢\left(\phi \to \psi \right)\to \left(\left(\psi \to \chi \right)\to \left(\phi \to \chi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wi	$$wff\left(\phi \to \psi \right)$$
3		wch	$$wff\chi$$
4	1 3	wi	$$wff\left(\psi \to \chi \right)$$
5	0 3	wi	$$wff\left(\phi \to \chi \right)$$
6	4 5	wi	$$wff\left(\left(\psi \to \chi \right)\to \left(\phi \to \chi \right)\right)$$
7	2 6	wi	$$wff\left(\left(\phi \to \psi \right)\to \left(\left(\psi \to \chi \right)\to \left(\phi \to \chi \right)\right)\right)$$