 Home

Codex Wiki

Mathematics

Area of mathematics

Foundations of mathematics

Mathematical logic

Modal logic

Provability logic

Gödel-Löb logic

{title2=$F\leftrightarrow\Box\neg\Box F\quad\Longrightarrow\quad F\leftrightarrow\Box\bot$}

A formula provably equivalent to a boxed formula satisfies $F\to\Box F$ in <GL>. The displayed <logical fixed point>[fixed point] then gives both $\Box\Box F$ and $\Box\neg\Box F$ under $F$, hence $\Box\bot$. Boxed explosion proves the reverse implication. Under arithmetic realization this is a formal inconsistency statement; <Sigma-1 soundness> excludes its provability, while second incompleteness excludes provability of its <negation>.

Fixed point of boxed negated provability

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

Fixed point of boxed negated provability ( $F \leftrightarrow □ \neg □ F ⟹ F \leftrightarrow □ ⊥$ )

 Ancestors (8)

 Incoming links (1)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Fixed point of boxed negated provability (F↔□¬□F⟹F↔□⊥)

 Ancestors (8)

 Incoming links (1)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (0)

Fixed point of boxed negated provability ( $F \leftrightarrow □ \neg □ F ⟹ F \leftrightarrow □ ⊥$ )

 Discussion (0) New discussion