Flypitch.FOL.Formula defines formulas over a first-order language together with the derived connectives, recursors, and the lifting/substitution lemmas used to manage de Bruijn variables.

inductive Flypitch.fol.preformula (L : Language) : ℕ → Type u

Formulas with l relation arguments still to be supplied.

• falsum {L : Language} : preformula L 0
• equal {L : Language} : term L → term L → preformula L 0
• rel {L : Language} {l : ℕ} : L.relations l → preformula L l
• apprel {L : Language} {l : ℕ} : preformula L (l + 1) → term L → preformula L l
• imp {L : Language} : preformula L 0 → preformula L 0 → preformula L 0
• all {L : Language} : preformula L 0 → preformula L 0

@[reducible, inline]

abbrev Flypitch.fol.formula (L : Language) : Type u_1

Closed formulas.

Equations

• Flypitch.fol.formula L = Flypitch.fol.preformula L 0

@[implicit_reducible]

instance Flypitch.fol.instBotFormula {L : Language} : Bot (formula L)

Equations

• Flypitch.fol.instBotFormula = { bot := Flypitch.fol.preformula.falsum }

def Flypitch.fol.«term_≃_» : Lean.TrailingParserDescr

Equations

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

def Flypitch.fol.«term_⟹_» : Lean.TrailingParserDescr

Equations

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

def Flypitch.fol.«term∀'_» : Lean.ParserDescr

Equations

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

def Flypitch.fol.not {L : Language} (f : formula L) : formula L

Derived negation.

Equations

• ∼f = f ⟹ ⊥

def Flypitch.fol.«term∼_» : Lean.ParserDescr

Equations

• Flypitch.fol.«term∼_» = Lean.ParserDescr.node `Flypitch.fol.«term∼_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 1024))

@[implicit_reducible]

instance Flypitch.fol.instTopFormula {L : Language} : Top (formula L)

Equations

• Flypitch.fol.instTopFormula = { top := ∼⊥ }

def Flypitch.fol.and {L : Language} (f₁ f₂ : formula L) : formula L

Derived conjunction.

Equations

• Flypitch.fol.and f₁ f₂ = ∼(f₁ ⟹ ∼f₂)

def Flypitch.fol.or {L : Language} (f₁ f₂ : formula L) : formula L

Derived disjunction.

Equations

• Flypitch.fol.or f₁ f₂ = ∼f₁ ⟹ f₂

def Flypitch.fol.biimp {L : Language} (f₁ f₂ : formula L) : formula L

Derived biconditional.

Equations

• Flypitch.fol.biimp f₁ f₂ = Flypitch.fol.and (f₁ ⟹ f₂) (f₂ ⟹ f₁)

def Flypitch.fol.ex {L : Language} (f : formula L) : formula L

Derived existential quantification.

Equations

• Flypitch.fol.ex f = ∼(∀' ∼f)

def Flypitch.fol.apps_rel {L : Language} {l : ℕ} : preformula L l → dvector (term L) l → formula L

Fully apply a relation formula to a tuple of term arguments.

Equations

• Flypitch.fol.apps_rel f Flypitch.dvector.nil = f
• Flypitch.fol.apps_rel f (Flypitch.dvector.cons t ts) = Flypitch.fol.apps_rel (f.apprel t) ts

@[simp]

theorem Flypitch.fol.apps_rel_zero {L : Language} (f : formula L) (ts : dvector (term L) 0) : apps_rel f ts = f

def Flypitch.fol.formula_of_relation {L : Language} {l : ℕ} (R : L.relations l) : arity' (term L) (formula L) l

View a relation symbol as an arity'-valued formula constructor.

Equations

• Flypitch.fol.formula_of_relation R = Flypitch.arity'.ofDVectorMap fun (ts : Flypitch.dvector (Flypitch.fol.term L) l) => Flypitch.fol.apps_rel (Flypitch.fol.preformula.rel R) ts

def Flypitch.fol.formula.rec' {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥) (hequal : (t₁ t₂ : term L) → C (t₁ ≃ t₂)) (hrel : {l : ℕ} → (R : L.relations l) → (ts : dvector (term L) l) → C (apps_rel (preformula.rel R) ts)) (himp : {f₁ f₂ : formula L} → C f₁ → C f₂ → C (f₁ ⟹ f₂)) (hall : {f : formula L} → C f → C (∀' f)) {l : ℕ} (f : preformula L l) (ts : dvector (term L) l) : C (apps_rel f ts)

Recursor for formulas presented as fully applied formulas.

Equations

• One or more equations did not get rendered due to their size.
• Flypitch.fol.formula.rec' hfalsum hequal hrel himp hall (Flypitch.fol.preformula.rel R) x✝ = hrel R x✝

def Flypitch.fol.formula.rec {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥) (hequal : (t₁ t₂ : term L) → C (t₁ ≃ t₂)) (hrel : {l : ℕ} → (R : L.relations l) → (ts : dvector (term L) l) → C (apps_rel (preformula.rel R) ts)) (himp : {f₁ f₂ : formula L} → C f₁ → C f₂ → C (f₁ ⟹ f₂)) (hall : {f : formula L} → C f → C (∀' f)) (f : formula L) : C f

Recursor on closed formulas.

Equations

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

theorem Flypitch.fol.formula.rec'_apps_rel {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥) (hequal : (t₁ t₂ : term L) → C (t₁ ≃ t₂)) (hrel : {l : ℕ} → (R : L.relations l) → (ts : dvector (term L) l) → C (apps_rel (preformula.rel R) ts)) (himp : {f₁ f₂ : formula L} → C f₁ → C f₂ → C (f₁ ⟹ f₂)) (hall : {f : formula L} → C f → C (∀' f)) {l : ℕ} (f : preformula L l) (ts : dvector (term L) l) : rec' hfalsum hequal (fun {l : ℕ} => hrel) (fun {f₁ f₂ : formula L} => himp) (fun {f : formula L} => hall) (apps_rel f ts) dvector.nil = rec' hfalsum hequal (fun {l : ℕ} => hrel) (fun {f₁ f₂ : formula L} => himp) (fun {f : formula L} => hall) f ts

Compatibility of formula.rec' with apps_rel.

theorem Flypitch.fol.formula.rec_apps_rel {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥) (hequal : (t₁ t₂ : term L) → C (t₁ ≃ t₂)) (hrel : {l : ℕ} → (R : L.relations l) → (ts : dvector (term L) l) → C (apps_rel (preformula.rel R) ts)) (himp : {f₁ f₂ : formula L} → C f₁ → C f₂ → C (f₁ ⟹ f₂)) (hall : {f : formula L} → C f → C (∀' f)) {l : ℕ} (R : L.relations l) (ts : dvector (term L) l) : rec hfalsum hequal (fun {l : ℕ} => hrel) (fun {f₁ f₂ : formula L} => himp) (fun {f : formula L} => hall) (apps_rel (preformula.rel R) ts) = hrel R ts

Compatibility of formula.rec with relation application.

def Flypitch.fol.lift_formula_at {L : Language} {l : ℕ} : preformula L l → ℕ → ℕ → preformula L l

Raise every free variable of index at least m in a formula by n.

Equations

• Flypitch.fol.lift_formula_at Flypitch.fol.preformula.falsum x✝¹ x✝ = Flypitch.fol.preformula.falsum
• Flypitch.fol.lift_formula_at (t₁ ≃ t₂) x✝¹ x✝ = (t₁ ↑' x✝¹ # x✝) ≃ t₂ ↑' x✝¹ # x✝
• Flypitch.fol.lift_formula_at (Flypitch.fol.preformula.rel R) x✝¹ x✝ = Flypitch.fol.preformula.rel R
• Flypitch.fol.lift_formula_at (f.apprel t) x✝¹ x✝ = (Flypitch.fol.lift_formula_at f x✝¹ x✝).apprel (t ↑' x✝¹ # x✝)
• Flypitch.fol.lift_formula_at (f₁ ⟹ f₂) x✝¹ x✝ = Flypitch.fol.lift_formula_at f₁ x✝¹ x✝ ⟹ Flypitch.fol.lift_formula_at f₂ x✝¹ x✝
• Flypitch.fol.lift_formula_at (∀' f) x✝¹ x✝ = ∀' Flypitch.fol.lift_formula_at f x✝¹ (x✝ + 1)

def Flypitch.fol.lift_formula {L : Language} {l : ℕ} : preformula L l → ℕ → preformula L l

Lift every free variable in a formula by n.

Equations

• Flypitch.fol.lift_formula x✝¹ x✝ = Flypitch.fol.lift_formula_at x✝¹ x✝ 0

def Flypitch.fol.lift_formula1 {L : Language} {l : ℕ} : preformula L l → preformula L l

Lift every free variable in a formula by one.

Equations

• Flypitch.fol.lift_formula1 x✝ = Flypitch.fol.lift_formula x✝ 1

theorem Flypitch.fol.lift_formula_def {L : Language} {l : ℕ} (f : preformula L l) (n : ℕ) : lift_formula_at f n 0 = lift_formula f n

lift_formula is lift_formula_at specialized to m = 0.

theorem Flypitch.fol.lift_formula_at_zero {L : Language} {l : ℕ} (f : preformula L l) (m : ℕ) : lift_formula_at f 0 m = f

Lifting by zero leaves a formula unchanged.

theorem Flypitch.fol.lift_formula_at_apps_rel {L : Language} {l : ℕ} (f : preformula L l) (ts : dvector (term L) l) (n m : ℕ) : lift_formula_at (apps_rel f ts) n m = apps_rel (lift_formula_at f n m) (dvector.map (fun (x : preterm L 0) => x ↑' n # m) ts)

Lifting commutes with relation application.

def Flypitch.fol.subst_formula {L : Language} {l : ℕ} : preformula L l → term L → ℕ → preformula L l

Substitute a term for variable n throughout a formula.

Equations

• Flypitch.fol.subst_formula Flypitch.fol.preformula.falsum x✝¹ x✝ = Flypitch.fol.preformula.falsum
• Flypitch.fol.subst_formula (t₁ ≃ t₂) x✝¹ x✝ = t₁[x✝¹ // x✝] ≃ t₂[x✝¹ // x✝]
• Flypitch.fol.subst_formula (Flypitch.fol.preformula.rel R) x✝¹ x✝ = Flypitch.fol.preformula.rel R
• Flypitch.fol.subst_formula (f.apprel t) x✝¹ x✝ = (Flypitch.fol.subst_formula f x✝¹ x✝).apprel (t[x✝¹ // x✝])
• Flypitch.fol.subst_formula (f₁ ⟹ f₂) x✝¹ x✝ = Flypitch.fol.subst_formula f₁ x✝¹ x✝ ⟹ Flypitch.fol.subst_formula f₂ x✝¹ x✝
• Flypitch.fol.subst_formula (∀' f) x✝¹ x✝ = ∀' Flypitch.fol.subst_formula f x✝¹ (x✝ + 1)

@[simp]

theorem Flypitch.fol.subst_formula_equal {L : Language} (t₁ t₂ s : term L) (n : ℕ) : subst_formula (t₁ ≃ t₂) s n = t₁[s // n] ≃ t₂[s // n]

theorem Flypitch.fol.subst_formula_apps_rel {L : Language} {l : ℕ} (f : preformula L l) (ts : dvector (term L) l) (s : term L) (n : ℕ) : subst_formula (apps_rel f ts) s n = apps_rel (subst_formula f s n) (dvector.map (fun (x : preterm L 0) => x[s // n]) ts)

Substitution commutes with relation application.

theorem Flypitch.fol.lift_formula_at2_small {L : Language} {l : ℕ} (f : preformula L l) (n n' : ℕ) {m m' : ℕ} : m' ≤ m → lift_formula_at (lift_formula_at f n m) n' m' = lift_formula_at (lift_formula_at f n' m') n (m + n')

Commute two lifts when the second cutoff is no larger than the first.

@[simp]

theorem Flypitch.fol.lift_formula1_lift_formula_at {L : Language} {l : ℕ} (f : preformula L l) (n m : ℕ) : lift_formula_at (lift_formula_at f n m) 1 0 = lift_formula_at (lift_formula f 1) n (m + 1)

A single lift can be moved past another lift by adjusting the cutoff.

theorem Flypitch.fol.lift_at_subst_formula_large {L : Language} {l : ℕ} (f : preformula L l) (s : term L) {n₁ : ℕ} (n₂ : ℕ) {m : ℕ} : m ≤ n₁ → subst_formula (lift_formula_at f n₂ m) s (n₁ + n₂) = lift_formula_at (subst_formula f s n₁) n₂ m

Substituting above the lift cutoff commutes with lifting.

theorem Flypitch.fol.lift_subst_formula_large {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n₁ n₂ : ℕ) : subst_formula (lift_formula f n₂) s (n₁ + n₂) = lift_formula (subst_formula f s n₁) n₂

Global lifting commutes with substitution above the lifted block.

theorem Flypitch.fol.lift_subst_formula_large' {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n₁ n₂ : ℕ) : subst_formula (lift_formula f n₂) s (n₂ + n₁) = lift_formula (subst_formula f s n₁) n₂

Commuting version of lift_subst_formula_large with the indices swapped.

@[simp]

theorem Flypitch.fol.lift_formula1_subst_shift {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n : ℕ) : subst_formula (lift_formula f 1) s (n + 1) = lift_formula (subst_formula f s n) 1

theorem Flypitch.fol.lift_at_subst_formula_medium {L : Language} {l : ℕ} (f : preformula L l) (s : term L) {n₁ n₂ m : ℕ} : m ≤ n₂ → n₂ ≤ m + n₁ → subst_formula (lift_formula_at f (n₁ + 1) m) s n₂ = lift_formula_at f n₁ m

Substituting inside the lifted block lowers the lift amount by one.

theorem Flypitch.fol.lift_at_subst_formula_eq {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n : ℕ) : subst_formula (lift_formula_at f 1 n) s n = f

Lifting once and substituting at the cutoff cancels out.

@[simp]

theorem Flypitch.fol.lift_formula1_subst {L : Language} {l : ℕ} (f : preformula L l) (s : term L) : subst_formula (lift_formula f 1) s 0 = f

theorem Flypitch.fol.lift_at_subst_formula_small {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n₁ n₂ m : ℕ) : subst_formula (lift_formula_at f n₁ (m + n₂ + 1)) (s ↑' n₁ # m) n₂ = lift_formula_at (subst_formula f s n₂) n₁ (m + n₂)

Substituting below the lift cutoff commutes with lifting the substituted term.

@[simp]

theorem Flypitch.fol.lift_at_subst_formula_small0 {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n₁ m : ℕ) : subst_formula (lift_formula_at f n₁ (m + 1)) (s ↑' n₁ # m) 0 = lift_formula_at (subst_formula f s 0) n₁ m

Special case of lift_at_subst_formula_small at variable 0.

theorem Flypitch.fol.subst_formula2 {L : Language} {l : ℕ} (f : preformula L l) (s₁ s₂ : term L) (n₁ n₂ : ℕ) : subst_formula (subst_formula f s₁ n₁) s₂ (n₁ + n₂) = subst_formula (subst_formula f s₂ (n₁ + n₂ + 1)) (s₁[s₂ // n₂]) n₁

Composition law for two substitutions into a formula.

@[simp]

theorem Flypitch.fol.subst_formula2_zero {L : Language} {l : ℕ} (f : preformula L l) (s₁ s₂ : term L) (n : ℕ) : subst_formula (subst_formula f s₁ 0) s₂ n = subst_formula (subst_formula f s₂ (n + 1)) (s₁[s₂ // n]) 0

Specialization of subst_formula2 with the first substitution at variable 0.

def Flypitch.fol.count_quantifiers {L : Language} {l : ℕ} : preformula L l → ℕ

Count the number of quantifiers appearing in a formula.

Equations

• Flypitch.fol.count_quantifiers Flypitch.fol.preformula.falsum = 0
• Flypitch.fol.count_quantifiers (a ≃ a_1) = 0
• Flypitch.fol.count_quantifiers (Flypitch.fol.preformula.rel a) = 0
• Flypitch.fol.count_quantifiers (a.apprel a_1) = 0
• Flypitch.fol.count_quantifiers (f₁ ⟹ f₂) = Flypitch.fol.count_quantifiers f₁ + Flypitch.fol.count_quantifiers f₂
• Flypitch.fol.count_quantifiers (∀' f) = Flypitch.fol.count_quantifiers f + 1

@[simp]

theorem Flypitch.fol.count_quantifiers_succ {L : Language} {l : ℕ} (f : preformula L (l + 1)) : count_quantifiers f = 0

def Flypitch.fol.quantifier_free {L : Language} {l : ℕ} (f : preformula L l) : Prop

Predicate asserting that a formula contains no quantifiers.

Equations

• Flypitch.fol.quantifier_free f = (Flypitch.fol.count_quantifiers f = 0)