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

Axiom ax-luk3 32202
Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1572 and pm2.24 119, but introduced as an axiom. One might think that the similar pm2.21 118 𝜑 → (𝜑𝜓)) is a valid replacement for this axiom. But this is not true, ax-3 8 is not derivable from this modification. This can be shown by designing carefully operators ¬ and on a finite set of primitive statements. In propositional logic such statements are and , but we can assume more and other primitives in our universe of statements. So we denote our primitive statements as phi0 , phi1 and phi2. The actual meaning of the statements are not important in this context, it rather counts how they behave under our operations ¬ and , and which of them we assume to hold unconditionally (phi1, phi2). For our disproving model, I give that information in tabular form below. The interested reader may check per hand, that all possible interpretations of ax-mp 5, ax-luk1 32200, ax-luk2 32201 and pm2.21 118 result in phi1 or phi2, meaning they always hold. But for wl-ax3 32214 we can find a counter example resulting in phi0, not a statement always true. The verification of a particular set of axioms in a given model is tedious and error prone, so I wrote a computer program, first checking this for me, and second, hunting for a counter example. Here is the result, after 9165 fruitlessly computer generated models:

ax-3 fails for phi2, phi2
number of statements: 3
always true phi1 phi2

Negation is defined as
----------------------------------------------------------------------
-. phi0-. phi1-. phi2
phi1phi0phi1

Implication is defined as
----------------------------------------------------------------------
p->qq: phi0q: phi1q: phi2
p: phi0phi1phi1phi1
p: phi1phi0phi1phi1
p: phi2phi0phi0phi0

(Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.)
Assertion
Ref Expression
ax-luk3 (𝜑 → (¬ 𝜑𝜓))

Detailed syntax breakdown of Axiom ax-luk3
StepHypRef Expression
1 wph . 2 wff 𝜑
21wn 3 . . 3 wff ¬ 𝜑
3 wps . . 3 wff 𝜓
42, 3wi 4 . 2 wff 𝜑𝜓)
51, 4wi 4 1 wff (𝜑 → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
This axiom is referenced by:  wl-con4i  32208  wl-pm2.24i  32209  wl-ax3  32214  wl-ax1  32215  wl-pm2.21  32218  wl-id  32224
  Copyright terms: Public domain W3C validator