Description: 1 of 3 axioms for
propositional calculus due to Lukasiewicz. Copy of
luk-1 1637 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.) |