Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Modal Logic of Finitely Symmetry-Preserving Iterated Extensions is Exactly S4

Frank Gilson

TL;DR

This work determines the exact ZF-provable modal logic of the symmetry-based necessity operator $Box_{\mathrm{sym}}$, showing it coincides with $\mathsf{S4}$. The argument combines soundness (axioms $T$ and $4$ from reflexivity and transitivity) with completeness established via two main tools: (i) a non-amalgamation lemma demonstrating that finite symmetry-preserving iterations above a branching cannot jointly realize two sibling extensions, and (ii) a $p$-morphism/finite-frame realization that embeds any finite reflexive-transitive frame into a model built from finite symmetry-preserving iterations. A crucial technical input is Karagila’s collapse result, which reduces finite symmetry-preserving iterations to a single symmetric step, enabling a template-based construction of Kripke frames. The construction yields a precise characterization of the modal logic of symmetric intermediate submodels, highlighting that directedness (axiom $(.2)$) fails in this regime. Taken together, the results illuminate the limits of necessity and possibility under finite symmetry-preserving iterations and provide a robust framework for analyzing modal truths in symmetric extension contexts.

Abstract

We determine the ZF-provable modal logic of the modality $\Box_{\mathrm{sym}}$, where $\Box_{\mathrm{sym}}\varphi$ means '$\varphi$ holds in every finite symmetry-preserving iteration' of the symmetric method. We prove that the exact logic is S4. Soundness (axioms T and 4) follows from reflexivity and transitivity of the underlying accessibility relation. Exactness is obtained by (i) a non-amalgamation lemma showing that axiom (.2) fails for finite symmetry-preserving iterations (no common finite symmetry-preserving iteration above the parent), and (ii) a $p$-morphism/finite-frame realization producing, within ZF, models whose $\Box_{\mathrm{sym}}$-theory matches any finite reflexive-transitive frame.

The Modal Logic of Finitely Symmetry-Preserving Iterated Extensions is Exactly S4

TL;DR

This work determines the exact ZF-provable modal logic of the symmetry-based necessity operator , showing it coincides with . The argument combines soundness (axioms and from reflexivity and transitivity) with completeness established via two main tools: (i) a non-amalgamation lemma demonstrating that finite symmetry-preserving iterations above a branching cannot jointly realize two sibling extensions, and (ii) a -morphism/finite-frame realization that embeds any finite reflexive-transitive frame into a model built from finite symmetry-preserving iterations. A crucial technical input is Karagila’s collapse result, which reduces finite symmetry-preserving iterations to a single symmetric step, enabling a template-based construction of Kripke frames. The construction yields a precise characterization of the modal logic of symmetric intermediate submodels, highlighting that directedness (axiom ) fails in this regime. Taken together, the results illuminate the limits of necessity and possibility under finite symmetry-preserving iterations and provide a robust framework for analyzing modal truths in symmetric extension contexts.

Abstract

We determine the ZF-provable modal logic of the modality , where means ' holds in every finite symmetry-preserving iteration' of the symmetric method. We prove that the exact logic is S4. Soundness (axioms T and 4) follows from reflexivity and transitivity of the underlying accessibility relation. Exactness is obtained by (i) a non-amalgamation lemma showing that axiom (.2) fails for finite symmetry-preserving iterations (no common finite symmetry-preserving iteration above the parent), and (ii) a -morphism/finite-frame realization producing, within ZF, models whose -theory matches any finite reflexive-transitive frame.
Paper Structure (34 sections, 34 theorems, 37 equations, 1 table)

This paper contains 34 sections, 34 theorems, 37 equations, 1 table.

Table of Contents

  1. Introduction
  2. Standing background.
  3. Possible vs. necessary.
  4. Scope and relation to prior work.
  5. Historical context.
  6. Modal and proof-theoretic preliminaries
  7. Homogeneity.
  8. Symmetric systems and finite iterations
  9. Notation discipline.
  10. Composition: finite symmetry-preserving iterations collapse to one step
  11. Factoring through intermediate HS-stages
  12. Notation.
  13. Productive iterations and block preservation
  14. Karagila-productive step (restated from Karagila2019).
  15. The partition construction and signals
  16. ...and 19 more sections

Key Result

Proposition 3.1

[proposition]prop:full-filter Let $(\mathcal{P},G,\mathcal{F}_{\mathrm{full}})$ be a symmetric system where $\mathcal{F}_{\mathrm{full}}$ is the full normal filter of subgroups of $G$ (i.e., the upward-closed, conjugation-closed family of all subgroups of $G$, generated by the trivial subgroup $\{1\

Theorems & Definitions (97)

  • Definition 2.1: Cohen forcing $\mathrm{Add}(\omega,\omega)$
  • Definition 2.2: Finite support for evaluation
  • Remark 2.3: Standard usage
  • Remark 2.4: Meaning of “ZF-provably valid”
  • Remark 2.5: Support calculus
  • Remark 2.6: Evaluation vs. symmetry support
  • Remark 2.7: Terminology
  • Proposition 3.1: Forcing as a special case of symmetry
  • proof
  • Definition 3.2: Symmetry-preserving iteration
  • ...and 87 more