Skolem hull #

source

def FFL.FirstOrder.Language.skolemFunction₁ (L : Language) :

Language

Skolem function of rank 1

Equations

L.skolemFunction₁ = { Func := fun (k : ℕ) => FFL.FirstOrder.Semisentence L (k + 1), Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Semisentence.skolem₁ {k : ℕ} {L : Language} (φ : Semisentence L (k + 1)) :

L.skolemFunction₁.Func k

Equations

φ.skolem₁ = φ

Instances For

source

@[instance_reducible]

instance FFL.FirstOrder.instEncodableSkolemFunction₁ (L : Language) [L.Encodable] :

L.skolemFunction₁.Encodable

Equations

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

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Tarski.Structure.skolem (L : Language) (M : Type v) [Nonempty M] [𝓼 : Structure L M] :

Structure L.skolemFunction₁ M

Equations

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

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.val_skolem_func {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {k : ℕ} {v : Fin k → M} (φ : Semisentence L (k + 1)) :

func φ.skolem₁ v = Classical.epsilon fun (z : M) => (Semiformula.Evalb (z :> v)) φ

source

def FFL.FirstOrder.Tarski.Structure.SkolemHull (L : Language) {M : Type v} [Nonempty M] [𝓼 : Structure L M] (s : Set M) :

Set M

The Skolem hull of subset of structure.

Equations

FFL.FirstOrder.Tarski.Structure.SkolemHull L s = Set.range fun (t : FFL.FirstOrder.Term L.skolemFunction₁ ↑s) => FFL.FirstOrder.Semiterm.val ![] Subtype.val t

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Tarski.Structure.SkolemHull₀ (L : Language) (M : Type v) [Nonempty M] [𝓼 : Structure L M] :

Set M

Equations

FFL.FirstOrder.Tarski.Structure.SkolemHull₀ L M = FFL.FirstOrder.Tarski.Structure.SkolemHull L ∅

Instances For

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.mem_iff {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {s : Set M} {x : M} :

x ∈ SkolemHull L s ↔ ∃ (t : Term L.skolemFunction₁ ↑s), Semiterm.val ![] Subtype.val t = x

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.val_mem {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {s : Set M} (t : Term L.skolemFunction₁ ↑s) :

Semiterm.val ![] Subtype.val t ∈ SkolemHull L s

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.subset {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {s : Set M} :

s ⊆ SkolemHull L s

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.closed {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {s : Set M} {k : ℕ} {v : Fin k → M} (hv : ∀ (i : Fin k), v i ∈ SkolemHull L s) {φ : Semisentence L (k + 1)} (H : ∃ (z : M), (Semiformula.Evalb (z :> v)) φ) :

∃ z ∈ SkolemHull L s, (Semiformula.Evalb (z :> v)) φ

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.closed_func {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] {s : Set M} [L.Eq] [Structure.Eq L M] {k : ℕ} {v : Fin k → M} (hv : ∀ (i : Fin k), v i ∈ SkolemHull L s) {f : L.Func k} :

func f v ∈ SkolemHull L s

source

@[instance_reducible, instance 50]

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.str {L : Language} {M : Type v} [Nonempty M] (𝓼 : Structure L M) (s : Set M) [L.Eq] [Structure.Eq L M] :

Structure L ↑(SkolemHull L s)

Equations

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

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.set_nonempty {L : Language} {M : Type v} [Nonempty M] (𝓼 : Structure L M) (s : Set M) :

(SkolemHull L s).Nonempty

source

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.nonempty {L : Language} {M : Type v} [Nonempty M] (𝓼 : Structure L M) (s : Set M) :

Nonempty ↑(SkolemHull L s)

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.str_func_def {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] {k : ℕ} (f : L.Func k) (v : Fin k → ↑(SkolemHull L s)) :

func f v = ⟨func f fun (i : Fin k) => ↑(v i), ⋯⟩

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.str_rel_def {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] {k : ℕ} (R : L.Rel k) (v : Fin k → ↑(SkolemHull L s)) :

rel R v ↔ rel R fun (i : Fin k) => ↑(v i)

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.str_val {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] {ξ : Type u_1} {n : ℕ} (t : Semiterm L ξ n) (b : Fin n → ↑(SkolemHull L s)) (f : ξ → ↑(SkolemHull L s)) :

↑(Semiterm.val b f t) = Semiterm.val (fun (x : Fin n) => ↑(b x)) (fun (x : ξ) => ↑(f x)) t

source

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.str_eval {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] {n : ℕ} {b : Fin n → ↑(SkolemHull L s)} {φ : Semisentence L n} :

(Semiformula.Evalb b) φ ↔ (Semiformula.Evalb fun (x : Fin n) => ↑(b x)) φ

source

@[instance 50]

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.elementaryEquiv {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] :

↑(SkolemHull L s) ≡ₑ[L] M

Downward Löwenheim-Skolem theorem for countable language (1)

source

@[instance 50]

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.eq {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] :

Structure.Eq L ↑(SkolemHull L s)

source

@[instance_reducible, instance 50]

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.membership {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [Membership M M] :

Membership ↑(SkolemHull L s) ↑(SkolemHull L s)

Equations

FFL.FirstOrder.Tarski.Structure.SkolemHull.membership = { mem := fun (y x : ↑(FFL.FirstOrder.Tarski.Structure.SkolemHull L s)) => ↑x ∈ ↑y }

source

@[instance 50]

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.mem {L : Language} {M : Type v} [Nonempty M] {𝓼 : Structure L M} {s : Set M} [L.Eq] [Structure.Eq L M] [Semiformula.Operator.Mem L] [Membership M M] [Structure.Mem L M] :

Structure.Mem L ↑(SkolemHull L s)

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.set_countable {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] [L.Encodable] {s : Set M} (hs : s.Countable) :

(SkolemHull L s).Countable

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.countable {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] [L.Encodable] {s : Set M} (hs : s.Countable) :

Countable ↑(SkolemHull L s)

source

instance FFL.FirstOrder.Tarski.Structure.SkolemHull.countable₀ {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] [L.Encodable] :

Countable ↑(SkolemHull₀ L M)

source

theorem FFL.FirstOrder.Tarski.Structure.SkolemHull.card_le_aleph0 {L : Language} {M : Type v} [Nonempty M] [𝓼 : Structure L M] [L.Encodable] {s : Set M} (hs : s.Countable) :

Cardinal.mk ↑(SkolemHull L s) ≤ Cardinal.aleph0

Downward Löwenheim-Skolem theorem for countable language (2)

Documentation

Foundation.FirstOrder.Tarski.Skolemization

Skolem hull #