Grzegorczyk Logic

Origin. Grzegorczyk (1967). Modal companion of intuitionistic logic; the logic of provability-together-with-truth. S4 + Grzegorczyk axiom. No infinite ascending chains. Foundation for provability and intuitionism connection.

Models. S4 frames with no infinite ascending R-chains. Transitive, reflexive, converse well-founded. Finite irreflexive part. Intuitionistic logic embedding.

Formalism.

Grzegorczyk axiom (Grz): □(□(A → □A) → A) → A

System Grz: K + T + 4 + Grz = S4 + Grz

Frame condition: Transitive, reflexive, no infinite ascending chains. Every sequence w₁ R w₂ R w₃ R ... eventually constant. "Finite depth modulo reflexivity"

Alternative: Reflexive, transitive, Noetherian upward. wRv and w≠v implies no infinite chain from v.

Intuitionistic embedding: IPC embeds into Grz via Gödel translation. □A interprets "A is provable/true." Grz is the greatest S4-companion of IPC (Blok–Esakia).

Comparison: K + Löb = GL (provability logic; 4 is derivable, and S4 + Löb is inconsistent) S4 + Grz = Grz (no infinite chains) K4 ⊆ GL ∩ Grz: T ∈ Grz \ GL, Löb ∈ GL \ Grz

Finite frames: A finite S4 frame validates Grz iff it is a partial order. Proper clusters refute it: on {a,b} with R total and V(p) = {a}, Grz fails at b. Infinite frames: must be well-founded upward on distinct points.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box / Necessity	True at all accessible worlds
◇	U+25C7	Diamond / Possibility	True at some accessible world
⊢	U+22A2	Derivability	Provable in the calculus
⊆	U+2286	Inclusion	Containment between logics
∩	U+2229	Intersection	Common theorems of two logics
\	—	Set difference	Theorems of one logic not the other
≠	U+2260	Non-identity	Distinct worlds in a chain
Grz	—	Grzegorczyk axiom	□(□(A → □A) → A) → A
R	—	Accessibility relation	Reflexive, transitive, Noetherian
IPC	—	Intuitionistic propositional calculus	Logic embedded by the Gödel translation
GL	—	Gödel–Löb logic	K + Löb; provability in PA
( )^T	—	Gödel translation	Embedding of IPC into a modal logic

Metatheory. Sound and complete for reflexive transitive frames containing no infinite strictly ascending chain, and it has the finite model property, being determined by the class of finite partial orders — equivalently by finite trees. It is therefore decidable, with satisfiability PSPACE-complete. Unlike S4, Grz is not canonical: converse well-foundedness is not preserved in the canonical frame, the Grz axiom is not a Sahlqvist formula, and the frame condition is not first-order definable, so Grz is a standard example of a Kripke-complete but non-elementary and non-canonical logic. The Blok–Esakia theorem makes the map sending an intermediate logic to its largest modal companion an isomorphism from the lattice of intermediate logics onto the lattice of normal extensions of Grz; in particular IPC ⊢ A iff Grz ⊢ A^T, and Grz is the greatest S4-companion of IPC. Goldblatt (1978) established a translation into provability logic: replacing each □B by □B ∧ B embeds Grz faithfully into GL, which is why Grz is described as the logic of provability-together-with-truth.

Applies to. Intuitionistic provability. Formal epistemology. Intermediate logic connection. Provability logic.

Limitations. Grz is not canonical and its defining condition is not elementary, so the canonical model argument and Sahlqvist correspondence both fail for it, and no first-order sentence over ⟨W, R⟩ defines its frame class. Because it contains T it is unsound for formal provability: adding Löb's axiom to any logic containing T yields inconsistency, so Grz and GL are incomparable — T lies in Grz but not GL, Löb in GL but not Grz. Converse well-foundedness rules out proper clusters, so Grz cannot model settings where two distinct alternatives are mutually accessible, which excludes the equivalence-relation readings of S5 and any symmetric accessibility. Being a modal companion of IPC, it inherits the limits of the Gödel translation, which covers only the propositional intuitionistic language and does not extend faithfully to first-order intuitionistic logic without further conditions on domains.