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

Axiom ax-luk2 34253
Description: 2 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-2 1642 or pm2.18 128, but introduced as an axiom. The core idea behind this axiom is, that if something can be implied from both an antecedent, and separately from its negation, then the antecedent is irrelevant to the consequent, and can safely be dropped. This is perhaps better seen from the following slightly extended version (related to pm2.65 194):

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

Ref Expression
ax-luk2 ((¬ 𝜑𝜑) → 𝜑)

Detailed syntax breakdown of Axiom ax-luk2
StepHypRef Expression
1 wph . . 3 wff 𝜑
21wn 3 . 2 wff ¬ 𝜑
32, 1, 1bj-0 33492 1 wff ((¬ 𝜑𝜑) → 𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  wl-luk-pm2.18d  34259  wl-luk-ax3  34266  wl-luk-pm2.27  34268  wl-luk-id  34276
  Copyright terms: Public domain W3C validator