Documentation

Foundation.Logic.Semantics

Basic definitions and properties of semantics-related notions #

This file defines the semantics of formulas based on Tarski's truth definitions. Also provides 𝓜 characterization of compactness.

Main Definitions #

Notation #

class LO.Semantics (F : outParam (Type u_1)) (M : Type u_2) :
Type (max u_1 u_2)
  • Realize : MFProp
Instances
    class LO.Semantics.Top (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
    • realize_top : ∀ (𝓜 : M), 𝓜
    Instances
      @[simp]
      theorem LO.Semantics.Top.realize_top {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.Top M] (𝓜 : M) :
      𝓜
      class LO.Semantics.Bot (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
      • realize_bot : ∀ (𝓜 : M), ¬𝓜
      Instances
        @[simp]
        theorem LO.Semantics.Bot.realize_bot {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.Bot M] (𝓜 : M) :
        ¬𝓜
        class LO.Semantics.And (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
        Instances
          @[simp]
          theorem LO.Semantics.And.realize_and {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.And M] {𝓜 : M} {p : F} {q : F} :
          𝓜 p q 𝓜 p 𝓜 q
          class LO.Semantics.Or (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
          Instances
            @[simp]
            theorem LO.Semantics.Or.realize_or {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.Or M] {𝓜 : M} {p : F} {q : F} :
            𝓜 p q 𝓜 p 𝓜 q
            class LO.Semantics.Imp (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
            • realize_imp : ∀ {𝓜 : M} {p q : F}, 𝓜 p q 𝓜 p𝓜 q
            Instances
              @[simp]
              theorem LO.Semantics.Imp.realize_imp {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.Imp M] {𝓜 : M} {p : F} {q : F} :
              𝓜 p q 𝓜 p𝓜 q
              class LO.Semantics.Not (M : Type u_1) {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] :
              Instances
                @[simp]
                theorem LO.Semantics.Not.realize_not {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [self : LO.Semantics.Not M] {𝓜 : M} {p : F} :
                𝓜 p ¬𝓜 p
                @[simp]
                theorem LO.Semantics.realize_iff {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Semantics.Tarski M] {𝓜 : M} {p : F} {q : F} :
                𝓜 p q (𝓜 p 𝓜 q)
                @[simp]
                theorem LO.Semantics.realize_list_conj {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Semantics.Tarski M] {𝓜 : M} {l : List F} :
                𝓜 l.conj pl, 𝓜 p
                @[simp]
                theorem LO.Semantics.realize_finset_conj {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Semantics.Tarski M] {𝓜 : M} {s : Finset F} :
                𝓜 s.conj ps, 𝓜 p
                @[simp]
                theorem LO.Semantics.realize_list_disj {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Semantics.Tarski M] {𝓜 : M} {l : List F} :
                𝓜 l.disj pl, 𝓜 p
                @[simp]
                theorem LO.Semantics.realize_finset_disj {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Semantics.Tarski M] {𝓜 : M} {s : Finset F} :
                𝓜 s.disj ps, 𝓜 p
                class LO.Semantics.RealizeSet {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) (T : Set F) :
                • RealizeSet : ∀ ⦃f : F⦄, f T𝓜 f
                Instances
                  theorem LO.Semantics.RealizeSet.RealizeSet {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {𝓜 : M} {T : Set F} [self : 𝓜 ⊧* T] ⦃f : F :
                  f T𝓜 f
                  def LO.Semantics.Valid (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (f : F) :
                  Equations
                  Instances For
                    def LO.Semantics.Satisfiable (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) :
                    Equations
                    Instances For
                      def LO.Semantics.models (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) :
                      Set M
                      Equations
                      Instances For
                        def LO.Semantics.theory {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) :
                        Set F
                        Equations
                        Instances For
                          class LO.Semantics.Meaningful {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) :
                          • exists_unrealize : ∃ (f : F), ¬𝓜 f
                          Instances
                            theorem LO.Semantics.Meaningful.exists_unrealize {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {𝓜 : M} [self : LO.Semantics.Meaningful 𝓜] :
                            ∃ (f : F), ¬𝓜 f
                            Equations
                            • =
                            theorem LO.Semantics.meaningful_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {𝓜 : M} :
                            LO.Semantics.Meaningful 𝓜 ∃ (f : F), ¬𝓜 f
                            theorem LO.Semantics.not_meaningful_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) :
                            ¬LO.Semantics.Meaningful 𝓜 ∀ (f : F), 𝓜 f
                            theorem LO.Semantics.realizeSet_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {𝓜 : M} {T : Set F} :
                            𝓜 ⊧* T ∀ ⦃f : F⦄, f T𝓜 f
                            theorem LO.Semantics.RealizeSet.realize {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {f : F} {T : Set F} (𝓜 : M) [𝓜 ⊧* T] (hf : f T) :
                            𝓜 f
                            theorem LO.Semantics.RealizeSet.of_subset {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {U : Set F} {𝓜 : M} (h : 𝓜 ⊧* U) (ss : T U) :
                            𝓜 ⊧* T
                            theorem LO.Semantics.RealizeSet.of_subset' {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {U : Set F} {𝓜 : M} [𝓜 ⊧* U] (ss : T U) :
                            𝓜 ⊧* T
                            instance LO.Semantics.RealizeSet.empty' {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) :
                            𝓜 ⊧*
                            Equations
                            • =
                            @[simp]
                            theorem LO.Semantics.RealizeSet.empty {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) :
                            𝓜 ⊧*
                            @[simp]
                            theorem LO.Semantics.RealizeSet.singleton_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {f : F} {𝓜 : M} :
                            𝓜 ⊧* {f} 𝓜 f
                            @[simp]
                            theorem LO.Semantics.RealizeSet.insert_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {f : F} {𝓜 : M} :
                            𝓜 ⊧* insert f T 𝓜 f 𝓜 ⊧* T
                            @[simp]
                            theorem LO.Semantics.RealizeSet.union_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {U : Set F} {𝓜 : M} :
                            𝓜 ⊧* T U 𝓜 ⊧* T 𝓜 ⊧* U
                            @[simp]
                            theorem LO.Semantics.RealizeSet.image_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {ι : Type u_3} {f : ιF} {A : Set ι} {𝓜 : M} :
                            𝓜 ⊧* f '' A iA, 𝓜 f i
                            @[simp]
                            theorem LO.Semantics.RealizeSet.range_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {ι : Sort u_3} {f : ιF} {𝓜 : M} :
                            𝓜 ⊧* Set.range f ∀ (i : ι), 𝓜 f i
                            @[simp]
                            theorem LO.Semantics.RealizeSet.setOf_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {P : FProp} {𝓜 : M} :
                            𝓜 ⊧* setOf P ∀ (f : F), P f𝓜 f
                            theorem LO.Semantics.Satisfiable.of_subset {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {U : Set F} (h : LO.Semantics.Satisfiable M U) (ss : T U) :
                            instance LO.Semantics.instSet (M : Type u_1) {F : Type u_2} [LO.Semantics F M] :
                            Equations
                            @[simp]
                            theorem LO.Semantics.empty_models (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (f : F) :
                            def LO.Semantics.Consequence (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) (f : F) :
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem LO.Semantics.set_models_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {f : F} {s : Set M} :
                                s f 𝓜s, 𝓜 f
                                Equations
                                • LO.Semantics.instTopSet = { realize_top := }
                                theorem LO.Semantics.set_meaningful_iff_nonempty {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [∀ (𝓜 : M), LO.Semantics.Meaningful 𝓜] {s : Set M} :
                                theorem LO.Semantics.consequence_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {f : F} :
                                T ⊨[M] f ∀ {𝓜 : M}, 𝓜 ⊧* T𝓜 f
                                theorem LO.Semantics.consequence_iff' {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {f : F} :
                                T ⊨[M] f ∀ (𝓜 : M) [inst : 𝓜 ⊧* T], 𝓜 f
                                theorem LO.Semantics.weakening {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {U : Set F} {f : F} (h : T ⊨[M] f) (ss : T U) :
                                U ⊨[M] f
                                theorem LO.Semantics.of_mem {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} {f : F} (h : f T) :
                                T ⊨[M] f
                                def LO.Cumulative {F : Type u_2} (T : Set F) :
                                Equations
                                Instances For
                                  theorem LO.Cumulative.subset_of_le {F : Type u_2} {T : Set F} (H : LO.Cumulative T) {s₁ : } {s₂ : } (h : s₁ s₂) :
                                  T s₁ T s₂
                                  theorem LO.Cumulative.finset_mem {F : Type u_2} {T : Set F} (H : LO.Cumulative T) {u : Finset F} (hu : u ⋃ (s : ), T s) :
                                  ∃ (s : ), u T s
                                  class LO.Compact (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] :
                                  Instances
                                    theorem LO.Compact.compact {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [self : LO.Compact M] {T : Set F} :
                                    theorem LO.Compact.conseq_compact {M : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [𝓢 : LO.Semantics F M] [LO.Compact M] {T : Set F} [LO.Semantics.Tarski M] [DecidableEq F] {f : F} :
                                    T ⊨[M] f ∃ (u : Finset F), u T u ⊨[M] f
                                    theorem LO.Compact.compact_cumulative {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.Compact M] {T : Set F} (hT : LO.Cumulative T) :
                                    LO.Semantics.Satisfiable M (⋃ (s : ), T s) ∀ (s : ), LO.Semantics.Satisfiable M (T s)