Logic Systems

This page is the actual full page of serious references. If you are looking for just a few systems but lots of flashy diagrams, you want http://www.cc.utah.edu/~nahaj/logic/structures/ which also gives an explaination of notations used and other housekeeping information.

This started as a list of Modal Logic systems I encountered. In the end it is a list of mostly modal logic systems. (But even at that, the list has grown LARGE.) Dr. Peter Suber has a list of the types of logics that covers the various types. It provides a bibliography of the various kinds of logics for a much wider class of logics than I cover, but no cross references of alternate names, and few individual representitives.

This list documents the fact that many systems have been investigated under different names, and that some names have historically been applied to several different systems. I'm not aware of any other such cross reference on the net (or anywhere else). If you are aware of such a reference, please drop me a line.

"To do" list

Jump to systems starting with: 0-9 | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

Jump to start of systems
Jump to Georgacarakos' "J" systems
Jump to Lewis' "S" systems
Sobociński's "K" sytems
Sobociński's "Z" systems
Bibliography

- 0-9 -

0p is called the Trivial System
"10 modalities calculus" (Becker) =[Parry, 1953, p150]= S5 (Lewis)
2' (Feys) =[Feys, 1965, p123]= T (Feys)
2r (Pledger) =[Pledger 1972 p270]= S5 (Lewis)
3q (Pledger) =[Pledger, 1972, p270]= K2 (Sobociński)
4q (Pledger) =[Pledger, 1972, p270]= K1 (Sobociński) =[Pledger, 1972, p270]= S4.1 (McKinsey) = [Pledger, 1972, p270]= S4M
4s =[Pledger, 1972, p270]= S4.2 (P.T. Geach)
6p (Pledger)
- 6pa (Pledger)
6s (Pledger) = ([Pledger, 1972, 271]) S4 (Lewis)
8p (Pledger)
- 8pa (Pledger) =[Pledger 1972, p279]= 8pc (Pledger) =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
- 8pb (Pledger) = 8pc =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
- 8pc (Pledger) =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
8q (Pledger)
- 8qa (Pledger)
10p (Pledger)
- 10pa (Pledger) reduces to 10pb (Pledger)
- 10pb (Pledger)
- 10pc (Pledger) = S8 (Alban) [Pledger, 1972, 271]
10r (Pledger)
- 10ra (Pledger)
12p (Pledger)
- 12pa (Pledger)
- 12pb (Pledger)
- 12pc (Pledger) reduces to 10pc (Pledger) = S8 (Alban)
12q (Pledger)
- 12qa (Pledger) reduces to 12qb (Pledger)
- 12qb (Pledger)
- 12qc (Pledger) reduces to 10pc (Pledger) = S8 (Alban)
12r (Pledger) = S3.5 (Åqvist) [Pledger, 1972, 271]
- 12ra (Pledger) reduces to 8pc =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
- 12rb (Pledger) reduces to 8pc =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
- 12rc (Pledger) reduces to 8pc =[Pledger 1972, p279]= S9 (Hughes and Cresswell)
12s (Pledger)
- 12sa (Pledger)
14q (Pledger)
- 14qa (Pledger)
- 14qb (Pledger)
- 14qc (Pledger) reduces to 10pc (Pledger) = S8 (Alban)
14r (Pledger)
- 14ra reduces to 14rb (Pledger)
- 14rb (Pledger)
- 14rc reduces to 10pc (Pledger) = S8 (Alban)
16s (Pledger) =[Sobociński, 1976a]= S3.01 (Sobociński)
- 16sa (Pledger) reduces to 16sb (Pledger)
- 16sb (Pledger)
- 16sc (Pledger) reduces to 10pc (Pledger) = S8 (Alban)
18r (Pledger)
- 18ra (Pledger)
- 18rb (Pledger)
- 18rc reduces to 10pc (Pledger) = S8 (Alban)
20s (Pledger) =[Pledger, 1972, 271]= S3 (Lewis)
- 20sa (Pledger) =[Pledger, 1972, 277]= S7 (Halldén)
- 20sb (Pledger) =[Pledger, 1972, 277-fn4]= S7.5 (Anderson)
- 20sc (Pledger) reduces to 10pc (Pledger) = S8 (Alban)

- A -

Aristotle (Αριστοτἑλης)

- B -

B (Brouwer) =[Chellas 1980, p131]= KTB =[Priest, 2001, p39]= = Kρσ
B (Moh Shaw-Kwei) [Feys, 1965, p139] (Quoting [Shaw-Kwei, 1958] "Modal systems with a finite number of Modalities" in the Journal Scientia Sinica #7, p388-412)
- B₁ (Moh Shaw-Kwei)
- B₂ (Moh Shaw-Kwei)
- B₃ (Moh Shaw-Kwei)
- ... B_n (Moh Shaw-Kwei) ... Infinite number of systems.
BCI (Meredith)
BCK (Meredith)
BCSK (Spinks) (Humberstone) [Humberstone, 2000]

- C -

C disambiguation
- C (Makinson) [Makinson, 1969, JSL]
- C (Chellas) [Priest, 2001, p74] (Original source is Chellas 1975, Journal of Philosophical Logic)
- C [Relevant Logic] =[Priest, 2001, p218]= RW
C (Chellas) [Priest, 2001, p74]
- C₁ (da Costa) [Priest, 2001, p88]
- C₂ (da Costa) [Priest, 2001, p88]
- ... C_n (Da Costa) ... Infinite number of systems
CLC (Bull) - implicational fragment of Dummett's LC [Bull, 1962]
CH (Bull) - implicational fragment of Heyting's Calculus [Bull, 1962]
C1 - Strict implicational fragment of S1
C2 - Strict implicational fragment of S2
C3 (Hacking) - Strict implicational fragment of S3
C4 (Anderson and Belnap) - Strict implicational fragment of S4 Also (Hacking)
- ?? - Strict implicational fragment of S4⁰ (Zeman) [Zeman 1979, NDJFL]
C5 - Strict implicational fragment of S5 (Lewis)
CT (Hacking) - Strict implicational fragment of T (Feys)
- ?? (Zeman)- Strict implicational fragment of T⁰ [Zeman 1979, NDJFL]
CM - Strict implicational fragment of M

- D -

D Disambiguation

D (Lemmon and Scott) = KD [Chellas, 1980, p131] = Kη [Priest, 2001, p39]
D (Prior) = [Zeman, 1973, p245]= S4.3.1 (Sobociński)

Systems:

D1 (Lemmon)
D2
- D2 (Lemmon)
- D2 (Jaskowski)
D3 (Lemmon)
D4
- D4 (Lemmon)
- D4 (D+4)
D45 (D+4+5)
D5
- D5 (Lemmon)
- D5 (D+5)

Deontic (or Deontik) Disambiguation

- E -

E disambiguation The System E can be:
- E = Equivalence Logic
- E (Anderson and Belnap) [Anderson and Belnap, 1962]
- E₁ (Anderson and Belnap) [Anderson and Belnap, 1962]
- E (Challas and others) Used to form:
  - EC
  - EK4
- E (H.B. Smith) [not named by Smith, but later by the late C. West. Churchman's "Towards a general logic of propositions"]
E1 (Lemmon)
E2 (Lemmon)
- E2⁰
E3 (Lemmon)
- E3⁰
E4 (Lemmon)
E5 (Lemmon)
E6
- E6⁰
E7
- E7⁰
EM (Challas) = M [Chellas, 1980, p237]
EMN
EN
EV [von Wright, 1951, p42] (Where he also creates system VE)
E+ [Hughes and Cresswell, 1996, p364]

- F -

- G -

G (Boolos) = KW (Segerberg) [Hughes & Cresswell, 1996, p139] = K4W [Boolos, 1993, p272 (index entry)] = PrL [Boolos, 1993, p272 (index entry)] = GL [Boolos, 1993, xvi]
- Boolos' GL is the same as KW (Segerberg) [Boolos, 1993, p272 (index entry)] [Boolos, 1993, xvi]
  - GLS (Boolos)
  - GLB (Boolos)

- H -

H Disambiguation

H (For Henkin) [Boolos, 1993, p149]
H (For Heyting) [McKinsey and Tarski, 1948]

Systems

HIC ("Heyting's Intuitionist Calculus")
HPC ("Heyting's Predicate Calculus") [Kreisel, JSL, 1962, p139]

- I -

I [Kripke, 1963]
ICI (Intuitionist Calculus of Implication) is also called PIC (Positive Implicational Calculus) [Zeman, 1973]
IIC "Implications fragment of the Intuitionist Calculus" [Bull, 1962]
Inconsistent Systems
Intuitionist PC
I4⁰ (Zeman)
IQ (Zeman) ["Implicit quantification"]
IT⁰ (Zeman)

- J -

J (Brown) [Brown, 1982, NDJFL]
J systems of Georgacarakos (Note that Pledger points out [Pledger, 1980, pg683] that Georgacarakos' J1 - J3 are three representitives of a much larger family of logics. -JH)
- J1 (Georgacarakos)
- J2 (Georgacarakos)
- J3 (Georgacarakos) = 8p (Pledger) [Pledger, 1980, p 683]
Johansson's Minimal Calculus (Johansson)

- K -

K (Segerberg) [Also called RN, MCN, EMCN]
- KC [Chagrov and Zakharyaschev, 1997]
- KF (Lemmon) [Lemmon and Scott, 1977]
- KH
- Kρ = T (Feys) [Priest, 2001, p39]
- Kρσ = B (Brower) [Priest, 2001, p39]
- Kρη = D (Lemmon) [Priest, 2001, p39]
- Kρτ = S4 (Lewis) [Priest, 2001, p39]
- Kρστ = S5 (Lewis) [Priest, 2001, p39]
- KT5 (K+T+5) =[Chellas, 1980, p139]= S5(Lewis)
- KW (Segerberg) = G (Boolos) [Hughes & Cresswell, 1996, p139] = GL (Boolos) [Boolos, 1993, xvi], = K4W [Boolos, 1993, p272 (index entry)] = PrL [Boolos, 1993, p272 (index entry)])
- K_T (Lemmon)
- K_B
- K_L
K1 (Sobociński) = S4M [Pledger, 1972, p270] = S4.1 (McKinsey) [Hughes and Cresswell, 1996, p143 (Ch 7, fn7)] = 4q (Pledger) [Pledger, 1972, p270]
- K1.1 (Sobociński)
  - K1.1.5
- K1.2 (Sobociński)
K2 (Sobociński)
- K2.1 (Sobociński)
K3 (Sobociński)
- K3.1 (Sobociński)
- K3.2
K4 disambiguation page
- K4 formed by system K + axiom Lp > LLp
  - KD4
  - K4W = KW (Segerberg) = G [Hughes and Cresswell, 1996, p139] = GL [Boolos, 1993, xvi] = PrL [Boolos, 1993, p272 (index entry)])
  - K4Z
- K4 (Sobociński) formed from system S4.4 plus the axiom LMp=>MLp
  - K4.1
  - K4.2
    - K4.2.1
    - K4.2Z
    - K4.2W
  - K4.3
    - K4.3.1
    - K4.3W
    - K4.3Z
K5 (Sobociński)
KE
KTB = B [Chellas, 1980, p131]

- L -

L Disambiguation

L (Curry) [Mentioned in Feys, 1965]
L (Emch) [Emch, 1936]
L (Church) [Church, 1936]
Ł (Łukasiewicz) [Smiley, NDJFL, 1961]
- Ł_ℵ (Łukasiewicz) [Priest, 2001, 217-218]
L (Kohn) [Kohn, 1977, NDJFL]

Systems

LA (?) [Curry, 1952, JSL V17 #2 (1952), p98-104]
LC (Dummett) [Dummett, 1959]
LD (Johansson) [Curry, 1952, JSL, v17, #1 (1952), 35-42]
LFX (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
LIC (Bull) [Bull, 1962]
LJ (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
LK (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
- LKY (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
LL (for Lewis and Langford) is a common late 1930's term for system S (Lewis) which was eventually called S3 (Lewis)
LM (Curry) [Curry, 1952, JSL V17 #2, p98-104]
- LMF (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
- LM* (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
LX (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]
- LXF (Curry) [Curry, 1952, JSL V17 #2 (1952), p98-104]

- M -

M Disambiguation

M (von Wright) is T (Feys) [Hughes & Cresswell, 1968, p125]
M (Chellas) = EM [Chellas, 1980, p237]
M (Megill and Bunder) [Megill and Bunder, 1996]

Systems:

MIPQ (Prior) [Prior, 1957 Time and modality.] [Bull 1964, p142]
The Marked system (Lp == Mp) (Halleck) is KF (Lemmon)
M' (von Wright) [von Wright, 1951, p84-85] is S4 (Lewis)
M'' (von Wright) [von Wright, 1951, p84-85]
M₁ [von Wright, 1951, p8]
M₂ [von Wright, 1951, p57]

- N -

N [Vredenduin, 1939]
νSa (Porte) [Feys, 1965, p142]
- νρSa (Porte) [Feys, 1965, p143]
  - νρνSa (Porte) = νρνρSa (Porte) = ρνSc (Porte) = ρνρSc (Porte) [Feys, 1965, p143]
    - νρνρSa (Porte) = νρνSa (Porte) [Feys, 1965, p143]
νSb (Porte) = νSc (Porte) [Feys, 1965, p142]
- νρSb (Porte) [Feys, 1965, p143]
  - νρνSb (Porte) = νρνρSb (Porte) [Feys, 1965, p143]
    - νρνρSb (Porte) = νρνSb (Porte) [Feys, 1965, p143]
νSc (Porte) = νSb (Porte) Feys, 1965, p142]
- νρSc (Porte) = S4 (Lewis) [Feys, 1965, p143]
  - νρνSc (Porte) = νρνρSc (Porte) [Feys, 1965, p143]
    - νρνρSc (Porte) = νρνSc (Porte) [Feys, 1965, p143]

- O -

OIC (Bull) [Bull, 1964a] [Meredith, 1966]

- P -

P₊ disambiguation
- P₊ (Hackstaff) = PPL [Hackstaff, 1966, p50]
- P₊ (Church) [Hackstaff, 1966, p50 fn]

P1 (Lemmon) = S1 (Lewis) [Lemmon, 1957, p178]
P2 (Lemmon) = S2 (Lewis) [Lemmon, 1957, p178]
P3 (Lemmon) = S3 (Lewis) [Lemmon, 1957, p178]
P4 (Lemmon) = S4 (Lewis) [Lemmon, 1957, p178]
P5 (Lemmon) = S5 (Lewis) [Lemmon, 1957, p178]
PIC (Positive Implicational Calculus) = ICI
PC ("Standard")
PC (Intuitionist)
PCI The pure implicational fragment of PC
Prl = KW (Segerberg) = G (Boolos) [Hughes and Cresswell, 1996, p139] = GL [Boolos, 1993, xvi], = K4W [Boolos, 1993, p272 (index entry)]
Positive Propositional Logic (PPL)
- PPL (Hilbert) = P₊ (Hackstaff) [Hackstaff, 1966, p50]
- PPL (Church) [Hackstaff, 1966, p50 footnote]
P-W (Anderson and Belnap) [Anderson and Belnap, "Entailment"]

- Q -

Q (Prior) [Hughes and Cresswell, 1968, p303-305]
QML (Barcan)

- R -

R = EMC [Chellas, 1980, p237]
R* (Routley) [NDJFL, Vol 7 (1966), pg 251-276]
+R* (Routley) [NDJFL, Vol 11, #3, 1970, page 295]
R1 (Canty) [Canty, 1965a]
- R1 (Canty)
- R1⁰ (Canty)
- R1* (Canty)
R2 (Canty) [Canty, 1965a]
- R2 (Canty)
- R2⁰ (Canty)
- R2* (Canty)
R3 (Canty) = S3 (Lewis) [Canty, 1965a, p317]
- R3⁰ = S3⁰ (Sobociński) [Canty, 1965a, p317]
- R3* = S3* (Sobociński) [Canty, 1965a, p314]
RW = C (Chellas) [Priest, 2001, p74]
ρSa (Porte) = ρSb (Porte) [Feys, 1965, p143]
- ρνSa (Porte) [Feys, 1965, p143]
  - ρνρSa (Porte) [Feys, 1965, p143]
ρSb (Porte) = ρSa (Porte) [Feys, 1965, p143]
- ρνSb (Porte) [Feys, 1965, p143]
  - ρνρSb (Porte) [Feys, 1965, p143]
ρSc (Porte) [Feys, 1965, p143]
- ρνSc (Porte) = ρνρSc (Porte) = νρνSc (Porte) = νρνSc (Porte) [Feys, 1965, p143, p144]
  - ρνρSc (Porte) = ρνSc (Porte) = νρνSc (Porte) = νρνSc (Porte) [Feys, 1965, p143, p144]

- S -

S disambiguation
- S (Lewis) [C.I.Lewis, 1936, p77] (referencing [Lewis & Langford, 1932, chapter 6]) With the ACTUAL source being : [Lewis, 1918, Chapter 5] (The final version of this system is equivalent to system S3 (Lewis), but is being kept separate for reasons of historical importance)
- S (Rubin) [Canty, 1965]
S0 (Halldén) [Halldén, 1948] (As quoted by [Feys, 1965, p139], quoting Halldén's paper in "Theoria", Volume 14, p265-269)
- S0.5 (Lemmon) [Lemmon 1957, p181]
  - S0.5⁰
- S0.9 (Lemmon) [Lemmon 1957, p180]
  - S0.9⁰
S.1 (Parry) Mentioned by [Lemmon 1957, p181fn]
S1 (Lewis)
- S1⁰ (Feys) [Sobociński, 1962, p53]
S2 (Lewis)
- S2⁰ (Feys) [Sobociński, 1962, p53]
- S2' (Feys) is T [Feys, 1965, p123]
S3 (Lewis) = 20s [Pledger, 1972, p271] [ And historicly, S3 (Lewis) = S (Lewis) = LL (Lewis and Langford), see teh S (Lewis) page for details. ]
- S'3 (Moh Shaw-Kwei) [Feys, 1965, p140,139]
- S3* (Sobociński) [Sobociński, 1962, p53] = R1* (Canty) [Canty, 1965a, p317]
  - S3** (Thomas) [Thomas, 1973, NDJFL]
- S3⁰ (Sobociński) [Sobociński, 1962, p53] = R1⁰ (Canty) [Canty, 1965a, p317]
- S3.01 (Sobociński) is 16s (Pledger) [Sobociński, 1976a]
- S3.02 (Sobocinski) = S3.03 (Sobociński) [Schumm, 1974]
  - S3.02⁰ (Sobociński) [Sobociński, 1976a]
- S3.03 (Sobociński) [Pledger, 1975, pg.271]
  - S3.03⁰ (Sobociński) [Sobociński, 1976a]
- S3.04 (Sobociński) [Pledger, 1975, pg.271]
  - S3.04⁰ (Sobociński) [Sobociński, 1976a]
- S3.3 (Hughes & Cresswell) [Hughes & Cresswell, 1968, 265] is actually S3.5 (Åqvist). [Pledger, 1972, sec 6, p276] [Pledger, 2000]
- S3.5 (Åqvist) = 12r (Pledger) [Pledger, 1972, p271]
- S3(S) (Lemmon) = S3.5 (Åqvist) = 12r (Pledger) [Pledger 2000] [Rennie, 1968 (JSL), p444]
S4 (Lewis) = KT4 = 6s (Pledger) [Pledger, 1972, p271] = Kρτ [Priest, 2001, p39] = νρSc (Porte) [Feys, 1965, p144]
- S4* (Kanger) = S4 (Lewis) [Feys, 1965, p178-185] [Hughes and Cresswell, 1996, p344]
- S4* (Onishi and Matsumoto) = S4 (Lewis) [Feys, 1965, p176-178]
- S4⁰ (Sobociński) [Sobociński, 1962, p53]
- S4.01 [Goldblatt, 1973a]
- S4.02 (Sobociński) [Sobociński, 1971]
- S4.03 (Georgacarakos) = S4.03 (Lenzen) [Lenzen, 1978, p249] !!!
- S4.04 (Zeman)
- S4.05
- S4.1 (Sobociński)
  - S4.1 Disambiguation
    - S4.1 (Sobociński)
    - S4.1 (McKinsey) = S4M [Hughes and Cresswell, 1996, p143, fn7]
  - S4.1.1 = S4.1 [Sobociński, NDJL, 1971, p372]
  - S4.1.2 (Sobociński) = S4.1.3 [Sobociński, NDJL, 1971, 372]
  - S4.1.3 = S4.1.2 [Sobociński, NDJL, 1971, 372]
- S4.2 (P.T. Geach)
  - S4.2.1
- S4.3 [Dummett and Lemmon, 1959]
  - S4.3.1 (Sobociński) is ([Zeman, 1973, p245] [Hughes and Cresswell, 1994, p180]) D (Prior) [Prior, 1967, p29]
  - S4.3.2
  - S4.3.3 (Zeman) =[Sobociński, NDJL, 1971, 372]= S4.1.3 =[Sobociński, NDJL, 1971, p373]= Z7 (Sobociński)
  - S4.3.4 (Zeman) =[Sobociński, NDJL, 1971, p373]= Z8 (Sobociński)
- S4.4 (Sobociński)
- S4.5 (Parry) =[Sobociński 1964, p74] [Hughes and Cresswell, 1968, p264] [Zeman, 1973, p230]= S5 (Lewis)
- S4.6 = S4.9 (Schumm) [Zeman, NDJFL, 1972, p118]
- S4.7 (Schumm) is S4.9 (Schumm) [Zeman, 1973, p266]
- S4.9 (Schumm)
- S4F
- S4M =[Hughes and Cresswell, 1996, p143, fn7]= S4.1 (McKinsey)
  - S4M1 [Hughes and Cresswell, 1996, p132]
S5 (Lewis) =[Pledger, 1972, p270]= 2r (Pledger) =[Priest, 2001, p39]= Kρστ =[Chellas, 1980, p139]= KT5 =[Hughes and Cresswell, 1996, p344 B]= S5* (Kanger). Not to be confused with S5-UC.
- S5* (Kanger) = ([Hughes and Cresswell, 1996, p344 B]) S5 (Lewis)
- S5⁰ =[Zeman, 1973, p181]= S5 (Lewis)
- S5-UC (S5, universally quantified)
- S52R* (Routley) [NDJFL, Vol 11, #3, 1970, page 294]
- +S52R* (Routley) [NDJFL, Vol 11, #3, 1970, page 290] [A second order modal logic - JH]
S6 (Alban)
- S6⁰
S7 (Halldén) =[Pledger 1972, p277]= 20sa (Pledger)
- S7⁰
- S7.5 disambiguation
  - S7.5 (Anderson) = 20sb (Pledger) [Pledger, 1972, p277-fn4]
  - S7.5 (Åqvist) = 8pc (Pledger) [Pledger, 1972, p277-fn4] which is S9 (Hughes and Cresswell) [Hughes & Cresswell, 1968, p272-fn301] Which is called S8.5 by Cresswell in [Cresswell, 1967, p59, bottom].
S8 (Alban) = 10pc (Pledger) [Pledger, 1972, p278]
- S8.1 (McCall and Nat) =[Pledger, 1972, p280-para2]= 8pc (Pledger) =[Hughes and Cresswell, 1968, p272-fn301]= S9 (Hughes and Cresswell)
- S8.1 (Åqvist) =[Hughes and Cresswell, 1968, p272-fn301]= S9 (Hughes and Cresswell)
- S8.5 appearing in [Cresswell, 1967] is also 8pc (Pledger) [Pledger, 1972, p280-para2] = S9 (Hughes and Cresswell) [Hughes and Cresswell, 1968, p272-fn301]
S9 (Hughes and Cresswell) [Hughes & Cresswell, 1968, p272-fn301]
Sa (Porte) [Feys, 1965, p141]
Sb (Porte) [Feys, 1965, p141]
Sc (Porte) [Feys, 1965, p141]

- T -

T (Feys) = KT =[Hughes and Cresswell, 1968, p125]= M (von Wright) =[Lemmon 1957, p179]= T (Gödel) =[Priest, 2001, p39]= Kρ =[Feys, 1965, p123]= 2' (Feys), or S2' (Feys)
- T⁰ (Thomas)
- T^x (Sobociński)
- T.0.4 (Zeman) [Zeman 1969 NDJFL]
- T.2 (Zeman) [Zeman 1969 NDJFL]
- T.4 (Zeman) [Zeman 1969 NDJFL]
"Ten modalities calculus" (Becker) =[Parry, 1953, p150]= S5 (Lewis)
TRC (Holmes) [Thomas Jech, JSL Vol 64, #4, 1999, pp1811-1819]
TRCL (Holmes) [Thomas Jech, JSL Vol 64, #4, 1999, pp1811-1819]
The Trivial system (Lp == p == Mp)

- U -

- V -

V1 (Sobociński) [Sobociński, 1970]
V2 (Sobociński) [Sobociński, 1970]
VE [von Wright, 1951, p42] (Where he also creates system EV)
The VER Verum system (Lp)

- W -

- X -

X (Georgacarakos) [Georgacarakos, 1978]

- Z -

Z1 (Sobociński) [Sobociński, 1971a, p371]
- Z1.5
Z2 (Sobociński) [Sobociński, 1971a, p371]
Z3 (Sobociński) [Sobociński, 1971a, p371]
Z4 (Sobociński) [Sobociński, 1971a, p371]
Z5 (Sobociński) [Sobociński, 1971a, p371]
Z6 (Sobociński) [Sobociński, 1971a, p371]
Z7 (Sobociński) [Sobociński, 1971a, p371] = S4.3.3 (Zeman)
Z8 (Sobociński) [Sobociński, 1971a, p371] = S4.3.4 (Zeman)
Z9 (Sobociński) [Sobociński, 1971a, p371] =[Sobociński, 1971a, p371]= S4.6 (Zeman) =[Zeman, 1972, p118, towards end.]= S4.9 (Schumm)

"To do" list

Systems originally added (many years ago) don't have, and do need, references more like the more modern ones have.
In cases where two axiomatizations of the same system have different extensions when a new axiom is added, these pages may have them with the same extension. Some of the cases I can blame on the original quoted authors, some are my own sloppyness. I'm working to get these fixed. (Thanks to Petr Pudlák for reminding me of the issue.)(Hughes and Cresswell cover the issue in passing several times.)
I need to be more careful about noting which ones were originally presented as axiom schemata, but are presented as axioms here.
I need to hunt down more original sources, so that presentations can be made to agree with those sources. (Since, for example, Hughes and Cresswell present axioms even in cases where the original was in terms of axiom schemata.)
I am aware of maybe twice as many named logics than appear on these pages. And I seem to be always finding new ones. And new ones are being published all the time. There will always be something to do.
A number of mappings between paraconsistent, relevant, and modal logics have recently been brought to my attention. The containment questions have expanded greatly.
Some early pages seem to have some confusion between the purely implicational fragment of a system and the system formed by using only the system's axioms for implication.

Community Requests

Large numbers of researchers have "pet problems" about some particular system they are working on. These include those looking for decision procedures (or proof there isn't one), completeness (or proof it isn't complete), etc. I've added a "Community Requests" section to some pages where specific questions about the system and who's looking for an answer.

If you are a researcher, and you want such a note added for a system you are working on, please contact John.Halleck@utah.edu .

Go to ...

© Copyright 2007 by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/index.html
This page was last modified on Monday, October 19th, 2009.