mathlib3 documentation

model_theory.syntax

Basics on First-Order Syntax #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.

Main Definitions #

Implementation Notes #

References #

For the Flypitch project:

source
inductive first_order.language.term (L : first_order.language) (α : Type u') :
Type (max u u')

A term on α is either a variable indexed by an element of α or a function symbol applied to simpler terms.

Instances for first_order.language.term
source
@[simp]
def first_order.language.term.var_finset {L : first_order.language} {α : Type u'} [decidable_eq α] :
L.term α → finset α

The finset of variables used in a given term.

Equations
source
@[simp]
def first_order.language.term.var_finset_left {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] :
L.term (α ⊕ β) → finset α

The finset of variables from the left side of a sum used in a given term.

Equations
source
@[simp]
def first_order.language.term.relabel {L : first_order.language} {α : Type u'} {β : Type v'} (g : α → β) :
L.term α → L.term β

Relabels a term's variables along a particular function.

Equations
source
theorem first_order.language.term.relabel_id {L : first_order.language} {α : Type u'} (t : L.term α) :
first_order.language.term.relabel id t = t
source
@[simp]
theorem first_order.language.term.relabel_id_eq_id {L : first_order.language} {α : Type u'} :
first_order.language.term.relabel id = id
source
@[simp]
theorem first_order.language.term.relabel_relabel {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (f : α → β) (g : β → γ) (t : L.term α) :
first_order.language.term.relabel g (first_order.language.term.relabel f t) = first_order.language.term.relabel (g ∘ f) t
source
@[simp]
theorem first_order.language.term.relabel_comp_relabel {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (f : α → β) (g : β → γ) :
first_order.language.term.relabel g ∘ first_order.language.term.relabel f = first_order.language.term.relabel (g ∘ f)
source
@[simp]
theorem first_order.language.term.relabel_equiv_apply {L : first_order.language} {α : Type u'} {β : Type v'} (g : α ≃ β) (ᾰ : L.term α) :
⇑(first_order.language.term.relabel_equiv g) ᾰ = first_order.language.term.relabel ⇑g ᾰ
source
def first_order.language.term.relabel_equiv {L : first_order.language} {α : Type u'} {β : Type v'} (g : α ≃ β) :
L.term α ≃ L.term β

Relabels a term's variables along a bijection.

Equations
source
@[simp]
theorem first_order.language.term.relabel_equiv_symm_apply {L : first_order.language} {α : Type u'} {β : Type v'} (g : α ≃ β) (ᾰ : L.term β) :
⇑((first_order.language.term.relabel_equiv g).symm) ᾰ = first_order.language.term.relabel ⇑(g.symm) ᾰ
source
def first_order.language.term.restrict_var {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] (t : L.term α) (f : ↥(t.var_finset) → β) :
L.term β

Restricts a term to use only a set of the given variables.

Equations
source
def first_order.language.term.restrict_var_left {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] {γ : Type u_1} (t : L.term (α ⊕ γ)) (f : ↥(t.var_finset_left) → β) :
L.term (β ⊕ γ)

Restricts a term to use only a set of the given variables on the left side of a sum.

Equations
source
def first_order.language.constants.term {L : first_order.language} {α : Type u'} (c : L.constants) :
L.term α

The representation of a constant symbol as a term.

Equations
source
def first_order.language.functions.apply₁ {L : first_order.language} {α : Type u'} (f : L.functions 1) (t : L.term α) :
L.term α

Applies a unary function to a term.

Equations
source
def first_order.language.functions.apply₂ {L : first_order.language} {α : Type u'} (f : L.functions 2) (t₁ t₂ : L.term α) :
L.term α

Applies a binary function to two terms.

Equations
source
@[simp]
def first_order.language.term.constants_to_vars {L : first_order.language} {α : Type u'} {γ : Type u_5} :
(L.with_constants γ).term α → L.term (γ ⊕ α)

Sends a term with constants to a term with extra variables.

Equations
source
@[simp]
def first_order.language.term.vars_to_constants {L : first_order.language} {α : Type u'} {γ : Type u_5} :
L.term (γ ⊕ α) → (L.with_constants γ).term α

Sends a term with extra variables to a term with constants.

Equations
source
@[simp]
theorem first_order.language.term.constants_vars_equiv_apply {L : first_order.language} {α : Type u'} {γ : Type u_5} (ᾰ : (L.with_constants γ).term α) :
⇑first_order.language.term.constants_vars_equiv ᾰ = ᾰ.constants_to_vars
source
def first_order.language.term.constants_vars_equiv {L : first_order.language} {α : Type u'} {γ : Type u_5} :
(L.with_constants γ).term α ≃ L.term (γ ⊕ α)

A bijection between terms with constants and terms with extra variables.

Equations
source
@[simp]
theorem first_order.language.term.constants_vars_equiv_symm_apply {L : first_order.language} {α : Type u'} {γ : Type u_5} (ᾰ : L.term (γ ⊕ α)) :
⇑(first_order.language.term.constants_vars_equiv.symm) ᾰ = ᾰ.vars_to_constants
source
def first_order.language.term.constants_vars_equiv_left {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} :
(L.with_constants γ).term (α ⊕ β) ≃ L.term ((γ ⊕ α) ⊕ β)

A bijection between terms with constants and terms with extra variables.

Equations
source
@[simp]
theorem first_order.language.term.constants_vars_equiv_left_apply {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (t : (L.with_constants γ).term (α ⊕ β)) :
⇑first_order.language.term.constants_vars_equiv_left t = first_order.language.term.relabel ⇑((equiv.sum_assoc γ α β).symm) t.constants_to_vars
source
@[simp]
theorem first_order.language.term.constants_vars_equiv_left_symm_apply {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (t : L.term ((γ ⊕ α) ⊕ β)) :
⇑(first_order.language.term.constants_vars_equiv_left.symm) t = (first_order.language.term.relabel ⇑(equiv.sum_assoc γ α β) t).vars_to_constants
source
@[protected, instance]
def first_order.language.term.inhabited_of_var {L : first_order.language} {α : Type u'} [inhabited α] :
inhabited (L.term α)
Equations
source
@[protected, instance]
def first_order.language.term.inhabited_of_constant {L : first_order.language} {α : Type u'} [inhabited L.constants] :
inhabited (L.term α)
Equations
source
def first_order.language.term.lift_at {L : first_order.language} {α : Type u'} {n : ℕ} (n' m : ℕ) :
L.term (α ⊕ fin n) → L.term (α ⊕ fin (n + n'))

Raises all of the fin-indexed variables of a term greater than or equal to m by n'.

Equations
source
@[simp]
def first_order.language.term.subst {L : first_order.language} {α : Type u'} {β : Type v'} :
L.term α → (α → L.term β) → L.term β

Substitutes the variables in a given term with terms.

Equations
source
@[simp]
def first_order.language.Lhom.on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L →ᴸ L') :
L.term α → L'.term α

Maps a term's symbols along a language map.

Equations
source
@[simp]
theorem first_order.language.Lhom.id_on_term {L : first_order.language} {α : Type u'} :
(first_order.language.Lhom.id L).on_term = id
source
@[simp]
theorem first_order.language.Lhom.comp_on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} {L'' : first_order.language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
(φ.comp ψ).on_term = φ.on_term ∘ ψ.on_term
source
def first_order.language.Lequiv.on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') :
L.term α ≃ L'.term α

Maps a term's symbols along a language equivalence.

Equations
source
@[simp]
theorem first_order.language.Lequiv.on_term_symm_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') (ᾰ : L'.term α) :
⇑(φ.on_term.symm) ᾰ = φ.inv_Lhom.on_term ᾰ
source
@[simp]
theorem first_order.language.Lequiv.on_term_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') (ᾰ : L.term α) :
⇑(φ.on_term) ᾰ = φ.to_Lhom.on_term ᾰ
source
inductive first_order.language.bounded_formula (L : first_order.language) (α : Type u') :
ℕ → Type (max u v u')

bounded_formula α n is the type of formulas with free variables indexed by α and up to n additional free variables.

Instances for first_order.language.bounded_formula
source
@[reducible]
def first_order.language.formula (L : first_order.language) (α : Type u') :
Type (max u v u')

formula α is the type of formulas with all free variables indexed by α.

Equations
source
@[reducible]
def first_order.language.sentence (L : first_order.language) :
Type (max u v)

A sentence is a formula with no free variables.

Equations
source
@[reducible]
def first_order.language.Theory (L : first_order.language) :
Type (max u v)

A theory is a set of sentences.

Equations
source
def first_order.language.relations.bounded_formula {L : first_order.language} {α : Type u'} {n l : ℕ} (R : L.relations n) (ts : fin n → L.term (α ⊕ fin l)) :
L.bounded_formula α l

Applies a relation to terms as a bounded formula.

Equations
source
def first_order.language.relations.bounded_formula₁ {L : first_order.language} {α : Type u'} {n : ℕ} (r : L.relations 1) (t : L.term (α ⊕ fin n)) :
L.bounded_formula α n

Applies a unary relation to a term as a bounded formula.

Equations
source
def first_order.language.relations.bounded_formula₂ {L : first_order.language} {α : Type u'} {n : ℕ} (r : L.relations 2) (t₁ t₂ : L.term (α ⊕ fin n)) :
L.bounded_formula α n

Applies a binary relation to two terms as a bounded formula.

Equations
source
def first_order.language.term.bd_equal {L : first_order.language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.term (α ⊕ fin n)) :
L.bounded_formula α n

The equality of two terms as a bounded formula.

Equations
source
def first_order.language.relations.formula {L : first_order.language} {α : Type u'} {n : ℕ} (R : L.relations n) (ts : fin n → L.term α) :
L.formula α

Applies a relation to terms as a bounded formula.

Equations
source
def first_order.language.relations.formula₁ {L : first_order.language} {α : Type u'} (r : L.relations 1) (t : L.term α) :
L.formula α

Applies a unary relation to a term as a formula.

Equations
source
def first_order.language.relations.formula₂ {L : first_order.language} {α : Type u'} (r : L.relations 2) (t₁ t₂ : L.term α) :
L.formula α

Applies a binary relation to two terms as a formula.

Equations
source
def first_order.language.term.equal {L : first_order.language} {α : Type u'} (t₁ t₂ : L.term α) :
L.formula α

The equality of two terms as a first-order formula.

Equations
source
@[protected, instance]
def first_order.language.bounded_formula.inhabited {L : first_order.language} {α : Type u'} {n : ℕ} :
inhabited (L.bounded_formula α n)
Equations
source
@[protected, instance]
def first_order.language.bounded_formula.has_bot {L : first_order.language} {α : Type u'} {n : ℕ} :
has_bot (L.bounded_formula α n)
Equations
source
@[protected]
def first_order.language.bounded_formula.not {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α n) :
L.bounded_formula α n

The negation of a bounded formula is also a bounded formula.

Equations
source
@[protected]
def first_order.language.bounded_formula.ex {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
L.bounded_formula α n

Puts an ∃ quantifier on a bounded formula.

Equations
source
@[protected, instance]
def first_order.language.bounded_formula.has_top {L : first_order.language} {α : Type u'} {n : ℕ} :
has_top (L.bounded_formula α n)
Equations
source
@[protected, instance]
def first_order.language.bounded_formula.has_inf {L : first_order.language} {α : Type u'} {n : ℕ} :
has_inf (L.bounded_formula α n)
Equations
source
@[protected, instance]
def first_order.language.bounded_formula.has_sup {L : first_order.language} {α : Type u'} {n : ℕ} :
has_sup (L.bounded_formula α n)
Equations
source
@[protected]
def first_order.language.bounded_formula.iff {L : first_order.language} {α : Type u'} {n : ℕ} (φ ψ : L.bounded_formula α n) :
L.bounded_formula α n

The biimplication between two bounded formulas.

Equations
source
@[simp]
def first_order.language.bounded_formula.free_var_finset {L : first_order.language} {α : Type u'} [decidable_eq α] {n : ℕ} :
L.bounded_formula α n → finset α

The finset of variables used in a given formula.

Equations
source
@[simp]
def first_order.language.bounded_formula.cast_le {L : first_order.language} {α : Type u'} {m n : ℕ} (h : m ≤ n) :
L.bounded_formula α m → L.bounded_formula α n

Casts L.bounded_formula α m as L.bounded_formula α n, where m ≤ n.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.cast_le_rfl {L : first_order.language} {α : Type u'} {n : ℕ} (h : n ≤ n) (φ : L.bounded_formula α n) :
first_order.language.bounded_formula.cast_le h φ = φ
source
@[simp]
theorem first_order.language.bounded_formula.cast_le_cast_le {L : first_order.language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (φ : L.bounded_formula α k) :
first_order.language.bounded_formula.cast_le mn (first_order.language.bounded_formula.cast_le km φ) = first_order.language.bounded_formula.cast_le _ φ
source
@[simp]
theorem first_order.language.bounded_formula.cast_le_comp_cast_le {L : first_order.language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) :
first_order.language.bounded_formula.cast_le mn ∘ first_order.language.bounded_formula.cast_le km = first_order.language.bounded_formula.cast_le _
source
def first_order.language.bounded_formula.restrict_free_var {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] {n : ℕ} (φ : L.bounded_formula α n) (f : ↥(φ.free_var_finset) → β) :
L.bounded_formula β n

Restricts a bounded formula to only use a particular set of free variables.

Equations
source
def first_order.language.bounded_formula.alls {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.formula α

Places universal quantifiers on all extra variables of a bounded formula.

Equations
source
def first_order.language.bounded_formula.exs {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.formula α

Places existential quantifiers on all extra variables of a bounded formula.

Equations
source
def first_order.language.bounded_formula.map_term_rel {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ} (ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin (g n))) (fr : Π (n : ℕ), L.relations n → L'.relations n) (h : Π (n : ℕ), L'.bounded_formula β (g (n + 1)) → L'.bounded_formula β (g n + 1)) {n : ℕ} :
L.bounded_formula α n → L'.bounded_formula β (g n)

Maps bounded formulas along a map of terms and a map of relations.

Equations
source
def first_order.language.bounded_formula.lift_at {L : first_order.language} {α : Type u'} {n : ℕ} (n' m : ℕ) :
L.bounded_formula α n → L.bounded_formula α (n + n')

Raises all of the fin-indexed variables of a formula greater than or equal to m by n'.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_map_term_rel {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} {L'' : first_order.language} (ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin n)) (fr : Π (n : ℕ), L.relations n → L'.relations n) (ft' : Π (n : ℕ), L'.term (β ⊕ fin n) → L''.term (γ ⊕ fin n)) (fr' : Π (n : ℕ), L'.relations n → L''.relations n) {n : ℕ} (φ : L.bounded_formula α n) :
first_order.language.bounded_formula.map_term_rel ft' fr' (λ (_x : ℕ), id) (first_order.language.bounded_formula.map_term_rel ft fr (λ (_x : ℕ), id) φ) = first_order.language.bounded_formula.map_term_rel (λ (_x : ℕ), ft' _x ∘ ft _x) (λ (_x : ℕ), fr' _x ∘ fr _x) (λ (_x : ℕ), id) φ
source
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_id_id_id {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α n) :
first_order.language.bounded_formula.map_term_rel (λ (_x : ℕ), id) (λ (_x : ℕ), id) (λ (_x : ℕ), id) φ = φ
source
def first_order.language.bounded_formula.map_term_rel_equiv {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ℕ), L.term (α ⊕ fin n) ≃ L'.term (β ⊕ fin n)) (fr : Π (n : ℕ), L.relations n ≃ L'.relations n) {n : ℕ} :
L.bounded_formula α n ≃ L'.bounded_formula β n

An equivalence of bounded formulas given by an equivalence of terms and an equivalence of relations.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_equiv_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ℕ), L.term (α ⊕ fin n) ≃ L'.term (β ⊕ fin n)) (fr : Π (n : ℕ), L.relations n ≃ L'.relations n) {n : ℕ} (ᾰ : L.bounded_formula α n) :
⇑(first_order.language.bounded_formula.map_term_rel_equiv ft fr) ᾰ = first_order.language.bounded_formula.map_term_rel (λ (n : ℕ), ⇑(ft n)) (λ (n : ℕ), ⇑(fr n)) (λ (_x : ℕ), id) ᾰ
source
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_equiv_symm_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ℕ), L.term (α ⊕ fin n) ≃ L'.term (β ⊕ fin n)) (fr : Π (n : ℕ), L.relations n ≃ L'.relations n) {n : ℕ} (ᾰ : L'.bounded_formula β n) :
⇑((first_order.language.bounded_formula.map_term_rel_equiv ft fr).symm) ᾰ = first_order.language.bounded_formula.map_term_rel (λ (n : ℕ), ⇑((ft n).symm)) (λ (n : ℕ), ⇑((fr n).symm)) (λ (_x : ℕ), id) ᾰ
source
def first_order.language.bounded_formula.relabel_aux {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) (k : ℕ) :
α ⊕ fin k → β ⊕ fin (n + k)

A function to help relabel the variables in bounded formulas.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.sum_elim_comp_relabel_aux {M : Type w} {α : Type u'} {β : Type v'} {n m : ℕ} {g : α → β ⊕ fin n} {v : β → M} {xs : fin (n + m) → M} :
sum.elim v xs ∘ first_order.language.bounded_formula.relabel_aux g m = sum.elim (sum.elim v (xs ∘ ⇑(fin.cast_add m)) ∘ g) (xs ∘ ⇑(fin.nat_add n))
source
@[simp]
theorem first_order.language.bounded_formula.relabel_aux_sum_inl {α : Type u'} {n : ℕ} (k : ℕ) :
first_order.language.bounded_formula.relabel_aux sum.inl k = sum.map id ⇑(fin.nat_add n)
source
def first_order.language.bounded_formula.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} (φ : L.bounded_formula α k) :
L.bounded_formula β (n + k)

Relabels a bounded formula's variables along a particular function.

Equations
source
def first_order.language.bounded_formula.relabel_equiv {L : first_order.language} {α : Type u'} {β : Type v'} (g : α ≃ β) {k : ℕ} :
L.bounded_formula α k ≃ L.bounded_formula β k

Relabels a bounded formula's free variables along a bijection.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.relabel_falsum {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} :
first_order.language.bounded_formula.relabel g first_order.language.bounded_formula.falsum = first_order.language.bounded_formula.falsum
source
@[simp]
theorem first_order.language.bounded_formula.relabel_bot {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} :
first_order.language.bounded_formula.relabel g ⊥ = ⊥
source
@[simp]
theorem first_order.language.bounded_formula.relabel_imp {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} (φ ψ : L.bounded_formula α k) :
first_order.language.bounded_formula.relabel g (φ.imp ψ) = (first_order.language.bounded_formula.relabel g φ).imp (first_order.language.bounded_formula.relabel g ψ)
source
@[simp]
theorem first_order.language.bounded_formula.relabel_not {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} (φ : L.bounded_formula α k) :
first_order.language.bounded_formula.relabel g φ.not = (first_order.language.bounded_formula.relabel g φ).not
source
@[simp]
theorem first_order.language.bounded_formula.relabel_all {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} (φ : L.bounded_formula α (k + 1)) :
first_order.language.bounded_formula.relabel g φ.all = (first_order.language.bounded_formula.relabel g φ).all
source
@[simp]
theorem first_order.language.bounded_formula.relabel_ex {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ fin n) {k : ℕ} (φ : L.bounded_formula α (k + 1)) :
first_order.language.bounded_formula.relabel g φ.ex = (first_order.language.bounded_formula.relabel g φ).ex
source
@[simp]
theorem first_order.language.bounded_formula.relabel_sum_inl {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α n) :
first_order.language.bounded_formula.relabel sum.inl φ = first_order.language.bounded_formula.cast_le _ φ
source
@[simp]
def first_order.language.bounded_formula.subst {L : first_order.language} {α : Type u'} {β : Type v'} {n : ℕ} (φ : L.bounded_formula α n) (f : α → L.term β) :
L.bounded_formula β n

Substitutes the variables in a given formula with terms.

Equations
source
def first_order.language.bounded_formula.constants_vars_equiv {L : first_order.language} {α : Type u'} {γ : Type u_5} {n : ℕ} :
(L.with_constants γ).bounded_formula α n ≃ L.bounded_formula (γ ⊕ α) n

A bijection sending formulas with constants to formulas with extra variables.

Equations
source
@[simp]
def first_order.language.bounded_formula.to_formula {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.formula (α ⊕ fin n)

Turns the extra variables of a bounded formula into free variables.

Equations
source
inductive first_order.language.bounded_formula.is_atomic {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → Prop

An atomic formula is either equality or a relation symbol applied to terms. Note that ⊥ and ⊤ are not considered atomic in this convention.

source
theorem first_order.language.bounded_formula.not_all_is_atomic {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
¬φ.all.is_atomic
source
theorem first_order.language.bounded_formula.not_ex_is_atomic {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
¬φ.ex.is_atomic
source
theorem first_order.language.bounded_formula.is_atomic.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.bounded_formula α m} (h : φ.is_atomic) (f : α → β ⊕ fin n) :
(first_order.language.bounded_formula.relabel f φ).is_atomic
source
theorem first_order.language.bounded_formula.is_atomic.lift_at {L : first_order.language} {α : Type u'} {l : ℕ} {φ : L.bounded_formula α l} {k m : ℕ} (h : φ.is_atomic) :
(first_order.language.bounded_formula.lift_at k m φ).is_atomic
source
theorem first_order.language.bounded_formula.is_atomic.cast_le {L : first_order.language} {α : Type u'} {n l : ℕ} {φ : L.bounded_formula α l} {h : l ≤ n} (hφ : φ.is_atomic) :
(first_order.language.bounded_formula.cast_le h φ).is_atomic
source
inductive first_order.language.bounded_formula.is_qf {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → Prop

A quantifier-free formula is a formula defined without quantifiers. These are all equivalent to boolean combinations of atomic formulas.

source
theorem first_order.language.bounded_formula.is_atomic.is_qf {L : first_order.language} {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} :
φ.is_atomic → φ.is_qf
source
theorem first_order.language.bounded_formula.is_qf_bot {L : first_order.language} {α : Type u'} {n : ℕ} :
⊥.is_qf
source
theorem first_order.language.bounded_formula.is_qf.not {L : first_order.language} {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} (h : φ.is_qf) :
φ.not.is_qf
source
theorem first_order.language.bounded_formula.is_qf.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.bounded_formula α m} (h : φ.is_qf) (f : α → β ⊕ fin n) :
(first_order.language.bounded_formula.relabel f φ).is_qf
source
theorem first_order.language.bounded_formula.is_qf.lift_at {L : first_order.language} {α : Type u'} {l : ℕ} {φ : L.bounded_formula α l} {k m : ℕ} (h : φ.is_qf) :
(first_order.language.bounded_formula.lift_at k m φ).is_qf
source
theorem first_order.language.bounded_formula.is_qf.cast_le {L : first_order.language} {α : Type u'} {n l : ℕ} {φ : L.bounded_formula α l} {h : l ≤ n} (hφ : φ.is_qf) :
(first_order.language.bounded_formula.cast_le h φ).is_qf
source
theorem first_order.language.bounded_formula.not_all_is_qf {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
¬φ.all.is_qf
source
theorem first_order.language.bounded_formula.not_ex_is_qf {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
¬φ.ex.is_qf
source
inductive first_order.language.bounded_formula.is_prenex {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → Prop

Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers applied to a quantifier-free formula.

source
theorem first_order.language.bounded_formula.is_qf.is_prenex {L : first_order.language} {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} :
φ.is_qf → φ.is_prenex
source
theorem first_order.language.bounded_formula.is_atomic.is_prenex {L : first_order.language} {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} (h : φ.is_atomic) :
φ.is_prenex
source
theorem first_order.language.bounded_formula.is_prenex.induction_on_all_not {L : first_order.language} {α : Type u'} {n : ℕ} {P : Π {n : ℕ}, L.bounded_formula α n → Prop} {φ : L.bounded_formula α n} (h : φ.is_prenex) (hq : ∀ {m : ℕ} {ψ : L.bounded_formula α m}, ψ.is_qf → P ψ) (ha : ∀ {m : ℕ} {ψ : L.bounded_formula α (m + 1)}, P ψ → P ψ.all) (hn : ∀ {m : ℕ} {ψ : L.bounded_formula α m}, P ψ → P ψ.not) :
P φ
source
theorem first_order.language.bounded_formula.is_prenex.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.bounded_formula α m} (h : φ.is_prenex) (f : α → β ⊕ fin n) :
(first_order.language.bounded_formula.relabel f φ).is_prenex
source
theorem first_order.language.bounded_formula.is_prenex.cast_le {L : first_order.language} {α : Type u'} {l : ℕ} {φ : L.bounded_formula α l} (hφ : φ.is_prenex) {n : ℕ} {h : l ≤ n} :
(first_order.language.bounded_formula.cast_le h φ).is_prenex
source
theorem first_order.language.bounded_formula.is_prenex.lift_at {L : first_order.language} {α : Type u'} {l : ℕ} {φ : L.bounded_formula α l} {k m : ℕ} (h : φ.is_prenex) :
(first_order.language.bounded_formula.lift_at k m φ).is_prenex
source
def first_order.language.bounded_formula.to_prenex_imp_right {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.bounded_formula α n → L.bounded_formula α n

An auxiliary operation to first_order.language.bounded_formula.to_prenex. If φ is quantifier-free and ψ is in prenex normal form, then φ.to_prenex_imp_right ψ is a prenex normal form for φ.imp ψ.

Equations
source
theorem first_order.language.bounded_formula.is_qf.to_prenex_imp_right {L : first_order.language} {α : Type u'} {n : ℕ} {φ ψ : L.bounded_formula α n} :
ψ.is_qf → φ.to_prenex_imp_right ψ = φ.imp ψ
source
theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp_right {L : first_order.language} {α : Type u'} {n : ℕ} {φ ψ : L.bounded_formula α n} (hφ : φ.is_qf) (hψ : ψ.is_prenex) :
(φ.to_prenex_imp_right ψ).is_prenex
source
def first_order.language.bounded_formula.to_prenex_imp {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.bounded_formula α n → L.bounded_formula α n

An auxiliary operation to first_order.language.bounded_formula.to_prenex. If φ and ψ are in prenex normal form, then φ.to_prenex_imp ψ is a prenex normal form for φ.imp ψ.

Equations
source
theorem first_order.language.bounded_formula.is_qf.to_prenex_imp {L : first_order.language} {α : Type u'} {n : ℕ} {φ ψ : L.bounded_formula α n} :
φ.is_qf → φ.to_prenex_imp ψ = φ.to_prenex_imp_right ψ
source
theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp {L : first_order.language} {α : Type u'} {n : ℕ} {φ ψ : L.bounded_formula α n} (hφ : φ.is_prenex) (hψ : ψ.is_prenex) :
(φ.to_prenex_imp ψ).is_prenex
source
def first_order.language.bounded_formula.to_prenex {L : first_order.language} {α : Type u'} {n : ℕ} :
L.bounded_formula α n → L.bounded_formula α n

For any bounded formula φ, φ.to_prenex is a semantically-equivalent formula in prenex normal form.

Equations
source
theorem first_order.language.bounded_formula.to_prenex_is_prenex {L : first_order.language} {α : Type u'} {n : ℕ} (φ : L.bounded_formula α n) :
φ.to_prenex.is_prenex
source
@[simp]
def first_order.language.Lhom.on_bounded_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} (g : L →ᴸ L') {k : ℕ} :
L.bounded_formula α k → L'.bounded_formula α k

Maps a bounded formula's symbols along a language map.

Equations
source
@[simp]
theorem first_order.language.Lhom.id_on_bounded_formula {L : first_order.language} {α : Type u'} {n : ℕ} :
(first_order.language.Lhom.id L).on_bounded_formula = id
source
@[simp]
theorem first_order.language.Lhom.comp_on_bounded_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : ℕ} {L'' : first_order.language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
(φ.comp ψ).on_bounded_formula = φ.on_bounded_formula ∘ ψ.on_bounded_formula
source
def first_order.language.Lhom.on_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} (g : L →ᴸ L') :
L.formula α → L'.formula α

Maps a formula's symbols along a language map.

Equations
source
def first_order.language.Lhom.on_sentence {L : first_order.language} {L' : first_order.language} (g : L →ᴸ L') :
L.sentence → L'.sentence

Maps a sentence's symbols along a language map.

Equations
source
def first_order.language.Lhom.on_Theory {L : first_order.language} {L' : first_order.language} (g : L →ᴸ L') (T : L.Theory) :
L'.Theory

Maps a theory's symbols along a language map.

Equations
source
@[simp]
theorem first_order.language.Lhom.mem_on_Theory {L : first_order.language} {L' : first_order.language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.sentence} :
φ ∈ g.on_Theory T ↔ ∃ (φ₀ : L.sentence), φ₀ ∈ T ∧ g.on_sentence φ₀ = φ
source
@[simp]
theorem first_order.language.Lequiv.on_bounded_formula_symm_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (ᾰ : L'.bounded_formula α n) :
⇑(φ.on_bounded_formula.symm) ᾰ = φ.inv_Lhom.on_bounded_formula ᾰ
source
def first_order.language.Lequiv.on_bounded_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') :
L.bounded_formula α n ≃ L'.bounded_formula α n

Maps a bounded formula's symbols along a language equivalence.

Equations
source
@[simp]
theorem first_order.language.Lequiv.on_bounded_formula_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (ᾰ : L.bounded_formula α n) :
⇑(φ.on_bounded_formula) ᾰ = φ.to_Lhom.on_bounded_formula ᾰ
source
theorem first_order.language.Lequiv.on_bounded_formula_symm {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') :
φ.on_bounded_formula.symm = φ.symm.on_bounded_formula
source
def first_order.language.Lequiv.on_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') :
L.formula α ≃ L'.formula α

Maps a formula's symbols along a language equivalence.

Equations
source
@[simp]
theorem first_order.language.Lequiv.on_formula_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') :
⇑(φ.on_formula) = φ.to_Lhom.on_formula
source
@[simp]
theorem first_order.language.Lequiv.on_formula_symm {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') :
φ.on_formula.symm = φ.symm.on_formula
source
@[simp]
theorem first_order.language.Lequiv.on_sentence_symm_apply {L : first_order.language} {L' : first_order.language} (φ : L ≃ᴸ L') (ᾰ : L'.bounded_formula empty 0) :
⇑(φ.on_sentence.symm) ᾰ = φ.inv_Lhom.on_bounded_formula ᾰ
source
def first_order.language.Lequiv.on_sentence {L : first_order.language} {L' : first_order.language} (φ : L ≃ᴸ L') :
L.sentence ≃ L'.sentence

Maps a sentence's symbols along a language equivalence.

Equations
source
@[simp]
theorem first_order.language.Lequiv.on_sentence_apply {L : first_order.language} {L' : first_order.language} (φ : L ≃ᴸ L') (ᾰ : L.bounded_formula empty 0) :
⇑(φ.on_sentence) ᾰ = φ.to_Lhom.on_bounded_formula ᾰ
source
def first_order.language.formula.relabel {L : first_order.language} {α : Type u'} {β : Type v'} (g : α → β) :
L.formula α → L.formula β

Relabels a formula's variables along a particular function.

Equations
source
def first_order.language.formula.graph {L : first_order.language} {n : ℕ} (f : L.functions n) :
L.formula (fin (n + 1))

The graph of a function as a first-order formula.

Equations
source
@[protected]
def first_order.language.formula.not {L : first_order.language} {α : Type u'} (φ : L.formula α) :
L.formula α

The negation of a formula.

Equations
source
@[protected]
def first_order.language.formula.imp {L : first_order.language} {α : Type u'} :
L.formula α → L.formula α → L.formula α

The implication between formulas, as a formula.

Equations
source
@[protected]
def first_order.language.formula.iff {L : first_order.language} {α : Type u'} (φ ψ : L.formula α) :
L.formula α

The biimplication between formulas, as a formula.

Equations
source
theorem first_order.language.formula.is_atomic_graph {L : first_order.language} {n : ℕ} (f : L.functions n) :
first_order.language.bounded_formula.is_atomic (first_order.language.formula.graph f)
source
def first_order.language.formula.equiv_sentence {L : first_order.language} {α : Type u'} :
L.formula α ≃ (L.with_constants α).sentence

A bijection sending formulas to sentences with constants.

Equations
source
theorem first_order.language.formula.equiv_sentence_not {L : first_order.language} {α : Type u'} (φ : L.formula α) :
⇑first_order.language.formula.equiv_sentence φ.not = first_order.language.formula.not (⇑first_order.language.formula.equiv_sentence φ)
source
theorem first_order.language.formula.equiv_sentence_inf {L : first_order.language} {α : Type u'} (φ ψ : L.formula α) :
⇑first_order.language.formula.equiv_sentence (φ ⊓ ψ) = ⇑first_order.language.formula.equiv_sentence φ ⊓ ⇑first_order.language.formula.equiv_sentence ψ
source
@[protected]
def first_order.language.relations.reflexive {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is reflexive.

Equations
source
@[protected]
def first_order.language.relations.irreflexive {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is irreflexive.

Equations
source
@[protected]
def first_order.language.relations.symmetric {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is symmetric.

Equations
source
@[protected]
def first_order.language.relations.antisymmetric {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is antisymmetric.

Equations
source
@[protected]
def first_order.language.relations.transitive {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is transitive.

Equations
source
@[protected]
def first_order.language.relations.total {L : first_order.language} (r : L.relations 2) :
L.sentence

The sentence indicating that a basic relation symbol is total.

Equations
source
@[protected]
def first_order.language.sentence.card_ge (L : first_order.language) (n : ℕ) :
L.sentence

A sentence indicating that a structure has n distinct elements.

Equations
source
def first_order.language.infinite_theory (L : first_order.language) :
L.Theory

A theory indicating that a structure is infinite.

Equations
Instances for first_order.language.infinite_theory
source
def first_order.language.nonempty_theory (L : first_order.language) :
L.Theory

A theory that indicates a structure is nonempty.

Equations
Instances for first_order.language.nonempty_theory
source
def first_order.language.distinct_constants_theory (L : first_order.language) {α : Type u'} (s : set α) :
(L.with_constants α).Theory

A theory indicating that each of a set of constants is distinct.

Equations
source
theorem first_order.language.monotone_distinct_constants_theory {L : first_order.language} {α : Type u'} :
monotone L.distinct_constants_theory
source
theorem first_order.language.directed_distinct_constants_theory {L : first_order.language} {α : Type u'} :
directed has_subset.subset L.distinct_constants_theory
source
theorem first_order.language.distinct_constants_theory_eq_Union {L : first_order.language} {α : Type u'} (s : set α) :
L.distinct_constants_theory s = ⋃ (t : finset ↥s), L.distinct_constants_theory ↑(finset.map (function.embedding.subtype (λ (x : α), x ∈ s)) t)