Axiom ax-luk3 33243

Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1582 and pm2.24 121, but introduced as an axiom. One might think that the similar pm2.21 120 ( -. ph -> ( ph -> ps ) ) 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 T. and F., 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 33241, ax-luk2 33242 and pm2.21 120 result in phi1 or phi2, meaning they always hold. But for wl-ax3 33255 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	|- ( ph -> ( -. ph -> ps ) )

Detailed syntax breakdown of Axiom ax-luk3

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2	1	wn 3	. . 3 wff -. ph
3		wps	. . 3 wff ps
4	2, 3	wi 4	. 2 wff ( -. ph -> ps )
5	1, 4	wi 4	1 wff ( ph -> ( -. ph -> ps ) )

This axiom is referenced by:  wl-con4i  33249  wl-pm2.24i  33250  wl-ax3  33255  wl-ax1  33256  wl-pm2.21  33259  wl-id  33265