**[Feys, 1937]**(as "T") (Original Source)**[Gödel, 1933]**(As "T") (Original Source)- [Hughes and Cresswell, 1996] (As "T")
- [Priest, 2001] (As "Kρ")
- [Prior, 1967]
**[von Wright, 1951]**(As "M") (Original Source)

The system T was originally investigated (with the name T) by Gödel ([Gödel, 1933]), (as reported in [Lemmon, 1957, p179])

This system was investigated independently, also under the name T, by R. Feys in [Feys, 1937] (as reported in [Lemmon, 1957, p179])

This system was independently investigated under the name "M" by G.H.
von Wright in his book "*An essay in modal logic*"
von Wright,
1951, appendex II, p85-90]
(as reported in
[Lemmon,
1957, p179])

Bolesław Sobociński proved "M" and "T" to be the same system
in "Note on a system of Feys - von Wright", in
*The Journal of Computing Systems*, v. 1(1953), p171-178
(as reported in
[Lemmon,
1957, p179])

So... You see this system as M (von Wright) or T (Feys) or even T (Feys and von Wright)

Feys investigated this system under the name 2' (Since he refered to "S1" as "1", "S2" as "2", this system should probably be called S2') [Feys, 1965, p123]

This system is also called Kρ (K rho) based on its frame constraints. [Priest, 2001, 241 (Index entry)]

T is characterized by reflexive frames. [Hughes and Cresswell, 1996, p43]

There is a decision procedure for T [von Wright, 1951, p85]

The system T is the result of K and the Lp>p [Axiom T] (Sometimes called the Axiom of Necessity) [Hughes and Cresswell, 1996, p41]

In other words, T is:

- PC
- Modus Ponens: From |- p and |- p>q, infer |- q
- Uniform substitution

- Rules
- Necessitation: From |- p infer |- Lp

- Axioms

The system T is:

- PC
- Definitions
- Lp =def ~M~p

- Rules
- Nescessitation: From |- p infer |- Lp
- REM: From |- a==b infer |- Ma==Mb

- Axioms
- M(a+b)==(Ma+Mb)
- p>Mp

The system T was defined by Gödel to be:

- The system PC
- Rules
- Necessitation (From |- a infer |- La)

- Axioms

The system M (later proved to be T) defined by von Wright was:

(von Wright used "N" for our "L")

- System PC
- Definitions
- Np =def ~N~p

- Rules
- From |- p=q, infer |- Mp = Mq
- Necessitation: From |- p, infer |- Lp

- Axioms
- a > Ma
- M(a+b) = (Ma + Mb)

[von Wright, 1951, appendex II, p85-86]

The system T is:

- PC
- Definitions
- Lp =def ~M~p

- Rules
- Necessitation: From |- p infer |- Lp

- Axioms
- K: L(p>q)>(Lp>Lq)
- p>Mp

The system T is the result of S1 and any axiom of the form LLα where LLα is a T theorem [Such as LL(p&p) or LL(any PC thesis) -JH] [Hughes and Cresswell, 1968, p227fn (and see 223-227)]

The system T is system T-0 plus Axiom p=>Mp [Zeman, 1973, p281]

Or in other words, system T is:

- Definitions
- [todo]

- Rules
- Axioms
- M1: (p&q)=>(q&p)
- M2: (p&q)=>p
- M3: ((p&q)&r)=>(p&(q&r))
- M4: p=>(p&p)
- M5: ((p=>q)&(q=>r))=>(p=>r)
- M6: p=>Mp
- LL(p>p) [Or LLα where alpha is any PC thesis.]

The system T is the tense logic K_{t}
plus the definition La == a & Ga
[Rescher and Urquhart,
1971, p126]

S4 = T + axiom 4 [Lemmon, 1957, p180]

X = T + M(MMp>LMq) > (MMp>LMq)

© Copyright 2006, by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/.html

This page was last modified on December 25th, 2006