Basics on First-Order Structures #
This file defines first-order languages and structures in the style of the Flypitch project.
Main Definitions #
- A
first_order.language.termis defined so thatL.term αis the type ofL-terms with free variables indexed byα. - A
first_order.language.formulais defined so thatL.formula αis the type ofL-formulas with free variables indexed byα. - A
first_order.language.sentenceis a formula with no free variables. - A
first_order.language.theoryis a set of sentences.
References #
For the Flypitch project:
- var : Π {L : first_order.language} {α : Type}, α → L.term α
- func : Π {L : first_order.language} {α : Type} {l : ℕ}, L.functions l → (fin l → L.term α) → L.term α
A term on α is either a variable indexed by an element of α
or a function symbol applied to simpler terms.
@[simp]
Relabels a term's variables along a particular function.
Equations
- first_order.language.term.relabel g (first_order.language.term.func f ts) = first_order.language.term.func f (λ (i : fin a_2), first_order.language.term.relabel g (ts i))
- first_order.language.term.relabel g (first_order.language.term.var i) = first_order.language.term.var (g i)
@[protected, instance]
@[protected, instance]
Equations
- first_order.language.term.has_coe = {coe := λ (c : L.const), first_order.language.term.func c fin_zero_elim}
@[simp]
def
first_order.language.realize_term
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{α : Type}
(v : α → M)
(t : L.term α) :
M
A term t with variables indexed by α can be evaluated by giving a value to each variable.
Equations
- first_order.language.realize_term v (first_order.language.term.func f ts) = first_order.language.Structure.fun_map f (λ (i : fin a_5), first_order.language.realize_term v (ts i))
- first_order.language.realize_term v (first_order.language.term.var k) = v k
@[simp]
theorem
first_order.language.realize_term_relabel
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{α β : Type}
(g : α → β)
(v : β → M)
(t : L.term α) :
@[simp]
theorem
first_order.language.hom.realize_term
{L : first_order.language}
{M : Type u_1}
{N : Type u_2}
[L.Structure M]
[L.Structure N]
{α : Type}
(v : α → M)
(t : L.term α)
(g : L.hom M N) :
first_order.language.realize_term (⇑g ∘ v) t = ⇑g (first_order.language.realize_term v t)
@[simp]
theorem
first_order.language.embedding.realize_term
{L : first_order.language}
{M : Type u_1}
{N : Type u_2}
[L.Structure M]
[L.Structure N]
{α : Type}
(v : α → M)
(t : L.term α)
(g : L.embedding M N) :
first_order.language.realize_term (⇑g ∘ v) t = ⇑g (first_order.language.realize_term v t)
@[simp]
theorem
first_order.language.equiv.realize_term
{L : first_order.language}
{M : Type u_1}
{N : Type u_2}
[L.Structure M]
[L.Structure N]
{α : Type}
(v : α → M)
(t : L.term α)
(g : L.equiv M N) :
first_order.language.realize_term (⇑g ∘ v) t = ⇑g (first_order.language.realize_term v t)
inductive
first_order.language.bounded_formula
(L : first_order.language)
(α : Type) :
ℕ → Type (max u v)
- bd_falsum : Π {L : first_order.language} {α : Type} {n : ℕ}, L.bounded_formula α n
- bd_equal : Π {L : first_order.language} {α : Type} {n : ℕ}, L.term (α ⊕ fin n) → L.term (α ⊕ fin n) → L.bounded_formula α n
- bd_rel : Π {L : first_order.language} {α : Type} {n l : ℕ}, L.relations l → (fin l → L.term (α ⊕ fin n)) → L.bounded_formula α n
- bd_imp : Π {L : first_order.language} {α : Type} {n : ℕ}, L.bounded_formula α n → L.bounded_formula α n → L.bounded_formula α n
- bd_all : Π {L : first_order.language} {α : Type} {n : ℕ}, L.bounded_formula α (n + 1) → L.bounded_formula α n
bounded_formula α n is the type of formulas with free variables indexed by α and up to n
additional free variables.
@[protected, instance]
def
first_order.language.bounded_formula.inhabited
(L : first_order.language)
{α : Type}
{n : ℕ} :
inhabited (L.bounded_formula α n)
formula α is the type of formulas with all free variables indexed by α.
Equations
- L.formula α = L.bounded_formula α 0
A sentence is a formula with no free variables.
A theory is a set of sentences.
@[simp]
theorem
first_order.language.bounded_formula.has_bot_bot
{L : first_order.language}
{α : Type}
{n : ℕ} :
@[protected, instance]
def
first_order.language.bounded_formula.has_bot
{L : first_order.language}
{α : Type}
{n : ℕ} :
has_bot (L.bounded_formula α n)
def
first_order.language.bd_not
{L : first_order.language}
{α : Type}
{n : ℕ}
(φ : L.bounded_formula α n) :
L.bounded_formula α n
The negation of a bounded formula is also a bounded formula.
Equations
@[protected, instance]
def
first_order.language.bounded_formula.has_top
{L : first_order.language}
{α : Type}
{n : ℕ} :
has_top (L.bounded_formula α n)
@[simp]
theorem
first_order.language.bounded_formula.has_top_top
{L : first_order.language}
{α : Type}
{n : ℕ} :
@[protected, instance]
def
first_order.language.bounded_formula.has_inf
{L : first_order.language}
{α : Type}
{n : ℕ} :
has_inf (L.bounded_formula α n)
Equations
- first_order.language.bounded_formula.has_inf = {inf := λ (f g : L.bounded_formula α n), first_order.language.bd_not (f.bd_imp (first_order.language.bd_not g))}
@[simp]
theorem
first_order.language.bounded_formula.has_inf_inf
{L : first_order.language}
{α : Type}
{n : ℕ}
(f g : L.bounded_formula α n) :
f ⊓ g = first_order.language.bd_not (f.bd_imp (first_order.language.bd_not g))
@[simp]
theorem
first_order.language.bounded_formula.has_sup_sup
{L : first_order.language}
{α : Type}
{n : ℕ}
(f g : L.bounded_formula α n) :
f ⊔ g = (first_order.language.bd_not f).bd_imp g
@[protected, instance]
def
first_order.language.bounded_formula.has_sup
{L : first_order.language}
{α : Type}
{n : ℕ} :
has_sup (L.bounded_formula α n)
Equations
- first_order.language.bounded_formula.has_sup = {sup := λ (f g : L.bounded_formula α n), (first_order.language.bd_not f).bd_imp g}
@[simp]
def
first_order.language.bounded_formula.relabel
{L : first_order.language}
{α β : Type}
(g : α → β)
{n : ℕ} :
L.bounded_formula α n → L.bounded_formula β n
Relabels a bounded formula's variables along a particular function.
Equations
- first_order.language.bounded_formula.relabel g f.bd_all = (first_order.language.bounded_formula.relabel g f).bd_all
- first_order.language.bounded_formula.relabel g (f₁.bd_imp f₂) = (first_order.language.bounded_formula.relabel g f₁).bd_imp (first_order.language.bounded_formula.relabel g f₂)
- first_order.language.bounded_formula.relabel g (first_order.language.bounded_formula.bd_rel R ts) = first_order.language.bounded_formula.bd_rel R (first_order.language.term.relabel (sum.elim (sum.inl ∘ g) sum.inr) ∘ ts)
- first_order.language.bounded_formula.relabel g (first_order.language.bounded_formula.bd_equal t₁ t₂) = first_order.language.bounded_formula.bd_equal (first_order.language.term.relabel (sum.elim (sum.inl ∘ g) sum.inr) t₁) (first_order.language.term.relabel (sum.elim (sum.inl ∘ g) sum.inr) t₂)
- first_order.language.bounded_formula.relabel g first_order.language.bounded_formula.bd_falsum = first_order.language.bounded_formula.bd_falsum
def
first_order.language.formula.equal
{L : first_order.language}
{α : Type}
(t₁ t₂ : L.term α) :
L.formula α
The equality of two terms as a first-order formula.
The graph of a function as a first-order formula.
Equations
@[protected, instance]
def
first_order.language.nonempty_bounded_formula
{L : first_order.language}
{α : Type}
(n : ℕ) :
nonempty (L.bounded_formula α n)
@[simp]
def
first_order.language.realize_bounded_formula
{L : first_order.language}
(M : Type u_1)
[L.Structure M]
{α : Type}
{l : ℕ}
(f : L.bounded_formula α l)
(v : α → M)
(xs : fin l → M) :
Prop
A bounded formula can be evaluated as true or false by giving values to each free variable.
Equations
- first_order.language.realize_bounded_formula M f.bd_all v xs = ∀ (x : M), first_order.language.realize_bounded_formula M f v (fin.cons x xs)
- first_order.language.realize_bounded_formula M (f₁.bd_imp f₂) v xs = (first_order.language.realize_bounded_formula M f₁ v xs → first_order.language.realize_bounded_formula M f₂ v xs)
- first_order.language.realize_bounded_formula M (first_order.language.bounded_formula.bd_rel R ts) v xs = first_order.language.Structure.rel_map R (λ (i : fin a_11), first_order.language.realize_term (sum.elim v xs) (ts i))
- first_order.language.realize_bounded_formula M (first_order.language.bounded_formula.bd_equal t₁ t₂) v xs = (first_order.language.realize_term (sum.elim v xs) t₁ = first_order.language.realize_term (sum.elim v xs) t₂)
- first_order.language.realize_bounded_formula M first_order.language.bounded_formula.bd_falsum v xs = false
@[simp]
theorem
first_order.language.realize_not
{L : first_order.language}
(M : Type u_1)
[L.Structure M]
{α : Type}
{l : ℕ}
(f : L.bounded_formula α l)
(v : α → M)
(xs : fin l → M) :
def
first_order.language.realize_formula
{L : first_order.language}
(M : Type u_1)
[L.Structure M]
{α : Type}
(f : L.formula α)
(v : α → M) :
Prop
A bounded formula can be evaluated as true or false by giving values to each free variable.
Equations
def
first_order.language.realize_sentence
{L : first_order.language}
(M : Type u_1)
[L.Structure M]
(φ : L.sentence) :
Prop
A sentence can be evaluated as true or false in a structure.
@[simp]
theorem
first_order.language.realize_bounded_formula_relabel
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{α β : Type}
{n : ℕ}
(g : α → β)
(v : β → M)
(xs : fin n → M)
(φ : L.bounded_formula α n) :
@[simp]
theorem
first_order.language.equiv.realize_bounded_formula
{L : first_order.language}
{M : Type u_1}
{N : Type u_2}
[L.Structure M]
[L.Structure N]
{α : Type}
{n : ℕ}
(v : α → M)
(xs : fin n → M)
(φ : L.bounded_formula α n)
(g : L.equiv M N) :
first_order.language.realize_bounded_formula N φ (⇑g ∘ v) (⇑g ∘ xs) ↔ first_order.language.realize_bounded_formula M φ v xs
@[simp]
theorem
first_order.language.realize_formula_relabel
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{α β : Type}
(g : α → β)
(v : β → M)
(φ : L.formula α) :
@[simp]
theorem
first_order.language.realize_formula_equiv
{L : first_order.language}
{M : Type u_1}
{N : Type u_2}
[L.Structure M]
[L.Structure N]
{α : Type}
(v : α → M)
(φ : L.formula α)
(g : L.equiv M N) :
first_order.language.realize_formula N φ (⇑g ∘ v) ↔ first_order.language.realize_formula M φ v
@[simp]
theorem
first_order.language.realize_equal
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{α : Type}
(t₁ t₂ : L.term α)
(x : α → M) :
@[simp]
theorem
first_order.language.realize_graph
{L : first_order.language}
{M : Type u_1}
[L.Structure M]
{l : ℕ}
(f : L.functions l)
(x : fin l → M)
(y : M) :