System KW (aka GL)

[Hughes and Cresswell, 1996]

[Boolos, 1993]

Notes

This is *** NOT *** the logic system you get from the combinators K and W. That logic doesn't currently have a page.

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 the usage of an early edition of [Boolos, 1993])

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:

Basis for


Go to ...


© 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 November 12th, 2009