Axiom ax-luk3

Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 and pm2.24 , but introduced as an axiom.

One might think that the similar pm2.21 ( -. ph -> ( ph -> ps ) ) is a valid replacement for this axiom. But this is not true, ax-3 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 by hand, that all possible interpretations of ax-mp , ax-luk1 , ax-luk2 and pm2.21 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 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
----------------------------------------------------------------------

	Ref	Expression
Assertion	ax-luk3	|- ( ph -> ( -. ph -> ps ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1	0	wn	|- -. ph
2		wps	|- ps
3	1 2	wi	|- ( -. ph -> ps )
4	0 3	wi	|- ( ph -> ( -. ph -> ps ) )