# System T (Feys, Gödel)

## History

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

## Notes

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

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

## Based on

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:

### OR

The system T is:

[Prior, 1967, p175]

### OR (Gödel)

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

[Lemmon, 1957, p179]

### OR (von Wright)

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
• Axioms
• a > Ma
• M(a+b) = (Ma + Mb)

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

### OR

The system T is:

[Prior, 1967, p175]

### OR

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

### OR

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

Or in other words, system T is:

[Zeman, 1973, p281]

### OR

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

## Basis for

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

B = T + axiom B

S5 = T + Mp>LMp

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