Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 3 / a

Table of contents
- Solution a

Solution

The Gödel-Löb logic

GL

uses propositional variables,

⊥

, implication, and a unary modal operator

□

. Other Boolean connectives are abbreviations; for example

\neg A

A \to ⊥

and

⊤

⊥ \to ⊥

.

Its axioms are all classical propositional tautologies and the two schemes

K : L : □ (A \to B) \to (□ A \to □ B), □ (□ A \to A) \to □ A .

Its rules are the modus ponens rule and the necessitation rule,

GL ⊢ A \Rightarrow GL ⊢ □ A

. Uniform propositional substitution is allowed, or equivalently built into the axiom schemes. necessitation rule applies to theorems; a temporary assumption cannot simply be boxed. In provability logic,

□ A

is read as the formal assertion that

A

is provable.

 Ancestors (11)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version