System GLB



This was designed as a basic proof logic, the G and L stand for Gödel and Löb. [Boolos, 1993, xxxvi] the B stands for "Bimodal". [Boolos, 1993, xxii]

Boolos points out this is a fragment of GLP (Dzhaparidze) ["P" for polymodal] published in the paper "The polymorphic logic of provability" from "Intensional Logics and the Logical Structure of Theories: Material from the Fourth Soviet-Finnish Symposium on Logic", Telavi, May 20-24, 1985, Metsniereba, Tbilisi, 1988 (Russian) [Boolos, 1993, p188 + Bibliography]

[I really don't have a way to portably show Boolos' "Number one in a box" symbol. So I'm just going to use G for the "1" box and H for the "1" diamond. My appologies to anyone that offends. -- JH] The G modality is intended to represent ω-provability, and the H modality to mean ω-consistancy.

Based on

[Boolos, 1993, p188]

Basis for

Go to ...

© Copyright 2000, by John Halleck, All Rights Reserved.
This page is
This page was last modified on October 24th, 2005