Logic Systems Axiom List
There are a limited number of axioms used to build various modal and
non-standard logic systems.
Notes
There are any number of numbering schemes for the many of the
axioms below. In fact, a different scheme in just about every
book on the topic. There is no way to combine them and resolve the
conflicts without having to rename some.
I've tried to have a consistent naming (numbering) scheme...
There were also a number of axioms I kept having to refer to that
don't even have a name. I've given them at least something one
can refer to.
Further reading
[Hackstaff, 1966]
[Hughes and Cresswell, 1996]
Logic Structures Pages
Logic Systems Pages
Operators
- > : Material implication
- => : Strict implication
- == : Equivalence
- <=> : Strict equivalence
- & : and
- + : or
- ~ : not
- M : Possibility
- L : Necessity
Non-modal axioms
Positive Propositional Logic
- Implication
- PL1: p > (q>p)
- PL2: (p>(q>r)) > ((p>q)>(p>r))
- And
- PL3: (p&q) > p
- PL4: (p&q) > q
- PL5: p > (q > (p&q))
- Or
- PL6: p > (p+q)
- PL7: q > (p+q)
- PL8:
(p>r) > ((q>r)>((p+q)>r))
- Equivalence
- PL9:
(p==q) > (p>q)
- PL10:
(p==q) > (q>p)
- PL11:
(p>q) > ((q>p)>(p==q))
Russell and Whitehead basis for PC
- (p + p) > p
- R2: q > (p+q)
- R3: (p+q) > (q+p)
- R4: (q>r) > ((p+q)>(p+r))
Standard PC
Intuitionist PC
(Scholz and Schröter)
- IP1: (p>~p) > ~p
- IP2: ~p > (p>q)
Heyting's actual Intuitionist PC
(Heyting)
- HA1: p => (p&p)
- HA2: (p&q) => (q&p)
- HA3: (p=>q) => ((p&r)=>(q&r))
- HA4: ((p=>q) & (q=>r))=>(p=>r)
- HA5: q => (p=>q) [This is clearly
axiom PL1 in disguise]
- HA6: (p & (p=>q))=>q
- HA7: p => (p+q)
- HA8: (p+q) => (q+p)
- HA9: ((p=>r)&(q=>r)) => ((p+q)=>r)
- HA10: ~p => (p=>q)
- HA11: ((p=>q)&(p=>~q)) => ~p
[Hackstaff,
1966, p223]
Fitch Calculus
- F1: ~p > (p>q)
[Same as IP2]
- F2: p == ~~p (Often called Double Negation)
- F3: ~(p+q) == ~p&~q [DeMorgan]
- F4: ~(p&q) == ~p+~q [DeMorgan]
Johansson Minimal Calculus
- J1: (p=>q) => (~q=>~p)
- J2: ~(p&~p)
Misc. axioms.
- Axioms of quantification.
- QD: forall(x, p>φ(x)) >
(p>forall(x, φ(x))
- Spec:
forall(x, φ(x)) >φ(y)
- Axioms of equality
- [... under construction ...]
- Other
- Combinators
Modal Logic
Lewis systems:
- AS1.1: (p&q) => (q&p)
- AS1.2: (p&q) => p
- AS1.3: p => (p&p)
- AS1.4: ((p&q)&r) => (p&(q&r))
- AS1.5: ((p=>q)&(q=>r)) => (p=>r)
- AS1.6: (p&(p=>q)) => q
- AS4.1: Lp => LLp (This is the strict form of
Axiom 4)
- H1: p => (p&p)
- H2: (p&q) => p
- H3: ((r&p)&~(q&r)) => (p&~q)
- H4: ~Mp > ~p
- H5: p => Mp
- H6: (p=>q) => (~Mq=>~Mp)
- H7: MMp => Mp
- H8: Mp => ~M~Mp
- MMp
- S': LMMp
- Sb: MLMMp
- S1: (L(p>q)&L(q>r)) > L(p>r)
- S2: M(p&q) => (Mp&Mq)
- S3: (p=>q) => (~Mp=>~Mq)
- E3: L(p>q) > L(Lp>Lq)
"Standard" Modal logics
- M: L(p&q) > (Lp&Lq)
- C: (Lp&Lq) > L(p&q)
- R: L(p&q) == (Lp&Lq)
- K: L(p>q) > (Lp>Lq)
- N: L(true)
- B: p > LMp
- D: Lp > Mp
- T Lp > p
- 4: Lp > LLp
- 5: Mp > LMp
[Hughes and Cresswell call this "E"]
- G1: MLp > LMp
- MS: LMp => MLp [Hughes and Cresswell call this "M"]
- N1: L(L(p>Lp)>p) > (MLp>p)
- N1S:L(L(p>Lp)>p) => (MLp>p)
- D1: L(Lp>q) + L(Lq>p)
- F: (LMp & LMq) > M(p&q)
- W: L(Lp>p) > Lp
- H: L(Lp==p) > Lp
- Mp: Mp
- F : Lp = Mp
- HCR1: MLp > (p>Lp)
- Triv: p == Lp
- Ver: Lp
Misc. Lewis style axioms. (Following the numbering of
[Zeman, 1973]
- M1: (p&q) => (q&p) [pg. 82]
[Same as AS1.1]
- M2: (p&q) => p [pg. 82]
[Same as AS1.2]
- M3: ((p&q)&r) => (p&(q&r)) [pg. 82]
[Same as AS1.4]
- M4: p => (p&p) [pg. 82]
[Same as AS1.3]
- M5: ((p=>q)&(q=>r)) => (p=>r) [pg. 82]
[Same as AS1.5]
- M6:
p => Mp [Same as H5]
- M7: M(p&q) => p
- M8: (p=>q) => (Mp=>Mq) [pg. 161]
- M9: MMp=>Mp [pg. 178]
- M10: Mp => LMp [pg. 181]
(This is the strict form of 5)
- M13:L(L(p>Lp)>p) => (MLp>p) (Same as
N1S)
- M16: p => (MLp>Lp)
- M17: (Lp=>q) + (MLq>p)
- M18: (MLp>p) + (LMq>MLq)
- M24: Lp + ((p=>q) + (p=>~q))
Sobocinski's
- F1: ~M((p&q) & ~p)
- F2:
~M((p&q) & ~(q&p)
- F3:
~M(((p&q)&r) & ~(p&(q&r))
- F4 [Also known as Z1]:
~M(p & ~(p&p))
- F5:
~M((~M(p&~q)&~M(q&~r)) & ~ ~M(p&~r))
[Sobociński,
1962, p53]
(With Sobociński's typo of F2 fixed - JH)
Hacking's systems
- C1: p => p
- C2:
(p=>(q=>r)) => ((p=>q)=>(p=>r))
[Clearly PL2 in strict form]
- C3b:
(q=>r) => ((p=>q)=>(p=>r))
- C3a: a => (b=>a)
[Where a and b are both strict. (I.E. have the form x => y)]
[Clearly PL1 in strict and restricted form]
- C4: a => (p=>a) [Where a is strict (of the
form x=>y)]
[Sobociński,
1962, p53]
- Z1 [Also known as F1]:
~M(p & ~(p&p))
- Z2: ~M((p&q)&~q)
- Z3:
~M(((r&p)&~(q&r))&~(p&~q))
- Z4:
~(~M(p&~q)&~~M(~Mq&~~Mp))
- Z5: ~(~Mp&~~p)
von Wright's systems (Following Hilpinen's numbering)
- I1: P(r,s) + P(~r,s)
- I2:
P(p&q,r) == (P(p,r) & P(q,r&p))
- I3: O(p,r) == ~P(~p,r)
- K1: O(p+~p,r)
- K2: ~(O(p,r)&O(~p,r))
- K3: O(p&q,r) == (O(p,r)&O(q,r))
- K4: O(p,r+s) == (O(p,r)&O(p,s))
- K5: P(p,r) == ~O(~p,r)
- vC1: Oq == ~P~q
- vC2: Pq + P~q
- vC3: P(q+r) == Pq + Pr
- vC4:
O(q&~q) is not valid. ~P(q&~q) is not valid.
(The principle of Deontic contingency)
- vC5: If q and r are logically equivalent,
then Pq and Pr are logically equivalent.
Misc. (Some of these really need names.)
- R1: (p&q) > p
- (p > q) > (r > (p > q))
- (~M~p=>Mp) => (p=>~M~Mp)
- M(MMp>LMq) > (MMp>LMq)
[Georgacarakos, 1978, pg 103]
- L(Lp > q) + (LMLq > p)
[Georgacarakos,
1977, pg 480]
- (LMLp & q) > L(p + Mq)
[Georgacarakos,
1977, p483]
- (L(p>q) & L(q>r)) > L(p>r)
[Lemmon,
1957, p177]
- L(p>q) > L(LLp>Lq)
[Lemmon,
1957, p177]
- (p>q) > ((q>r)>(p>r))
[Hilbert and Bernays,
1934, p68]
- ((p>(p>q)) > (p>q)
[Hilbert and Bernays,
1959, p39]
- p > p
[Hilbert and Bernays,
1959, p39]
Cross Reference
(Grossly in progress)
- Hilbert's PL1 = Russell and Whitehead's R1
= Zeeman's C2
[Zeman,
1973, pg 109]
= Heyting's HA1
Meta Proof Notes
If a system having the rule Modus Ponens for an operator ">",
and can prove:
Then it has the Deduction theorem, and therefore allows hypothetical syllogism.
[Hackstaff,
1966, p121]
Note that the first axiom p>p [Cpp] is actually provable from
PL1 and PL2, given the rules modus ponens (for >) and universal
substitution.
Any system having Modus Ponens for an implicational operator >
and the theorem (A > (B > (A & B))) has the derived rule of
Adjunction for &.
[Simons,
1953, p313]
Go to ...
© Copyright 2006 by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/axioms/index.html
This page was last modified on January 28th, 8.