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 35152
Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1659 and pm2.24 124, but introduced as an axiom. One might think that the similar pm2.21 123 𝜑 → (𝜑𝜓)) 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 by hand, that all possible interpretations of ax-mp 5, ax-luk1 35150, ax-luk2 35151 and pm2.21 123 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 35164 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 phi1 phi0 phi1

Implication is defined as
----------------------------------------------------------------------
 p->q q: phi0 q: phi1 q: phi2 p: phi0 phi1 phi1 phi1 p: phi1 phi0 phi1 phi1 p: phi2 phi0 phi0 phi0

(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-luk-con4i  35158  wl-luk-pm2.24i  35159  wl-luk-ax3  35164  wl-luk-ax1  35165  wl-luk-pm2.21  35168  wl-luk-id  35174
 Copyright terms: Public domain W3C validator