Axiom ax-luk3 35519

Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1661 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 35517, ax-luk2 35518 and pm2.21 123 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 35531 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

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2	1	wn 3	. . 3 wff ¬ 𝜑
3		wps	. . 3 wff 𝜓
4	2, 3	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
5	1, 4	wi 4	1 wff (𝜑 → (¬ 𝜑 → 𝜓))

This axiom is referenced by:  wl-luk-con4i  35525  wl-luk-pm2.24i  35526  wl-luk-ax3  35531  wl-luk-ax1  35532  wl-luk-pm2.21  35535  wl-luk-id  35541