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