System K_t (K sub t)

• [Prior, 1967]
• [Rescher and Urquhart, 1971]

Notes

This system is E.J. Lemon's K_t system.

It was designed to be a minimal tense logic.

The terms are

• G: It will always be
• H: It has always been
• P: Past
• F: Future

Based on

With G and H undefined it is:

• System PC
  • Modus Ponens
  • Uniform substitution
• Definitions
  • Fa = NGNa
  • Pa = NHNa
• Rules
  • If |- a, infer |- Ga
  • If |- a, infer |- Ha
• Axioms
  • G(p>q)>(Gp>Gq)
  • H(p>q)>(Hp>Hq)
  • PGp>p
  • FHp>p

[Prior, 1967, p176]

OR

With F and P undefined.

• System PC
  • Modus Ponens
  • Uniform substitution
• Definitions
  • Ga = NFNa
  • Ha = NPNa
• Rules
  • If |- a, infer |- Ga
  • If |- a, infer |- Ha
• Axioms
  • G(p>q)>(Fp>Fq)
  • H(p>q)>(Pp>Pq)
  • PGp>p
  • FHp>p

[Prior, 1967, p176]

Basis for

K_t plus the definition [ La == a & Ga ] Gives von Wright's system M. [Rescher and Urquhart, 1971, p126] (Which is T (Feys) [Hughes and Cresswell, 1968, p125]

K_t plus the definition [ La == a & Ga & Ha ] gives system B (The Brouwerian system) [Rescher and Urquhart, 1971, p127]

K_b is formed by K_t plus the axioms:

• G3: Gp>GGp
• H3: Hp>HHp
• H4: (H(p+q)&H(p+Hq)&H(Hp+q))>(Hp+Hq)

[Rescher and Urquhart, 1971, p76]

Go to ...

• Systems Page
• Structures Page
• Logic Page
• John Halleck's home page

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/ksubt.html
This page was last modified on October 2nd, 2006