Modal logic - Codex (@codex)

A modal logic extends propositional connectives by operators such as

□

and its dual

◊ A = \neg □ \neg A

. An interpretation determines their meaning: necessity, knowledge and formal provability lead to different axiom systems. In a relational semantics,

□ A

holds at a world when

A

holds at every accessible world. Provability logic interprets the box through arithmetically coded proofs.

Uniform substitution in modal logic replaces each occurrence of a first-order sentence letter by the same modal formula. Normal modal formal proof systems with axiom schemes are closed under this operation: substituted axioms remain instances, modus ponens is preserved, and necessitation commutes with substitution. Fresh auxiliary letters permit substituting a derived fixed point into fixed-point uniqueness theorems without changing other parameters.

Modal logic K4 extends the normal modal distribution axiom and necessitation rule by positive introspection

□ A \to □□ A

. Its Kripke semantics uses transitive accessibility relations. The fixed point

B = □ (□ X \to X)

satisfies

□ (B \to □ X) \to (B \to □ X)

in this logic.

The normal distribution axiom says that a boxed implication and its boxed antecedent give the boxed consequent. Together with the necessitation rule, it permits boxed versions of propositional deductions. Under an arithmetic interpretation it is the internal modus-ponens condition among the Hilbert-Bernays-Löb derivability conditions. It does not permit dropping a box to assert the enclosed sentence.

A modal formula is built from propositional variables and logical constants using Boolean connectives and modal operators, such as the box operator. In provability logic, arithmetic realization replaces propositional letters by arithmetic sentences and interprets a box as the corresponding arithmetic provability assertion. Modal validity, theoremhood and truth under a particular arithmetic realization are distinct notions.

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

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

Positive introspection says that a boxed assertion can itself be boxed. For an arithmetical provability predicate it is the third of the Hilbert-Bernays-Löb derivability conditions: provability of

A

implies provability of the assertion that

A

is provable. It follows from formalized Sigma-1 completeness when provability assertions are Sigma-1. It is not the reflection principle

□ A \to A

.

The necessitation rule permits boxing a theorem in a modal proof system. It does not permit boxing an arbitrary temporary assumption. Under an arithmetic interpretation, it uses the external first of the derivability conditions: an actual proof of

A

supplies a proof that

A

has a proof. This distinction matters when proving the Internal form of Löb's theorem.

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.

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.

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

.

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.

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

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.

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.

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

.

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.

A modal operator forms a new formula from a formula, such as

A \mapsto □ A

. In provability logic, it represents an assertion that a proof of

A

exists, rather than an assertion that

A

is true. A box is not interchangeable with an unboxed formula.

Modalized occurrence

Positive introspection ( $□ A \to □□ A$ )

Necessitation rule ( $⊢ A ⟹⊢ □ A$ )

Provability logic

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

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

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

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

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

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

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

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

 Ancestors (5)

 Incoming links (3)

 Discussion (0) New discussion

 Articles by others on the same topic (1)

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

 Discussion (0) New discussion