Flypitch.FOL.Bounded packages terms and formulas together with proofs that their free variables stay below a prescribed bound. These bounded wrappers are used to represent closed syntax and to build Henkin witnesses later in the development.

def Flypitch.fol.bounded_preterm (L : Language) (n l : ℕ) : Type u

Terms with free variables bounded by n.

Equations

• Flypitch.fol.bounded_preterm L n l = { t : Flypitch.fol.preterm L l // Flypitch.fol.bounded_term_at t n }

@[reducible, inline]

abbrev Flypitch.fol.bounded_term (L : Language) (n : ℕ) : Type u

Closed terms with free variables bounded by n.

Equations

• Flypitch.fol.bounded_term L n = Flypitch.fol.bounded_preterm L n 0

@[reducible, inline]

abbrev Flypitch.fol.closed_preterm (L : Language) (l : ℕ) : Type u

Closed partially applied terms.

Equations

• Flypitch.fol.closed_preterm L l = Flypitch.fol.bounded_preterm L 0 l

@[reducible, inline]

abbrev Flypitch.fol.closed_term (L : Language) : Type u

Closed terms, i.e. terms with no free variables.

Equations

• Flypitch.fol.closed_term L = Flypitch.fol.bounded_term L 0

@[implicit_reducible]

instance Flypitch.fol.bounded_preterm.instCoeOutPreterm {L : Language} {n l : ℕ} : CoeOut (bounded_preterm L n l) (preterm L l)

Equations

• Flypitch.fol.bounded_preterm.instCoeOutPreterm = { coe := Subtype.val }

def Flypitch.fol.bounded_preterm.fst {L : Language} {n l : ℕ} (t : bounded_preterm L n l) : preterm L l

Equations

• t.fst = ↑t

theorem Flypitch.fol.bounded_preterm.eta {L : Language} {n l : ℕ} (t : bounded_preterm L n l) : ⟨↑t, ⋯⟩ = t

Eta-expansion for bounded terms as subtypes.

def Flypitch.fol.bounded_preterm.cast {L : Language} {n m l : ℕ} (h : n ≤ m) (t : bounded_preterm L n l) : bounded_preterm L m l

Reinterpret a bounded term at a larger variable bound.

Equations

• Flypitch.fol.bounded_preterm.cast h t = ⟨↑t, ⋯⟩

def Flypitch.fol.bounded_preterm.cast1 {L : Language} {n l : ℕ} (t : bounded_preterm L n l) : bounded_preterm L (n + 1) l

A bounded term remains bounded when the bound is increased by one.

Equations

• t.cast1 = Flypitch.fol.bounded_preterm.cast ⋯ t

theorem Flypitch.fol.bounded_preterm.cast_fst {L : Language} {n m l : ℕ} (h : n ≤ m) (t : bounded_preterm L n l) : (cast h t).fst = t.fst

theorem Flypitch.fol.bounded_preterm.cast1_fst {L : Language} {n l : ℕ} (t : bounded_preterm L n l) : t.cast1.fst = t.fst

def Flypitch.fol.bd_var {L : Language} {n : ℕ} (k : Fin n) : bounded_term L n

The bounded variable corresponding to an element of Fin n.

Equations

• Flypitch.fol.bd_var k = ⟨&↑k, ⋯⟩

def Flypitch.fol.bd_func {L : Language} {n l : ℕ} (f : L.functions l) : bounded_preterm L n l

A function symbol viewed as a bounded partially applied term.

Equations

• Flypitch.fol.bd_func f = ⟨Flypitch.fol.preterm.func f, trivial⟩

def Flypitch.fol.bd_app {L : Language} {n l : ℕ} (t : bounded_preterm L n (l + 1)) (s : bounded_term L n) : bounded_preterm L n l

Application of bounded terms preserves boundedness.

Equations

• Flypitch.fol.bd_app t s = ⟨(↑t).app ↑s, ⋯⟩

def Flypitch.fol.bd_const {L : Language} {n : ℕ} (c : L.constants) : bounded_term L n

Constants are exactly bounded nullary function symbols.

Equations

• Flypitch.fol.bd_const c = Flypitch.fol.bd_func c

def Flypitch.fol.bd_apps {L : Language} {n l : ℕ} : bounded_preterm L n l → dvector (bounded_term L n) l → bounded_term L n

Fully apply a bounded partially applied term to bounded arguments.

Equations

• Flypitch.fol.bd_apps t Flypitch.dvector.nil = t
• Flypitch.fol.bd_apps t (Flypitch.dvector.cons s ts) = Flypitch.fol.bd_apps (Flypitch.fol.bd_app t s) ts

def Flypitch.fol.bounded_preformula (L : Language) (n l : ℕ) : Type u

Formulas with free variables bounded by n.

Equations

• Flypitch.fol.bounded_preformula L n l = { f : Flypitch.fol.preformula L l // Flypitch.fol.bounded_formula_at f n }

@[reducible, inline]

abbrev Flypitch.fol.bounded_formula (L : Language) (n : ℕ) : Type u

Closed formulas with free variables bounded by n.

Equations

• Flypitch.fol.bounded_formula L n = Flypitch.fol.bounded_preformula L n 0

@[reducible, inline]

abbrev Flypitch.fol.presentence (L : Language) (l : ℕ) : Type u

Closed partially applied formulas.

Equations

• Flypitch.fol.presentence L l = Flypitch.fol.bounded_preformula L 0 l

@[implicit_reducible]

instance Flypitch.fol.bounded_preformula.instCoeOutPreformula {L : Language} {n l : ℕ} : CoeOut (bounded_preformula L n l) (preformula L l)

Equations

• Flypitch.fol.bounded_preformula.instCoeOutPreformula = { coe := Subtype.val }

def Flypitch.fol.bounded_preformula.fst {L : Language} {n l : ℕ} (f : bounded_preformula L n l) : preformula L l

Equations

• f.fst = ↑f

theorem Flypitch.fol.bounded_preformula.eta {L : Language} {n l : ℕ} (f : bounded_preformula L n l) : ⟨↑f, ⋯⟩ = f

Eta-expansion for bounded formulas as subtypes.

def Flypitch.fol.bounded_preformula.cast {L : Language} {n m l : ℕ} (h : n ≤ m) (f : bounded_preformula L n l) : bounded_preformula L m l

Reinterpret a bounded formula at a larger free-variable bound.

Equations

• Flypitch.fol.bounded_preformula.cast h f = ⟨↑f, ⋯⟩

def Flypitch.fol.bounded_preformula.cast1 {L : Language} {n l : ℕ} (f : bounded_preformula L n l) : bounded_preformula L (n + 1) l

A bounded formula remains bounded when the bound is increased by one.

Equations

• f.cast1 = Flypitch.fol.bounded_preformula.cast ⋯ f

theorem Flypitch.fol.bounded_preformula.cast_fst {L : Language} {n m l : ℕ} (h : n ≤ m) (f : bounded_preformula L n l) : (cast h f).fst = f.fst

theorem Flypitch.fol.bounded_preformula.cast1_fst {L : Language} {n l : ℕ} (f : bounded_preformula L n l) : f.cast1.fst = f.fst

def Flypitch.fol.bd_falsum {L : Language} {n : ℕ} : bounded_formula L n

The bounded version of falsum.

Equations

• Flypitch.fol.bd_falsum = ⟨⊥, trivial⟩

def Flypitch.fol.bd_equal {L : Language} {n : ℕ} (t₁ t₂ : bounded_term L n) : bounded_formula L n

Equality of bounded terms as a bounded formula.

Equations

• Flypitch.fol.bd_equal t₁ t₂ = ⟨↑t₁ ≃ ↑t₂, ⋯⟩

def Flypitch.fol.bd_rel {L : Language} {n l : ℕ} (R : L.relations l) : bounded_preformula L n l

A relation symbol viewed as a bounded partially applied formula.

Equations

• Flypitch.fol.bd_rel R = ⟨Flypitch.fol.preformula.rel R, trivial⟩

def Flypitch.fol.bd_apprel {L : Language} {n l : ℕ} (f : bounded_preformula L n (l + 1)) (t : bounded_term L n) : bounded_preformula L n l

Apply a bounded partially applied formula to a bounded term.

Equations

• Flypitch.fol.bd_apprel f t = ⟨(↑f).apprel ↑t, ⋯⟩

def Flypitch.fol.bd_imp {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_formula L n

Implication preserves boundedness.

Equations

• Flypitch.fol.bd_imp f₁ f₂ = ⟨↑f₁ ⟹ ↑f₂, ⋯⟩

def Flypitch.fol.bd_all {L : Language} {n : ℕ} (f : bounded_formula L (n + 1)) : bounded_formula L n

Universal quantification lowers the free-variable bound by one.

Equations

• Flypitch.fol.bd_all f = ⟨∀' ↑f, ⋯⟩

@[implicit_reducible]

instance Flypitch.fol.instBotBounded_formula {L : Language} {n : ℕ} : Bot (bounded_formula L n)

Equations

• Flypitch.fol.instBotBounded_formula = { bot := Flypitch.fol.bd_falsum }

def Flypitch.fol.bd_not {L : Language} {n : ℕ} (f : bounded_formula L n) : bounded_formula L n

Negation on bounded formulas.

Equations

• Flypitch.fol.bd_not f = Flypitch.fol.bd_imp f Flypitch.fol.bd_falsum

def Flypitch.fol.bd_and {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_formula L n

Conjunction on bounded formulas.

Equations

• Flypitch.fol.bd_and f₁ f₂ = Flypitch.fol.bd_not (Flypitch.fol.bd_imp f₁ (Flypitch.fol.bd_not f₂))

def Flypitch.fol.bd_or {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_formula L n

Disjunction on bounded formulas.

Equations

• Flypitch.fol.bd_or f₁ f₂ = Flypitch.fol.bd_imp (Flypitch.fol.bd_not f₁) f₂

def Flypitch.fol.bd_biimp {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_formula L n

Biconditional on bounded formulas.

Equations

• Flypitch.fol.bd_biimp f₁ f₂ = Flypitch.fol.bd_and (Flypitch.fol.bd_imp f₁ f₂) (Flypitch.fol.bd_imp f₂ f₁)

def Flypitch.fol.bd_ex {L : Language} {n : ℕ} (f : bounded_formula L (n + 1)) : bounded_formula L n

Existential quantification on bounded formulas.

Equations

• Flypitch.fol.bd_ex f = Flypitch.fol.bd_not (Flypitch.fol.bd_all (Flypitch.fol.bd_not f))

def Flypitch.fol.bd_apps_rel {L : Language} {n l : ℕ} : bounded_preformula L n l → dvector (bounded_term L n) l → bounded_formula L n

Fully apply a bounded relation formula to bounded arguments.

Equations

• Flypitch.fol.bd_apps_rel f Flypitch.dvector.nil = f
• Flypitch.fol.bd_apps_rel f (Flypitch.dvector.cons t ts) = Flypitch.fol.bd_apps_rel (Flypitch.fol.bd_apprel f t) ts

theorem Flypitch.fol.bd_var_fst {L : Language} {n : ℕ} (k : Fin n) : bounded_preterm.fst (bd_var k) = &↑k

theorem Flypitch.fol.bd_func_fst {L : Language} {n l : ℕ} (f : L.functions l) : (bd_func f).fst = preterm.func f

theorem Flypitch.fol.bd_app_fst {L : Language} {n l : ℕ} (t : bounded_preterm L n (l + 1)) (s : bounded_term L n) : (bd_app t s).fst = t.fst.app (bounded_preterm.fst s)

theorem Flypitch.fol.bd_equal_fst {L : Language} {n : ℕ} (t₁ t₂ : bounded_term L n) : bounded_preformula.fst (bd_equal t₁ t₂) = bounded_preterm.fst t₁ ≃ bounded_preterm.fst t₂

theorem Flypitch.fol.bd_rel_fst {L : Language} {n l : ℕ} (R : L.relations l) : (bd_rel R).fst = preformula.rel R

theorem Flypitch.fol.bd_apprel_fst {L : Language} {n l : ℕ} (f : bounded_preformula L n (l + 1)) (t : bounded_term L n) : (bd_apprel f t).fst = f.fst.apprel (bounded_preterm.fst t)

theorem Flypitch.fol.bd_imp_fst {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_preformula.fst (bd_imp f₁ f₂) = bounded_preformula.fst f₁ ⟹ bounded_preformula.fst f₂

theorem Flypitch.fol.bd_all_fst {L : Language} {n : ℕ} (f : bounded_formula L (n + 1)) : bounded_preformula.fst (bd_all f) = ∀' bounded_preformula.fst f

theorem Flypitch.fol.bd_not_fst {L : Language} {n : ℕ} (f : bounded_formula L n) : bounded_preformula.fst (bd_not f) = ∼(bounded_preformula.fst f)

theorem Flypitch.fol.bd_and_fst {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_preformula.fst (bd_and f₁ f₂) = and (bounded_preformula.fst f₁) (bounded_preformula.fst f₂)

theorem Flypitch.fol.bd_or_fst {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_preformula.fst (bd_or f₁ f₂) = or (bounded_preformula.fst f₁) (bounded_preformula.fst f₂)

theorem Flypitch.fol.bd_biimp_fst {L : Language} {n : ℕ} (f₁ f₂ : bounded_formula L n) : bounded_preformula.fst (bd_biimp f₁ f₂) = biimp (bounded_preformula.fst f₁) (bounded_preformula.fst f₂)

theorem Flypitch.fol.bd_ex_fst {L : Language} {n : ℕ} (f : bounded_formula L (n + 1)) : bounded_preformula.fst (bd_ex f) = ex (bounded_preformula.fst f)