System KW (aka GL)

[Hughes and Cresswell, 1996]

[Boolos, 1993]


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


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
This page was last modified on November 12th, 2009