Merge remote-tracking branch 'origin/master' into update-20260217

Author: SnO2WMaN

.github/workflows/ci.yml

@@ -21,6 +21,7 @@ jobs:
   build:
     name: Build project
     runs-on: ubuntu-latest
+    needs: mk-all-check
     steps:
       - uses: actions/checkout@v6
       - name: Setup elan
@@ -73,7 +74,7 @@ jobs:
           lake exe graph ./import_graph.html
 
       - name: Upload lean artifacts
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         with:
           name: lean-artifacts
           path: |
@@ -132,7 +133,7 @@ jobs:
       - uses: pandoc/actions/setup@v1
 
       - name: Download lean artifacts
-        uses: actions/download-artifact@v7
+        uses: actions/download-artifact@v8
         with:
           name: lean-artifacts
       - name: Copy from artifacts to pages
@@ -157,5 +158,5 @@ jobs:
       - uses: actions/upload-pages-artifact@v4
         with:
           path: pages
-      - uses: actions/deploy-pages@v4
+      - uses: actions/deploy-pages@v5
         id: deployment

CONTRIBUTING.md

@@ -1,5 +1,8 @@
 # Contribution
 
+1. Follow the [commit convention](#commit-convention).
+2. Run [import all](#import-all).
+
 ## Commit convention
 
 Follow usual conventional commit for PR title (we always squash merge).
@@ -16,7 +19,7 @@ Choose `<type>` from below (should be one, but like `fix/doc` might be ok).
 - `ci`: Configure GitHub Actions.
 - `chore`: Maintaining other things (ex: version-up).
 
-`scope` is optional, specify like `FirstOrder`, `Modal` if needed.
+`scope` is optional, specify like `FirstOrder`, `Modal/Kripke` if needed.
 
 ## Usual commands
 
@@ -26,6 +29,12 @@ Choose `<type>` from below (should be one, but like `fix/doc` might be ok).
 lake build Foundation
 ```
 
+### Import all
+
+```shell
+lake exe mk_all --module
+```
+
 ### References
 
 Format [references.bib](./references.bib) when adding references.

Foundation.lean

@@ -358,10 +358,8 @@ public import Foundation.Modal.Maximal.Basic
 public import Foundation.Modal.Maximal.Makinson
 public import Foundation.Modal.Maximal.Unprovability
 public import Foundation.Modal.MaximalConsistentSet
-public import Foundation.Modal.ModalCompanion
 public import Foundation.Modal.ModalCompanion.Corsi
 public import Foundation.Modal.ModalCompanion.Corsi.VF
-public import Foundation.Modal.ModalCompanion.Standard
 public import Foundation.Modal.ModalCompanion.Standard.Basic
 public import Foundation.Modal.ModalCompanion.Standard.Cl
 public import Foundation.Modal.ModalCompanion.Standard.Int
@@ -417,11 +415,11 @@ public import Foundation.Modal.PLoN.Logic
 public import Foundation.Modal.PLoN.Logic.N
 public import Foundation.Modal.Tableau
 public import Foundation.Modal.VanBentham.StandardTranslation
-public import Foundation.Propositional.ClassicalSemantics.Basic
-public import Foundation.Propositional.ClassicalSemantics.Hilbert
-public import Foundation.Propositional.ClassicalSemantics.NNFormula
-public import Foundation.Propositional.ClassicalSemantics.Tait
-public import Foundation.Propositional.ClassicalSemantics.ZeroSubst
+public import Foundation.Propositional.Boolean.Basic
+public import Foundation.Propositional.Boolean.Hilbert
+public import Foundation.Propositional.Boolean.NNFormula
+public import Foundation.Propositional.Boolean.Tait
+public import Foundation.Propositional.Boolean.ZeroSubst
 public import Foundation.Propositional.ConsistentTableau
 public import Foundation.Propositional.Decidable
 public import Foundation.Propositional.Dialectica.Basic
@@ -444,29 +442,23 @@ public import Foundation.Propositional.Entailment.KreiselPutnam
 public import Foundation.Propositional.Entailment.LC
 public import Foundation.Propositional.Entailment.Minimal.Basic
 public import Foundation.Propositional.Entailment.Scott
-public import Foundation.Propositional.FMT.AxiomSer
+public import Foundation.Propositional.FMT.Axiom.Ser
 public import Foundation.Propositional.FMT.Basic
 public import Foundation.Propositional.FMT.Completeness
-public import Foundation.Propositional.FMT.Hilbert
-public import Foundation.Propositional.FMT.Logic
-public import Foundation.Propositional.FMT.Logic.VF
-public import Foundation.Propositional.FMT.Logic.VF_Ser
+public import Foundation.Propositional.FMT.Hilbert.Basic
+public import Foundation.Propositional.FMT.Hilbert.VF
+public import Foundation.Propositional.FMT.Hilbert.VF_Ser
 public import Foundation.Propositional.Formula.Basic
 public import Foundation.Propositional.Formula.NNFormula
 public import Foundation.Propositional.Heyting.Semantics
-public import Foundation.Propositional.Hilbert.Axiom
-public import Foundation.Propositional.Hilbert.F
 public import Foundation.Propositional.Hilbert.F.Basic
 public import Foundation.Propositional.Hilbert.F.Deduction
 public import Foundation.Propositional.Hilbert.F.Disjunctive
 public import Foundation.Propositional.Hilbert.F_WF
-public import Foundation.Propositional.Hilbert.Standard
-public import Foundation.Propositional.Hilbert.Standard.Basic
-public import Foundation.Propositional.Hilbert.Standard.Glivenko
-public import Foundation.Propositional.Hilbert.VF
+public import Foundation.Propositional.Hilbert.Minimal.Basic
+public import Foundation.Propositional.Hilbert.Minimal.Glivenko
 public import Foundation.Propositional.Hilbert.VF.Basic
 public import Foundation.Propositional.Hilbert.VF.Disjunctive
-public import Foundation.Propositional.Hilbert.WF
 public import Foundation.Propositional.Hilbert.WF.Basic
 public import Foundation.Propositional.Hilbert.WF_VF
 public import Foundation.Propositional.Kripke.AxiomDummett
@@ -476,43 +468,40 @@ public import Foundation.Propositional.Kripke.AxiomWLEM
 public import Foundation.Propositional.Kripke.Basic
 public import Foundation.Propositional.Kripke.Completeness
 public import Foundation.Propositional.Kripke.Filtration
-public import Foundation.Propositional.Kripke.Hilbert
-public import Foundation.Propositional.Kripke.Logic.Cl
-public import Foundation.Propositional.Kripke.Logic.Int
-public import Foundation.Propositional.Kripke.Logic.KC
-public import Foundation.Propositional.Kripke.Logic.KreiselPutnam
-public import Foundation.Propositional.Kripke.Logic.LC
+public import Foundation.Propositional.Kripke.Hilbert.Basic
+public import Foundation.Propositional.Kripke.Hilbert.Cl
+public import Foundation.Propositional.Kripke.Hilbert.Int.Basic
+public import Foundation.Propositional.Kripke.Hilbert.Int.DP
+public import Foundation.Propositional.Kripke.Hilbert.KC
+public import Foundation.Propositional.Kripke.Hilbert.KreiselPutnam
+public import Foundation.Propositional.Kripke.Hilbert.LC
 public import Foundation.Propositional.Kripke.Preservation
 public import Foundation.Propositional.Kripke.Rooted
-public import Foundation.Propositional.Kripke2.AxiomCorfl
-public import Foundation.Propositional.Kripke2.AxiomHrd
-public import Foundation.Propositional.Kripke2.AxiomPCon
-public import Foundation.Propositional.Kripke2.AxiomPSCon
-public import Foundation.Propositional.Kripke2.AxiomRfl
-public import Foundation.Propositional.Kripke2.AxiomSer
-public import Foundation.Propositional.Kripke2.AxiomSym
-public import Foundation.Propositional.Kripke2.AxiomTra
+public import Foundation.Propositional.Kripke2.Axiom.Corfl
+public import Foundation.Propositional.Kripke2.Axiom.Hrd
+public import Foundation.Propositional.Kripke2.Axiom.PCon
+public import Foundation.Propositional.Kripke2.Axiom.PSCon
+public import Foundation.Propositional.Kripke2.Axiom.Rfl
+public import Foundation.Propositional.Kripke2.Axiom.Ser
+public import Foundation.Propositional.Kripke2.Axiom.Sym
+public import Foundation.Propositional.Kripke2.Axiom.Tra
 public import Foundation.Propositional.Kripke2.Basic
-public import Foundation.Propositional.Kripke2.FTheory
-public import Foundation.Propositional.Kripke2.Hilbert
-public import Foundation.Propositional.Kripke2.Logic
-public import Foundation.Propositional.Kripke2.Logic.F
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Sym
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1_Hrd
-public import Foundation.Propositional.Kripke2.Logic.F_Ser
-public import Foundation.Propositional.Kripke2.Logic.F_Sym
-public import Foundation.Propositional.Kripke2.Logic.F_Tra1
-public import Foundation.Propositional.Kripke2.Logic.F_Tra1_Hrd
+public import Foundation.Propositional.Kripke2.Hilbert.Basic
+public import Foundation.Propositional.Kripke2.Hilbert.F
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Sym
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1
+public import Foundation.Propositional.Kripke2.Hilbert.F_Ser
+public import Foundation.Propositional.Kripke2.Hilbert.F_Sym
+public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1
 public import Foundation.Propositional.Logic.Basic
 public import Foundation.Propositional.Logic.Letterless_Int_Cl
 public import Foundation.Propositional.Logic.PostComplete
-public import Foundation.Propositional.Logic.Slash
+public import Foundation.Propositional.Logic.Superintuitionistic
 public import Foundation.Propositional.Neighborhood.NB.Basic
-public import Foundation.Propositional.Neighborhood.NB.Hilbert
-public import Foundation.Propositional.Neighborhood.NB.Logic
-public import Foundation.Propositional.Neighborhood.NB.Logic.WF
+public import Foundation.Propositional.Neighborhood.NB.Hilbert.Basic
+public import Foundation.Propositional.Neighborhood.NB.Hilbert.WF
+public import Foundation.Propositional.Slash
 public import Foundation.Propositional.Tait.Calculus
 public import Foundation.Propositional.Translation
 public import Foundation.ProvabilityLogic.Arithmetic
@@ -529,6 +518,8 @@ public import Foundation.ProvabilityLogic.Realization
 public import Foundation.ProvabilityLogic.S.Completeness
 public import Foundation.ProvabilityLogic.S.Soundness
 public import Foundation.ProvabilityLogic.SolovaySentences
+public import Foundation.SecondOrder.Derivation
+public import Foundation.SecondOrder.Semantics
 public import Foundation.SecondOrder.Syntax.Formula
 public import Foundation.SecondOrder.Syntax.Rew
 public import Foundation.Semantics.Algebra.Modal.Basic

Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean

@@ -164,7 +164,7 @@ lemma neg {φ : Semiformula L ξ n} : Hierarchy Γ s φ → Hierarchy Γ.alt s (
 @[simp] lemma neg_iff {φ : Semiformula L ξ n} : Hierarchy Γ s (∼φ) ↔ Hierarchy Γ.alt s φ :=
   ⟨fun h => by simpa using neg h, fun h => by simpa using neg h⟩
 
-@[simp] lemma imp_iff {φ ψ : Semiformula L ξ n} : Hierarchy Γ s (φ ➝ ψ) ↔ (Hierarchy Γ.alt s φ ∧ Hierarchy Γ s ψ) := by simp [Semiformula.imp_eq]
+@[simp] lemma imp_iff {φ ψ : Semiformula L ξ n} : Hierarchy Γ s (φ 🡒 ψ) ↔ (Hierarchy Γ.alt s φ ∧ Hierarchy Γ s ψ) := by simp [Semiformula.imp_eq]
 
 set_option linter.flexible false in
 @[simp] lemma ball_iff {Γ s n} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) :
@@ -336,11 +336,11 @@ lemma of_open {φ : Semiformula L ξ n} : φ.Open → Hierarchy Γ s φ := by
 variable {L : Language} [L.ORing]
 
 lemma iff_iff {φ ψ : Semiformula L ξ n} :
-    Hierarchy b s (φ ⭤ ψ) ↔ (Hierarchy b s φ ∧ Hierarchy b.alt s φ ∧ Hierarchy b s ψ ∧ Hierarchy b.alt s ψ) := by
+    Hierarchy b s (φ 🡘 ψ) ↔ (Hierarchy b s φ ∧ Hierarchy b.alt s φ ∧ Hierarchy b s ψ ∧ Hierarchy b.alt s ψ) := by
   simp [Semiformula.iff_eq]; tauto
 
 @[simp] lemma iff_iff₀ {φ ψ : Semiformula L ξ n} :
-    Hierarchy b 0 (φ ⭤ ψ) ↔ (Hierarchy b 0 φ ∧ Hierarchy b 0 ψ) := by
+    Hierarchy b 0 (φ 🡘 ψ) ↔ (Hierarchy b 0 φ ∧ Hierarchy b 0 ψ) := by
   simp [Semiformula.iff_eq]; tauto
 
 @[simp] lemma matrix_conj_iff {b s n} {φ : Fin m → Semiformula L ξ n} :

Foundation/FirstOrder/Arithmetic/Basic/Misc.lean

@@ -65,7 +65,7 @@ def Semiformula.toStringORing : ∀ {n}, Semiformula ℒₒᵣ ξ n → String
   | _,         nrel Language.LT.lt v => (v 0).toStringORing ++ " \\not < " ++ (v 1).toStringORing
   | _,                         φ ⋏ ψ => "[" ++ φ.toStringORing ++ "]" ++ " \\land " ++ "[" ++ ψ.toStringORing ++ "]"
   | _,                         φ ⋎ ψ => "[" ++ φ.toStringORing ++ "]" ++ " \\lor "  ++ "[" ++ ψ.toStringORing ++ "]"
-  | n, ∀⁰ (rel Language.LT.lt v ➝ φ) => "(\\forall x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
+  | n, ∀⁰ (rel Language.LT.lt v 🡒 φ) => "(\\forall x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
   | n, ∃⁰ (rel Language.LT.lt v ⋏ φ) => "(\\exists x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
   | n,                          ∀⁰ φ => "(\\forall x_{" ++ toString n ++ "}) " ++ "[" ++ φ.toStringORing ++ "]"
   | n,                          ∃⁰ φ => "(\\exists x_{" ++ toString n ++ "}) " ++ "[" ++ φ.toStringORing ++ "]"

Foundation/FirstOrder/Arithmetic/Definability/Definable.lean

@@ -789,13 +789,13 @@ lemma ball_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     ⟨ .mkSigma (∃⁰ (bf.val ⋏ (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
       by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
   | 𝚷 => exact
-    ⟨ .mkPi (∀⁰ (bf.val ➝ (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
+    ⟨ .mkPi (∀⁰ (bf.val 🡒 (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
       by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
   | 𝚫 =>
     exact .of_sigma_of_pi
       ⟨ .mkSigma (∃⁰ (bf.val ⋏ (∀⁰[“#0 < #1”] φ.sigma.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
           by intro v; simp [hbf.df.iff, hp.df.iff, HierarchySymbol.Semiformula.val_sigma] ⟩
-      ⟨ .mkPi (∀⁰ (bf.val ➝ (∀⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
+      ⟨ .mkPi (∀⁰ (bf.val 🡒 (∀⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
         by intro v; simp [hbf.df.iff, hp.df.iff, hp.proper.iff'] ⟩
 
 lemma bexs_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
@@ -808,13 +808,13 @@ lemma bexs_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     ⟨ .mkSigma (∃⁰ (bf.val ⋏ (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
       by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
   | 𝚷 => exact
-    ⟨ .mkPi (∀⁰ (bf.val ➝ (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
+    ⟨ .mkPi (∀⁰ (bf.val 🡒 (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
       by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
   | 𝚫 =>
     exact .of_sigma_of_pi
       ⟨ .mkSigma (∃⁰ (bf.val ⋏ (∃⁰[“#0 < #1”] φ.sigma.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
           by intro v; simp [hbf.df.iff, hp.df.iff, HierarchySymbol.Semiformula.val_sigma] ⟩
-      ⟨ .mkPi (∀⁰ (bf.val ➝ (∃⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
+      ⟨ .mkPi (∀⁰ (bf.val 🡒 (∃⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
         by intro v; simp [hbf.df.iff, hp.df.iff, hp.proper.iff'] ⟩
 
 lemma ball_le [V ⊧ₘ* 𝗣𝗔⁻] {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}