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

• LO.Semantics: The realization of 𝓜 formula.
• LO.Compact: The semantic compactness of Foundation.

Notation

• 𝓜 ⊧ φ: a proposition that states 𝓜 satisfies φ.
• 𝓜 ⊧* T: a proposition that states that 𝓜 satisfies each formulae in a set T.

class LO.Semantics (F : outParam (Type u_1)) (M : Type u_2) : Type (max u_1 u_2)

• Realize : M → F → Prop

def LO.Semantics.«term_⊧_» : Lean.TrailingParserDescr

Equations

• LO.Semantics.«term_⊧_» = Lean.ParserDescr.trailingNode `LO.Semantics.«term_⊧_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 46))

class LO.Semantics.Top (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_top : ∀ (𝓜 : M), 𝓜 ⊧ ⊤

class LO.Semantics.Bot (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_bot : ∀ (𝓜 : M), ¬𝓜 ⊧ ⊥

class LO.Semantics.And (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_and : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ⋏ ψ ↔ 𝓜 ⊧ φ ∧ 𝓜 ⊧ ψ

class LO.Semantics.Or (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_or : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ⋎ ψ ↔ 𝓜 ⊧ φ ∨ 𝓜 ⊧ ψ

class LO.Semantics.Imp (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_imp : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ➝ ψ ↔ 𝓜 ⊧ φ → 𝓜 ⊧ ψ

class LO.Semantics.Not (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] : Prop

• realize_not : ∀ {𝓜 : M} {φ : F}, 𝓜 ⊧ ∼φ ↔ ¬𝓜 ⊧ φ

class LO.Semantics.Tarski (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] extends LO.Semantics.Top M, LO.Semantics.Bot M, LO.Semantics.And M, LO.Semantics.Or M, LO.Semantics.Imp M, LO.Semantics.Not M : Prop

• realize_top : ∀ (𝓜 : M), 𝓜 ⊧ ⊤
• realize_bot : ∀ (𝓜 : M), ¬𝓜 ⊧ ⊥
• realize_and : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ⋏ ψ ↔ 𝓜 ⊧ φ ∧ 𝓜 ⊧ ψ
• realize_or : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ⋎ ψ ↔ 𝓜 ⊧ φ ∨ 𝓜 ⊧ ψ
• realize_imp : ∀ {𝓜 : M} {φ ψ : F}, 𝓜 ⊧ φ ➝ ψ ↔ 𝓜 ⊧ φ → 𝓜 ⊧ ψ
• realize_not : ∀ {𝓜 : M} {φ : F}, 𝓜 ⊧ ∼φ ↔ ¬𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.realize_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ ⭤ ψ ↔ (𝓜 ⊧ φ ↔ 𝓜 ⊧ ψ)

@[simp]

theorem LO.Semantics.realize_list_conj {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] {𝓜 : M} {l : List F} : 𝓜 ⊧ l.conj ↔ ∀ φ ∈ l, 𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.realize_finset_conj {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] {𝓜 : M} {s : Finset F} : 𝓜 ⊧ s.conj ↔ ∀ φ ∈ s, 𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.realize_list_disj {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] {𝓜 : M} {l : List F} : 𝓜 ⊧ l.disj ↔ ∃ φ ∈ l, 𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.realize_finset_disj {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] {𝓜 : M} {s : Finset F} : 𝓜 ⊧ s.disj ↔ ∃ φ ∈ s, 𝓜 ⊧ φ

class LO.Semantics.RealizeSet {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) (T : Set F) : Prop

• RealizeSet : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f

def LO.Semantics.«term_⊧*_» : Lean.TrailingParserDescr

Equations

• LO.Semantics.«term_⊧*_» = Lean.ParserDescr.trailingNode `LO.Semantics.«term_⊧*_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧* ") (Lean.ParserDescr.cat `term 46))

def LO.Semantics.Valid (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (f : F) : Prop

Equations

• LO.Semantics.Valid M f = ∀ (𝓜 : M), 𝓜 ⊧ f

def LO.Semantics.Satisfiable (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) : Prop

Equations

• LO.Semantics.Satisfiable M T = ∃ (𝓜 : M), 𝓜 ⊧* T

def LO.Semantics.models (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) : Set M

Equations

• LO.Semantics.models M T = {𝓜 : M | 𝓜 ⊧* T}

def LO.Semantics.theory {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) : Set F

Equations

• LO.Semantics.theory 𝓜 = {φ : F | 𝓜 ⊧ φ}

class LO.Semantics.Meaningful {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] (𝓜 : M) : Prop

• exists_unrealize : ∃ (f : F), ¬𝓜 ⊧ f

instance LO.Semantics.instMeaningfulOfBot {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Bot M] (𝓜 : M) : LO.Semantics.Meaningful 𝓜

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.not_satisfiable_finset {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] [DecidableEq F] (t : Finset F) : ¬LO.Semantics.Satisfiable M ↑t ↔ LO.Semantics.Valid M (Finset.image (fun (x : F) => ∼x) t).disj

theorem LO.Semantics.satisfiableSet_iff_models_nonempty {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} : LO.Semantics.Satisfiable M T ↔ (LO.Semantics.models M T).Nonempty

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 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 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 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 ↔ ∀ i ∈ A, 𝓜 ⊧ 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 : F → Prop} {𝓜 : M} : 𝓜 ⊧* setOf P ↔ ∀ (f : F), P f → 𝓜 ⊧ f

theorem LO.Semantics.valid_neg_iff {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Tarski M] (f : F) : LO.Semantics.Valid M (∼f) ↔ ¬LO.Semantics.Satisfiable M {f}

theorem LO.Semantics.Satisfiable.of_subset {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T U : Set F} (h : LO.Semantics.Satisfiable M U) (ss : T ⊆ U) : LO.Semantics.Satisfiable M T

instance LO.Semantics.instSet (M : Type u_1) {F : Type u_2} [LO.Semantics F M] : LO.Semantics F (Set M)

Equations

• LO.Semantics.instSet M = { Realize := fun (s : Set M) (f : F) => ∀ ⦃𝓜 : M⦄, 𝓜 ∈ s → 𝓜 ⊧ f }

@[simp]

theorem LO.Semantics.empty_models (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (f : F) : ∅ ⊧ f

def LO.Semantics.Consequence (M : Type u_1) {F : Type u_2} [𝓢 : LO.Semantics F M] (T : Set F) (f : F) : Prop

Equations

• (T ⊨[M] f) = (LO.Semantics.models M T ⊧ f)

def LO.Semantics.«term_⊨[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

instance LO.Semantics.instTopSet {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [LO.Semantics.Top M] : LO.Semantics.Top (Set M)

Equations

• ⋯ = ⋯

theorem LO.Semantics.set_meaningful_iff_nonempty {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.LogicalConnective F] [∀ (𝓜 : M), LO.Semantics.Meaningful 𝓜] {s : Set M} : LO.Semantics.Meaningful s ↔ s.Nonempty

theorem LO.Semantics.meaningful_iff_satisfiableSet {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} [LO.LogicalConnective F] [∀ (𝓜 : M), LO.Semantics.Meaningful 𝓜] : LO.Semantics.Satisfiable M T ↔ LO.Semantics.Meaningful (LO.Semantics.models M T)

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.consequence_iff_not_satisfiable {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T : Set F} [LO.LogicalConnective F] [LO.Semantics.Tarski M] {f : F} : T ⊨[M] f ↔ ¬LO.Semantics.Satisfiable M (insert (∼f) T)

theorem LO.Semantics.weakening {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] {T 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) : Prop

Equations

• LO.Cumulative T = ∀ (s : ℕ), T s ⊆ T (s + 1)

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] : Prop

• compact : ∀ {T : Set F}, LO.Semantics.Satisfiable M T ↔ ∀ (u : Finset F), ↑u ⊆ T → LO.Semantics.Satisfiable M ↑u

theorem LO.Compact.conseq_compact {M : Type u_1} {F : Type u_2} [𝓢 : LO.Semantics F M] [LO.Compact M] {T : Set F} [LO.LogicalConnective 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)