Formalized Formal Logic

Monthly Report 2025/11🔗

This page is the monthly report summarizing commits between 2025/11/02 and 2025/11/30. There are 3 major topics in this month.

Kripke Semantics of Classical First-Order Logic

Author: Palalansoukî

We formalized the Kripke semantics of classical first-order logic, a.k.a. weak forcing and proved its soundness theorem. This semantics is used when we working on forcing arguments.

Kripke semantics of classical first-order logic is defined by interpretting its negation translation as usual Kripke semantics of intuitionistic first-order logic.

🔗theorem
LO.FirstOrder.KripkeModel.weaklyForces₀_iff_forces.{u_1, u_2, u_3}
  {L : FirstOrder.Language} [L.Relational] {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2} [FirstOrder.KripkeModel L ℙ Name] {p : ℙ}
  {φ : FirstOrder.Sentence L} :
  p ⊩ᶜ φ ↔ p ⊩ FirstOrder.Semiformula.doubleNegation φ
LO.FirstOrder.KripkeModel.weaklyForces₀_iff_forces.{u_1,
    u_2, u_3}
  {L : FirstOrder.Language} [L.Relational]
  {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2}
  [FirstOrder.KripkeModel L ℙ Name]
  {p : ℙ} {φ : FirstOrder.Sentence L} :
  p ⊩ᶜ φ ↔
    p ⊩
      FirstOrder.Semiformula.doubleNegation
        φ

This semantics satisfises monotonicity, genericity and soundness.

🔗theorem
LO.FirstOrder.KripkeModel.WeaklyForces₀.monotone.{u_1, u_2, u_3}
  {L : FirstOrder.Language} [L.Relational] {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2} [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L} {p : ℙ} : p ⊩ᶜ φ → ∀ q ≤ p, q ⊩ᶜ φ
LO.FirstOrder.KripkeModel.WeaklyForces₀.monotone.{u_1,
    u_2, u_3}
  {L : FirstOrder.Language} [L.Relational]
  {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2}
  [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L} {p : ℙ} :
  p ⊩ᶜ φ → ∀ q ≤ p, q ⊩ᶜ φ
🔗theorem
LO.FirstOrder.KripkeModel.WeaklyForces₀.generic_iff.{u_1, u_2, u_3}
  {L : FirstOrder.Language} [L.Relational] {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2} [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L} {p : ℙ} :
  p ⊩ᶜ φ ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ
LO.FirstOrder.KripkeModel.WeaklyForces₀.generic_iff.{u_1,
    u_2, u_3}
  {L : FirstOrder.Language} [L.Relational]
  {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2}
  [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L} {p : ℙ} :
  p ⊩ᶜ φ ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ
🔗theorem
LO.FirstOrder.KripkeModel.WeaklyForces₀.sound.{u_1, u_2, u_3}
  {L : FirstOrder.Language} [L.Relational] {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2} [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L} {T : FirstOrder.Theory L} (b : T ⊢ φ) :
  ℙ ∀⊩ᶜ* T → ℙ ∀⊩ᶜ φ
LO.FirstOrder.KripkeModel.WeaklyForces₀.sound.{u_1,
    u_2, u_3}
  {L : FirstOrder.Language} [L.Relational]
  {ℙ : Type u_1} [Preorder ℙ]
  {Name : Type u_2}
  [FirstOrder.KripkeModel L ℙ Name]
  {φ : FirstOrder.Sentence L}
  {T : FirstOrder.Theory L} (b : T ⊢ φ) :
  ℙ ∀⊩ᶜ* T → ℙ ∀⊩ᶜ φ

Downward Löwenheim-Skolem Theorem

Author: Palalansoukî

We formalized the downward Löwenheim-Skolem theorem for countable languages. This theorem states that all structure of countable language, with its subset s, has a minimal elementary substructure contains s, namely a Skolem hull of s.

🔗def
LO.FirstOrder.Structure.SkolemHull.{u, v} (L : FirstOrder.Language)
  {M : Type v} [Nonempty M] [𝓼 : FirstOrder.Structure L M] (s : Set M) :
  Set M
LO.FirstOrder.Structure.SkolemHull.{u, v}
  (L : FirstOrder.Language) {M : Type v}
  [Nonempty M]
  [𝓼 : FirstOrder.Structure L M]
  (s : Set M) : Set M

The Skolem hull of subset of structure.

🔗theorem
LO.FirstOrder.Structure.SkolemHull.subset.{u, v}
  {L : FirstOrder.Language} {M : Type v} [Nonempty M]
  [𝓼 : FirstOrder.Structure L M] {s : Set M} :
  s ⊆ FirstOrder.Structure.SkolemHull L s
LO.FirstOrder.Structure.SkolemHull.subset.{u,
    v}
  {L : FirstOrder.Language} {M : Type v}
  [Nonempty M]
  [𝓼 : FirstOrder.Structure L M]
  {s : Set M} :
  s ⊆ FirstOrder.Structure.SkolemHull L s
🔗theorem
LO.FirstOrder.Structure.SkolemHull.elementaryEquiv.{u, v}
  {L : FirstOrder.Language} {M : Type v} [Nonempty M]
  {𝓼 : FirstOrder.Structure L M} {s : Set M} [L.Eq]
  [FirstOrder.Structure.Eq L M] :
  ↑(FirstOrder.Structure.SkolemHull L s) ≡ₑ[L] M
LO.FirstOrder.Structure.SkolemHull.elementaryEquiv.{u,
    v}
  {L : FirstOrder.Language} {M : Type v}
  [Nonempty M]
  {𝓼 : FirstOrder.Structure L M}
  {s : Set M} [L.Eq]
  [FirstOrder.Structure.Eq L M] :
  ↑(FirstOrder.Structure.SkolemHull L
        s) ≡ₑ[L]
    M

Downward Löwenheim-Skolem theorem for countable language (1)

And if the subset is countable, then the cardinality of the Skolem hull is at most countable.

🔗theorem
LO.FirstOrder.Structure.SkolemHull.card_le_aleph0.{u, v}
  {L : FirstOrder.Language} {M : Type v} [Nonempty M]
  [𝓼 : FirstOrder.Structure L M] [L.Encodable] {s : Set M}
  (hs : s.Countable) :
  Cardinal.mk ↑(FirstOrder.Structure.SkolemHull L s) ≤ Cardinal.aleph0
LO.FirstOrder.Structure.SkolemHull.card_le_aleph0.{u,
    v}
  {L : FirstOrder.Language} {M : Type v}
  [Nonempty M]
  [𝓼 : FirstOrder.Structure L M]
  [L.Encodable] {s : Set M}
  (hs : s.Countable) :
  Cardinal.mk
      ↑(FirstOrder.Structure.SkolemHull L
          s) ≤
    Cardinal.aleph0

Downward Löwenheim-Skolem theorem for countable language (2)

Interpretability Logic and Veltman Semantics II

Author: SnO2WMaN

This is a continuation of last month's report on Interpretability Logic and Veltman Semantics. We formalized the frame conditions for the several axioms M, M₀, P, P₀, W, Wstar (\mathsf{KW^*}), KW2, KW1Zero (Švejdar's \mathsf{KW1^0}), R, Rstar (\mathsf{R^*}), and separate the sublogics and extensions of IL.

Here is the current diagram of sublogics and extensions of IL we formalized.

Figure of Sublogics and Extensions of `IL`

Note that solid arrows means proper extensions and dashed arrows mean not. In Veltman semantics, many of dashed arrows cannot be separated. For example, axiom R and axiom P₀ are characterized by the same frame condition in Veltman semantics.

🔗theorem
LO.InterpretabilityLogic.Veltman.TFAE_HasAxiomR
  {F : InterpretabilityLogic.Veltman.Frame} [F.IsIL] :
  [F.HasAxiomR,
      F ⊧
        InterpretabilityLogic.Axioms.R
          (InterpretabilityLogic.Formula.atom 0)
          (InterpretabilityLogic.Formula.atom 1)
          (InterpretabilityLogic.Formula.atom 2),
      F ⊧
        InterpretabilityLogic.Axioms.P₀
          (InterpretabilityLogic.Formula.atom 0)
          (InterpretabilityLogic.Formula.atom 1)].TFAE
LO.InterpretabilityLogic.Veltman.TFAE_HasAxiomR
  {F :
    InterpretabilityLogic.Veltman.Frame}
  [F.IsIL] :
  [F.HasAxiomR,
      F ⊧
        InterpretabilityLogic.Axioms.R
          (InterpretabilityLogic.Formula.atom
            0)
          (InterpretabilityLogic.Formula.atom
            1)
          (InterpretabilityLogic.Formula.atom
            2),
      F ⊧
        InterpretabilityLogic.Axioms.P₀
          (InterpretabilityLogic.Formula.atom
            0)
          (InterpretabilityLogic.Formula.atom
            1)].TFAE

It can be separated by Verbrugge semantics.

Commits

  • 939c95d0: refactor(Propositional): Rename slash operation (#652)

  • ae01fdbd: add(Propositional): Corsi's Subintuitionistic Logics Part.1 (#648)

  • eaec7d6b: add(FirstOrder/SetTheory): transitive model (#646)

  • b6086365: feat(FirstOrder): downward Löwenheim-Skolem theorem (#645)

  • cf2dd056: fix: typo (#643)

  • 4e445871: refactor(InterpretabilityLogic): Rename extensions of IL (#642)

  • 3b30775e: ci: Remove concurrency restriction (#644)

  • fde948a8: add(InterpretabilityLogic/Veltman): ILR ⪱ ILRW (#640)

  • e7360604: ci: Revert removing github.sha from cache key (#641)

  • ec113467: ci: Remove BRAINSia/free-disk-space action (#639)

  • 419d43a9: docs: Fix FUNDING.yml (#638)

  • b2b0985d: chore(deps): bump actions/upload-pages-artifact from 3 to 4 (#637)

  • 77d7bd94: chore(deps): bump actions/checkout from 4 to 5 (#636)

  • 42104ce0: docs: Update README.md for financial supports (#635)

  • 2f7e8463: ci: Fix cache strategy (#634)

  • 6dffa9a5: add(InterpretabilityLogic): Logic ILRStar (#629)

  • 215d1666: add(InterpretabilityLogic/Veltman): Frame condition on axiom M₀ (#630)

  • f5b6c320: ci: Fix caching problem (#632)

  • 11a14cee: docs: Monthly Reports 2025/10 (#621)

  • b8837832: add(InterpretabilityLogic/Veltman): Frame condition on axiom R (#628)

  • b8745ddd: add(InterpretabilityLogic/Veltman): Frame condition on axiom F (#627)

  • 8ee1b7d9: add(InterpretabilityLogic/Veltman): Frame condition on axiom W (#619)

  • faaeca41: refactor(Prop): Move HilbertStyle to Propositional/Entailment (#592)

  • 584942ab: chore: Update to v4.25.0-rc2 (#620)

  • f830b90e: add(FirstOrder): soundness of Kripke semantics of classical logic (#613)

  • c1fbcc23: add(InterpretabilityLogic/Veltman): Frame condition on axiom P (#618)

  • c02e0caf: add(InterpretabilityLogic/Veltman): Frame condition on axiom M (#617)

  • 75bf19f7: add(InterpretabilityLogic/Veltman): Separate sublogics of IL Part.1 (#616)

  • ab3dd9a2: docs: Fix typo (#615)

  • 772dce9e: docs: Update README for 2025/10 (#614)

  • e50bb0ea: add(InterpretabilityLogic): Syntactical analysis on Sublogics of IL (#611)