System T (Feys, Gödel)


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]

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:


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

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


The system T is:

[Prior, 1967, p175]


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:

[Zeman, 1973, p281]


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)

Go to ...

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is
This page was last modified on December 25th, 2006