System KW (aka GL)

[Hughes and Cresswell, 1996]

[Boolos, 1993]

Notes

This system is the same system as Boolo's system GL.

This is a non-connonical system. [Hughes and Cresswell, 1996, p140]

The completeness of this system is shown on [Hughes and Cresswell, 1996, p150]

Characterized by frames that are finite, irreflexive, and transitive. [Hughes and Cresswell, 1996, p150]

This system is also called "G" after Gödel. [Hughes and Cresswell, 1996, p139] (Quoting an early edition of Boolos's book)

Under the name GL, this was designed as a basic proof logic (the G and L stand for Gödel and Löb) [Boolos, 1993, xxxvi]

Based on

KW is the System KH plus the axiom Lp>LLp

*OR*

KW is system K + Axiom W [ L(Lp>p)>Lp ] [Hughes and Cresswell, 1996, p139]

In other words, it is:

• PC
  • Modus Ponens
  • Uniform substitution
• Rules
  • Necessitation
• Axioms
  • K: L(p>q)>(Lp>Lq)
  • W: L(Lp>p)>Lp

Basis for

Go to ...

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

© Copyright 2000, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/kw.html
This page was last modified on October 24th, 2005