Grzegorczyk Logic

Origin. Grzegorczyk (1967). Modal logic of provability in intuitionistic arithmetic. 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 ⊨ □A ↔ A (for propositional A).

Comparison: S4 + Löb = GL (provability logic) S4 + Grz = Grz (no infinite chains) GL ∩ Grz = S4

Finite frames: All finite S4 frames validate Grz. Infinite frames: must be well-founded upward.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box	Necessity
Grz	—	Grzegorczyk	Axiom schema
R	—	Accessibility	Frame relation
IPC	—	Intuitionistic	Int prop calc

Metatheory. Decidable. Finite model property (with non-standard sense). Complete for finite trees. Kripke complete.

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

Limitations. Less known than S4, GL. Specialized applications. Intuitionistic connection subtle.