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 #
𝓜 ⊧ p
: a proposition that states𝓜
satisfiesp
.𝓜 ⊧* T
: a proposition that states that𝓜
satisfies each formulae in a setT
.
Equations
- LO.Semantics.«term_⊧_» = Lean.ParserDescr.trailingNode `LO.Semantics.term_⊧_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 46))
Instances For
class
LO.Semantics.Top
(M : Type u_1)
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F 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]
:
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}
:
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}
:
class
LO.Semantics.Imp
(M : Type u_1)
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
:
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}
:
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}
:
class
LO.Semantics.Tarski
(M : Type u_1)
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
extends
LO.Semantics.Top
,
LO.Semantics.Bot
,
LO.Semantics.And
,
LO.Semantics.Or
,
LO.Semantics.Imp
,
LO.Semantics.Not
:
Instances
@[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}
:
@[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}
:
@[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}
:
@[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}
:
@[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}
:
class
LO.Semantics.RealizeSet
{M : Type u_1}
{F : Type u_2}
[𝓢 : LO.Semantics F M]
(𝓜 : M)
(T : Set 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⦄
:
Equations
- LO.Semantics.«term_⊧*_» = Lean.ParserDescr.trailingNode `LO.Semantics.term_⊧*_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧* ") (Lean.ParserDescr.cat `term 46))
Instances For
Equations
- LO.Semantics.Valid M f = ∀ (𝓜 : M), 𝓜 ⊧ f
Instances For
Equations
- LO.Semantics.Satisfiable M T = ∃ (𝓜 : M), 𝓜 ⊧* T
Instances For
Equations
- LO.Semantics.models M T = {𝓜 : M | 𝓜 ⊧* T}
Instances For
Equations
- LO.Semantics.theory 𝓜 = {f : F | 𝓜 ⊧ f}
Instances For
Instances
theorem
LO.Semantics.Meaningful.exists_unrealize
{M : Type u_1}
{F : Type u_2}
[𝓢 : LO.Semantics F M]
{𝓜 : M}
[self : LO.Semantics.Meaningful 𝓜]
:
instance
LO.Semantics.instMeaningfulOfBot
{M : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
[LO.Semantics.Bot M]
(𝓜 : M)
:
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}
:
theorem
LO.Semantics.not_satisfiable_finset
{M : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
[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 : 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}
:
@[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}
:
@[simp]
theorem
LO.Semantics.RealizeSet.setOf_iff
{M : Type u_1}
{F : Type u_2}
[𝓢 : LO.Semantics F M]
{P : F → Prop}
{𝓜 : M}
:
theorem
LO.Semantics.valid_neg_iff
{M : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
[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 : 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]
:
LO.Semantics F (Set M)
Equations
- LO.Semantics.instSet M = { Realize := fun (s : Set M) (f : F) => ∀ ⦃𝓜 : M⦄, 𝓜 ∈ s → 𝓜 ⊧ f }
@[simp]
def
LO.Semantics.Consequence
(M : Type u_1)
{F : Type u_2}
[𝓢 : LO.Semantics F M]
(T : Set F)
(f : F)
:
Equations
- (T ⊨[M] f) = (LO.Semantics.models M T ⊧ f)
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}
:
instance
LO.Semantics.instTopSet
{M : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
[LO.Semantics.Top M]
:
LO.Semantics.Top (Set M)
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}
:
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}
[∀ (𝓜 : M), LO.Semantics.Meaningful 𝓜]
:
theorem
LO.Semantics.consequence_iff_not_satisfiable
{M : Type u_1}
{F : Type u_2}
[LO.LogicalConnective F]
[𝓢 : LO.Semantics F M]
{T : Set F}
[LO.Semantics.Tarski M]
{f : 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)
:
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₂
- compact : ∀ {T : Set F}, LO.Semantics.Satisfiable M T ↔ ∀ (u : Finset F), ↑u ⊆ T → LO.Semantics.Satisfiable M ↑u
Instances
theorem
LO.Compact.compact
{M : Type u_1}
{F : Type u_2}
[𝓢 : LO.Semantics F M]
[self : LO.Compact M]
{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.LogicalConnective F]
[𝓢 : LO.Semantics F M]
[LO.Compact M]
{T : Set F}
[LO.Semantics.Tarski M]
[DecidableEq F]
{f : 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)