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

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

With G and H undefined it is:

- System PC
- 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

With F and P undefined.

- System PC
- 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

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]

© 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