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

Axiom ax-luk1 32873
Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 1577 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
StepHypRef Expression
1 wph . 2 wff 𝜑
2 wps . 2 wff 𝜓
3 wch . . 3 wff 𝜒
41, 3wi 4 . . 3 wff (𝜑𝜒)
52, 3, 4bj-0 32175 . 2 wff ((𝜓𝜒) → (𝜑𝜒))
61, 2, 5bj-0 32175 1 wff ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  wl-imim1i  32877  wl-imim2i  32885  wl-ax3  32887  wl-pm2.27  32889  wl-imim2  32894
  Copyright terms: Public domain W3C validator