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 : FirstOrder.Language) (α : Type u') : Type (max u u')

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

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

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

The Finset of variables used in a given term.

Equations

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

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

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

Equations

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

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

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} => FirstOrder.Language.Term.relabel g (ts i)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Relabels a term's variables along a bijection.

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

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.Term.restrictVar (FirstOrder.Language.var a) f = FirstOrder.Language.var (f { val := a, property := (_ : a ∈ {a}) })

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

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.Term.restrictVarLeft (FirstOrder.Language.var (Sum.inl a)) f = FirstOrder.Language.var (Sum.inl (f { val := a, property := (_ : a ∈ {a}) }))
• FirstOrder.Language.Term.restrictVarLeft (FirstOrder.Language.var (Sum.inr a)) _f = FirstOrder.Language.var (Sum.inr a)

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

The representation of a constant symbol as a term.

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

Applies a unary function to a term.

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

Applies a binary function to two terms.

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

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.Term.constantsToVars (FirstOrder.Language.var a) = FirstOrder.Language.var (Sum.inr a)

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

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

Equations

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

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquiv_apply {L : FirstOrder.Language} {α : Type u'} {γ : Type u_3} : ∀ (a : FirstOrder.Language.Term (FirstOrder.Language.withConstants L γ) α), ↑FirstOrder.Language.Term.constantsVarsEquiv a = FirstOrder.Language.Term.constantsToVars a

@[simp]

theorem FirstOrder.Language.Term.constantsVarsEquiv_symm_apply {L : FirstOrder.Language} {α : Type u'} {γ : Type u_3} : ∀ (a : FirstOrder.Language.Term L (γ ⊕ α)), ↑FirstOrder.Language.Term.constantsVarsEquiv.symm a = FirstOrder.Language.Term.varsToConstants a

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

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

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

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

@[simp]

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

@[simp]

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

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

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

def FirstOrder.Language.Term.liftAt {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (n' : ℕ) (m : ℕ) : FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.Term L (α ⊕ Fin (n + n'))

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

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

Substitutes the variables in a given term with terms.

Equations

• FirstOrder.Language.Term.subst (FirstOrder.Language.var a) x = x a
• FirstOrder.Language.Term.subst (FirstOrder.Language.func f ts) x = FirstOrder.Language.func f fun i => FirstOrder.Language.Term.subst (ts i) x

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

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

Maps a term's symbols along a language map.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Lequiv.onTerm_symm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') : ∀ (a : FirstOrder.Language.Term L' α), ↑(FirstOrder.Language.Lequiv.onTerm φ).symm a = FirstOrder.Language.LHom.onTerm φ.invLHom a

@[simp]

theorem FirstOrder.Language.Lequiv.onTerm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') : ∀ (a : FirstOrder.Language.Term L α), ↑(FirstOrder.Language.Lequiv.onTerm φ) a = FirstOrder.Language.LHom.onTerm φ.toLHom a

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

Maps a term's symbols along a language equivalence.

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

• falsum: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α n
• equal: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.BoundedFormula L α n
• rel: {L : FirstOrder.Language} → {α : Type u'} → {n l : ℕ} → FirstOrder.Language.Relations L l → (Fin l → FirstOrder.Language.Term L (α ⊕ Fin n)) → FirstOrder.Language.BoundedFormula L α n
• imp: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α n → FirstOrder.Language.BoundedFormula L α n → FirstOrder.Language.BoundedFormula L α n
• all: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α (n + 1) → FirstOrder.Language.BoundedFormula L α n

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

@[reducible]

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

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

@[reducible]

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

A sentence is a formula with no free variables.

@[reducible]

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

A theory is a set of sentences.

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

Applies a relation to terms as a bounded formula.

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

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

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

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

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

The equality of two terms as a bounded formula.

def FirstOrder.Language.Relations.formula {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (R : FirstOrder.Language.Relations L n) (ts : Fin n → FirstOrder.Language.Term L α) : FirstOrder.Language.Formula L α

Applies a relation to terms as a bounded formula.

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

Applies a unary relation to a term as a formula.

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

Applies a binary relation to two terms as a formula.

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

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

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

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

@[match_pattern]

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

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

@[match_pattern]

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

Puts an ∃ quantifier on a bounded formula.

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

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

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

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

The biimplication between two bounded formulas.

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

The Finset of variables used in a given formula.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.freeVarFinset FirstOrder.Language.BoundedFormula.falsum = ∅
• FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.varFinsetLeft t₁ ∪ FirstOrder.Language.Term.varFinsetLeft t₂
• FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.rel _R ts) = Finset.biUnion Finset.univ fun i => FirstOrder.Language.Term.varFinsetLeft (ts i)
• FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.freeVarFinset f

def FirstOrder.Language.BoundedFormula.castLE {L : FirstOrder.Language} {α : Type u'} {m : ℕ} {n : ℕ} (_h : m ≤ n) : FirstOrder.Language.BoundedFormula L α m → FirstOrder.Language.BoundedFormula L α 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 (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.BoundedFormula.castLE (_ : x + 1 ≤ x + 1) f)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• FirstOrder.Language.BoundedFormula.alls φ = φ
• FirstOrder.Language.BoundedFormula.alls φ = FirstOrder.Language.BoundedFormula.alls (FirstOrder.Language.BoundedFormula.all φ)

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

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

Equations

• FirstOrder.Language.BoundedFormula.exs φ = φ
• FirstOrder.Language.BoundedFormula.exs φ = FirstOrder.Language.BoundedFormula.exs (FirstOrder.Language.BoundedFormula.ex φ)

def FirstOrder.Language.BoundedFormula.mapTermRel {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ} (ft : (n : ℕ) → FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.Term L' (β ⊕ Fin (g n))) (fr : (n : ℕ) → FirstOrder.Language.Relations L n → FirstOrder.Language.Relations L' n) (h : (n : ℕ) → FirstOrder.Language.BoundedFormula L' β (g (n + 1)) → FirstOrder.Language.BoundedFormula L' β (g n + 1)) {n : ℕ} : FirstOrder.Language.BoundedFormula L α n → FirstOrder.Language.BoundedFormula L' β (g n)

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

Equations

• One or more equations did not get rendered due to their size.
• 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 => ft x (ts i)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def FirstOrder.Language.BoundedFormula.mapTermRelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} (ft : (n : ℕ) → FirstOrder.Language.Term L (α ⊕ Fin n) ≃ FirstOrder.Language.Term L' (β ⊕ Fin n)) (fr : (n : ℕ) → FirstOrder.Language.Relations L n ≃ FirstOrder.Language.Relations L' n) {n : ℕ} : FirstOrder.Language.BoundedFormula L α n ≃ FirstOrder.Language.BoundedFormula L' β n

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

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.

@[simp]

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 ∘ FirstOrder.Language.BoundedFormula.relabelAux g m = Sum.elim (Sum.elim v (xs ∘ Fin.castAdd m) ∘ g) (xs ∘ Fin.natAdd n)

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Substitutes the variables in a given formula with terms.

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.toFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• FirstOrder.Language.BoundedFormula.toFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.equal t₁ t₂
• FirstOrder.Language.BoundedFormula.toFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.Relations.formula _R ts

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

take the disjunction of a finite set of formulas

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

take the conjunction of a finite set of formulas

inductive FirstOrder.Language.BoundedFormula.IsAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} : FirstOrder.Language.BoundedFormula L α n → Prop

• equal: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ : FirstOrder.Language.Term L (α ⊕ Fin n)), FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Term.bdEqual t₁ t₂)
• rel: ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (R : FirstOrder.Language.Relations L l) (ts : Fin l → FirstOrder.Language.Term L (α ⊕ Fin n)), FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Relations.boundedFormula R ts)

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

theorem FirstOrder.Language.BoundedFormula.not_all_isAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : FirstOrder.Language.BoundedFormula L α (n + 1)) : ¬FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.BoundedFormula.all φ)

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

theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : FirstOrder.Language.BoundedFormula L α m} (h : FirstOrder.Language.BoundedFormula.IsAtomic φ) (f : α → β ⊕ Fin n) : FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.BoundedFormula.relabel f φ)

theorem FirstOrder.Language.BoundedFormula.IsAtomic.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : FirstOrder.Language.BoundedFormula L α l} {k : ℕ} {m : ℕ} (h : FirstOrder.Language.BoundedFormula.IsAtomic φ) : FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.BoundedFormula.liftAt k m φ)

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

inductive FirstOrder.Language.BoundedFormula.IsQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} : FirstOrder.Language.BoundedFormula L α n → Prop

• falsum: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, FirstOrder.Language.BoundedFormula.IsQF FirstOrder.Language.BoundedFormula.falsum
• of_isAtomic: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsAtomic φ → FirstOrder.Language.BoundedFormula.IsQF φ
• imp: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsQF φ₁ → FirstOrder.Language.BoundedFormula.IsQF φ₂ → FirstOrder.Language.BoundedFormula.IsQF (FirstOrder.Language.BoundedFormula.imp φ₁ φ₂)

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

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} : FirstOrder.Language.BoundedFormula.IsAtomic φ → FirstOrder.Language.BoundedFormula.IsQF φ

theorem FirstOrder.Language.BoundedFormula.isQF_bot {L : FirstOrder.Language} {α : Type u'} {n : ℕ} : FirstOrder.Language.BoundedFormula.IsQF ⊥

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

theorem FirstOrder.Language.BoundedFormula.IsQF.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : FirstOrder.Language.BoundedFormula L α m} (h : FirstOrder.Language.BoundedFormula.IsQF φ) (f : α → β ⊕ Fin n) : FirstOrder.Language.BoundedFormula.IsQF (FirstOrder.Language.BoundedFormula.relabel f φ)

theorem FirstOrder.Language.BoundedFormula.IsQF.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : FirstOrder.Language.BoundedFormula L α l} {k : ℕ} {m : ℕ} (h : FirstOrder.Language.BoundedFormula.IsQF φ) : FirstOrder.Language.BoundedFormula.IsQF (FirstOrder.Language.BoundedFormula.liftAt k m φ)

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

theorem FirstOrder.Language.BoundedFormula.not_all_isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : FirstOrder.Language.BoundedFormula L α (n + 1)) : ¬FirstOrder.Language.BoundedFormula.IsQF (FirstOrder.Language.BoundedFormula.all φ)

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

inductive FirstOrder.Language.BoundedFormula.IsPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} : FirstOrder.Language.BoundedFormula L α n → Prop

• of_isQF: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsQF φ → FirstOrder.Language.BoundedFormula.IsPrenex φ
• all: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α (n + 1)}, FirstOrder.Language.BoundedFormula.IsPrenex φ → FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.all φ)
• ex: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α (n + 1)}, FirstOrder.Language.BoundedFormula.IsPrenex φ → FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.ex φ)

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

theorem FirstOrder.Language.BoundedFormula.IsQF.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} : FirstOrder.Language.BoundedFormula.IsQF φ → FirstOrder.Language.BoundedFormula.IsPrenex φ

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} (h : FirstOrder.Language.BoundedFormula.IsAtomic φ) : FirstOrder.Language.BoundedFormula.IsPrenex φ

theorem FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {n : ℕ} → FirstOrder.Language.BoundedFormula L α n → Prop} {φ : FirstOrder.Language.BoundedFormula L α n} (h : FirstOrder.Language.BoundedFormula.IsPrenex φ) (hq : {m : ℕ} → {ψ : FirstOrder.Language.BoundedFormula L α m} → FirstOrder.Language.BoundedFormula.IsQF ψ → P m ψ) (ha : {m : ℕ} → {ψ : FirstOrder.Language.BoundedFormula L α (m + 1)} → P (m + 1) ψ → P m (FirstOrder.Language.BoundedFormula.all ψ)) (hn : {m : ℕ} → {ψ : FirstOrder.Language.BoundedFormula L α m} → P m ψ → P m (FirstOrder.Language.BoundedFormula.not ψ)) : P n φ

theorem FirstOrder.Language.BoundedFormula.IsPrenex.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : FirstOrder.Language.BoundedFormula L α m} (h : FirstOrder.Language.BoundedFormula.IsPrenex φ) (f : α → β ⊕ Fin n) : FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.relabel f φ)

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

theorem FirstOrder.Language.BoundedFormula.IsPrenex.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : FirstOrder.Language.BoundedFormula L α l} {k : ℕ} {m : ℕ} (h : FirstOrder.Language.BoundedFormula.IsPrenex φ) : FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.liftAt k m φ)

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

An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ is quantifier-free and ψ is in prenex normal form, then φ.toPrenexImpRight ψ is a prenex normal form for φ.imp ψ.

theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {ψ : FirstOrder.Language.BoundedFormula L α n} : FirstOrder.Language.BoundedFormula.IsQF ψ → FirstOrder.Language.BoundedFormula.toPrenexImpRight φ ψ = FirstOrder.Language.BoundedFormula.imp φ ψ

theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {ψ : FirstOrder.Language.BoundedFormula L α n} (hφ : FirstOrder.Language.BoundedFormula.IsQF φ) (hψ : FirstOrder.Language.BoundedFormula.IsPrenex ψ) : FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.toPrenexImpRight φ ψ)

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

An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ and ψ are in prenex normal form, then φ.toPrenexImp ψ is a prenex normal form for φ.imp ψ.

theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {ψ : FirstOrder.Language.BoundedFormula L α n} : FirstOrder.Language.BoundedFormula.IsQF φ → FirstOrder.Language.BoundedFormula.toPrenexImp φ ψ = FirstOrder.Language.BoundedFormula.toPrenexImpRight φ ψ

theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {ψ : FirstOrder.Language.BoundedFormula L α n} (hφ : FirstOrder.Language.BoundedFormula.IsPrenex φ) (hψ : FirstOrder.Language.BoundedFormula.IsPrenex ψ) : FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.toPrenexImp φ ψ)

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

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.toPrenex FirstOrder.Language.BoundedFormula.falsum = ⊥
• FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.bdEqual t₁ t₂
• FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.BoundedFormula.rel _R ts
• FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.BoundedFormula.toPrenex f)

theorem FirstOrder.Language.BoundedFormula.toPrenex_isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : FirstOrder.Language.BoundedFormula L α n) : FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.toPrenex φ)

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

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.LHom.onBoundedFormula g FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• FirstOrder.Language.LHom.onBoundedFormula g (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.LHom.onBoundedFormula g f)

@[simp]

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

@[simp]

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

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

Maps a formula's symbols along a language map.

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

Maps a sentence's symbols along a language map.

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

Maps a theory's symbols along a language map.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Maps a formula's symbols along a language equivalence.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Maps a sentence's symbols along a language equivalence.

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

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

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

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

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

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

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

Relabels a formula's variables along a particular function.

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

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

@[inline, reducible]

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

The negation of a formula.

@[inline, reducible]

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

The implication between formulas, as a formula.

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

Given a map f : α → β ⊕ γ, iAlls f φ transforms a L.Formula α into a L.Formula β by renaming variables with the map f and then universally quantifying over all variables Sum.inr _.

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

Given a map f : α → β ⊕ γ, iExs f φ transforms a L.Formula α into a L.Formula β by renaming variables with the map f and then universally quantifying over all variables Sum.inr _.

@[inline, reducible]

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

The biimplication between formulas, as a formula.

theorem FirstOrder.Language.Formula.isAtomic_graph {L : FirstOrder.Language} {n : ℕ} (f : FirstOrder.Language.Functions L n) : FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Formula.graph f)

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

A bijection sending formulas to sentences with constants.

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

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

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

The sentence indicating that a basic relation symbol is reflexive.

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

The sentence indicating that a basic relation symbol is irreflexive.

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

The sentence indicating that a basic relation symbol is symmetric.

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

The sentence indicating that a basic relation symbol is antisymmetric.

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

The sentence indicating that a basic relation symbol is transitive.

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

The sentence indicating that a basic relation symbol is total.

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

A sentence indicating that a structure has n distinct elements.

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

A theory indicating that a structure is infinite.

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

A theory that indicates a structure is nonempty.

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

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

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

theorem FirstOrder.Language.directed_distinctConstantsTheory {L : FirstOrder.Language} {α : Type u'} : Directed (fun x x_1 => x ⊆ x_1) (FirstOrder.Language.distinctConstantsTheory L)

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