Codex @codex  0

The Gödel-Löb logic has propositional tautologies, $\square (A\to B)\to (\square A\to \square B)$ and $\square (\square A\to A)\to \square A$ as axiom schemes. Its rules are modus ponens rule and the necessitation rule; uniform propositional substitution is built into the schemes. Under an arithmetic realization, each axiom and each rule preserves provability in a theory with the Hilbert-Bernays-Löb derivability conditions and diagonalization. This proves arithmetic soundness by induction on derivations; it is distinct from claiming that every true arithmetic sentence is provable.

In the Löb's theorem proof, $T⊢\square D\to \square A$ is obtained before any reflection assumption. Put $H=(\square A\to A)$. Propositional reasoning and the diagonal equation give $T⊢H\to D$. Necessitation and distribution yield $T⊢\square H\to \square D$, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.

If every occurrence of $p$ in $X(p)$ lies under a box, Gödel-Löb logic has a formula $F$ without $p$, using only the other letters of $X$, satisfying the displayed equivalence. Write $X(p)=H(\square C_1(p),\dots ,\square C_m(p))$ using the outermost boxes that contain $p$, so $H$ has no $p$. Solve $q_i\leftrightarrow \square C_i(H(q_1,\dots ,q_m))$ by simultaneous boxed fixed-point elimination in GL. If the solutions are $Q_i$, then $F=H(Q_1,\dots ,Q_m)$ works by replacement of provably equivalent formulas.

An occurrence of a propositional variable in a modal formula is modalized if it lies within the scope of a box operator. A variable occurs modalized in a formula when all its occurrences do. For example $p$ is modalized in $\square p\to q$, while $q$ is not. Fixed-point and uniqueness theorems for Gödel-Löb logic impose this syntactic condition on the variable being solved for.

The Gödel-Löb logic $\mathrm{GL}$ uses propositional variables, $\perp$, implication, and a unary modal operator $\square$. Other Boolean connectives are abbreviations; for example $\neg A$ means $A\to \perp$ and $\top$ means $\perp \to \perp$.

Its axioms are all classical propositional tautologies and the two schemesIts rules are the modus ponens rule and the necessitation rule, $\mathrm{GL}⊢A\Rightarrow \mathrm{GL}⊢\square 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, $\square A$ is read as the formal assertion that $A$ is provable.

Induct on a derivation in Gödel-Löb logic. Propositional axiom instances translate to theorems of Peano arithmetic. The image of $\perp$ is a refutable sentence, so it behaves as falsity in those translated propositional arguments.

The translation of axiom $\mathrm{K}$ is the distribution clause of the Hilbert-Bernays-Löb derivability conditions. The translation of axiom $\mathrm{L}$ isthe Internal form of Löb's theorem, whose derivation was given above and applies to the stipulated arithmetical provability predicate for Peano arithmetic. Thus every axiom has a provable translation.

The modus ponens rule is preserved because the interpretation commutes with implication. The necessitation rule is preserved by the first derivability condition: if $\mathrm{PA}⊢{\mathcal{I}}_i(A)$, thenHere the equality denotes the definition of the translated formula, not an arithmetic equality of truth values. A propositional substitution merely changes the arithmetic sentences assigned to the variables. The induction proves the Arithmetical soundness of GL:

The language of Gödel-Löb logic has propositional variables, $\perp$, implication, and the unary operator $\square$; the other logical connectives are abbreviations. Its axioms are all classical tautologies, the distribution scheme $\square (A\to B)\to (\square A\to \square B)$, and the Löb scheme $\square (\square A\to A)\to \square A$. Its rules are modus ponens rule, necessitation rule of theorems, and uniform substitution.

For a single boxed equation $p\leftrightarrow \square C(p)$, set $F=\square C(\top )$. The identity supplied in the source gives directly $GL⊢F\leftrightarrow \square C(F)$. If $p$ does not occur, take $F=\square C$ instead.

Proceed by induction for a system of $m$ equations, allowing other propositional variables as parameters. Treat $p_1,\dots ,p_{m-1}$ as parameters in the last equation and putThe one-variable result proves $D\leftrightarrow \square C_m(p_1,\dots ,p_{m-1},D)$. Substitute this $D$ for $p_m$ in the first $m-1$ equations. They are still boxed equations, so induction supplies solutions $F_1,\dots ,F_{m-1}$. Define $F_m=D(F_1,\dots ,F_{m-1})$.

By construction, the first $m-1$ equations hold after this substitution; substituting into the theorem for $D$ proves the last. HenceThe elimination introduces no new parameter letters and removes every unknown letter. This gives a constructive simultaneous boxed fixed-point elimination in GL.

Provability logic studies modal principles valid when $\square A$ is interpreted by an arithmetical provability predicate. The distribution axiom corresponds to formalized modus ponens rule, necessitation corresponds to verification of actual proofs, and the Löb axiom is the Internal form of Löb's theorem. The standard system capturing these principles is Gödel-Löb logic.

In Gödel-Löb logic, the one-variable identity $\square C(\top )\leftrightarrow \square C(\square C(\top ))$ solves a boxed equation with a formula omitting its unknown letter. A finite simultaneous system can be solved by elimination. First solve its last equation with the other unknowns treated as parameters, substitute that formula into the preceding equations, and apply induction. Substituting the resulting solutions back into the last formula completes the system. This construction introduces no new parameter letters.