Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-luk3 | Structured version Visualization version GIF version |
Description: 3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of
luk-3 1572 and pm2.24 119, but introduced as an axiom.
One might think that the similar pm2.21 118 (¬ 𝜑 → (𝜑 → 𝜓)) 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 per
hand, that all possible interpretations of ax-mp 5, ax-luk1 32200, ax-luk2 32201
and pm2.21 118 result in phi1 or phi2, meaning they always hold. But for
wl-ax3 32214 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 ----------------------------------------------------------------------
Implication is defined as ----------------------------------------------------------------------
(Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
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 (𝜑 → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This axiom is referenced by: wl-con4i 32208 wl-pm2.24i 32209 wl-ax3 32214 wl-ax1 32215 wl-pm2.21 32218 wl-id 32224 |
Copyright terms: Public domain | W3C validator |