There are a limited number of axioms used to build various modal and non-standard logic systems.

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.

- > : Material implication
- => : Strict implication
- == : Equivalence
- <=> : Strict equivalence
- & : and
- + : or
- ~ : not
- M : Possibility
- L : Necessity

- Implication
- And
- Or
- Equivalence

Russell and Whitehead basis for PC

- PC1: (~p>~q) > (q>p)

Intuitionist PC (Scholz and Schröter)

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

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

Misc. axioms.

- Axioms of quantification.
- Axioms of equality
- [... under construction ...]

- Other
- Peirce: ((p>q)>p)>p [CCCpqpp]

- Combinators
- K: p > (q>p) [CpCqp]
- C: (p>(q>r)) > (q>(p>r)) [CCpCqrCqCpr]
- B: (p>q) > ((r>p)>(r>q)) [CCpqCCrpCrq]
- B': (p>q) > ((q>r)>(p>r)) [CCpqCCqrCpr]
- W: (p>(p>q)) > (p>q) [CCpCpqCpq]
- I: p > p [Cpp]
- S: (p>(q>r)) > ((p>q)>(p>r)) [CCpCqrCCpqCpr]

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) => (~Mq=>~Mp)
- 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]

(Grossly in progress)

If a system having the rule Modus Ponens for an operator ">",
**and** can prove:

- I: p>p [Cpp] (This is the "I" combinator)
- PL1:p>(q>p) [CpCqp] (This is the K combinator)
- PL2:(p>(q>r))>((p>q)>(p>r)) [CCpCqrCCpqCpr] (This is the S combinator)

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]

© Copyright 2006-2010 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 October 13th, 2009.