 Home

Codex Wiki

Mathematics

Area of mathematics

Foundations of mathematics

Mathematical logic

First-order logic

First-order theory

Gödel numbering

Arithmetical provability predicate

{c}
{title2=$\Box(A\to B)\to(\Box A\to\Box B),\quad\Box A\to\Box\Box A$}

= Derivability conditions
{synonym}

For an <arithmetical provability predicate> write $\Box A=\operatorname{Pr}_T(\ulcorner A\urcorner)$. The conditions are: if $T\vdash A$ then $T\vdash\Box A$; $T\vdash\Box(A\to B)\to(\Box A\to\Box B)$; and $T\vdash\Box A\to\Box\Box A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under <modus ponens rule> and positive introspection. None licenses reflection from a proved sentence $\Box A$ to $A$.

Hilbert-Bernays-Löb derivability conditions

Equivalence of a Gödel sentence and a consistency statement

Full local reflection in a one-sentence extension is inconsistent

Gödel-Löb logic

Löb's theorem

Normal modal distribution axiom

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

Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 1 / e / Solution

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

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 / A / 3 / a / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 3 / a / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2009 / A / 1 / b / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2009 / A / 3 / c / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 1 / a / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 1 / b / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 2 / c / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 2 / d / Solution

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 3 / a / Solution

Positive introspection

Refutable sentences have the consistency nonprovability statement

Sigma-1 completeness

codex/derivability-conditions

Hilbert-Bernays-Löb derivability conditions ( $□ (A \to B) \to (□ A \to □ B), □ A \to □□ A$ )

 Ancestors (9)

 Incoming links (20)

 Synonyms (1)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Hilbert-Bernays-Löb derivability conditions (□(A→B)→(□A→□B),□A→□□A)