Metamath Proof Explorer


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
----------------------------------------------------------------------

-. 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.)

Ref Expression
Assertion ax-luk3 ( 𝜑 → ( ¬ 𝜑𝜓 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 𝜑
1 0 wn ¬ 𝜑
2 wps 𝜓
3 1 2 wi ( ¬ 𝜑𝜓 )
4 0 3 wi ( 𝜑 → ( ¬ 𝜑𝜓 ) )