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 (M : Type u_1) (F : outParam (Type u_2)) : Type (max u_1 u_2)

Semantics M F denotes semantics of formulae F for models M`

• Models : 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))

@[reducible, inline]

abbrev LO.Semantics.NotModels {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) (φ : F) : Prop

The negation of 𝓜 ⊧ φ

Equations

• (𝓜 ⊭ φ) = ¬𝓜 ⊧ φ

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))

Tarski's truth definitions

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

Tarski's truth definition for ⊤.

• models_verum (𝓜 : M) : 𝓜 ⊧ ⊤

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

Tarski's truth definition for ⊥.

• models_falsum (𝓜 : M) : ¬𝓜 ⊧ ⊥

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

Tarski's truth definition for ⋏.

• models_and {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ ⋏ ψ ↔ 𝓜 ⊧ φ ∧ 𝓜 ⊧ ψ

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

Tarski's truth definition for ⋎.

• models_or {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ ⋎ ψ ↔ 𝓜 ⊧ φ ∨ 𝓜 ⊧ ψ

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

Tarski's truth definition for 🡒.

• models_imply {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ 🡒 ψ ↔ 𝓜 ⊧ φ → 𝓜 ⊧ ψ

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

Tarski's truth definition for ∼.

• models_not {𝓜 : M} {φ : F} : 𝓜 ⊧ ∼φ ↔ ¬𝓜 ⊧ φ

class LO.Semantics.Tarski (M : Type u_1) {F : Type u_2} [𝓢 : Semantics M F] [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

Tarski's truth definitions.

• models_verum (𝓜 : M) : 𝓜 ⊧ ⊤
• models_falsum (𝓜 : M) : ¬𝓜 ⊧ ⊥
• models_and {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ ⋏ ψ ↔ 𝓜 ⊧ φ ∧ 𝓜 ⊧ ψ
• models_or {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ ⋎ ψ ↔ 𝓜 ⊧ φ ∨ 𝓜 ⊧ ψ
• models_imply {𝓜 : M} {φ ψ : F} : 𝓜 ⊧ φ 🡒 ψ ↔ 𝓜 ⊧ φ → 𝓜 ⊧ ψ
• models_not {𝓜 : M} {φ : F} : 𝓜 ⊧ ∼φ ↔ ¬𝓜 ⊧ φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Semantics.models_list_conj' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] {𝓜 : M} {α : Type u_3} {l : List α} {ι : α → F} : 𝓜 ⊧ List.conj' ι l ↔ ∀ i ∈ l, 𝓜 ⊧ ι i

@[simp]

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

@[simp]

theorem LO.Semantics.models_finset_conj' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] {𝓜 : M} {α : Type u_3} {s : Finset α} {ι : α → F} : 𝓜 ⊧ s.conj' ι ↔ ∀ i ∈ s, 𝓜 ⊧ ι i

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Semantics.models_list_disj' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] {𝓜 : M} {α : Type u_3} {l : List α} {ι : α → F} : 𝓜 ⊧ List.disj' ι l ↔ ∃ i ∈ l, 𝓜 ⊧ ι i

@[simp]

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

@[simp]

theorem LO.Semantics.models_finset_disj' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] {𝓜 : M} {α : Type u_3} {s : Finset α} {ι : α → F} : 𝓜 ⊧ s.disj' ι ↔ ∃ i ∈ s, 𝓜 ⊧ ι i

A semantics and satisfiability over a set of formulas

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

𝓜 ⊧* T denotes 𝓜 ⊧ φ for all φ in T.

• models_set ⦃φ : F⦄ : φ ∈ T → 𝓜 ⊧ φ

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} [𝓢 : Semantics M F] (φ : F) : Prop

Equations

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

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

Equations

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

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

A set of models satisfies set of formulae T.

Equations

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

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

A set of formulae satisfied by model 𝓜.

Equations

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

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

• exists_unmodels : ∃ (φ : F), 𝓜 ⊭ φ

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

theorem LO.Semantics.meaningful_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {𝓜 : M} : Meaningful 𝓜 ↔ ∃ (φ : F), 𝓜 ⊭ φ

theorem LO.Semantics.not_meaningful_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) : ¬Meaningful 𝓜 ↔ ∀ (φ : F), 𝓜 ⊧ φ

theorem LO.Semantics.modelsSet_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {𝓜 : M} {T : Set F} : 𝓜 ⊧* T ↔ ∀ ⦃φ : F⦄, φ ∈ T → 𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.modelsTheory_theory {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) : 𝓜 ⊧* theory 𝓜

@[simp]

theorem LO.Semantics.theory_satisfiable {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) : Satisfiable M (theory 𝓜)

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

@[simp]

theorem LO.Semantics.satisfiable_conj₂ {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] [DecidableEq F] (l : List F) : Satisfiable M {⋀l} ↔ Satisfiable M {φ : F | φ ∈ l}

@[simp]

theorem LO.Semantics.satisfiable_fconj {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [LogicalConnective F] [Tarski M] [DecidableEq F] (s : Finset F) : Satisfiable M {s.conj} ↔ Satisfiable M {φ : F | φ ∈ s}

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

theorem LO.Semantics.ModelsSet.models {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {φ : F} {T : Set F} (𝓜 : M) [𝓜 ⊧* T] (hf : φ ∈ T) : 𝓜 ⊧ φ

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

theorem LO.Semantics.ModelsSet.of_subset' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T U : Set F} {𝓜 : M} [𝓜 ⊧* U] (ss : T ⊆ U) : 𝓜 ⊧* T

instance LO.Semantics.ModelsSet.empty' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) : 𝓜 ⊧* ∅

@[simp]

theorem LO.Semantics.ModelsSet.empty {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] (𝓜 : M) : 𝓜 ⊧* ∅

@[simp]

theorem LO.Semantics.ModelsSet.singleton_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {φ : F} {𝓜 : M} : 𝓜 ⊧* {φ} ↔ 𝓜 ⊧ φ

@[simp]

theorem LO.Semantics.ModelsSet.insert_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T : Set F} {φ : F} {𝓜 : M} : 𝓜 ⊧* insert φ T ↔ 𝓜 ⊧ φ ∧ 𝓜 ⊧* T

@[simp]

theorem LO.Semantics.ModelsSet.union_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T U : Set F} {𝓜 : M} : 𝓜 ⊧* T ∪ U ↔ 𝓜 ⊧* T ∧ 𝓜 ⊧* U

@[simp]

theorem LO.Semantics.ModelsSet.image_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {ι : Type u_3} {φ : ι → F} {A : Set ι} {𝓜 : M} : 𝓜 ⊧* φ '' A ↔ ∀ i ∈ A, 𝓜 ⊧ φ i

@[simp]

theorem LO.Semantics.ModelsSet.range_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {ι : Sort u_3} {φ : ι → F} {𝓜 : M} : 𝓜 ⊧* Set.range φ ↔ ∀ (i : ι), 𝓜 ⊧ φ i

@[simp]

theorem LO.Semantics.ModelsSet.setOf_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {P : F → Prop} {𝓜 : M} : 𝓜 ⊧* setOf P ↔ ∀ (φ : F), P φ → 𝓜 ⊧ φ

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

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

Logical consequence

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

The logical conseqence.

Equations

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

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} [𝓢 : Semantics M F] {φ : F} {s : Set M} : s ⊧ φ ↔ ∀ 𝓜 ∈ s, 𝓜 ⊧ φ

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

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

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

theorem LO.Semantics.consequence_iff {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T : Set F} {φ : F} : T ⊨[M] φ ↔ ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ φ

theorem LO.Semantics.consequence_iff' {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T : Set F} {φ : F} : T ⊨[M] φ ↔ ∀ (𝓜 : M) [𝓜 ⊧* T], 𝓜 ⊧ φ

theorem LO.Semantics.consequence_iff_not_satisfiable {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T : Set F} [LogicalConnective F] [Tarski M] {φ : F} : T ⊨[M] φ ↔ ¬Satisfiable M (insert (∼φ) T)

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

theorem LO.Semantics.of_mem {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] {T : Set F} {φ : F} (h : φ ∈ T) : T ⊨[M] φ

Compactness

def LO.Cumulative {F : Type u_2} (T : ℕ → Set F) : Prop

A cumulative sequence of sets.

Equations

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

theorem LO.Cumulative.subset_of_le {F : Type u_2} {T : ℕ → Set F} (H : Cumulative T) {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : T s₁ ⊆ T s₂

theorem LO.Cumulative.finset_mem {F : Type u_2} {T : ℕ → Set F} (H : 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} [𝓢 : Semantics M F] : Prop

A Semantics M F is compact if, for any set of formulas, the satisfiability of the set is equivalent to the satisfiability of every finite subset of it.

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

theorem LO.Compact.conseq_compact {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [Compact M] {T : Set F} [LogicalConnective F] [Semantics.Tarski M] [DecidableEq F] {φ : F} : T ⊨[M] φ ↔ ∃ (u : Finset F), ↑u ⊆ T ∧ ↑u ⊨[M] φ

theorem LO.Compact.compact_cumulative {M : Type u_1} {F : Type u_2} [𝓢 : Semantics M F] [Compact M] {T : ℕ → Set F} (hT : Cumulative T) : Semantics.Satisfiable M (⋃ (s : ℕ), T s) ↔ ∀ (s : ℕ), Semantics.Satisfiable M (T s)