Basics on First-Order Syntax

This file defines first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.

Main Definitions

• A FirstOrder.Language.Term is defined so that L.Term α is the type of L-terms with free variables indexed by α.
• A FirstOrder.Language.Formula is defined so that L.Formula α is the type of L-formulas with free variables indexed by α.
• A FirstOrder.Language.Sentence is a formula with no free variables.
• A FirstOrder.Language.Theory is a set of sentences.
• The variables of terms and formulas can be relabelled with FirstOrder.Language.Term.relabel, FirstOrder.Language.BoundedFormula.relabel, and FirstOrder.Language.Formula.relabel.
• Given an operation on terms and an operation on relations, FirstOrder.Language.BoundedFormula.mapTermRel gives an operation on formulas.
• FirstOrder.Language.BoundedFormula.castLE adds more Fin-indexed variables.
• FirstOrder.Language.BoundedFormula.liftAt raises the indexes of the Fin-indexed variables above a particular index.
• FirstOrder.Language.Term.subst and FirstOrder.Language.BoundedFormula.subst substitute variables with given terms.
• Language maps can act on syntactic objects with functions such as FirstOrder.Language.LHom.onFormula.
• FirstOrder.Language.Term.constantsVarsEquiv and FirstOrder.Language.BoundedFormula.constantsVarsEquiv switch terms and formulas between having constants in the language and having extra variables indexed by the same type.

Implementation Notes

• Formulas use a modified version of de Bruijn variables. Specifically, a L.BoundedFormula α n is a formula with some variables indexed by a type α, which cannot be quantified over, and some indexed by Fin n, which can. For any φ : L.BoundedFormula α (n + 1), we define the formula ∀' φ : L.BoundedFormula α n by universally quantifying over the variable indexed by n : Fin (n + 1).

References

For the Flypitch project:

• [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
• [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]

inductive FirstOrder.Language.Term (L : 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.

• var {L : Language} {α : Type u'} : α → L.Term α
• func {L : Language} {α : Type u'} {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) : L.Term α

instance FirstOrder.Language.Term.instDecidableEq {L : Language} {α : Type u'} [DecidableEq α] [(n : ℕ) → DecidableEq (L.Functions n)] : DecidableEq (L.Term α)

Equations

• (FirstOrder.Language.var a).instDecidableEq (FirstOrder.Language.var b) = decidable_of_iff (a = b) ⋯
• (FirstOrder.Language.func f xs).instDecidableEq (FirstOrder.Language.func g ys) = if h : m = n then decidable_of_iff (f = ⋯ ▸ g ∧ ∀ (i : Fin m), xs i = ys (Fin.cast h i)) ⋯ else isFalse ⋯
• (FirstOrder.Language.var a).instDecidableEq (FirstOrder.Language.func _f _ts) = isFalse ⋯
• (FirstOrder.Language.func _f _ts).instDecidableEq (FirstOrder.Language.var a) = isFalse ⋯

def FirstOrder.Language.Term.varFinset {L : Language} {α : Type u'} [DecidableEq α] : L.Term α → Finset α

The Finset of variables used in a given term.

Equations

• (FirstOrder.Language.var i).varFinset = {i}
• (FirstOrder.Language.func _f ts).varFinset = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinset

def FirstOrder.Language.Term.varFinsetLeft {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] : L.Term (α ⊕ β) → Finset α

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

Equations

• (FirstOrder.Language.var (Sum.inl i)).varFinsetLeft = {i}
• (FirstOrder.Language.var (Sum.inr _i)).varFinsetLeft = ∅
• (FirstOrder.Language.func _f ts).varFinsetLeft = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinsetLeft

def FirstOrder.Language.Term.relabel {L : Language} {α : Type u'} {β : Type v'} (g : α → β) : L.Term α → L.Term β

Relabels a term's variables along a particular function.

Equations

• FirstOrder.Language.Term.relabel g (FirstOrder.Language.var i) = FirstOrder.Language.var (g i)
• FirstOrder.Language.Term.relabel g (FirstOrder.Language.func _f ts) = FirstOrder.Language.func _f fun {i : Fin l} => FirstOrder.Language.Term.relabel g (ts i)

theorem FirstOrder.Language.Term.relabel_id {L : Language} {α : Type u'} (t : L.Term α) : relabel id t = t

@[simp]

theorem FirstOrder.Language.Term.relabel_id_eq_id {L : Language} {α : Type u'} : relabel id = id

@[simp]

theorem FirstOrder.Language.Term.relabel_relabel {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : α → β) (g : β → γ) (t : L.Term α) : relabel g (relabel f t) = relabel (g ∘ f) t

@[simp]

theorem FirstOrder.Language.Term.relabel_comp_relabel {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : α → β) (g : β → γ) : relabel g ∘ relabel f = relabel (g ∘ f)

def FirstOrder.Language.Term.relabelEquiv {L : Language} {α : Type u'} {β : Type v'} (g : α ≃ β) : L.Term α ≃ L.Term β

Relabels a term's variables along a bijection.

Equations

• FirstOrder.Language.Term.relabelEquiv g = { toFun := FirstOrder.Language.Term.relabel ⇑g, invFun := FirstOrder.Language.Term.relabel ⇑g.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.Term.relabelEquiv_symm_apply {L : Language} {α : Type u'} {β : Type v'} (g : α ≃ β) (a✝ : L.Term β) : (relabelEquiv g).symm a✝ = relabel (⇑g.symm) a✝

@[simp]

theorem FirstOrder.Language.Term.relabelEquiv_apply {L : Language} {α : Type u'} {β : Type v'} (g : α ≃ β) (a✝ : L.Term α) : (relabelEquiv g) a✝ = relabel (⇑g) a✝

def FirstOrder.Language.Term.restrictVar {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] (t : L.Term α) (_f : { x : α // x ∈ t.varFinset } → β) : L.Term β

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

Equations

• (FirstOrder.Language.var a).restrictVar f = FirstOrder.Language.var (f ⟨a, ⋯⟩)
• (FirstOrder.Language.func F ts).restrictVar f = FirstOrder.Language.func F fun (i : Fin l) => (ts i).restrictVar (f ∘ Set.inclusion ⋯)

def FirstOrder.Language.Term.restrictVarLeft {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] {γ : Type u_2} (t : L.Term (α ⊕ γ)) (_f : { x : α // x ∈ t.varFinsetLeft } → β) : L.Term (β ⊕ γ)

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

Equations

• (FirstOrder.Language.var (Sum.inl a)).restrictVarLeft f = FirstOrder.Language.var (Sum.inl (f ⟨a, ⋯⟩))
• (FirstOrder.Language.var (Sum.inr a)).restrictVarLeft _f = FirstOrder.Language.var (Sum.inr a)
• (FirstOrder.Language.func F ts).restrictVarLeft f = FirstOrder.Language.func F fun (i : Fin l) => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)

def FirstOrder.Language.Constants.term {L : Language} {α : Type u'} (c : L.Constants) : L.Term α

The representation of a constant symbol as a term.

Equations

• c.term = FirstOrder.Language.func c default

def FirstOrder.Language.Functions.apply₁ {L : Language} {α : Type u'} (f : L.Functions 1) (t : L.Term α) : L.Term α

Applies a unary function to a term.

Equations

• f.apply₁ t = FirstOrder.Language.func f ![t]

def FirstOrder.Language.Functions.apply₂ {L : Language} {α : Type u'} (f : L.Functions 2) (t₁ t₂ : L.Term α) : L.Term α

Applies a binary function to two terms.

Equations

• f.apply₂ t₁ t₂ = FirstOrder.Language.func f ![t₁, t₂]

def FirstOrder.Language.Term.constantsToVars {L : Language} {α : Type u'} {γ : Type u_1} : (L.withConstants γ).Term α → L.Term (γ ⊕ α)

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

Equations

• One or more equations did not get rendered due to their size.
• (FirstOrder.Language.var a).constantsToVars = FirstOrder.Language.var (Sum.inr a)

def FirstOrder.Language.Term.varsToConstants {L : Language} {α : Type u'} {γ : Type u_1} : L.Term (γ ⊕ α) → (L.withConstants γ).Term α

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

Equations

• (FirstOrder.Language.var (Sum.inr a)).varsToConstants = FirstOrder.Language.var a
• (FirstOrder.Language.var (Sum.inl c)).varsToConstants = FirstOrder.Language.Constants.term (Sum.inr c)
• (FirstOrder.Language.func f ts).varsToConstants = FirstOrder.Language.func (Sum.inl f) fun (i : Fin l) => (ts i).varsToConstants

def FirstOrder.Language.Term.constantsVarsEquiv {L : Language} {α : Type u'} {γ : Type u_1} : (L.withConstants γ).Term α ≃ L.Term (γ ⊕ α)

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

Equations

• FirstOrder.Language.Term.constantsVarsEquiv = { toFun := FirstOrder.Language.Term.constantsToVars, invFun := FirstOrder.Language.Term.varsToConstants, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquiv_symm_apply {L : Language} {α : Type u'} {γ : Type u_1} (a✝ : L.Term (γ ⊕ α)) : constantsVarsEquiv.symm a✝ = a✝.varsToConstants

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquiv_apply {L : Language} {α : Type u'} {γ : Type u_1} (a✝ : (L.withConstants γ).Term α) : constantsVarsEquiv a✝ = a✝.constantsToVars

def FirstOrder.Language.Term.constantsVarsEquivLeft {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} : (L.withConstants γ).Term (α ⊕ β) ≃ L.Term ((γ ⊕ α) ⊕ β)

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

Equations

• FirstOrder.Language.Term.constantsVarsEquivLeft = FirstOrder.Language.Term.constantsVarsEquiv.trans (FirstOrder.Language.Term.relabelEquiv (Equiv.sumAssoc γ α β)).symm

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquivLeft_apply {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : (L.withConstants γ).Term (α ⊕ β)) : constantsVarsEquivLeft t = relabel (⇑(Equiv.sumAssoc γ α β).symm) t.constantsToVars

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : L.Term ((γ ⊕ α) ⊕ β)) : constantsVarsEquivLeft.symm t = (relabel (⇑(Equiv.sumAssoc γ α β)) t).varsToConstants

instance FirstOrder.Language.Term.inhabitedOfVar {L : Language} {α : Type u'} [Inhabited α] : Inhabited (L.Term α)

Equations

• FirstOrder.Language.Term.inhabitedOfVar = { default := FirstOrder.Language.var default }

instance FirstOrder.Language.Term.inhabitedOfConstant {L : Language} {α : Type u'} [Inhabited L.Constants] : Inhabited (L.Term α)

Equations

• FirstOrder.Language.Term.inhabitedOfConstant = { default := default.term }

def FirstOrder.Language.Term.liftAt {L : 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

• FirstOrder.Language.Term.liftAt n' m = FirstOrder.Language.Term.relabel (Sum.map id fun (i : Fin n) => if ↑i < m then Fin.castAdd n' i else i.addNat n')

def FirstOrder.Language.Term.subst {L : Language} {α : Type u'} {β : Type v'} : L.Term α → (α → L.Term β) → L.Term β

Substitutes the variables in a given term with terms.

Equations

• (FirstOrder.Language.var a).subst x✝ = x✝ a
• (FirstOrder.Language.func f ts).subst x✝ = FirstOrder.Language.func f fun (i : Fin l) => (ts i).subst x✝

def FirstOrder.«term&_» : Lean.ParserDescr

&n is notation for the n-th free variable of a bounded formula.

Equations

• FirstOrder.«term&_» = Lean.ParserDescr.node `FirstOrder.«term&_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1023))

def FirstOrder.Language.LHom.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L →ᴸ L') : L.Term α → L'.Term α

Maps a term's symbols along a language map.

Equations

• φ.onTerm (FirstOrder.Language.var i) = FirstOrder.Language.var i
• φ.onTerm (FirstOrder.Language.func _f ts) = FirstOrder.Language.func (φ.onFunction _f) fun (i : Fin l) => φ.onTerm (ts i)

@[simp]

theorem FirstOrder.Language.LHom.id_onTerm {L : Language} {α : Type u'} : (LHom.id L).onTerm = id

@[simp]

theorem FirstOrder.Language.LHom.comp_onTerm {L : Language} {L' : Language} {α : Type u'} {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') : (φ.comp ψ).onTerm = φ.onTerm ∘ ψ.onTerm

def FirstOrder.Language.LEquiv.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') : L.Term α ≃ L'.Term α

Maps a term's symbols along a language equivalence.

Equations

• φ.onTerm = { toFun := φ.toLHom.onTerm, invFun := φ.invLHom.onTerm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.LEquiv.onTerm_apply {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') (a✝ : L.Term α) : φ.onTerm a✝ = φ.toLHom.onTerm a✝

@[simp]

theorem FirstOrder.Language.LEquiv.onTerm_symm_apply {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') (a✝ : L'.Term α) : φ.onTerm.symm a✝ = φ.invLHom.onTerm a✝

@[deprecated FirstOrder.Language.LEquiv.onTerm (since := "2025-03-31")]

def FirstOrder.Language.Lequiv.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') : L.Term α ≃ L'.Term α

Maps a term's symbols along a language equivalence. Deprecated in favor of LEquiv.onTerm.

Equations

• @FirstOrder.Language.Lequiv.onTerm = @FirstOrder.Language.LEquiv.onTerm

inductive FirstOrder.Language.BoundedFormula (L : Language) (α : Type u') : ℕ → Type (max u v u')

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

• falsum {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n
• equal {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : L.BoundedFormula α n
• rel {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : L.BoundedFormula α n
• imp {L : Language} {α : Type u'} {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) : L.BoundedFormula α n

  The implication between two bounded formulas

• all {L : Language} {α : Type u'} {n : ℕ} (f : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n

  The universal quantifier over bounded formulas

@[reducible, inline]

abbrev FirstOrder.Language.Formula (L : Language) (α : Type u') : Type (max u v u')

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

Equations

• L.Formula α = L.BoundedFormula α 0

@[reducible, inline]

abbrev FirstOrder.Language.Sentence (L : Language) : Type (max u v)

A sentence is a formula with no free variables.

Equations

• L.Sentence = L.Formula Empty

@[reducible, inline]

abbrev FirstOrder.Language.Theory (L : Language) : Type (max u v)

A theory is a set of sentences.

Equations

• L.Theory = Set L.Sentence

def FirstOrder.Language.Relations.boundedFormula {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations n) (ts : Fin n → L.Term (α ⊕ Fin l)) : L.BoundedFormula α l

Applies a relation to terms as a bounded formula.

Equations

• R.boundedFormula ts = FirstOrder.Language.BoundedFormula.rel R ts

def FirstOrder.Language.Relations.boundedFormula₁ {L : Language} {α : Type u'} {n : ℕ} (r : L.Relations 1) (t : L.Term (α ⊕ Fin n)) : L.BoundedFormula α n

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

Equations

• r.boundedFormula₁ t = r.boundedFormula ![t]

def FirstOrder.Language.Relations.boundedFormula₂ {L : Language} {α : Type u'} {n : ℕ} (r : L.Relations 2) (t₁ t₂ : L.Term (α ⊕ Fin n)) : L.BoundedFormula α n

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

Equations

• r.boundedFormula₂ t₁ t₂ = r.boundedFormula ![t₁, t₂]

def FirstOrder.Language.Term.bdEqual {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : L.BoundedFormula α n

The equality of two terms as a bounded formula.

Equations

• t₁.bdEqual t₂ = FirstOrder.Language.BoundedFormula.equal t₁ t₂

def FirstOrder.Language.Relations.formula {L : 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

• R.formula ts = R.boundedFormula fun (i : Fin n) => FirstOrder.Language.Term.relabel Sum.inl (ts i)

def FirstOrder.Language.Relations.formula₁ {L : Language} {α : Type u'} (r : L.Relations 1) (t : L.Term α) : L.Formula α

Applies a unary relation to a term as a formula.

Equations

• r.formula₁ t = r.formula ![t]

def FirstOrder.Language.Relations.formula₂ {L : Language} {α : Type u'} (r : L.Relations 2) (t₁ t₂ : L.Term α) : L.Formula α

Applies a binary relation to two terms as a formula.

Equations

• r.formula₂ t₁ t₂ = r.formula ![t₁, t₂]

def FirstOrder.Language.Term.equal {L : Language} {α : Type u'} (t₁ t₂ : L.Term α) : L.Formula α

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

Equations

• t₁.equal t₂ = (FirstOrder.Language.Term.relabel Sum.inl t₁).bdEqual (FirstOrder.Language.Term.relabel Sum.inl t₂)

instance FirstOrder.Language.BoundedFormula.instInhabited {L : Language} {α : Type u'} {n : ℕ} : Inhabited (L.BoundedFormula α n)

Equations

• FirstOrder.Language.BoundedFormula.instInhabited = { default := FirstOrder.Language.BoundedFormula.falsum }

instance FirstOrder.Language.BoundedFormula.instBot {L : Language} {α : Type u'} {n : ℕ} : Bot (L.BoundedFormula α n)

Equations

• FirstOrder.Language.BoundedFormula.instBot = { bot := FirstOrder.Language.BoundedFormula.falsum }

@[match_pattern]

def FirstOrder.Language.BoundedFormula.not {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : L.BoundedFormula α n

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

Equations

• φ.not = φ.imp ⊥

@[match_pattern]

def FirstOrder.Language.BoundedFormula.ex {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n

Puts an ∃ quantifier on a bounded formula.

Equations

• φ.ex = φ.not.all.not

instance FirstOrder.Language.BoundedFormula.instTop {L : Language} {α : Type u'} {n : ℕ} : Top (L.BoundedFormula α n)

Equations

• FirstOrder.Language.BoundedFormula.instTop = { top := ⊥.not }

instance FirstOrder.Language.BoundedFormula.instMin {L : Language} {α : Type u'} {n : ℕ} : Min (L.BoundedFormula α n)

Equations

• FirstOrder.Language.BoundedFormula.instMin = { min := fun (f g : L.BoundedFormula α n) => (f.imp g.not).not }

instance FirstOrder.Language.BoundedFormula.instMax {L : Language} {α : Type u'} {n : ℕ} : Max (L.BoundedFormula α n)

Equations

• FirstOrder.Language.BoundedFormula.instMax = { max := fun (f g : L.BoundedFormula α n) => f.not.imp g }

def FirstOrder.Language.BoundedFormula.iff {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormula α n) : L.BoundedFormula α n

The biimplication between two bounded formulas.

Equations

• φ.iff ψ = φ.imp ψ ⊓ ψ.imp φ

def FirstOrder.Language.BoundedFormula.freeVarFinset {L : Language} {α : Type u'} [DecidableEq α] {n : ℕ} : L.BoundedFormula α n → Finset α

The Finset of variables used in a given formula.

Equations

• FirstOrder.Language.BoundedFormula.falsum.freeVarFinset = ∅
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset = t₁.varFinsetLeft ∪ t₂.varFinsetLeft
• (FirstOrder.Language.BoundedFormula.rel _R ts).freeVarFinset = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinsetLeft
• (f₁.imp f₂).freeVarFinset = f₁.freeVarFinset ∪ f₂.freeVarFinset
• f.all.freeVarFinset = f.freeVarFinset

def FirstOrder.Language.BoundedFormula.castLE {L : Language} {α : Type u'} {m n : ℕ} (_h : m ≤ n) : L.BoundedFormula α m → L.BoundedFormula α n

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.castLE x✝ FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• FirstOrder.Language.BoundedFormula.castLE x✝ (f₁.imp f₂) = (FirstOrder.Language.BoundedFormula.castLE x✝ f₁).imp (FirstOrder.Language.BoundedFormula.castLE x✝ f₂)
• FirstOrder.Language.BoundedFormula.castLE x✝ f.all = (FirstOrder.Language.BoundedFormula.castLE ⋯ f).all

@[simp]

theorem FirstOrder.Language.BoundedFormula.castLE_rfl {L : Language} {α : Type u'} {n : ℕ} (h : n ≤ n) (φ : L.BoundedFormula α n) : castLE h φ = φ

@[simp]

theorem FirstOrder.Language.BoundedFormula.castLE_castLE {L : Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k) : castLE mn (castLE km φ) = castLE ⋯ φ

@[simp]

theorem FirstOrder.Language.BoundedFormula.castLE_comp_castLE {L : Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) : castLE mn ∘ castLE km = castLE ⋯

def FirstOrder.Language.BoundedFormula.restrictFreeVar {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] {n : ℕ} (φ : L.BoundedFormula α n) (_f : { x : α // x ∈ φ.freeVarFinset } → β) : L.BoundedFormula β n

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.falsum.restrictFreeVar _f = FirstOrder.Language.BoundedFormula.falsum
• (FirstOrder.Language.BoundedFormula.rel R ts).restrictFreeVar f = FirstOrder.Language.BoundedFormula.rel R fun (i : Fin l) => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
• (φ₁.imp φ₂).restrictFreeVar f = (φ₁.restrictFreeVar (f ∘ Set.inclusion ⋯)).imp (φ₂.restrictFreeVar (f ∘ Set.inclusion ⋯))
• φ.all.restrictFreeVar f = (φ.restrictFreeVar f).all

def FirstOrder.Language.BoundedFormula.alls {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n → L.Formula α

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

Equations

• φ.alls = φ
• φ.alls = φ.all.alls

def FirstOrder.Language.BoundedFormula.exs {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n → L.Formula α

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

Equations

• φ.exs = φ
• φ.exs = φ.ex.exs

def FirstOrder.Language.BoundedFormula.mapTermRel {L : Language} {L' : 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'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) {n : ℕ} : L.BoundedFormula α n → L'.BoundedFormula β (g n)

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

Equations

• FirstOrder.Language.BoundedFormula.mapTermRel ft fr h FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal (ft x✝ t₁) (ft x✝ t₂)
• FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.BoundedFormula.rel (fr l _R) fun (i : Fin l) => ft x✝ (ts i)
• FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (f₁.imp f₂) = (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₁).imp (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₂)
• FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f.all = (h x✝ (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f)).all

def FirstOrder.Language.BoundedFormula.liftAt {L : Language} {α : Type u'} {n : ℕ} (n' _m : ℕ) : L.BoundedFormula α n → L.BoundedFormula α (n + n')

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

Equations

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.mapTermRel_mapTermRel {L : Language} {L' : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} {L'' : 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.BoundedFormula α n) : mapTermRel ft' fr' (fun (x : ℕ) => id) (mapTermRel ft fr (fun (x : ℕ) => id) φ) = mapTermRel (fun (x : ℕ) => ft' x ∘ ft x) (fun (x : ℕ) => fr' x ∘ fr x) (fun (x : ℕ) => id) φ

@[simp]

theorem FirstOrder.Language.BoundedFormula.mapTermRel_id_id_id {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : mapTermRel (fun (x : ℕ) => id) (fun (x : ℕ) => id) (fun (x : ℕ) => id) φ = φ

def FirstOrder.Language.BoundedFormula.mapTermRelEquiv {L : Language} {L' : 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.BoundedFormula α n ≃ L'.BoundedFormula β n

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

Equations

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply {L : Language} {L' : Language} {α : Type u'} {β : Type v'} (ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)) (fr : (n : ℕ) → L.Relations n ≃ L'.Relations n) {n : ℕ} (a✝ : L.BoundedFormula α n) : (mapTermRelEquiv ft fr) a✝ = mapTermRel (fun (n : ℕ) => ⇑(ft n)) (fun (n : ℕ) => ⇑(fr n)) (fun (x : ℕ) => id) a✝

@[simp]

theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply {L : Language} {L' : Language} {α : Type u'} {β : Type v'} (ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)) (fr : (n : ℕ) → L.Relations n ≃ L'.Relations n) {n : ℕ} (a✝ : L'.BoundedFormula β n) : (mapTermRelEquiv ft fr).symm a✝ = mapTermRel (fun (n : ℕ) => ⇑(ft n).symm) (fun (n : ℕ) => ⇑(fr n).symm) (fun (x : ℕ) => id) a✝

def FirstOrder.Language.BoundedFormula.relabelAux {α : 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

• FirstOrder.Language.BoundedFormula.relabelAux g k = Sum.map id ⇑finSumFinEquiv ∘ ⇑(Equiv.sumAssoc β (Fin n) (Fin k)) ∘ Sum.map g id

@[simp]

theorem FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux {M : Type w} {α : Type u'} {β : Type v'} {n m : ℕ} {g : α → β ⊕ Fin n} {v : β → M} {xs : Fin (n + m) → M} : Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ Fin.castAdd m) ∘ g) (xs ∘ Fin.natAdd n)

@[deprecated FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux (since := "2025-02-21")]

theorem FirstOrder.Language.BoundedFormula.sum_elim_comp_relabelAux {M : Type w} {α : Type u'} {β : Type v'} {n m : ℕ} {g : α → β ⊕ Fin n} {v : β → M} {xs : Fin (n + m) → M} : Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ Fin.castAdd m) ∘ g) (xs ∘ Fin.natAdd n)

Alias of FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux.

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelAux_sumInl {α : Type u'} {n : ℕ} (k : ℕ) : relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)

@[deprecated FirstOrder.Language.BoundedFormula.relabelAux_sumInl (since := "2025-02-21")]

theorem FirstOrder.Language.BoundedFormula.relabelAux_sum_inl {α : Type u'} {n : ℕ} (k : ℕ) : relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)

Alias of FirstOrder.Language.BoundedFormula.relabelAux_sumInl.

def FirstOrder.Language.BoundedFormula.relabel {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k) : L.BoundedFormula β (n + k)

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

Equations

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

def FirstOrder.Language.BoundedFormula.relabelEquiv {L : Language} {α : Type u'} {β : Type v'} (g : α ≃ β) {k : ℕ} : L.BoundedFormula α k ≃ L.BoundedFormula β k

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

Equations

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_falsum {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} : relabel g falsum = falsum

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_bot {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} : relabel g ⊥ = ⊥

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_imp {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ ψ : L.BoundedFormula α k) : relabel g (φ.imp ψ) = (relabel g φ).imp (relabel g ψ)

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_not {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k) : relabel g φ.not = (relabel g φ).not

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_all {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α (k + 1)) : relabel g φ.all = (relabel g φ).all

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_ex {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α (k + 1)) : relabel g φ.ex = (relabel g φ).ex

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel_sumInl {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : relabel Sum.inl φ = castLE ⋯ φ

@[deprecated FirstOrder.Language.BoundedFormula.relabel_sumInl (since := "2025-02-21")]

theorem FirstOrder.Language.BoundedFormula.relabel_sum_inl {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : relabel Sum.inl φ = castLE ⋯ φ

Alias of FirstOrder.Language.BoundedFormula.relabel_sumInl.

def FirstOrder.Language.BoundedFormula.subst {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} (φ : L.BoundedFormula α n) (f : α → L.Term β) : L.BoundedFormula β n

Substitutes the variables in a given formula with terms.

Equations

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

def FirstOrder.Language.BoundedFormula.constantsVarsEquiv {L : Language} {α : Type u'} {γ : Type u_1} {n : ℕ} : (L.withConstants γ).BoundedFormula α n ≃ L.BoundedFormula (γ ⊕ α) n

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

Equations

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

def FirstOrder.Language.BoundedFormula.toFormula {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n → L.Formula (α ⊕ Fin n)

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

Equations

• FirstOrder.Language.BoundedFormula.falsum.toFormula = FirstOrder.Language.BoundedFormula.falsum
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).toFormula = t₁.equal t₂
• (FirstOrder.Language.BoundedFormula.rel _R ts).toFormula = _R.formula ts
• (f₁.imp f₂).toFormula = FirstOrder.Language.BoundedFormula.imp f₁.toFormula f₂.toFormula
• f.all.toFormula = (FirstOrder.Language.BoundedFormula.relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f.toFormula).all

noncomputable def FirstOrder.Language.BoundedFormula.iSup {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} [Finite β] (f : β → L.BoundedFormula α n) : L.BoundedFormula α n

Take the disjunction of a finite set of formulas

Equations

• FirstOrder.Language.BoundedFormula.iSup f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊔ x2) ⊥ (List.map f Finset.univ.toList)

noncomputable def FirstOrder.Language.BoundedFormula.iInf {L : Language} {α : Type u'} {β : Type v'} {n : ℕ} [Finite β] (f : β → L.BoundedFormula α n) : L.BoundedFormula α n

Take the conjunction of a finite set of formulas

Equations

• FirstOrder.Language.BoundedFormula.iInf f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊓ x2) ⊤ (List.map f Finset.univ.toList)

def FirstOrder.Language.LHom.onBoundedFormula {L : Language} {L' : Language} {α : Type u'} (g : L →ᴸ L') {k : ℕ} : L.BoundedFormula α k → L'.BoundedFormula α k

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

Equations

• g.onBoundedFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• g.onBoundedFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = (g.onTerm t₁).bdEqual (g.onTerm t₂)
• g.onBoundedFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = (g.onRelation _R).boundedFormula (g.onTerm ∘ ts)
• g.onBoundedFormula (f₁.imp f₂) = (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)
• g.onBoundedFormula f.all = (g.onBoundedFormula f).all

@[simp]

theorem FirstOrder.Language.LHom.id_onBoundedFormula {L : Language} {α : Type u'} {n : ℕ} : (LHom.id L).onBoundedFormula = id

@[simp]

theorem FirstOrder.Language.LHom.comp_onBoundedFormula {L : Language} {L' : Language} {α : Type u'} {n : ℕ} {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') : (φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula

def FirstOrder.Language.LHom.onFormula {L : Language} {L' : Language} {α : Type u'} (g : L →ᴸ L') : L.Formula α → L'.Formula α

Maps a formula's symbols along a language map.

Equations

• g.onFormula = g.onBoundedFormula

def FirstOrder.Language.LHom.onSentence {L : Language} {L' : Language} (g : L →ᴸ L') : L.Sentence → L'.Sentence

Maps a sentence's symbols along a language map.

Equations

• g.onSentence = g.onFormula

def FirstOrder.Language.LHom.onTheory {L : Language} {L' : Language} (g : L →ᴸ L') (T : L.Theory) : L'.Theory

Maps a theory's symbols along a language map.

Equations

• g.onTheory T = g.onSentence '' T

@[simp]

theorem FirstOrder.Language.LHom.mem_onTheory {L : Language} {L' : Language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence} : φ ∈ g.onTheory T ↔ ∃ φ₀ ∈ T, g.onSentence φ₀ = φ

def FirstOrder.Language.LEquiv.onBoundedFormula {L : Language} {L' : Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') : L.BoundedFormula α n ≃ L'.BoundedFormula α n

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

Equations

• φ.onBoundedFormula = { toFun := φ.toLHom.onBoundedFormula, invFun := φ.invLHom.onBoundedFormula, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.LEquiv.onBoundedFormula_apply {L : Language} {L' : Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (a✝ : L.BoundedFormula α n) : φ.onBoundedFormula a✝ = φ.toLHom.onBoundedFormula a✝

@[simp]

theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply {L : Language} {L' : Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (a✝ : L'.BoundedFormula α n) : φ.onBoundedFormula.symm a✝ = φ.invLHom.onBoundedFormula a✝

theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm {L : Language} {L' : Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') : φ.onBoundedFormula.symm = φ.symm.onBoundedFormula

def FirstOrder.Language.LEquiv.onFormula {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') : L.Formula α ≃ L'.Formula α

Maps a formula's symbols along a language equivalence.

Equations

• φ.onFormula = φ.onBoundedFormula

@[simp]

theorem FirstOrder.Language.LEquiv.onFormula_apply {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') : ⇑φ.onFormula = φ.toLHom.onFormula

@[simp]

theorem FirstOrder.Language.LEquiv.onFormula_symm {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') : φ.onFormula.symm = φ.symm.onFormula

def FirstOrder.Language.LEquiv.onSentence {L : Language} {L' : Language} (φ : L ≃ᴸ L') : L.Sentence ≃ L'.Sentence

Maps a sentence's symbols along a language equivalence.

Equations

• φ.onSentence = φ.onFormula

@[simp]

theorem FirstOrder.Language.LEquiv.onSentence_symm_apply {L : Language} {L' : Language} (φ : L ≃ᴸ L') (a✝ : L'.BoundedFormula Empty 0) : φ.onSentence.symm a✝ = φ.invLHom.onBoundedFormula a✝

@[simp]

theorem FirstOrder.Language.LEquiv.onSentence_apply {L : Language} {L' : Language} (φ : L ≃ᴸ L') (a✝ : L.BoundedFormula Empty 0) : φ.onSentence a✝ = φ.toLHom.onBoundedFormula a✝

def FirstOrder.«term_='_» : Lean.TrailingParserDescr

The equality of two terms as a bounded formula.

Equations

• FirstOrder.«term_='_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_='_» 88 88 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =' ") (Lean.ParserDescr.cat `term 89))

def FirstOrder.«term_⟹_» : Lean.TrailingParserDescr

The implication between two bounded formulas

Equations

• FirstOrder.«term_⟹_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_⟹_» 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 62))

def FirstOrder.«term∀'_» : Lean.ParserDescr

The universal quantifier over bounded formulas

Equations

• FirstOrder.«term∀'_» = Lean.ParserDescr.node `FirstOrder.«term∀'_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀'") (Lean.ParserDescr.cat `term 110))

def FirstOrder.«term∼_» : Lean.ParserDescr

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

Equations

• FirstOrder.«term∼_» = Lean.ParserDescr.node `FirstOrder.«term∼_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 1023))

def FirstOrder.«term_⇔_» : Lean.TrailingParserDescr

The biimplication between two bounded formulas.

Equations

• FirstOrder.«term_⇔_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_⇔_» 61 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 62))

def FirstOrder.«term∃'_» : Lean.ParserDescr

Puts an ∃ quantifier on a bounded formula.

Equations

• FirstOrder.«term∃'_» = Lean.ParserDescr.node `FirstOrder.«term∃'_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃'") (Lean.ParserDescr.cat `term 110))

def FirstOrder.Language.Formula.relabel {L : Language} {α : Type u'} {β : Type v'} (g : α → β) : L.Formula α → L.Formula β

Relabels a formula's variables along a particular function.

Equations

• FirstOrder.Language.Formula.relabel g = FirstOrder.Language.BoundedFormula.relabel (Sum.inl ∘ g)

def FirstOrder.Language.Formula.graph {L : Language} {n : ℕ} (f : L.Functions n) : L.Formula (Fin (n + 1))

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

Equations

• FirstOrder.Language.Formula.graph f = (FirstOrder.Language.var 0).equal (FirstOrder.Language.func f fun (i : Fin n) => FirstOrder.Language.var i.succ)

@[reducible, inline]

abbrev FirstOrder.Language.Formula.not {L : Language} {α : Type u'} (φ : L.Formula α) : L.Formula α

The negation of a formula.

Equations

• φ.not = FirstOrder.Language.BoundedFormula.not φ

@[reducible, inline]

abbrev FirstOrder.Language.Formula.imp {L : Language} {α : Type u'} : L.Formula α → L.Formula α → L.Formula α

The implication between formulas, as a formula.

Equations

• FirstOrder.Language.Formula.imp = FirstOrder.Language.BoundedFormula.imp

noncomputable def FirstOrder.Language.Formula.iAlls {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α

iAlls f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by universally quantifying over all variables Sum.inr _.

Equations

• FirstOrder.Language.Formula.iAlls β φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls

noncomputable def FirstOrder.Language.Formula.iExs {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α

iExs f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by existentially quantifying over all variables Sum.inr _.

Equations

• FirstOrder.Language.Formula.iExs β φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id (⇑(Classical.choice ⋯)) a) φ).exs

noncomputable def FirstOrder.Language.Formula.iExsUnique {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α

iExsUnique f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by existentially quantifying over all variables Sum.inr _ and asserting that the solution should be unique

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.Formula.iff {L : Language} {α : Type u'} (φ ψ : L.Formula α) : L.Formula α

The biimplication between formulas, as a formula.

Equations

• φ.iff ψ = FirstOrder.Language.BoundedFormula.iff φ ψ

def FirstOrder.Language.Formula.equivSentence {L : Language} {α : Type u'} : L.Formula α ≃ (L.withConstants α).Sentence

A bijection sending formulas to sentences with constants.

Equations

• FirstOrder.Language.Formula.equivSentence = (FirstOrder.Language.BoundedFormula.constantsVarsEquiv.trans (FirstOrder.Language.BoundedFormula.relabelEquiv (Equiv.sumEmpty α Empty))).symm

theorem FirstOrder.Language.Formula.equivSentence_not {L : Language} {α : Type u'} (φ : L.Formula α) : equivSentence φ.not = Formula.not (equivSentence φ)

theorem FirstOrder.Language.Formula.equivSentence_inf {L : Language} {α : Type u'} (φ ψ : L.Formula α) : equivSentence (φ ⊓ ψ) = equivSentence φ ⊓ equivSentence ψ

def FirstOrder.Language.Relations.reflexive {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is reflexive.

Equations

• r.reflexive = (r.boundedFormula₂ ((FirstOrder.Language.var ∘ Sum.inr) 0) ((FirstOrder.Language.var ∘ Sum.inr) 0)).all

def FirstOrder.Language.Relations.irreflexive {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is irreflexive.

Equations

• r.irreflexive = (r.boundedFormula₂ ((FirstOrder.Language.var ∘ Sum.inr) 0) ((FirstOrder.Language.var ∘ Sum.inr) 0)).not.all

def FirstOrder.Language.Relations.symmetric {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is symmetric.

Equations

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

def FirstOrder.Language.Relations.antisymmetric {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is antisymmetric.

Equations

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

def FirstOrder.Language.Relations.transitive {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is transitive.

Equations

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

def FirstOrder.Language.Relations.total {L : Language} (r : L.Relations 2) : L.Sentence

The sentence indicating that a basic relation symbol is total.

Equations

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

def FirstOrder.Language.Sentence.cardGe (L : Language) (n : ℕ) : L.Sentence

A sentence indicating that a structure has n distinct elements.

Equations

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

def FirstOrder.Language.infiniteTheory (L : Language) : L.Theory

A theory indicating that a structure is infinite.

Equations

• L.infiniteTheory = Set.range (FirstOrder.Language.Sentence.cardGe L)

def FirstOrder.Language.nonemptyTheory (L : Language) : L.Theory

A theory that indicates a structure is nonempty.

Equations

• L.nonemptyTheory = {FirstOrder.Language.Sentence.cardGe L 1}

def FirstOrder.Language.distinctConstantsTheory (L : Language) {α : Type u'} (s : Set α) : (L.withConstants α).Theory

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

Equations

• L.distinctConstantsTheory s = (fun (ab : α × α) => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (Set.diagonal α)ᶜ)

theorem FirstOrder.Language.distinctConstantsTheory_mono {L : Language} {α : Type u'} {s t : Set α} (h : s ⊆ t) : L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t

theorem FirstOrder.Language.monotone_distinctConstantsTheory {L : Language} {α : Type u'} : Monotone L.distinctConstantsTheory

theorem FirstOrder.Language.directed_distinctConstantsTheory {L : Language} {α : Type u'} : Directed (fun (x1 x2 : (L.withConstants α).Theory) => x1 ⊆ x2) L.distinctConstantsTheory

theorem FirstOrder.Language.distinctConstantsTheory_eq_iUnion {L : Language} {α : Type u'} (s : Set α) : L.distinctConstantsTheory s = ⋃ (t : Finset ↑s), L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) t)