Provability logic

Provability logic studies modal principles valid when

□ 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.

Table of contents
- Gödel-Löb logic Provability logic

Gödel-Löb logic ( $GL$ )

 0  0

The Gödel-Löb logic has propositional tautologies,

□ (A \to B) \to (□ A \to □ B)

and

□ (□ A \to A) \to □ 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.

Löb axiom implies positive introspection ( $□ X \to □□ X$ )

 0  0

The Löb axiom

□ (□ A \to A) \to □ A

over normal modal logic already implies

□ X \to □□ X

. Put

C = □ X \land X

. Distribution gives

□ C \to □ X

, hence

X \to (□ C \to C)

. Necessitation and distribution give

□ X \to □ (□ C \to C)

; the Löb axiom gives

□ C

, which implies

□□ X

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

 0  0

A formula provably equivalent to a boxed formula satisfies

F \to □ F

in GL. The displayed fixed point then gives both

□□ F

and

□ \neg □ F

under

F

, hence

□ ⊥

. 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.

Modalized fixed-point theorem for GL ( $G L ⊢ F \leftrightarrow X (F)$ )

 0  0

If every occurrence of

p

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 (□ C_{1} (p), \dots, □ C_{m} (p))

using the outermost boxes that contain

p

, so

H

has no

p

. Solve

q_{i} \leftrightarrow □ 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.

Simultaneous boxed fixed-point elimination in GL ( $F_{i} \leftrightarrow □ C_{i} (F_{1}, \dots, F_{m})$ )

 0  0

In Gödel-Löb logic, the one-variable identity

□ C (⊤) \leftrightarrow □ C (□ C (⊤))

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.

GL fixed point by truth substitution ( $GL ⊢ □ Y (⊤) \leftrightarrow □ Y (□ Y (⊤))$ )

 0  0

Let

U = □ Y (⊤)

and

V = □ Y (U)

. Boxed replacement gives

□ U \to (U \leftrightarrow V)

, and positive introspection gives

U \to V

. For the reverse implication rewrite it as

V \to (□ U \to U)

, necessitate, use

V \to □ V

, and apply the Löb axiom to obtain

V \to □ U \to U

. This explicit one-variable construction needs no reflection axiom.

GL fixed point for a provability implication ( $F = (□ q \to q), GL ⊢ F \leftrightarrow (□ F \to q)$ )

 0  0

The Löb axiom gives

□ F \to □ q

. The tautology

q \to F

, necessitated and distributed, gives

□ q \to □ F

. Thus

□ F \leftrightarrow □ q

, and replacing the antecedent in

□ F \to q

gives exactly

F

. Setting

q = ⊥

produces a negative-provability fixed point, provably equivalent to

\neg □ ⊥

Arithmetical soundness of GL ( $GL ⊢ A ⟹ PA ⊢ A^{*}$ )

 0  0

Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret

□

by an arithmetical provability predicate. Propositional axioms remain theorems. The K axiom uses the second of the derivability conditions, and the Löb axiom uses the Internal form of Löb's theorem. Modus ponens rule is preserved directly, and the necessitation rule uses the first derivability condition. Induction on a GL proof therefore proves the displayed soundness implication for Peano arithmetic with the stipulated provability predicate.

 Ancestors (6)

 Incoming links (9)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (1)

Provability logic by

Wikipedia Bot  1

 View more

Provability logic is a branch of mathematical logic that studies formal systems of provability. Specifically, it deals with the properties and behaviors of provability predicates, which are statements or operators that express the idea that a certain statement is provable within a given formal system. One of the most prominent systems within provability logic is known as Gödel's provability logic, often represented by the modal system $ GL $ (Gödel-Löb logic).

 Read the full article

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

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

 Discussion (0) New discussion