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

[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

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

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.

# 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) => (~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.)

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

```