NF weak partition development: Flypitch4.Fol.

Valuation helpers (subst_realize)

def NFChoice.Fol.substRealize {S : Type u} (v : ℕ → S) (x : S) (n k : ℕ) : S

Given a valuation v, a nat n, and an x : S, return v truncated to its first n values, with the rest of the values replaced by x.

Equations

• NFChoice.Fol.substRealize v x n k = if k < n then v k else if n < k then v (k - 1) else x

@[simp]

theorem NFChoice.Fol.subst_realize_lt {S : Type u} (v : ℕ → S) (x : S) {n k : ℕ} (H : k < n) : substRealize v x n k = v k

@[simp]

theorem NFChoice.Fol.subst_realize_gt {S : Type u} (v : ℕ → S) (x : S) {n k : ℕ} (H : n < k) : substRealize v x n k = v (k - 1)

@[simp]

theorem NFChoice.Fol.subst_realize_var_eq {S : Type u} (v : ℕ → S) (x : S) (n : ℕ) : substRealize v x n n = x

theorem NFChoice.Fol.subst_realize_congr {S : Type u} {v v' : ℕ → S} (hv : ∀ (k : ℕ), v k = v' k) (x : S) (n k : ℕ) : substRealize v x n k = substRealize v' x n k

theorem NFChoice.Fol.subst_realize2 {S : Type u} (v : ℕ → S) (x x' : S) (n₁ n₂ k : ℕ) : substRealize (substRealize v x' (n₁ + n₂)) x n₁ k = substRealize (substRealize v x n₁) x' (n₁ + n₂ + 1) k

theorem NFChoice.Fol.subst_realize2_0 {S : Type u} (v : ℕ → S) (x x' : S) (n k : ℕ) : substRealize (substRealize v x' n) x 0 k = substRealize (substRealize v x 0) x' (n + 1) k

theorem NFChoice.Fol.subst_realize_irrel {S : Type u} {v₁ v₂ : ℕ → S} {n : ℕ} (hv : ∀ k < n, v₁ k = v₂ k) (x : S) {k : ℕ} (hk : k < n + 1) : substRealize v₁ x 0 k = substRealize v₂ x 0 k

theorem NFChoice.Fol.lift_subst_realize_cancel {S : Type u} (v : ℕ → S) (k : ℕ) : substRealize (fun (n : ℕ) => v (n + 1)) (v 0) 0 k = v k

theorem NFChoice.Fol.subst_fin_realize_eq {S : Type u} {n : ℕ} {v₁ : DVec S n} {v₂ : ℕ → S} (hv : ∀ (k : ℕ) (hk : k < n), v₁.nth k hk = v₂ k) (x : S) (k : ℕ) (hk : k < n + 1) : (DVec.cons x v₁).nth k hk = substRealize v₂ x 0 k

Language

structure NFChoice.Fol.Language : Type (u + 1)

Flypitch construction Language, retained by the first-order soundness and completeness development.

• functions : ℕ → Type u

  The functions component of the corresponding first-order structure.

• relations : ℕ → Type u

  The relations component of the corresponding first-order structure.

def NFChoice.Fol.Language.constants (L : Language) : Type u

Flypitch construction Language.constants, retained by the first-order soundness and completeness development.

Equations

• L.constants = L.functions 0

preterm and term

inductive NFChoice.Fol.preterm (L : Language) : ℕ → Type u

preterm L l is a partially applied term. If applied to l terms, it becomes a term (l=0). We use de Bruijn variables.

• var {L : Language} (_k : ℕ) : preterm L 0
• func {L : Language} {l : ℕ} (_f : L.functions l) : preterm L l
• app {L : Language} {l : ℕ} (_t : preterm L (l + 1)) (_s : preterm L 0) : preterm L l

@[reducible]

def NFChoice.Fol.term (L : Language) : Type u

Flypitch construction term, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.term L = NFChoice.Fol.preterm L 0

def NFChoice.Fol.«term&_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term&_» = Lean.ParserDescr.node `NFChoice.Fol.«term&_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1024))

def NFChoice.Fol.apps {L : Language} {l : ℕ} : preterm L l → DVec (term L) l → term L

Flypitch construction apps, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.apps t NFChoice.DVec.nil = t
• NFChoice.Fol.apps t (NFChoice.DVec.cons t' ts) = NFChoice.Fol.apps (t.app t') ts

@[simp]

theorem NFChoice.Fol.apps_zero {L : Language} (t : term L) (ts : DVec (term L) 0) : apps t ts = t

theorem NFChoice.Fol.apps_eq_app {L : Language} {l : ℕ} (t : preterm L (l + 1)) (s : term L) (ts : DVec (term L) l) : ∃ (t' : preterm L (0 + 1)) (s' : preterm L 0), apps t (DVec.cons s ts) = t'.app s'

def NFChoice.Fol.preterm.changeArity' {L : Language} {l l' : ℕ} : l = l' → (_t : preterm L l) → preterm L l'

Flypitch construction change_arity', retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.preterm.changeArity' x✝ &k = x✝ ▸ &k
• NFChoice.Fol.preterm.changeArity' x✝ (NFChoice.Fol.preterm.func f) = NFChoice.Fol.preterm.func (x✝ ▸ f)
• NFChoice.Fol.preterm.changeArity' x✝ (t₁.app t₂) = (NFChoice.Fol.preterm.changeArity' ⋯ t₁).app t₂

@[simp]

theorem NFChoice.Fol.preterm.change_arity'_rfl {L : Language} {l : ℕ} (t : preterm L l) : changeArity' ⋯ t = t

theorem NFChoice.Fol.apps_ne_var {L : Language} {l : ℕ} {f : L.functions l} {ts : DVec (term L) l} {k : ℕ} : apps (preterm.func f) ts ≠ &k

theorem NFChoice.Fol.apps_inj' {L : Language} {l : ℕ} {t t' : preterm L l} {ts ts' : DVec (term L) l} (h : apps t ts = apps t' ts') : t = t' ∧ ts = ts'

theorem NFChoice.Fol.apps_inj {L : Language} {l : ℕ} {f f' : L.functions l} {ts ts' : DVec (term L) l} (h : apps (preterm.func f) ts = apps (preterm.func f') ts') : f = f' ∧ ts = ts'

def NFChoice.Fol.term_of_function {L : Language} {l : ℕ} (f : L.functions l) : Arity' (term L) (term L) l

Flypitch construction term_of_function, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.term_of_function f = NFChoice.Arity'.ofDvectorMap (NFChoice.Fol.apps (NFChoice.Fol.preterm.func f))

def NFChoice.Fol.term.rec {L : Language} {C : term L → Sort v} (hvar : (k : ℕ) → C &k) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : DVec (term L) l) → ((t : term L) → DVec.pmem t ts → C t) → C (apps (preterm.func f) ts)) (t : term L) : C t

Flypitch construction term.rec, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.term.rec hvar hfunc t = NFChoice.Fol.term.rec.go hvar hfunc t NFChoice.DVec.nil fun (s : NFChoice.Fol.term L) (hs : NFChoice.DVec.pmem s NFChoice.DVec.nil) => Empty.elim hs

def NFChoice.Fol.term.rec.go {L : Language} {C : term L → Sort v} (hvar : (k : ℕ) → C &k) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : DVec (term L) l) → ((t : term L) → DVec.pmem t ts → C t) → C (apps (preterm.func f) ts)) {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) (ih_ts : (s : term L) → DVec.pmem s ts → C s) : C (apps t ts)

Structural recursion accumulator.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.term.rec.go hvar hfunc (&k) ts_1 x_4 = ⋯.mpr (hvar k)
• NFChoice.Fol.term.rec.go hvar hfunc (NFChoice.Fol.preterm.func f) ts ih_ts = hfunc f ts ih_ts

def NFChoice.Fol.term.elim' {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : ⦃l : ℕ⦄ → L.functions l → DVec (term L) l → DVec C l → C) {l : ℕ} (_t : preterm L l) (_ts : DVec (term L) l) (_ih_ts : DVec C l) : C

Flypitch construction term.elim', retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.term.elim' hvar hfunc (&k) x_4 x_5 = hvar k
• NFChoice.Fol.term.elim' hvar hfunc (NFChoice.Fol.preterm.func f) x✝¹ x✝ = hfunc f x✝¹ x✝

def NFChoice.Fol.term.elim {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : ⦃l : ℕ⦄ → L.functions l → DVec (term L) l → DVec C l → C) (_t : term L) : C

Flypitch construction term.elim, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.term.elim hvar hfunc t = NFChoice.Fol.term.elim' hvar hfunc t NFChoice.DVec.nil NFChoice.DVec.nil

theorem NFChoice.Fol.term.elim'_apps {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : ⦃l : ℕ⦄ → L.functions l → DVec (term L) l → DVec C l → C) {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) : elim' hvar hfunc (apps t ts) DVec.nil DVec.nil = elim' hvar hfunc t ts (DVec.map (elim hvar hfunc) ts)

theorem NFChoice.Fol.term.elim_apps {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : ⦃l : ℕ⦄ → L.functions l → DVec (term L) l → DVec C l → C) {l : ℕ} (f : L.functions l) (ts : DVec (term L) l) : elim hvar hfunc (apps (preterm.func f) ts) = hfunc f ts (DVec.map (elim hvar hfunc) ts)

lift_term_at — lifting variables

def NFChoice.Fol.liftTermAt {L : Language} {l : ℕ} : preterm L l → ℕ → ℕ → preterm L l

lift_term_at t n m raises variables in t which are ≥ m by n.

Equations

• (&k ↑' x✝¹ # x✝) = &(if x✝ ≤ k then k + x✝¹ else k)
• (NFChoice.Fol.preterm.func f ↑' x✝¹ # x✝) = NFChoice.Fol.preterm.func f
• (t₁.app t₂ ↑' x✝¹ # x✝) = (t₁ ↑' x✝¹ # x✝).app (t₂ ↑' x✝¹ # x✝)

def NFChoice.Fol.«term_↑'_#_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

@[reducible]

def NFChoice.Fol.liftTerm {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : preterm L l

Flypitch construction lift_term, retained by the first-order soundness and completeness development.

Equations

• t ↑ n = t ↑' n # 0

def NFChoice.Fol.«term_↑_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_↑_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_↑_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑ ") (Lean.ParserDescr.cat `term 101))

@[reducible]

def NFChoice.Fol.liftTerm1 {L : Language} {l : ℕ} (t : preterm L l) : preterm L l

Flypitch construction lift_term1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.liftTerm1 t = t ↑ 1

@[simp]

theorem NFChoice.Fol.lift_term_def {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : (t ↑' n # 0) = t ↑ n

theorem NFChoice.Fol.injective_lift_term_at {L : Language} {l n m : ℕ} : Function.Injective fun (t : preterm L l) => t ↑' n # m

@[simp]

theorem NFChoice.Fol.lift_term_at_zero {L : Language} {l : ℕ} (t : preterm L l) (m : ℕ) : (t ↑' 0 # m) = t

theorem NFChoice.Fol.lift_term_zero {L : Language} {l : ℕ} (t : preterm L l) : t ↑ 0 = t

theorem NFChoice.Fol.lift_term_at2_small {L : Language} {l : ℕ} (t : preterm L l) (n n' : ℕ) {m m' : ℕ} : m' ≤ m → ((t ↑' n # m) ↑' n' # m') = (t ↑' n' # m') ↑' n # m + n'

Iterated lifts: smaller new position

theorem NFChoice.Fol.lift_term_at2_medium {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m m' : ℕ} : m ≤ m' → m' ≤ m + n → ((t ↑' n # m) ↑' n' # m') = t ↑' n + n' # m

theorem NFChoice.Fol.lift_term2_medium {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m' : ℕ} (h : m' ≤ n) : (t ↑ n ↑' n' # m') = t ↑ (n + n')

theorem NFChoice.Fol.lift_term2 {L : Language} {l : ℕ} (t : preterm L l) (n n' : ℕ) : t ↑ n ↑ n' = t ↑ (n + n')

theorem NFChoice.Fol.lift_term_at2_eq {L : Language} {l : ℕ} (t : preterm L l) (n n' m : ℕ) : ((t ↑' n # m) ↑' n' # m + n) = t ↑' n + n' # m

theorem NFChoice.Fol.lift_term_at2_large {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m m' : ℕ} (H : m + n ≤ m') : ((t ↑' n # m) ↑' n' # m') = (t ↑' n' # m' - n) ↑' n # m

theorem NFChoice.Fol.lift_term_var0 {L : Language} (n : ℕ) : &0 ↑ n = &n

@[simp]

theorem NFChoice.Fol.lift_term_at_apps {L : Language} {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) (n m : ℕ) : (apps t ts ↑' n # m) = apps (t ↑' n # m) (DVec.map (fun (x : preterm L 0) => x ↑' n # m) ts)

theorem NFChoice.Fol.lift_term_apps {L : Language} {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) (n : ℕ) : apps t ts ↑ n = apps (t ↑ n) (DVec.map (fun (x : preterm L 0) => x ↑ n) ts)

subst_term — substitution

def NFChoice.Fol.substTerm {L : Language} {l : ℕ} : preterm L l → term L → ℕ → preterm L l

subst_term t s n substitutes s for (&n) in t and reduces variable levels above n.

Equations

• NFChoice.Fol.substTerm (&k) x✝¹ x✝ = NFChoice.Fol.substRealize NFChoice.Fol.preterm.var (x✝¹ ↑ x✝) x✝ k
• NFChoice.Fol.substTerm (NFChoice.Fol.preterm.func f) x✝¹ x✝ = NFChoice.Fol.preterm.func f
• NFChoice.Fol.substTerm (t₁.app t₂) x✝¹ x✝ = (NFChoice.Fol.substTerm t₁ x✝¹ x✝).app (NFChoice.Fol.substTerm t₂ x✝¹ x✝)

@[simp]

theorem NFChoice.Fol.subst_term_var_lt {L : Language} (s : term L) {k n : ℕ} (H : k < n) : substTerm (&k) s n = &k

@[simp]

theorem NFChoice.Fol.subst_term_var_gt {L : Language} (s : term L) {k n : ℕ} (H : n < k) : substTerm (&k) s n = &(k - 1)

@[simp]

theorem NFChoice.Fol.subst_term_var_eq {L : Language} (s : term L) (n : ℕ) : substTerm (&n) s n = s ↑' n # 0

theorem NFChoice.Fol.subst_term_var0 {L : Language} (s : term L) : substTerm (&0) s 0 = s

@[simp]

theorem NFChoice.Fol.subst_term_func {L : Language} {l : ℕ} (f : L.functions l) (s : term L) (n : ℕ) : substTerm (preterm.func f) s n = preterm.func f

@[simp]

theorem NFChoice.Fol.subst_term_app {L : Language} {l : ℕ} (t₁ : preterm L (l + 1)) (t₂ s : term L) (n : ℕ) : substTerm (t₁.app t₂) s n = (substTerm t₁ s n).app (substTerm t₂ s n)

@[simp]

theorem NFChoice.Fol.subst_term_apps {L : Language} {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) (s : term L) (n : ℕ) : substTerm (apps t ts) s n = apps (substTerm t s n) (DVec.map (fun (x : preterm L 0) => substTerm x s n) ts)

theorem NFChoice.Fol.lift_at_subst_term_large {L : Language} {l : ℕ} (t : preterm L l) (s : term L) {n₁ : ℕ} (n₂ : ℕ) {m : ℕ} : m ≤ n₁ → substTerm (t ↑' n₂ # m) s (n₁ + n₂) = substTerm t s n₁ ↑' n₂ # m

Lift then substitute: large case (substituted var is above the lift range)

theorem NFChoice.Fol.lift_subst_term_large {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : substTerm (t ↑ n₂) s (n₁ + n₂) = substTerm t s n₁ ↑ n₂

theorem NFChoice.Fol.lift_subst_term_large' {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : substTerm (t ↑ n₂) s (n₂ + n₁) = substTerm t s n₁ ↑ n₂

theorem NFChoice.Fol.lift_at_subst_term_medium {L : Language} {l : ℕ} (t : preterm L l) (s : term L) {n₁ n₂ m : ℕ} : m ≤ n₂ → n₂ ≤ m + n₁ → substTerm (t ↑' n₁ + 1 # m) s n₂ = t ↑' n₁ # m

Lift then substitute: medium case (substituted var is within the lift range)

theorem NFChoice.Fol.lift_subst_term_medium {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : substTerm (t ↑ (n₁ + n₂ + 1)) s n₁ = t ↑ (n₁ + n₂)

theorem NFChoice.Fol.lift_at_subst_term_eq {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n : ℕ) : substTerm (t ↑' 1 # n) s n = t

@[simp]

theorem NFChoice.Fol.lift_term1_subst_term {L : Language} {l : ℕ} (t : preterm L l) (s : term L) : substTerm (t ↑ 1) s 0 = t

theorem NFChoice.Fol.lift_at_subst_term_small {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ m : ℕ) : substTerm (t ↑' n₁ # m + n₂ + 1) (s ↑' n₁ # m) n₂ = substTerm t s n₂ ↑' n₁ # m + n₂

Lift then substitute: small case

theorem NFChoice.Fol.subst_term2 {L : Language} {l : ℕ} (t : preterm L l) (s₁ s₂ : term L) (n₁ n₂ : ℕ) : substTerm (substTerm t s₁ n₁) s₂ (n₁ + n₂) = substTerm (substTerm t s₂ (n₁ + n₂ + 1)) (substTerm s₁ s₂ n₂) n₁

Double substitution lemma

theorem NFChoice.Fol.subst_term2_0 {L : Language} {l : ℕ} (t : preterm L l) (s₁ s₂ : term L) (n : ℕ) : substTerm (substTerm t s₁ 0) s₂ n = substTerm (substTerm t s₂ (n + 1)) (substTerm s₁ s₂ n) 0

theorem NFChoice.Fol.lift_subst_term_cancel {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : substTerm (t ↑' 1 # n + 1) (&0) n = t

preformula and formula

inductive NFChoice.Fol.preformula {L : Language} : ℕ → Type u

preformula L l is a partially applied formula. If applied to l terms, it becomes a formula (l=0).

• falsum {L : Language} : preformula 0
• equal {L : Language} (t₁ t₂ : term L) : preformula 0
• rel {L : Language} {l : ℕ} (R : L.relations l) : preformula l
• apprel {L : Language} {l : ℕ} (f : preformula (l + 1)) (t : term L) : preformula l
• imp {L : Language} (f₁ f₂ : preformula 0) : preformula 0
• all {L : Language} (f : preformula 0) : preformula 0

@[reducible]

def NFChoice.Fol.formula (L : Language) : Type u

Flypitch construction formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.formula L = NFChoice.Fol.preformula 0

def NFChoice.Fol.«term⊥'» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term⊥'» = Lean.ParserDescr.node `NFChoice.Fol.«term⊥'» 1024 (Lean.ParserDescr.symbol "⊥'")

def NFChoice.Fol.«term_≃_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.«term_⟹_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.«term∀'_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.not' {L : Language} (f : formula L) : formula L

Flypitch construction not', retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.not' f = NFChoice.Fol.preformula.imp f ⊥'

def NFChoice.Fol.«term∼_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.and' {L : Language} (f₁ f₂ : formula L) : formula L

Flypitch construction and', retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.and' f₁ f₂ = NFChoice.Fol.not' (NFChoice.Fol.preformula.imp f₁ (NFChoice.Fol.not' f₂))

def NFChoice.Fol.«term_⊓'_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊓'_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊓'_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓' ") (Lean.ParserDescr.cat `term 69))

def NFChoice.Fol.or' {L : Language} (f₁ f₂ : formula L) : formula L

Flypitch construction or', retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.or' f₁ f₂ = NFChoice.Fol.preformula.imp (NFChoice.Fol.not' f₁) f₂

def NFChoice.Fol.«term_⊔'_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊔'_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊔'_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔' ") (Lean.ParserDescr.cat `term 68))

def NFChoice.Fol.biimp {L : Language} (f₁ f₂ : formula L) : formula L

Flypitch construction biimp, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.biimp f₁ f₂ = NFChoice.Fol.and' (NFChoice.Fol.preformula.imp f₁ f₂) (NFChoice.Fol.preformula.imp f₂ f₁)

def NFChoice.Fol.«term_⇔_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.ex' {L : Language} (f : formula L) : formula L

Flypitch construction ex', retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.ex' f = NFChoice.Fol.not' (NFChoice.Fol.preformula.all (NFChoice.Fol.not' f))

def NFChoice.Fol.«term∃'_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.appsRel {L : Language} {l : ℕ} : preformula l → DVec (term L) l → formula L

Flypitch construction apps_rel, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.appsRel f NFChoice.DVec.nil = f
• NFChoice.Fol.appsRel f (NFChoice.DVec.cons t ts) = NFChoice.Fol.appsRel (f.apprel t) ts

@[simp]

theorem NFChoice.Fol.apps_rel_zero {L : Language} (f : formula L) (ts : DVec (term L) 0) : appsRel f ts = f

def NFChoice.Fol.formulaOfRelation {L : Language} {l : ℕ} (R : L.relations l) : Arity' (term L) (formula L) l

Flypitch construction formula_of_relation, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.formulaOfRelation R = NFChoice.Arity'.ofDvectorMap (NFChoice.Fol.appsRel (NFChoice.Fol.preformula.rel R))

def NFChoice.Fol.formula.rec' {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥') (hequal : (t₁ t₂ : term L) → C (preformula.equal t₁ t₂)) (hrel : ⦃l : ℕ⦄ → (R : L.relations l) → (ts : DVec (term L) l) → C (appsRel (preformula.rel R) ts)) (himp : ⦃f₁ f₂ : formula L⦄ → C f₁ → C f₂ → C (preformula.imp f₁ f₂)) (hall : ⦃f : formula L⦄ → C f → C (preformula.all f)) {l : ℕ} (f : preformula l) (ts : DVec (term L) l) : C (appsRel f ts)

Flypitch construction formula.rec', retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.formula.rec' hfalsum hequal hrel himp hall (NFChoice.Fol.preformula.rel R) x✝ = hrel R x✝
• NFChoice.Fol.formula.rec' hfalsum hequal hrel himp hall (f.apprel t) x✝ = NFChoice.Fol.formula.rec' hfalsum hequal hrel himp hall f (NFChoice.DVec.cons t x✝)

def NFChoice.Fol.formula.rec {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥') (hequal : (t₁ t₂ : term L) → C (preformula.equal t₁ t₂)) (hrel : ⦃l : ℕ⦄ → (R : L.relations l) → (ts : DVec (term L) l) → C (appsRel (preformula.rel R) ts)) (himp : ⦃f₁ f₂ : formula L⦄ → C f₁ → C f₂ → C (preformula.imp f₁ f₂)) (hall : ⦃f : formula L⦄ → C f → C (preformula.all f)) (f : formula L) : C f

Flypitch construction formula.rec, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.formula.rec hfalsum hequal hrel himp hall f = ⋯ ▸ NFChoice.Fol.formula.rec' hfalsum hequal hrel himp hall f NFChoice.DVec.nil

theorem NFChoice.Fol.formula.rec'_apps_rel {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥') (hequal : (t₁ t₂ : term L) → C (preformula.equal t₁ t₂)) (hrel : ⦃l : ℕ⦄ → (R : L.relations l) → (ts : DVec (term L) l) → C (appsRel (preformula.rel R) ts)) (himp : ⦃f₁ f₂ : formula L⦄ → C f₁ → C f₂ → C (preformula.imp f₁ f₂)) (hall : ⦃f : formula L⦄ → C f → C (preformula.all f)) {l : ℕ} (f : preformula l) (ts : DVec (term L) l) : rec' hfalsum hequal hrel himp hall (appsRel f ts) DVec.nil = rec' hfalsum hequal hrel himp hall f ts

theorem NFChoice.Fol.formula.rec_apps_rel {L : Language} {C : formula L → Sort v} (hfalsum : C ⊥') (hequal : (t₁ t₂ : term L) → C (preformula.equal t₁ t₂)) (hrel : ⦃l : ℕ⦄ → (R : L.relations l) → (ts : DVec (term L) l) → C (appsRel (preformula.rel R) ts)) (himp : ⦃f₁ f₂ : formula L⦄ → C f₁ → C f₂ → C (preformula.imp f₁ f₂)) (hall : ⦃f : formula L⦄ → C f → C (preformula.all f)) {l : ℕ} (R : L.relations l) (ts : DVec (term L) l) : rec hfalsum hequal hrel himp hall (appsRel (preformula.rel R) ts) = hrel R ts

lift_formula_at — lifting variables in formulas

def NFChoice.Fol.liftFormulaAt {L : Language} {l : ℕ} : preformula l → ℕ → ℕ → preformula l

Flypitch construction lift_formula_at, retained by the first-order soundness and completeness development.

Equations

• (⊥' ↑f' x✝¹ # x✝) = ⊥'
• (NFChoice.Fol.preformula.equal t₁ t₂ ↑f' x✝¹ # x✝) = NFChoice.Fol.preformula.equal (t₁ ↑' x✝¹ # x✝) (t₂ ↑' x✝¹ # x✝)
• (NFChoice.Fol.preformula.rel R ↑f' x✝¹ # x✝) = NFChoice.Fol.preformula.rel R
• (f.apprel t ↑f' x✝¹ # x✝) = (f ↑f' x✝¹ # x✝).apprel (t ↑' x✝¹ # x✝)
• (f₁.imp f₂ ↑f' x✝¹ # x✝) = (f₁ ↑f' x✝¹ # x✝).imp (f₂ ↑f' x✝¹ # x✝)
• (f.all ↑f' x✝¹ # x✝) = (f ↑f' x✝¹ # x✝ + 1).all

def NFChoice.Fol.«term_↑f'_#_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

@[reducible]

def NFChoice.Fol.liftFormula {L : Language} {l : ℕ} (f : preformula l) (n : ℕ) : preformula l

Flypitch construction lift_formula, retained by the first-order soundness and completeness development.

Equations

• f ↑f n = f ↑f' n # 0

def NFChoice.Fol.«term_↑f_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_↑f_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_↑f_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑f ") (Lean.ParserDescr.cat `term 101))

@[reducible]

def NFChoice.Fol.liftFormula1 {L : Language} {l : ℕ} (f : preformula l) : preformula l

Flypitch construction lift_formula1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.liftFormula1 f = f ↑f 1

@[simp]

theorem NFChoice.Fol.lift_formula_def {L : Language} {l : ℕ} (f : preformula l) (n : ℕ) : (f ↑f' n # 0) = f ↑f n

@[simp]

theorem NFChoice.Fol.lift_formula1_not {L : Language} (n : ℕ) (f : formula L) : not' f ↑f n = not' (f ↑f n)

theorem NFChoice.Fol.injective_lift_formula_at {L : Language} {l n m : ℕ} : Function.Injective fun (f : preformula l) => f ↑f' n # m

@[simp]

theorem NFChoice.Fol.lift_formula_at_zero {L : Language} {l : ℕ} (f : preformula l) (m : ℕ) : (f ↑f' 0 # m) = f

theorem NFChoice.Fol.lift_formula_at2_small {L : Language} {l : ℕ} (f : preformula l) (n n' : ℕ) {m m' : ℕ} : m' ≤ m → ((f ↑f' n # m) ↑f' n' # m') = (f ↑f' n' # m') ↑f' n # m + n'

theorem NFChoice.Fol.lift_formula_at2_medium {L : Language} {l : ℕ} (f : preformula l) (n n' : ℕ) {m m' : ℕ} : m ≤ m' → m' ≤ m + n → ((f ↑f' n # m) ↑f' n' # m') = f ↑f' n + n' # m

theorem NFChoice.Fol.lift_formula_at2_eq {L : Language} {l : ℕ} (f : preformula l) (n n' m : ℕ) : ((f ↑f' n # m) ↑f' n' # m + n) = f ↑f' n + n' # m

theorem NFChoice.Fol.lift_formula_at2_large {L : Language} {l : ℕ} (f : preformula l) (n n' : ℕ) {m m' : ℕ} (H : m + n ≤ m') : ((f ↑f' n # m) ↑f' n' # m') = (f ↑f' n' # m' - n) ↑f' n # m

@[simp]

theorem NFChoice.Fol.lift_formula_at_apps_rel {L : Language} {l : ℕ} (f : preformula l) (ts : DVec (term L) l) (n m : ℕ) : (appsRel f ts ↑f' n # m) = appsRel (f ↑f' n # m) (DVec.map (fun (x : preterm L 0) => x ↑' n # m) ts)

theorem NFChoice.Fol.lift_formula_apps_rel {L : Language} {l : ℕ} (f : preformula l) (ts : DVec (term L) l) (n : ℕ) : appsRel f ts ↑f n = appsRel (f ↑f n) (DVec.map (fun (x : preterm L 0) => x ↑ n) ts)

subst_formula — substitution into formulas

def NFChoice.Fol.substFormula {L : Language} {l : ℕ} : preformula l → term L → ℕ → preformula l

Flypitch construction subst_formula, retained by the first-order soundness and completeness development.

Equations

• ⊥' [x✝¹ // x✝]f = ⊥'
• NFChoice.Fol.preformula.equal t₁ t₂ [x✝¹ // x✝]f = NFChoice.Fol.preformula.equal (NFChoice.Fol.substTerm t₁ x✝¹ x✝) (NFChoice.Fol.substTerm t₂ x✝¹ x✝)
• NFChoice.Fol.preformula.rel R [x✝¹ // x✝]f = NFChoice.Fol.preformula.rel R
• f.apprel t [x✝¹ // x✝]f = f [x✝¹ // x✝]f.apprel (NFChoice.Fol.substTerm t x✝¹ x✝)
• f₁.imp f₂ [x✝¹ // x✝]f = f₁ [x✝¹ // x✝]f.imp (f₂ [x✝¹ // x✝]f)
• f.all [x✝¹ // x✝]f = f [x✝¹ // x✝ + 1]f.all

def NFChoice.Fol.«term_[_//_]f» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

theorem NFChoice.Fol.subst_formula_equal {L : Language} (t₁ t₂ s : term L) (n : ℕ) : preformula.equal t₁ t₂ [s // n]f = preformula.equal (substTerm t₁ s n) (substTerm t₂ s n)

@[simp]

theorem NFChoice.Fol.subst_formula_biimp {L : Language} (f₁ f₂ : formula L) (s : term L) (n : ℕ) : biimp f₁ f₂ [s // n]f = biimp (f₁ [s // n]f) (f₂ [s // n]f)

theorem NFChoice.Fol.lift_at_subst_formula_large {L : Language} {l : ℕ} (f : preformula l) (s : term L) {n₁ : ℕ} (n₂ : ℕ) {m : ℕ} : m ≤ n₁ → (f ↑f' n₂ # m) [s // n₁ + n₂]f = f [s // n₁]f ↑f' n₂ # m

theorem NFChoice.Fol.lift_subst_formula_large {L : Language} {l : ℕ} (f : preformula l) (s : term L) {n₁ n₂ : ℕ} : f ↑f n₂ [s // n₁ + n₂]f = (f [s // n₁]f) ↑f n₂

theorem NFChoice.Fol.lift_subst_formula_large' {L : Language} {l : ℕ} (f : preformula l) (s : term L) {n₁ n₂ : ℕ} : f ↑f n₂ [s // n₂ + n₁]f = (f [s // n₁]f) ↑f n₂

theorem NFChoice.Fol.lift_at_subst_formula_medium {L : Language} {l : ℕ} (f : preformula l) (s : term L) {n₁ n₂ m : ℕ} : m ≤ n₂ → n₂ ≤ m + n₁ → (f ↑f' n₁ + 1 # m) [s // n₂]f = f ↑f' n₁ # m

theorem NFChoice.Fol.lift_subst_formula_medium {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n₁ n₂ : ℕ) : f ↑f (n₁ + n₂ + 1) [s // n₁]f = f ↑f (n₁ + n₂)

theorem NFChoice.Fol.lift_at_subst_formula_eq {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n : ℕ) : (f ↑f' 1 # n) [s // n]f = f

@[simp]

theorem NFChoice.Fol.lift_formula1_subst {L : Language} {l : ℕ} (f : preformula l) (s : term L) : f ↑f 1 [s // 0]f = f

theorem NFChoice.Fol.lift_at_subst_formula_small {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n₁ n₂ m : ℕ) : (f ↑f' n₁ # m + n₂ + 1) [s ↑' n₁ # m // n₂]f = f [s // n₂]f ↑f' n₁ # m + n₂

theorem NFChoice.Fol.lift_at_subst_formula_small0 {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n₁ m : ℕ) : (f ↑f' n₁ # m + 1) [s ↑' n₁ # m // 0]f = f [s // 0]f ↑f' n₁ # m

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

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

theorem NFChoice.Fol.lift_subst_formula_cancel {L : Language} {l : ℕ} (f : preformula l) (n : ℕ) : (f ↑f' 1 # n + 1) [&0 // n]f = f

@[simp]

theorem NFChoice.Fol.subst_formula_apps_rel {L : Language} {l : ℕ} (f : preformula l) (ts : DVec (term L) l) (s : term L) (n : ℕ) : appsRel f ts [s // n]f = appsRel (f [s // n]f) (DVec.map (fun (x : preterm L 0) => substTerm x s n) ts)

count_quantifiers and quantifier_free

def NFChoice.Fol.countQuantifiers {L : Language} {l : ℕ} : preformula l → ℕ

Flypitch construction count_quantifiers, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.countQuantifiers ⊥' = 0
• NFChoice.Fol.countQuantifiers (NFChoice.Fol.preformula.equal t₁ t₂) = 0
• NFChoice.Fol.countQuantifiers (NFChoice.Fol.preformula.rel R) = 0
• NFChoice.Fol.countQuantifiers (f.apprel t) = 0
• NFChoice.Fol.countQuantifiers (f₁.imp f₂) = NFChoice.Fol.countQuantifiers f₁ + NFChoice.Fol.countQuantifiers f₂
• NFChoice.Fol.countQuantifiers f.all = NFChoice.Fol.countQuantifiers f + 1

@[simp]

theorem NFChoice.Fol.count_quantifiers_succ {L : Language} {l : ℕ} (f : preformula (l + 1)) : countQuantifiers f = 0

@[simp]

theorem NFChoice.Fol.count_quantifiers_subst {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n : ℕ) : countQuantifiers (f [s // n]f) = countQuantifiers f

def NFChoice.Fol.quantifierFree {L : Language} {l : ℕ} : preformula l → Prop

Flypitch construction quantifier_free, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.quantifierFree f = (NFChoice.Fol.countQuantifiers f = 0)

prf — the proof system (src/fol.lean lines 816-824)

inductive NFChoice.Fol.prf {L : Language} : Set (formula L) → formula L → Type u

prf Γ A is the type of proofs of A from hypotheses Γ in classical first-order logic.

• axm {L : Language} {Γ : Set (formula L)} {A : formula L} (h : A ∈ Γ) : prf Γ A
• impI {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : prf (insert A Γ) B) : prf Γ (preformula.imp A B)
• impE {L : Language} {Γ : Set (formula L)} (A : preformula 0) {B : preformula 0} (h₁ : prf Γ (A.imp B)) (h₂ : prf Γ A) : prf Γ B
• falsumE {L : Language} {Γ : Set (formula L)} {A : formula L} (h : prf (insert (not' A) Γ) ⊥') : prf Γ A
• allI {L : Language} {Γ : Set (preformula 0)} {A : formula L} (h : prf (liftFormula1 '' Γ) A) : prf Γ (preformula.all A)
• allE₂ {L : Language} {Γ : Set (formula L)} (A : preformula 0) (t : term L) (h : prf Γ A.all) : prf Γ (A [t // 0]f)
• ref {L : Language} (Γ : Set (formula L)) (t : term L) : prf Γ (preformula.equal t t)
• subst₂ {L : Language} {Γ : Set (formula L)} (s t : term L) (f : formula L) (h₁ : prf Γ (preformula.equal s t)) (h₂ : prf Γ (f [s // 0]f)) : prf Γ (f [t // 0]f)

def NFChoice.Fol.«term_⊢_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊢_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊢_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 52))

def NFChoice.Fol.provable {L : Language} (T : Set (formula L)) (f : formula L) : Prop

Flypitch construction provable, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.provable T f = Nonempty (NFChoice.Fol.prf T f)

def NFChoice.Fol.«term_⊢'_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊢'_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊢'_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢' ") (Lean.ParserDescr.cat `term 52))

Derived proof rules (src/fol.lean lines 832-1103)

def NFChoice.Fol.allE {L : Language} {Γ : Set (formula L)} (A : formula L) (t : term L) {B : preformula 0} (H₁ : prf Γ (preformula.all A)) (H₂ : A [t // 0]f = B) : prf Γ B

Flypitch construction allE, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.allE A t H₁ H₂ = H₂ ▸ NFChoice.Fol.prf.allE₂ A t H₁

def NFChoice.Fol.prfSubst {L : Language} {Γ : Set (formula L)} {s t : term L} (f₁ : formula L) {f₂ : preformula 0} (H₁ : prf Γ (preformula.equal s t)) (H₂ : prf Γ (f₁ [s // 0]f)) (H₃ : f₁ [t // 0]f = f₂) : prf Γ f₂

Flypitch construction prf_subst, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.prfSubst f₁ H₁ H₂ H₃ = H₃ ▸ NFChoice.Fol.prf.subst₂ s t f₁ H₁ H₂

def NFChoice.Fol.axm1 {L : Language} {Γ : Set (formula L)} {A : formula L} : prf (insert A Γ) A

Flypitch construction axm1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.axm1 = NFChoice.Fol.prf.axm ⋯

def NFChoice.Fol.axm2 {L : Language} {Γ : Set (formula L)} {A B : formula L} : prf (insert A (insert B Γ)) B

Flypitch construction axm2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.axm2 = NFChoice.Fol.prf.axm ⋯

noncomputable def NFChoice.Fol.weakening {L : Language} {Γ Δ : Set (formula L)} {f : formula L} (H₁ : Γ ⊆ Δ) (H₂ : prf Γ f) : prf Δ f

Flypitch construction weakening, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.prfLift {L : Language} {Γ : Set (formula L)} {f : formula L} (n m : ℕ) (H : prf Γ f) : prf ((fun (f' : preformula 0) => f' ↑f' n # m) '' Γ) (f ↑f' n # m)

Flypitch construction prf_lift, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.prfSubstitution {L : Language} {Γ : Set (formula L)} {f : formula L} (t : term L) (n : ℕ) (H : prf Γ f) : prf ((fun (x : preformula 0) => x [t // n]f) '' Γ) (f [t // n]f)

Flypitch construction prf_substitution, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.reflectPrfLift1 {L : Language} {Γ : Set (formula L)} {f : formula L} (h : prf (liftFormula1 '' Γ) (f ↑f 1)) : prf Γ f

Flypitch construction reflect_prf_lift1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.reflectPrfLift1 h = ⋯.mpr (⋯.mp (NFChoice.Fol.prfSubstitution (&0) 0 h))

noncomputable def NFChoice.Fol.weakening1 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H : prf Γ f₂) : prf (insert f₁ Γ) f₂

Flypitch construction weakening1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.weakening1 H = NFChoice.Fol.weakening ⋯ H

noncomputable def NFChoice.Fol.weakening2 {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (H : prf (insert f₁ Γ) f₂) : prf (insert f₁ (insert f₃ Γ)) f₂

Flypitch construction weakening2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.weakening2 H = NFChoice.Fol.weakening ⋯ H

noncomputable def NFChoice.Fol.deduction {L : Language} {Γ : Set (formula L)} {A B : formula L} (H : prf Γ (preformula.imp A B)) : prf (insert A Γ) B

Flypitch construction deduction, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.deduction H = NFChoice.Fol.prf.impE A (NFChoice.Fol.weakening1 H) NFChoice.Fol.axm1

noncomputable def NFChoice.Fol.exfalso {L : Language} {Γ : Set (formula L)} {A : formula L} (H : prf Γ ⊥') : prf Γ A

Flypitch construction exfalso, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.exfalso H = (NFChoice.Fol.weakening1 H).falsumE

theorem NFChoice.Fol.exfalso' {L : Language} {Γ : Set (formula L)} {A : formula L} (H : provable Γ ⊥') : provable Γ A

noncomputable def NFChoice.Fol.notI {L : Language} {Γ : Set (formula L)} {A : formula L} (H : prf Γ (preformula.imp A ⊥')) : prf Γ (not' A)

Flypitch construction notI, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.notI H = H

noncomputable def NFChoice.Fol.andI {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H₁ : prf Γ f₁) (H₂ : prf Γ f₂) : prf Γ (and' f₁ f₂)

Flypitch construction andI, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.andI H₁ H₂ = (NFChoice.Fol.prf.impE f₂ (NFChoice.Fol.prf.impE f₁ NFChoice.Fol.axm1 (NFChoice.Fol.weakening1 H₁)) (NFChoice.Fol.weakening1 H₂)).impI

noncomputable def NFChoice.Fol.andE1 {L : Language} {Γ : Set (formula L)} {f₁ : formula L} (f₂ : formula L) (H : prf Γ (and' f₁ f₂)) : prf Γ f₁

Flypitch construction andE1, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.andE2 {L : Language} {Γ : Set (formula L)} (f₁ : formula L) {f₂ : formula L} (H : prf Γ (and' f₁ f₂)) : prf Γ f₂

Flypitch construction andE2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.andE2 f₁ H = (NFChoice.Fol.prf.impE (NFChoice.Fol.preformula.imp f₁ (NFChoice.Fol.not' f₂)) (NFChoice.Fol.weakening1 H) NFChoice.Fol.axm2.impI).falsumE

noncomputable def NFChoice.Fol.orI1 {L : Language} {Γ : Set (formula L)} {A B : formula L} (H : prf Γ A) : prf Γ (or' A B)

Flypitch construction orI1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.orI1 H = (NFChoice.Fol.exfalso (NFChoice.Fol.prf.impE A NFChoice.Fol.axm1 (NFChoice.Fol.weakening1 H))).impI

noncomputable def NFChoice.Fol.orI2 {L : Language} {Γ : Set (formula L)} {A B : formula L} (H : prf Γ B) : prf Γ (or' A B)

Flypitch construction orI2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.orI2 H = (NFChoice.Fol.weakening1 H).impI

noncomputable def NFChoice.Fol.orE {L : Language} {Γ : Set (formula L)} {A B C : formula L} (H₁ : prf Γ (or' A B)) (H₂ : prf (insert A Γ) C) (H₃ : prf (insert B Γ) C) : prf Γ C

Flypitch construction orE, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.biimpI {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H₁ : prf (insert f₁ Γ) f₂) (H₂ : prf (insert f₂ Γ) f₁) : prf Γ (biimp f₁ f₂)

Flypitch construction biimpI, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.biimpI H₁ H₂ = NFChoice.Fol.andI H₁.impI H₂.impI

noncomputable def NFChoice.Fol.biimpE1 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H : prf Γ (biimp f₁ f₂)) : prf (insert f₁ Γ) f₂

Flypitch construction biimpE1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.biimpE1 H = NFChoice.Fol.deduction (NFChoice.Fol.andE1 (NFChoice.Fol.preformula.imp f₂ f₁) H)

noncomputable def NFChoice.Fol.biimpE2 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H : prf Γ (biimp f₁ f₂)) : prf (insert f₂ Γ) f₁

Flypitch construction biimpE2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.biimpE2 H = NFChoice.Fol.deduction (NFChoice.Fol.andE2 (NFChoice.Fol.preformula.imp f₁ f₂) H)

noncomputable def NFChoice.Fol.exI {L : Language} {Γ : Set (formula L)} {f : formula L} (t : term L) (H : prf Γ (f [t // 0]f)) : prf Γ (ex' f)

Flypitch construction exI, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.exI t H = (NFChoice.Fol.prf.impE (f [t // 0]f) (NFChoice.Fol.prf.allE₂ (NFChoice.Fol.not' f) t NFChoice.Fol.axm1) (NFChoice.Fol.weakening1 H)).impI

noncomputable def NFChoice.Fol.exE {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H₁ : prf Γ (ex' f₁)) (H₂ : prf (insert f₁ (liftFormula1 '' Γ)) (liftFormula1 f₂)) : prf Γ f₂

Flypitch construction exE, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.exNotOfNotAll {L : Language} {Γ : Set (formula L)} {f : formula L} (H : prf Γ (not' (preformula.all f))) : prf Γ (ex' (not' f))

Flypitch construction ex_not_of_not_all, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.notAndSelf {L : Language} {Γ : Set (formula L)} {f : formula L} (H : prf Γ (and' f (not' f))) : prf Γ ⊥'

Flypitch construction not_and_self, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.notAndSelf H = NFChoice.Fol.prf.impE f (NFChoice.Fol.andE2 f H) (NFChoice.Fol.andE1 (NFChoice.Fol.not' f) H)

noncomputable def NFChoice.Fol.prfSymm {L : Language} {Γ : Set (formula L)} {s t : term L} (H : prf Γ (preformula.equal s t)) : prf Γ (preformula.equal t s)

Flypitch construction prf_symm, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.prfSymm H = NFChoice.Fol.prfSubst (NFChoice.Fol.preformula.equal (&0) (s ↑ 1)) H (⋯.mpr (NFChoice.Fol.prf.ref Γ s)) ⋯

noncomputable def NFChoice.Fol.prfTrans {L : Language} {Γ : Set (formula L)} {t₁ t₂ t₃ : term L} (H : prf Γ (preformula.equal t₁ t₂)) (H' : prf Γ (preformula.equal t₂ t₃)) : prf Γ (preformula.equal t₁ t₃)

Flypitch construction prf_trans, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.prfTrans H H' = NFChoice.Fol.prfSubst (NFChoice.Fol.preformula.equal (t₁ ↑ 1) &0) H' (⋯.mpr H) ⋯

noncomputable def NFChoice.Fol.prfCongr {L : Language} {Γ : Set (formula L)} {t₁ t₂ : term L} (s : term L) (H : prf Γ (preformula.equal t₁ t₂)) : prf Γ (preformula.equal (substTerm s t₁ 0) (substTerm s t₂ 0))

Flypitch construction prf_congr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.prfCongr s H = NFChoice.Fol.prfSubst (NFChoice.Fol.preformula.equal (NFChoice.Fol.substTerm s t₁ 0 ↑ 1) s) H (⋯.mpr (NFChoice.Fol.prf.ref Γ (NFChoice.Fol.substTerm s t₁ 0))) ⋯

noncomputable def NFChoice.Fol.appCongr {L : Language} {Γ : Set (formula L)} {t₁ t₂ : term L} (s : preterm L 1) (H : prf Γ (preformula.equal t₁ t₂)) : prf Γ (preformula.equal (s.app t₁) (s.app t₂))

Flypitch construction app_congr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.appCongr s H = ⋯.mp (NFChoice.Fol.prfCongr ((s ↑ 1).app &0) H)

noncomputable def NFChoice.Fol.apprelCongr {L : Language} {Γ : Set (formula L)} {t₁ t₂ : term L} (f : preformula 1) (H : prf Γ (preformula.equal t₁ t₂)) (H₂ : prf Γ (f.apprel t₁)) : prf Γ (f.apprel t₂)

Flypitch construction apprel_congr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.apprelCongr f H H₂ = NFChoice.Fol.prfSubst ((f ↑f 1).apprel &0) H (⋯.mpr H₂) ⋯

noncomputable def NFChoice.Fol.impTrans {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (H₁ : prf Γ (preformula.imp f₁ f₂)) (H₂ : prf Γ (preformula.imp f₂ f₃)) : prf Γ (preformula.imp f₁ f₃)

Flypitch construction imp_trans, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.impTrans H₁ H₂ = (NFChoice.Fol.prf.impE f₂ (NFChoice.Fol.weakening1 H₂) (NFChoice.Fol.prf.impE f₁ (NFChoice.Fol.weakening1 H₁) NFChoice.Fol.axm1)).impI

noncomputable def NFChoice.Fol.biimpReflCertificate {L : Language} (Γ : Set (formula L)) (f : formula L) : prf Γ (biimp f f)

Flypitch construction biimp_refl, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.biimpReflCertificate Γ f = NFChoice.Fol.biimpI NFChoice.Fol.axm1 NFChoice.Fol.axm1

noncomputable def NFChoice.Fol.biimpTrans {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (H₁ : prf Γ (biimp f₁ f₂)) (H₂ : prf Γ (biimp f₂ f₃)) : prf Γ (biimp f₁ f₃)

Flypitch construction biimp_trans, retained by the first-order soundness and completeness development.

Equations

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

def NFChoice.Fol.equalPreterms {L : Language} (T : Set (formula L)) {l : ℕ} (t₁ t₂ : preterm L l) : Type u

Flypitch construction equal_preterms, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.equalPreterms T t₁ t₂ = ((ts : NFChoice.DVec (NFChoice.Fol.term L) l) → NFChoice.Fol.prf T (NFChoice.Fol.preformula.equal (NFChoice.Fol.apps t₁ ts) (NFChoice.Fol.apps t₂ ts)))

noncomputable def NFChoice.Fol.equalPretermsApp {L : Language} {T : Set (formula L)} {l : ℕ} {t t' : preterm L (l + 1)} {s s' : term L} (Ht : equalPreterms T t t') (Hs : prf T (preformula.equal s s')) : equalPreterms T (t.app s) (t'.app s')

Flypitch construction equal_preterms_app, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.equalPretermsRefl {L : Language} (T : Set (formula L)) {l : ℕ} (t : preterm L l) : equalPreterms T t t

Flypitch construction equal_preterms_refl, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.equalPretermsRefl T t xs = NFChoice.Fol.prf.ref T (NFChoice.Fol.apps t xs)

def NFChoice.Fol.equivPreformulae {L : Language} (T : Set (formula L)) {l : ℕ} (f₁ f₂ : preformula l) : Type u

Flypitch construction equiv_preformulae, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.equivPreformulae T f₁ f₂ = ((ts : NFChoice.DVec (NFChoice.Fol.term L) l) → NFChoice.Fol.prf T (NFChoice.Fol.biimp (NFChoice.Fol.appsRel f₁ ts) (NFChoice.Fol.appsRel f₂ ts)))

noncomputable def NFChoice.Fol.equivPreformulaeApprel {L : Language} {T : Set (formula L)} {l : ℕ} {f f' : preformula (l + 1)} {s s' : term L} (Ht : equivPreformulae T f f') (Hs : prf T (preformula.equal s s')) : equivPreformulae T (f.apprel s) (f'.apprel s')

Flypitch construction equiv_preformulae_apprel, retained by the first-order soundness and completeness development.

Equations

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

noncomputable def NFChoice.Fol.equivPreformulaeRefl {L : Language} (T : Set (formula L)) {l : ℕ} (f : preformula l) : equivPreformulae T f f

Flypitch construction equiv_preformulae_refl, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.equivPreformulaeRefl T f xs = NFChoice.Fol.biimpReflCertificate T (NFChoice.Fol.appsRel f xs)

theorem NFChoice.Fol.impI' {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : provable (insert A Γ) B) : provable Γ (preformula.imp A B)

theorem NFChoice.Fol.impE' {L : Language} {Γ : Set (formula L)} (A : formula L) {B : formula L} (h₁ : provable Γ (preformula.imp A B)) (h₂ : provable Γ A) : provable Γ B

theorem NFChoice.Fol.falsumE' {L : Language} {Γ : Set (formula L)} {A : formula L} (h : provable (insert (not' A) Γ) ⊥') : provable Γ A

theorem NFChoice.Fol.allI' {L : Language} {Γ : Set (formula L)} {A : formula L} (h : provable (liftFormula1 '' Γ) A) : provable Γ (preformula.all A)

theorem NFChoice.Fol.allE' {L : Language} {Γ : Set (formula L)} (A : formula L) (t : term L) {B : formula L} (H₁ : provable Γ (preformula.all A)) (H₂ : A [t // 0]f = B) : provable Γ B

theorem NFChoice.Fol.allE₂' {L : Language} {Γ : Set (formula L)} {A : formula L} {t : term L} (h : provable Γ (preformula.all A)) : provable Γ (A [t // 0]f)

theorem NFChoice.Fol.ref' {L : Language} (Γ : Set (formula L)) (t : term L) : provable Γ (preformula.equal t t)

theorem NFChoice.Fol.subst' {L : Language} {Γ : Set (formula L)} {s t : term L} (f₁ : formula L) {f₂ : formula L} (H₁ : provable Γ (preformula.equal s t)) (H₂ : provable Γ (f₁ [s // 0]f)) (H₃ : f₁ [t // 0]f = f₂) : provable Γ f₂

theorem NFChoice.Fol.subst₂' {L : Language} {Γ : Set (formula L)} (s t : term L) (f : formula L) (h₁ : provable Γ (preformula.equal s t)) (h₂ : provable Γ (f [s // 0]f)) : provable Γ (f [t // 0]f)

theorem NFChoice.Fol.weakening' {L : Language} {Γ Δ : Set (formula L)} {f : formula L} (H₁ : Γ ⊆ Δ) (H₂ : provable Γ f) : provable Δ f

theorem NFChoice.Fol.weakening1' {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H : provable Γ f₂) : provable (insert f₁ Γ) f₂

theorem NFChoice.Fol.weakening2' {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (H : provable (insert f₁ Γ) f₂) : provable (insert f₁ (insert f₃ Γ)) f₂

theorem NFChoice.Fol.apprel_congr' {L : Language} {Γ : Set (formula L)} {t₁ t₂ : term L} (f : preformula 1) (H : prf Γ (preformula.equal t₁ t₂)) : provable Γ (f.apprel t₁) ↔ provable Γ (f.apprel t₂)

theorem NFChoice.Fol.prf_all_iff {L : Language} {Γ : Set (formula L)} {f : formula L} : provable Γ (preformula.all f) ↔ provable (liftFormula1 '' Γ) f

theorem NFChoice.Fol.iff_of_biimp {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (H : provable Γ (biimp f₁ f₂)) : provable Γ f₁ ↔ provable Γ f₂

theorem NFChoice.Fol.prf_by_cases {L : Language} {Γ : Set (formula L)} (f₁ : formula L) {f₂ : formula L} (H₁ : provable (insert f₁ Γ) f₂) (H₂ : provable (insert (not' f₁) Γ) f₂) : provable Γ f₂

Theory and consistency (src/fol.lean lines 1105-)

def NFChoice.Fol.Theory (L : Language) : Type u

Flypitch construction Theory, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Theory L = Set (NFChoice.Fol.formula L)

def NFChoice.Fol.isConsistent {L : Language} (T : Theory L) : Prop

Flypitch construction is_consistent, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.isConsistent T = ¬NFChoice.Fol.provable T ⊥'

Structure — L-structures (src/fol.lean line 1109)

structure NFChoice.Fol.Structure (L : Language) : Type (u + 1)

Flypitch construction Structure, retained by the first-order soundness and completeness development.

• carrier : Type u

  The carrier component of the corresponding first-order structure.

• funMap {n : ℕ} : L.functions n → DVec self.carrier n → self.carrier

  The fun_map component of the corresponding first-order structure.

• relMap {n : ℕ} : L.relations n → DVec self.carrier n → Prop

  The rel_map component of the corresponding first-order structure.

@[instance_reducible]

instance NFChoice.Fol.instCoeSortStructureType {L : Language} : CoeSort (Structure L) (Type u)

Equations

• NFChoice.Fol.instCoeSortStructureType = { coe := fun (S : NFChoice.Fol.Structure L) => S.carrier }

realize_term — realization of terms in a structure

def NFChoice.Fol.realizeTerm {L : Language} {S : Structure L} (v : ℕ → S.carrier) {l : ℕ} (_t : preterm L l) (_xs : DVec S.carrier l) : S.carrier

Flypitch construction realize_term, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.realizeTerm v (&k) x_3 = v k
• NFChoice.Fol.realizeTerm v (NFChoice.Fol.preterm.func f) x✝ = S.funMap f x✝
• NFChoice.Fol.realizeTerm v (t₁.app t₂) x✝ = NFChoice.Fol.realizeTerm v t₁ (NFChoice.DVec.cons (NFChoice.Fol.realizeTerm v t₂ NFChoice.DVec.nil) x✝)

theorem NFChoice.Fol.realize_term_congr {L : Language} {S : Structure L} {v v' : ℕ → S.carrier} (h : ∀ (n : ℕ), v n = v' n) {l : ℕ} (t : preterm L l) (xs : DVec S.carrier l) : realizeTerm v t xs = realizeTerm v' t xs

theorem NFChoice.Fol.realize_term_subst {L : Language} {S : Structure L} (v : ℕ → S.carrier) {l : ℕ} (n : ℕ) (t : preterm L l) (s : term L) (xs : DVec S.carrier l) : realizeTerm (substRealize v (realizeTerm v (s ↑ n) DVec.nil) n) t xs = realizeTerm v (substTerm t s n) xs

theorem NFChoice.Fol.realize_term_subst_lift {L : Language} {S : Structure L} (v : ℕ → S.carrier) (x : S.carrier) (m : ℕ) {l : ℕ} (t : preterm L l) (xs : DVec S.carrier l) : realizeTerm (substRealize v x m) (t ↑' 1 # m) xs = realizeTerm v t xs

realize_formula — satisfaction relation

def NFChoice.Fol.realizeFormula {L : Language} {S : Structure L} {l : ℕ} : (ℕ → S.carrier) → preformula l → DVec S.carrier l → Prop

Flypitch construction realize_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.realizeFormula x✝ ⊥' x_4 = False
• NFChoice.Fol.realizeFormula x✝ (NFChoice.Fol.preformula.equal t₁ t₂) x_4 = (NFChoice.Fol.realizeTerm x✝ t₁ NFChoice.DVec.nil = NFChoice.Fol.realizeTerm x✝ t₂ NFChoice.DVec.nil)
• NFChoice.Fol.realizeFormula x✝¹ (NFChoice.Fol.preformula.rel R) x✝ = S.relMap R x✝
• NFChoice.Fol.realizeFormula x✝¹ (f.apprel t) x✝ = NFChoice.Fol.realizeFormula x✝¹ f (NFChoice.DVec.cons (NFChoice.Fol.realizeTerm x✝¹ t NFChoice.DVec.nil) x✝)
• NFChoice.Fol.realizeFormula x✝ (f₁.imp f₂) xs = (NFChoice.Fol.realizeFormula x✝ f₁ xs → NFChoice.Fol.realizeFormula x✝ f₂ xs)
• NFChoice.Fol.realizeFormula x✝ f.all x_4 = ∀ (x : S.carrier), NFChoice.Fol.realizeFormula (NFChoice.Fol.substRealize x✝ x 0) f NFChoice.DVec.nil

theorem NFChoice.Fol.realize_formula_congr {L : Language} {S : Structure L} {l : ℕ} {v v' : ℕ → S.carrier} (_h : ∀ (n : ℕ), v n = v' n) (f : preformula l) (xs : DVec S.carrier l) : realizeFormula v f xs ↔ realizeFormula v' f xs

theorem NFChoice.Fol.realize_formula_subst {L : Language} {S : Structure L} {l : ℕ} (v : ℕ → S.carrier) (n : ℕ) (f : preformula l) (s : term L) (xs : DVec S.carrier l) : realizeFormula (substRealize v (realizeTerm v (s ↑ n) DVec.nil) n) f xs ↔ realizeFormula v (f [s // n]f) xs

theorem NFChoice.Fol.realize_formula_subst0 {L : Language} {S : Structure L} {l : ℕ} (v : ℕ → S.carrier) (f : preformula l) (s : term L) (xs : DVec S.carrier l) : realizeFormula (substRealize v (realizeTerm v s DVec.nil) 0) f xs ↔ realizeFormula v (f [s // 0]f) xs

theorem NFChoice.Fol.realize_formula_subst_lift {L : Language} {S : Structure L} {l : ℕ} (v : ℕ → S.carrier) (x : S.carrier) (m : ℕ) (f : preformula l) (xs : DVec S.carrier l) : realizeFormula (substRealize v x m) (f ↑f' 1 # m) xs = realizeFormula v f xs

Semantic notions — satisfaction and models

def NFChoice.Fol.satisfiedIn {L : Language} (S : Structure L) (f : formula L) : Prop

Flypitch construction satisfied_in, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.satisfiedIn S f = ∀ (v : ℕ → S.carrier), NFChoice.Fol.realizeFormula v f NFChoice.DVec.nil

def NFChoice.Fol.«term_⊨ₛ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊨ₛ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊨ₛ_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ₛ ") (Lean.ParserDescr.cat `term 52))

def NFChoice.Fol.allSatisfiedIn {L : Language} (S : Structure L) (T : Set (formula L)) : Prop

Flypitch construction all_satisfied_in, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.allSatisfiedIn S T = ∀ ⦃f : NFChoice.Fol.formula L⦄, f ∈ T → NFChoice.Fol.satisfiedIn S f

def NFChoice.Fol.satisfied {L : Language} (T : Set (formula L)) (f : formula L) : Prop

Flypitch construction satisfied, retained by the first-order soundness and completeness development.

Equations

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

def NFChoice.Fol.«term_⊨_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊨_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊨_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ ") (Lean.ParserDescr.cat `term 52))

def NFChoice.Fol.allSatisfied {L : Language} (T T' : Set (formula L)) : Prop

Flypitch construction all_satisfied, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.allSatisfied T T' = ∀ ⦃f : NFChoice.Fol.formula L⦄, f ∈ T' → NFChoice.Fol.satisfied T f

theorem NFChoice.Fol.satisfied_in_trans {L : Language} {S : Structure L} {T : Set (formula L)} {f : formula L} (H' : allSatisfiedIn S T) (H : satisfied T f) : satisfiedIn S f

theorem NFChoice.Fol.all_satisfied_in_trans {L : Language} {S : Structure L} {T T' : Set (formula L)} (H' : allSatisfiedIn S T) (H : allSatisfied T T') : allSatisfiedIn S T'

theorem NFChoice.Fol.satisfied_of_mem {L : Language} {T : Set (formula L)} {f : formula L} (hf : f ∈ T) : satisfied T f

theorem NFChoice.Fol.all_satisfied_of_subset {L : Language} {T T' : Set (formula L)} (h : T' ⊆ T) : allSatisfied T T'

theorem NFChoice.Fol.satisfied_trans {L : Language} {T₁ T₂ : Set (formula L)} {f : formula L} (H' : allSatisfied T₁ T₂) (H : satisfied T₂ f) : satisfied T₁ f

theorem NFChoice.Fol.all_satisfied_trans {L : Language} {T₁ T₂ T₃ : Set (formula L)} (H' : allSatisfied T₁ T₂) (H : allSatisfied T₂ T₃) : allSatisfied T₁ T₃

theorem NFChoice.Fol.satisfied_weakening {L : Language} {T T' : Set (formula L)} (H : T ⊆ T') {f : formula L} (HT : satisfied T f) : satisfied T' f

Soundness (src/fol.lean lines 1247-1261)

theorem NFChoice.Fol.formula_soundness {L : Language} {Γ : Set (formula L)} {A : formula L} (H : prf Γ A) : satisfied Γ A

bounded_preterm, bounded_term, closed_preterm

(src/fol.lean lines 1265-1660)

inductive NFChoice.Fol.BoundedPreterm (L : Language) (n : ℕ) : ℕ → Type u

A bounded preterm: bounded_preterm L n l is a partially applied term with at most n free de Bruijn variables (indexed by Fin n) needing l more arguments.

• bd_var {L : Language} {n : ℕ} (_k : Fin n) : BoundedPreterm L n 0
• bd_func {L : Language} {n l : ℕ} (_f : L.functions l) : BoundedPreterm L n l
• bd_app {L : Language} {n l : ℕ} (_t : BoundedPreterm L n (l + 1)) (_s : BoundedPreterm L n 0) : BoundedPreterm L n l

@[reducible, inline]

abbrev NFChoice.Fol.boundedTerm (L : Language) (n : ℕ) : Type u

A fully applied bounded term with at most n free variables.

Equations

• NFChoice.Fol.boundedTerm L n = NFChoice.Fol.BoundedPreterm L n 0

@[reducible, inline]

abbrev NFChoice.Fol.closedPreterm (L : Language) (l : ℕ) : Type u

A closed preterm (no free variables), needing l more arguments.

Equations

• NFChoice.Fol.closedPreterm L l = NFChoice.Fol.BoundedPreterm L 0 l

@[reducible, inline]

abbrev NFChoice.Fol.closedTerm (L : Language) : Type u

A closed term: no free variables and fully applied.

Equations

• NFChoice.Fol.closedTerm L = NFChoice.Fol.closedPreterm L 0

def NFChoice.Fol.«term&ᵇ_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term&ᵇ_» = Lean.ParserDescr.node `NFChoice.Fol.«term&ᵇ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&ᵇ") (Lean.ParserDescr.cat `term 1024))

def NFChoice.Fol.bdConst {L : Language} {n : ℕ} (c : L.constants) : boundedTerm L n

Flypitch construction bd_const, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdConst c = NFChoice.Fol.bd_func c

def NFChoice.Fol.bdApps' {L : Language} {n l m : ℕ} : BoundedPreterm L n (l + m) → DVec (boundedTerm L n) m → BoundedPreterm L n l

Apply a bounded preterm of level l + m to m bounded terms to get level l.

Equations

• NFChoice.Fol.bdApps' t NFChoice.DVec.nil = t
• NFChoice.Fol.bdApps' t (NFChoice.DVec.cons x_4 xs) = NFChoice.Fol.bdApps' (t.bd_app x_4) xs

def NFChoice.Fol.bdApps {L : Language} {n l : ℕ} : BoundedPreterm L n l → DVec (boundedTerm L n) l → boundedTerm L n

Apply a bounded preterm of level l to l bounded terms to get a bounded term.

Equations

• NFChoice.Fol.bdApps t NFChoice.DVec.nil = t
• NFChoice.Fol.bdApps t (NFChoice.DVec.cons t' ts) = NFChoice.Fol.bdApps (t.bd_app t') ts

def NFChoice.Fol.BoundedPreterm.fst {L : Language} {n l : ℕ} : BoundedPreterm L n l → preterm L l

Forget boundedness: map a bounded preterm to an ordinary preterm.

Equations

• (NFChoice.Fol.bd_var k).fst = &↑k
• (NFChoice.Fol.bd_func f).fst = NFChoice.Fol.preterm.func f
• (t.bd_app s).fst = t.fst.app s.fst

theorem NFChoice.Fol.BoundedPreterm.eq {L : Language} {n l : ℕ} {t₁ t₂ : BoundedPreterm L n l} : t₁.fst = t₂.fst → t₁ = t₂

Equality of bounded preterms is determined by their underlying preterms.

theorem NFChoice.Fol.BoundedPreterm.eq_iff {L : Language} {n l : ℕ} {t₁ t₂ : BoundedPreterm L n l} : t₁ = t₂ ↔ t₁.fst = t₂.fst

def NFChoice.Fol.BoundedPreterm.cast {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} : BoundedPreterm L n l → BoundedPreterm L m l

Cast a bounded_preterm L n l to one with a larger bound m ≥ n.

Equations

• NFChoice.Fol.BoundedPreterm.cast h (NFChoice.Fol.bd_var k) = NFChoice.Fol.bd_var ⟨↑k, ⋯⟩
• NFChoice.Fol.BoundedPreterm.cast h (NFChoice.Fol.bd_func f) = NFChoice.Fol.bd_func f
• NFChoice.Fol.BoundedPreterm.cast h (t.bd_app s) = (NFChoice.Fol.BoundedPreterm.cast h t).bd_app (NFChoice.Fol.BoundedPreterm.cast h s)

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_bd_app {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} {t : BoundedPreterm L n (l + 1)} {s : BoundedPreterm L n 0} : BoundedPreterm.cast h (t.bd_app s) = (BoundedPreterm.cast h t).bd_app (BoundedPreterm.cast h s)

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_bd_apps {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} {t : BoundedPreterm L n l} {ts : DVec (boundedTerm L n) l} : BoundedPreterm.cast h (bdApps t ts) = bdApps (BoundedPreterm.cast h t) (DVec.map (fun (x : boundedTerm L n) => BoundedPreterm.cast h x) ts)

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_irrel {L : Language} {n m : ℕ} {h h' : n ≤ m} {l : ℕ} (t : BoundedPreterm L n l) : BoundedPreterm.cast h t = BoundedPreterm.cast h' t

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_rfl {L : Language} {n : ℕ} {h : n ≤ n} {l : ℕ} (t : BoundedPreterm L n l) : BoundedPreterm.cast h t = t

def NFChoice.Fol.BoundedPreterm.castEq {L : Language} {n m l : ℕ} (h : n = m) (t : BoundedPreterm L n l) : BoundedPreterm L m l

Flypitch construction cast_eq, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.BoundedPreterm.castEq h t = NFChoice.Fol.BoundedPreterm.cast ⋯ t

def NFChoice.Fol.BoundedPreterm.cast1 {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) : BoundedPreterm L (n + 1) l

Flypitch construction cast1, retained by the first-order soundness and completeness development.

Equations

• t.cast1 = NFChoice.Fol.BoundedPreterm.cast ⋯ t

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_fst {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} (t : BoundedPreterm L n l) : (BoundedPreterm.cast h t).fst = t.fst

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_eq_fst {L : Language} {n m l : ℕ} (h : n = m) (t : BoundedPreterm L n l) : (BoundedPreterm.castEq h t).fst = t.fst

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast1_fst {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) : t.cast1.fst = t.fst

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_eq_rfl {L : Language} {n m l : ℕ} (h : n = m) (t : BoundedPreterm L n l) : BoundedPreterm.castEq ⋯ (BoundedPreterm.castEq h t) = t

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_eq_irrel {L : Language} {n m l : ℕ} (h h' : n = m) (t : BoundedPreterm L n l) : BoundedPreterm.castEq h t = BoundedPreterm.castEq h' t

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_eq_bd_app {L : Language} {n m : ℕ} (h : n = m) {l : ℕ} {t : BoundedPreterm L n (l + 1)} {s : BoundedPreterm L n 0} : BoundedPreterm.castEq h (t.bd_app s) = (BoundedPreterm.castEq h t).bd_app (BoundedPreterm.castEq h s)

@[simp]

theorem NFChoice.Fol.BoundedPreterm.cast_eq_bd_apps {L : Language} {n m : ℕ} (h : n = m) {l : ℕ} {t : BoundedPreterm L n l} {ts : DVec (boundedTerm L n) l} : BoundedPreterm.castEq h (bdApps t ts) = bdApps (BoundedPreterm.castEq h t) (DVec.map (fun (x : boundedTerm L n) => BoundedPreterm.castEq h x) ts)

@[reducible]

def NFChoice.Fol.closedPreterm.cast0 {L : Language} (n : ℕ) {l : ℕ} (t : closedPreterm L l) : BoundedPreterm L n l

Flypitch construction cast0, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.closedPreterm.cast0 n t = NFChoice.Fol.BoundedPreterm.cast ⋯ t

theorem NFChoice.Fol.closedPreterm.cast0_fst {L : Language} {n l : ℕ} (t : closedPreterm L l) : (closedPreterm.cast0 n t).fst = BoundedPreterm.fst t

@[simp]

theorem NFChoice.Fol.closedPreterm.cast_of_cast0 {L : Language} {n l : ℕ} {t : closedPreterm L l} : closedPreterm.cast0 n t = BoundedPreterm.cast ⋯ t

bounded_term.rec — custom recursion principle

def NFChoice.Fol.boundedTerm.rec {L : Language} {n : ℕ} {C : boundedTerm L n → Sort v} (hvar : (k : Fin n) → C (bd_var k)) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : DVec (boundedTerm L n) l) → ((t : boundedTerm L n) → DVec.pmem t ts → C t) → C (bdApps (bd_func f) ts)) (t : boundedTerm L n) : C t

Custom recursion principle for bounded terms, analogous to term.rec.

Equations

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

def NFChoice.Fol.boundedTerm.rec.go {L : Language} {n : ℕ} {C : boundedTerm L n → Sort v} (hvar : (k : Fin n) → C (bd_var k)) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : DVec (boundedTerm L n) l) → ((t : boundedTerm L n) → DVec.pmem t ts → C t) → C (bdApps (bd_func f) ts)) {l : ℕ} (t : BoundedPreterm L n l) (ts : DVec (boundedTerm L n) l) (ih_ts : (s : boundedTerm L n) → DVec.pmem s ts → C s) : C (bdApps t ts)

Structural recursion accumulator.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.boundedTerm.rec.go hvar hfunc (NFChoice.Fol.bd_var k) ts_1 x_4 = ⋯.mpr (hvar k)
• NFChoice.Fol.boundedTerm.rec.go hvar hfunc (NFChoice.Fol.bd_func f) ts ih_ts = hfunc f ts ih_ts

def NFChoice.Fol.boundedTerm.rec1 {L : Language} {n : ℕ} {C : boundedTerm L (n + 1) → Sort v} (hvar : (k : Fin (n + 1)) → C (bd_var k)) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : DVec (boundedTerm L (n + 1)) l) → ((t : boundedTerm L (n + 1)) → DVec.pmem t ts → C t) → C (bdApps (bd_func f) ts)) (t : boundedTerm L (n + 1)) : C t

Version of bounded_term.rec specialized to n + 1.

Equations

• NFChoice.Fol.boundedTerm.rec1 hvar hfunc = NFChoice.Fol.boundedTerm.rec hvar fun {l : ℕ} => hfunc

Lift and substitution — irrel lemmas

theorem NFChoice.Fol.lift_bounded_term_irrel {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) (n' : ℕ) {m : ℕ} (_h : n ≤ m) : (t.fst ↑' n' # m) = t.fst

theorem NFChoice.Fol.subst_bounded_term_irrel {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) {n' : ℕ} (s : term L) (_h : n ≤ n') : substTerm t.fst s n' = t.fst

realize_bounded_term

def NFChoice.Fol.realizeBoundedTerm {L : Language} {S : Structure L} {n : ℕ} (v : DVec S.carrier n) {l : ℕ} (_t : BoundedPreterm L n l) (_xs : DVec S.carrier l) : S.carrier

Realize a bounded preterm given a valuation vector v : DVec S n and extra args xs : DVec S l.

Equations

• NFChoice.Fol.realizeBoundedTerm v (NFChoice.Fol.bd_var k) x_3 = v.nth ↑k ⋯
• NFChoice.Fol.realizeBoundedTerm v (NFChoice.Fol.bd_func f) x✝ = S.funMap f x✝
• NFChoice.Fol.realizeBoundedTerm v (t₁.bd_app t₂) x✝ = NFChoice.Fol.realizeBoundedTerm v t₁ (NFChoice.DVec.cons (NFChoice.Fol.realizeBoundedTerm v t₂ NFChoice.DVec.nil) x✝)

def NFChoice.Fol.«term_[_;;;_]» : Lean.TrailingParserDescr

Notation for realizing a bounded term with an empty extra argument list.

Equations

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

def NFChoice.Fol.«term_[_;;;_;;;_]» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

@[reducible]

def NFChoice.Fol.realizeClosedTerm {L : Language} (S : Structure L) (t : closedTerm L) : S.carrier

Flypitch construction realize_closed_term, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.realizeClosedTerm S t = NFChoice.Fol.realizeBoundedTerm NFChoice.DVec.nil t NFChoice.DVec.nil

theorem NFChoice.Fol.realize_bounded_term_eq {L : Language} {S : Structure L} {n : ℕ} {v₁ : DVec S.carrier n} {v₂ : ℕ → S.carrier} (hv : ∀ (k : ℕ) (hk : k < n), v₁.nth k hk = v₂ k) {l : ℕ} (t : BoundedPreterm L n l) (xs : DVec S.carrier l) : realizeBoundedTerm v₁ t xs = realizeTerm v₂ t.fst xs

theorem NFChoice.Fol.realize_bounded_term_irrel' {L : Language} {S : Structure L} {n n' : ℕ} {v₁ : DVec S.carrier n} {v₂ : DVec S.carrier n'} (h : ∀ (m : ℕ) (hn : m < n) (hn' : m < n'), v₁.nth m hn = v₂.nth m hn') {l : ℕ} (t : BoundedPreterm L n l) (t' : BoundedPreterm L n' l) (ht : t.fst = t'.fst) (xs : DVec S.carrier l) : realizeBoundedTerm v₁ t xs = realizeBoundedTerm v₂ t' xs

theorem NFChoice.Fol.realize_bounded_term_irrel {L : Language} {S : Structure L} {n : ℕ} {v₁ : DVec S.carrier n} (t : boundedTerm L n) (t' : closedTerm L) (ht : BoundedPreterm.fst t = BoundedPreterm.fst t') : realizeBoundedTerm v₁ t DVec.nil = realizeClosedTerm S t'

@[simp]

theorem NFChoice.Fol.realize_bounded_term_cast_eq_irrel {L : Language} {S : Structure L} {n m l : ℕ} {h : n = m} {v : DVec S.carrier m} {t : BoundedPreterm L n l} (xs : DVec S.carrier l) : realizeBoundedTerm v (BoundedPreterm.castEq h t) xs = realizeBoundedTerm (DVec.cast ⋯ v) t xs

@[simp]

theorem NFChoice.Fol.realize_bounded_term_dvector_cast_irrel {L : Language} {S : Structure L} {n m l : ℕ} {h : n = m} {v : DVec S.carrier n} {t : BoundedPreterm L n l} {xs : DVec S.carrier l} : realizeBoundedTerm (DVec.cast h v) (BoundedPreterm.cast ⋯ t) xs = realizeBoundedTerm v t xs

lift_bounded_term_at — lifting bounded terms

def NFChoice.Fol.liftBoundedTermAt {L : Language} {n l : ℕ} (_t : BoundedPreterm L n l) (n' _m : ℕ) : BoundedPreterm L (n + n') l

Lift a bounded term by inserting n' new variables at position m.

Equations

• (NFChoice.Fol.bd_var k ↑ᵇ' x✝¹ # x✝) = if x✝ ≤ ↑k then NFChoice.Fol.bd_var ⟨↑k + x✝¹, ⋯⟩ else NFChoice.Fol.bd_var ⟨↑k, ⋯⟩
• (NFChoice.Fol.bd_func f ↑ᵇ' x✝¹ # x✝) = NFChoice.Fol.bd_func f
• (t₁.bd_app t₂ ↑ᵇ' x✝¹ # x✝) = (t₁ ↑ᵇ' x✝¹ # x✝).bd_app (t₂ ↑ᵇ' x✝¹ # x✝)

def NFChoice.Fol.«term_↑ᵇ'_#_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

@[reducible]

def NFChoice.Fol.liftBoundedTerm {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) (n' : ℕ) : BoundedPreterm L (n + n') l

Flypitch construction lift_bounded_term, retained by the first-order soundness and completeness development.

Equations

• t ↑ᵇ n' = t ↑ᵇ' n' # 0

def NFChoice.Fol.«term_↑ᵇ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_↑ᵇ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_↑ᵇ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑ᵇ ") (Lean.ParserDescr.cat `term 101))

@[reducible]

def NFChoice.Fol.liftBoundedTerm1 {L : Language} {n' l : ℕ} (t : BoundedPreterm L n' l) : BoundedPreterm L (n' + 1) l

Flypitch construction lift_bounded_term1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.liftBoundedTerm1 t = t ↑ᵇ 1

@[simp]

theorem NFChoice.Fol.lift_bounded_term_fst {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) (n' m : ℕ) : (t ↑ᵇ' n' # m).fst = t.fst ↑' n' # m

subst_bounded_term — substitution in bounded terms

def NFChoice.Fol.substBoundedTerm {L : Language} {n n' l : ℕ} (_t : BoundedPreterm L (n + n' + 1) l) (_s : boundedTerm L n') : BoundedPreterm L (n + n') l

Substitute the variable at position n (within the bound `n

• n' + 1) with a bounded term s`.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.substBoundedTerm (NFChoice.Fol.bd_func f) x✝ = NFChoice.Fol.bd_func f
• NFChoice.Fol.substBoundedTerm (t₁.bd_app t₂) x✝ = (NFChoice.Fol.substBoundedTerm t₁ x✝).bd_app (NFChoice.Fol.substBoundedTerm t₂ x✝)

def NFChoice.Fol.«term_[_///_]» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

theorem NFChoice.Fol.subst_bounded_term_var_lt {L : Language} {n n' : ℕ} (s : boundedTerm L n') (k : Fin (n + n' + 1)) (h : ↑k < n) : (substBoundedTerm (bd_var k) s).fst = &↑k

theorem NFChoice.Fol.subst_bounded_term_var_gt {L : Language} {n n' : ℕ} (s : boundedTerm L n') (k : Fin (n + n' + 1)) (h : n < ↑k) : (substBoundedTerm (bd_var k) s).fst = &(↑k - 1)

theorem NFChoice.Fol.subst_bounded_term_var_eq {L : Language} {n n' : ℕ} (s : boundedTerm L n') (k : Fin (n + n' + 1)) (h : ↑k = n) : (substBoundedTerm (bd_var k) s).fst = BoundedPreterm.fst s ↑' n # 0

@[simp]

theorem NFChoice.Fol.subst_bounded_term_bd_app {L : Language} {n n' l : ℕ} (t₁ : BoundedPreterm L (n + n' + 1) (l + 1)) (t₂ : boundedTerm L (n + n' + 1)) (s : boundedTerm L n') : substBoundedTerm (t₁.bd_app t₂) s = (substBoundedTerm t₁ s).bd_app (substBoundedTerm t₂ s)

@[simp]

theorem NFChoice.Fol.subst_bounded_term_fst {L : Language} {n n' l : ℕ} (t : BoundedPreterm L (n + n' + 1) l) (s : boundedTerm L n') : (substBoundedTerm t s).fst = substTerm t.fst (BoundedPreterm.fst s) n

def NFChoice.Fol.subst0BoundedTerm {L : Language} {n l : ℕ} (t : BoundedPreterm L (n + 1) l) (s : boundedTerm L n) : BoundedPreterm L n l

Substitute the last (max) variable with a closed term.

Equations

• NFChoice.Fol.subst0BoundedTerm t s = NFChoice.Fol.BoundedPreterm.castEq ⋯ (NFChoice.Fol.substBoundedTerm (NFChoice.Fol.BoundedPreterm.castEq ⋯ t) s)

@[simp]

theorem NFChoice.Fol.subst0_bounded_term_fst {L : Language} {n l : ℕ} (t : BoundedPreterm L (n + 1) l) (s : boundedTerm L n) : (subst0BoundedTerm t s).fst = substTerm t.fst (BoundedPreterm.fst s) 0

def NFChoice.Fol.substmaxBoundedTerm {L : Language} {n l : ℕ} (t : BoundedPreterm L (n + 1) l) (s : closedTerm L) : BoundedPreterm L n l

Substitute the last (max) variable with a closed term.

Equations

• NFChoice.Fol.substmaxBoundedTerm t s = NFChoice.Fol.substBoundedTerm t s

@[simp]

theorem NFChoice.Fol.substmax_bounded_term_bd_app {L : Language} {n l : ℕ} (t₁ : BoundedPreterm L (n + 1) (l + 1)) (t₂ : boundedTerm L (n + 1)) (s : closedTerm L) : substmaxBoundedTerm (t₁.bd_app t₂) s = (substmaxBoundedTerm t₁ s).bd_app (substmaxBoundedTerm t₂ s)

theorem NFChoice.Fol.substmax_eq_subst0_term {L : Language} {l : ℕ} (t : BoundedPreterm L 1 l) (s : closedTerm L) : subst0BoundedTerm t s = substmaxBoundedTerm t s

theorem NFChoice.Fol.substmax_var_lt {L : Language} {n : ℕ} (k : Fin (n + 1)) (s : closedTerm L) (h : ↑k < n) : substmaxBoundedTerm (bd_var k) s = bd_var ⟨↑k, h⟩

theorem NFChoice.Fol.substmax_var_eq {L : Language} {n : ℕ} (k : Fin (n + 1)) (s : closedTerm L) (h : ↑k = n) : substmaxBoundedTerm (bd_var k) s = closedPreterm.cast0 n s

def NFChoice.Fol.boundedTermOfFunction {L : Language} {l n : ℕ} (f : L.functions l) : Arity' (boundedTerm L n) (boundedTerm L n) l

Flypitch construction bounded_term_of_function, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.boundedTermOfFunction f = NFChoice.Arity'.ofDvectorMap (NFChoice.Fol.bdApps (NFChoice.Fol.bd_func f))

realize_bounded_term lemmas

@[simp]

theorem NFChoice.Fol.realize_bounded_term_bd_app {L : Language} {S : Structure L} {n l : ℕ} (t : BoundedPreterm L n (l + 1)) (s : boundedTerm L n) (xs : DVec S.carrier n) (xs' : DVec S.carrier l) : realizeBoundedTerm xs (t.bd_app s) xs' = realizeBoundedTerm xs t (DVec.cons (realizeBoundedTerm xs s DVec.nil) xs')

@[simp]

theorem NFChoice.Fol.realize_closed_term_bd_apps {L : Language} {S : Structure L} {l : ℕ} (t : closedPreterm L l) (ts : DVec (closedTerm L) l) : realizeClosedTerm S (bdApps t ts) = realizeBoundedTerm DVec.nil t (DVec.map (fun (t' : BoundedPreterm L 0 0) => realizeBoundedTerm DVec.nil t' DVec.nil) ts)

theorem NFChoice.Fol.realize_bounded_term_bd_apps {L : Language} {S : Structure L} {n l : ℕ} (xs : DVec S.carrier n) (t : BoundedPreterm L n l) (ts : DVec (boundedTerm L n) l) : realizeBoundedTerm xs (bdApps t ts) DVec.nil = realizeBoundedTerm xs t (DVec.map (fun (t : BoundedPreterm L n 0) => realizeBoundedTerm xs t DVec.nil) ts)

@[simp]

theorem NFChoice.Fol.realize_cast_bounded_term {L : Language} {S : Structure L} {n m : ℕ} {h : n ≤ m} {t : boundedTerm L n} {v : DVec S.carrier m} : realizeBoundedTerm v (BoundedPreterm.cast h t) DVec.nil = realizeBoundedTerm (DVec.trunc n h v) t DVec.nil

theorem NFChoice.Fol.realize_closed_term_v_irrel {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {t : boundedTerm L 0} : realizeBoundedTerm v (BoundedPreterm.cast ⋯ t) DVec.nil = realizeClosedTerm S t

When realizing a closed term, the realizing dvector is irrelevant.

bounded_preformula, bounded_formula, presentence, sentence

(src/fol.lean lines 1660-2200)

inductive NFChoice.Fol.BoundedPreformula (L : Language) : ℕ → ℕ → Type u

A bounded pre-formula: bounded_preformula L n l is a partially applied formula with at most n free de Bruijn variables (< n), needing l more term arguments. bounded_formula L n = bounded_preformula L n 0, and sentence L = bounded_preformula L 0 0.

• bd_falsum {L : Language} {n : ℕ} : BoundedPreformula L n 0
• bd_equal {L : Language} {n : ℕ} (_t₁ _t₂ : boundedTerm L n) : BoundedPreformula L n 0
• bd_rel {L : Language} {n l : ℕ} (_R : L.relations l) : BoundedPreformula L n l
• bd_apprel {L : Language} {n l : ℕ} (_f : BoundedPreformula L n (l + 1)) (_t : boundedTerm L n) : BoundedPreformula L n l
• bd_imp {L : Language} {n : ℕ} (_f₁ _f₂ : BoundedPreformula L n 0) : BoundedPreformula L n 0
• bd_all {L : Language} {n : ℕ} (_f : BoundedPreformula L (n + 1) 0) : BoundedPreformula L n 0

@[reducible]

def NFChoice.Fol.boundedFormula (L : Language) (n : ℕ) : Type u

Flypitch construction bounded_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.boundedFormula L n = NFChoice.Fol.BoundedPreformula L n 0

@[reducible]

def NFChoice.Fol.presentence (L : Language) (l : ℕ) : Type u

Flypitch construction presentence, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.presentence L l = NFChoice.Fol.BoundedPreformula L 0 l

@[reducible]

def NFChoice.Fol.sentence (L : Language) : Type u

Flypitch construction sentence, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.sentence L = NFChoice.Fol.presentence L 0

instance NFChoice.Fol.nonempty_bounded_formula {L : Language} (n : ℕ) : Nonempty (boundedFormula L n)

bounded_preformula notations

def NFChoice.Fol.bdNot {L : Language} {n : ℕ} (f : boundedFormula L n) : boundedFormula L n

Flypitch construction bd_not, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdNot f = NFChoice.Fol.bd_imp f NFChoice.Fol.bd_falsum

def NFChoice.Fol.«term∼ᵇ_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.bdAnd {L : Language} {n : ℕ} (f₁ f₂ : boundedFormula L n) : boundedFormula L n

Flypitch construction bd_and, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdAnd f₁ f₂ = NFChoice.Fol.bdNot (NFChoice.Fol.bd_imp f₁ (NFChoice.Fol.bdNot f₂))

def NFChoice.Fol.«term_⊓ᵇ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊓ᵇ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊓ᵇ_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ᵇ ") (Lean.ParserDescr.cat `term 69))

def NFChoice.Fol.bdOr {L : Language} {n : ℕ} (f₁ f₂ : boundedFormula L n) : boundedFormula L n

Flypitch construction bd_or, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdOr f₁ f₂ = NFChoice.Fol.bd_imp (NFChoice.Fol.bdNot f₁) f₂

def NFChoice.Fol.«term_⊔ᵇ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊔ᵇ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊔ᵇ_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ᵇ ") (Lean.ParserDescr.cat `term 68))

def NFChoice.Fol.bdBiimp {L : Language} {n : ℕ} (f₁ f₂ : boundedFormula L n) : boundedFormula L n

Flypitch construction bd_biimp, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdBiimp f₁ f₂ = NFChoice.Fol.bdAnd (NFChoice.Fol.bd_imp f₁ f₂) (NFChoice.Fol.bd_imp f₂ f₁)

def NFChoice.Fol.«term_⇔ᵇ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.Fol.bdEx {L : Language} {n : ℕ} (f : boundedFormula L (n + 1)) : boundedFormula L n

Flypitch construction bd_ex, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdEx f = NFChoice.Fol.bdNot (NFChoice.Fol.bd_all (NFChoice.Fol.bdNot f))

def NFChoice.Fol.«term∃ᵇ_» : Lean.ParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

bd_apps_rel

def NFChoice.Fol.bdAppsRel {L : Language} {n l : ℕ} (_f : BoundedPreformula L n l) (_ts : DVec (boundedTerm L n) l) : boundedFormula L n

Flypitch construction bd_apps_rel, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.bdAppsRel f NFChoice.DVec.nil = f
• NFChoice.Fol.bdAppsRel f (NFChoice.DVec.cons t ts) = NFChoice.Fol.bdAppsRel (f.bd_apprel t) ts

@[simp]

theorem NFChoice.Fol.bd_apps_rel_zero {L : Language} {n : ℕ} (f : boundedFormula L n) (ts : DVec (boundedTerm L n) 0) : bdAppsRel f ts = f

namespace bounded_preformula

def NFChoice.Fol.BoundedPreformula.fst {L : Language} {n l : ℕ} : BoundedPreformula L n l → preformula l

Forget boundedness: map a bounded_preformula to an ordinary preformula.

Equations

• NFChoice.Fol.bd_falsum.fst = ⊥'
• (NFChoice.Fol.bd_equal t₁ t₂).fst = NFChoice.Fol.preformula.equal (NFChoice.Fol.BoundedPreterm.fst t₁) (NFChoice.Fol.BoundedPreterm.fst t₂)
• (NFChoice.Fol.bd_rel R).fst = NFChoice.Fol.preformula.rel R
• (f.bd_apprel t).fst = f.fst.apprel (NFChoice.Fol.BoundedPreterm.fst t)
• (f₁.bd_imp f₂).fst = f₁.fst.imp f₂.fst
• f.bd_all.fst = f.fst.all

@[simp]

theorem NFChoice.Fol.BoundedPreformula.fst_bd_not {L : Language} {n : ℕ} {f : boundedFormula L n} : BoundedPreformula.fst (bdNot f) = not' (BoundedPreformula.fst f)

@[simp]

theorem NFChoice.Fol.BoundedPreformula.fst_bd_or {L : Language} {n : ℕ} {f₁ f₂ : boundedFormula L n} : BoundedPreformula.fst (bdOr f₁ f₂) = or' (BoundedPreformula.fst f₁) (BoundedPreformula.fst f₂)

theorem NFChoice.Fol.BoundedPreformula.fst_bd_imp {L : Language} {n : ℕ} {f₁ f₂ : boundedFormula L n} : (bd_imp f₁ f₂).fst = (BoundedPreformula.fst f₁).imp (BoundedPreformula.fst f₂)

@[simp]

theorem NFChoice.Fol.BoundedPreformula.fst_bd_and {L : Language} {n : ℕ} {f₁ f₂ : boundedFormula L n} : BoundedPreformula.fst (bdAnd f₁ f₂) = and' (BoundedPreformula.fst f₁) (BoundedPreformula.fst f₂)

@[simp]

theorem NFChoice.Fol.BoundedPreformula.fst_bd_ex {L : Language} {n : ℕ} {f : boundedFormula L (n + 1)} : BoundedPreformula.fst (bdEx f) = ex' (BoundedPreformula.fst f)

theorem NFChoice.Fol.BoundedPreformula.eq {L : Language} {n l : ℕ} {f₁ f₂ : BoundedPreformula L n l} : f₁.fst = f₂.fst → f₁ = f₂

Equality of bounded_preformulas is determined by their underlying preformulas.

theorem NFChoice.Fol.BoundedPreformula.eq_iff {L : Language} {n l : ℕ} {f₁ f₂ : BoundedPreformula L n l} : f₁ = f₂ ↔ f₁.fst = f₂.fst

def NFChoice.Fol.BoundedPreformula.cast {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} : BoundedPreformula L n l → BoundedPreformula L m l

Cast a bounded_preformula to one with a larger variable bound.

Equations

• NFChoice.Fol.BoundedPreformula.cast h NFChoice.Fol.bd_falsum = NFChoice.Fol.bd_falsum
• NFChoice.Fol.BoundedPreformula.cast h (NFChoice.Fol.bd_equal t₁ t₂) = NFChoice.Fol.bd_equal (NFChoice.Fol.BoundedPreterm.cast h t₁) (NFChoice.Fol.BoundedPreterm.cast h t₂)
• NFChoice.Fol.BoundedPreformula.cast h (NFChoice.Fol.bd_rel R) = NFChoice.Fol.bd_rel R
• NFChoice.Fol.BoundedPreformula.cast h (f.bd_apprel t) = (NFChoice.Fol.BoundedPreformula.cast h f).bd_apprel (NFChoice.Fol.BoundedPreterm.cast h t)
• NFChoice.Fol.BoundedPreformula.cast h (f₁.bd_imp f₂) = (NFChoice.Fol.BoundedPreformula.cast h f₁).bd_imp (NFChoice.Fol.BoundedPreformula.cast h f₂)
• NFChoice.Fol.BoundedPreformula.cast h f.bd_all = (NFChoice.Fol.BoundedPreformula.cast ⋯ f).bd_all

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_irrel {L : Language} {n m l : ℕ} (h h' : n ≤ m) (f : BoundedPreformula L n l) : BoundedPreformula.cast h f = BoundedPreformula.cast h' f

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_rfl {L : Language} {n : ℕ} {h : n ≤ n} {l : ℕ} (f : BoundedPreformula L n l) : BoundedPreformula.cast h f = f

def NFChoice.Fol.BoundedPreformula.castEq {L : Language} {n m l : ℕ} (h : n = m) (f : BoundedPreformula L n l) : BoundedPreformula L m l

Flypitch construction cast_eq, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.BoundedPreformula.castEq h f = NFChoice.Fol.BoundedPreformula.cast ⋯ f

def NFChoice.Fol.BoundedPreformula.castEqr {L : Language} {n m l : ℕ} (h : n = m) (f : BoundedPreformula L m l) : BoundedPreformula L n l

Flypitch construction cast_eqr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.BoundedPreformula.castEqr h f = NFChoice.Fol.BoundedPreformula.cast ⋯ f

theorem NFChoice.Fol.BoundedPreformula.cast_bd_apps_rel {L : Language} {n m : ℕ} (h : n ≤ m) {l : ℕ} (f : BoundedPreformula L n l) (ts : DVec (boundedTerm L n) l) : BoundedPreformula.cast h (bdAppsRel f ts) = bdAppsRel (BoundedPreformula.cast h f) (DVec.map (fun (t : boundedTerm L n) => BoundedPreterm.cast h t) ts)

def NFChoice.Fol.BoundedPreformula.cast1 {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) : BoundedPreformula L (n + 1) l

Flypitch construction cast1, retained by the first-order soundness and completeness development.

Equations

• f.cast1 = NFChoice.Fol.BoundedPreformula.cast ⋯ f

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_fst {L : Language} {l n m : ℕ} (h : n ≤ m) (f : BoundedPreformula L n l) : (BoundedPreformula.cast h f).fst = f.fst

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_eq_fst {L : Language} {l n m : ℕ} (h : n = m) (f : BoundedPreformula L n l) : (BoundedPreformula.castEq h f).fst = f.fst

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast1_fst {L : Language} {l n : ℕ} (f : BoundedPreformula L n l) : f.cast1.fst = f.fst

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_eq_rfl {L : Language} {l n m : ℕ} (h : n = m) (f : BoundedPreformula L n l) : BoundedPreformula.castEq ⋯ (BoundedPreformula.castEq h f) = f

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_eq_irrel {L : Language} {l n m : ℕ} (h h' : n = m) (f : BoundedPreformula L n l) : BoundedPreformula.castEq h f = BoundedPreformula.castEq h' f

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_eq_all {L : Language} {n m : ℕ} (h : n = m) {f : BoundedPreformula L (n + 1) 0} : BoundedPreformula.castEq h f.bd_all = (BoundedPreformula.castEq ⋯ f).bd_all

@[simp]

theorem NFChoice.Fol.BoundedPreformula.cast_eq_trans {L : Language} {n m o l : ℕ} {h : n = m} {h' : m = o} {f : BoundedPreformula L n l} : BoundedPreformula.castEq h' (BoundedPreformula.castEq h f) = BoundedPreformula.castEq ⋯ f

theorem NFChoice.Fol.BoundedPreformula.cast_eq_hrfl {L : Language} {n m l : ℕ} {h : n = m} {f : BoundedPreformula L n l} : BoundedPreformula.castEq h f ≍ f

def NFChoice.Fol.BoundedPreformula.quantifierFree {L : Language} {l n : ℕ} (f : BoundedPreformula L n l) : Prop

A bounded_preformula is quantifier-free if its underlying preformula is.

Equations

• f.quantifierFree = NFChoice.Fol.quantifierFree f.fst

namespace presentence

@[reducible]

def NFChoice.Fol.presentence.cast0 {L : Language} {l : ℕ} (n : ℕ) (f : presentence L l) : BoundedPreformula L n l

Flypitch construction cast0, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.presentence.cast0 n f = NFChoice.Fol.BoundedPreformula.cast ⋯ f

theorem NFChoice.Fol.presentence.cast0_fst {L : Language} {l : ℕ} (n : ℕ) (f : presentence L l) : (presentence.cast0 n f).fst = BoundedPreformula.fst f

Irrel lemmas for bounded formulas

theorem NFChoice.Fol.lift_bounded_formula_irrel {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) (n' : ℕ) {m : ℕ} (_h : n ≤ m) : (f.fst ↑f' n' # m) = f.fst

theorem NFChoice.Fol.lift_sentence_irrel {L : Language} (f : sentence L) : BoundedPreformula.fst f ↑f 1 = BoundedPreformula.fst f

@[simp]

theorem NFChoice.Fol.subst_bounded_formula_irrel {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) {n' : ℕ} (s : term L) (_h : n ≤ n') : f.fst [s // n']f = f.fst

theorem NFChoice.Fol.subst_sentence_irrel {L : Language} (f : sentence L) (n : ℕ) (s : term L) : BoundedPreformula.fst f [s // n]f = BoundedPreformula.fst f

realize_bounded_formula

def NFChoice.Fol.realizeBoundedFormula {L : Language} {S : Structure L} {n l : ℕ} (_v : DVec S.carrier n) (_f : BoundedPreformula L n l) (_xs : DVec S.carrier l) : Prop

Flypitch construction realize_bounded_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.realizeBoundedFormula x✝ NFChoice.Fol.bd_falsum x_6 = False
• NFChoice.Fol.realizeBoundedFormula x✝ (NFChoice.Fol.bd_equal t₁ t₂) x_6 = (NFChoice.Fol.realizeBoundedTerm x✝ t₁ NFChoice.DVec.nil = NFChoice.Fol.realizeBoundedTerm x✝ t₂ NFChoice.DVec.nil)
• NFChoice.Fol.realizeBoundedFormula x✝¹ (NFChoice.Fol.bd_rel R) x✝ = S.relMap R x✝
• NFChoice.Fol.realizeBoundedFormula x✝¹ (f.bd_apprel t) x✝ = NFChoice.Fol.realizeBoundedFormula x✝¹ f (NFChoice.DVec.cons (NFChoice.Fol.realizeBoundedTerm x✝¹ t NFChoice.DVec.nil) x✝)
• NFChoice.Fol.realizeBoundedFormula x✝ (f₁.bd_imp f₂) xs = (NFChoice.Fol.realizeBoundedFormula x✝ f₁ xs → NFChoice.Fol.realizeBoundedFormula x✝ f₂ xs)
• NFChoice.Fol.realizeBoundedFormula x✝ f.bd_all xs = ∀ (x : S.carrier), NFChoice.Fol.realizeBoundedFormula (NFChoice.DVec.cons x x✝) f xs

@[reducible]

def NFChoice.Fol.realizeSentence {L : Language} (S : Structure L) (f : sentence L) : Prop

Flypitch construction realize_sentence, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.realizeSentence S f = NFChoice.Fol.realizeBoundedFormula NFChoice.DVec.nil f NFChoice.DVec.nil

def NFChoice.Fol.«term_⊨ₘ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊨ₘ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊨ₘ_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ₘ ") (Lean.ParserDescr.cat `term 52))

realize_bounded_formula lemmas

theorem NFChoice.Fol.realize_bounded_formula_iff_aux {L : Language} {S : Structure L} {n l : ℕ} (f : BoundedPreformula L n l) (v₁ : DVec S.carrier n) (v₂ : ℕ → S.carrier) (_hv : ∀ (k : ℕ) (hk : k < n), v₁.nth k hk = v₂ k) (xs : DVec S.carrier l) : realizeBoundedFormula v₁ f xs ↔ realizeFormula v₂ f.fst xs

theorem NFChoice.Fol.realize_bounded_formula_iff {L : Language} {S : Structure L} {n : ℕ} {v₁ : DVec S.carrier n} {v₂ : ℕ → S.carrier} (hv : ∀ (k : ℕ) (hk : k < n), v₁.nth k hk = v₂ k) {l : ℕ} (f : BoundedPreformula L n l) (xs : DVec S.carrier l) : realizeBoundedFormula v₁ f xs ↔ realizeFormula v₂ f.fst xs

theorem NFChoice.Fol.realize_bounded_formula_iff_of_fst {L : Language} {S : Structure L} {n : ℕ} {v₁ w₁ : DVec S.carrier n} {v₂ w₂ : ℕ → S.carrier} (hv₁ : ∀ (k : ℕ) (hk : k < n), v₁.nth k hk = v₂ k) (hw₁ : ∀ (k : ℕ) (hk : k < n), w₁.nth k hk = w₂ k) {l₁ l₂ : ℕ} (t₁ : BoundedPreformula L n l₁) (t₂ : BoundedPreformula L n l₂) (xs₁ : DVec S.carrier l₁) (xs₂ : DVec S.carrier l₂) (H : realizeFormula v₂ t₁.fst xs₁ ↔ realizeFormula w₂ t₂.fst xs₂) : realizeBoundedFormula v₁ t₁ xs₁ ↔ realizeBoundedFormula w₁ t₂ xs₂

theorem NFChoice.Fol.realize_bounded_formula_irrel' {L : Language} {S : Structure L} {n n' : ℕ} {v₁ : DVec S.carrier n} {v₂ : DVec S.carrier n'} (h : ∀ (m : ℕ) (hn : m < n) (hn' : m < n'), v₁.nth m hn = v₂.nth m hn') {l : ℕ} (f : BoundedPreformula L n l) (f' : BoundedPreformula L n' l) (hf : f.fst = f'.fst) (xs : DVec S.carrier l) : realizeBoundedFormula v₁ f xs ↔ realizeBoundedFormula v₂ f' xs

theorem NFChoice.Fol.realize_bounded_formula_irrel {L : Language} {S : Structure L} {n : ℕ} {v₁ : DVec S.carrier n} (f : boundedFormula L n) (f' : sentence L) (hf : BoundedPreformula.fst f = BoundedPreformula.fst f') (xs : DVec S.carrier 0) : realizeBoundedFormula v₁ f xs ↔ realizeSentence S f'

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_cast_eq_irrel {L : Language} {S : Structure L} {n m l : ℕ} {h : n = m} {v : DVec S.carrier m} {f : BoundedPreformula L n l} {xs : DVec S.carrier l} : realizeBoundedFormula v (BoundedPreformula.castEq h f) xs = realizeBoundedFormula (DVec.cast ⋯ v) f xs

bounded_formula_of_relation

def NFChoice.Fol.boundedFormulaOfRelation {L : Language} {l n : ℕ} (R : L.relations l) : Arity' (boundedTerm L n) (boundedFormula L n) l

Flypitch construction bounded_formula_of_relation, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.boundedFormulaOfRelation R = NFChoice.Arity'.ofDvectorMap (NFChoice.Fol.bdAppsRel (NFChoice.Fol.bd_rel R))

Recursors for bounded_preformula / bounded_formula

(src/fol.lean lines 1984-2038)

def NFChoice.Fol.BoundedPreformula.rec1 {L : Language} {C : (n l : ℕ) → BoundedPreformula L (n + 1) l → Sort v} (H0 : {n : ℕ} → C n 0 bd_falsum) (H1 : {n : ℕ} → (t₁ t₂ : boundedTerm L (n + 1)) → C n 0 (bd_equal t₁ t₂)) (H2 : {n l : ℕ} → (R : L.relations l) → C n l (bd_rel R)) (H3 : {n l : ℕ} → (f : BoundedPreformula L (n + 1) (l + 1)) → (t : boundedTerm L (n + 1)) → C n (l + 1) f → C n l (f.bd_apprel t)) (H4 : {n : ℕ} → (f₁ f₂ : boundedFormula L (n + 1)) → C n 0 f₁ → C n 0 f₂ → C n 0 (bd_imp f₁ f₂)) (H5 : {n : ℕ} → (f : boundedFormula L (n + 2)) → C (n + 1) 0 f → C n 0 (bd_all f)) ⦃n l : ℕ⦄ (f : BoundedPreformula L (n + 1) l) : C n l f

Recursor for bounded_preformula at n+1 (i.e., where there is at least one free variable).

Equations

• NFChoice.Fol.BoundedPreformula.rec1 H0 H1 H2 H3 H4 H5 = fun ⦃n _l : ℕ⦄ (f : NFChoice.Fol.BoundedPreformula L (n + 1) _l) => NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 (n + 1) _l f

def NFChoice.Fol.BoundedPreformula.rec1.key {L : Language} {C : (n l : ℕ) → BoundedPreformula L (n + 1) l → Sort v} (H0 : {n : ℕ} → C n 0 bd_falsum) (H1 : {n : ℕ} → (t₁ t₂ : boundedTerm L (n + 1)) → C n 0 (bd_equal t₁ t₂)) (H2 : {n l : ℕ} → (R : L.relations l) → C n l (bd_rel R)) (H3 : {n l : ℕ} → (f : BoundedPreformula L (n + 1) (l + 1)) → (t : boundedTerm L (n + 1)) → C n (l + 1) f → C n l (f.bd_apprel t)) (H4 : {n : ℕ} → (f₁ f₂ : boundedFormula L (n + 1)) → C n 0 f₁ → C n 0 f₂ → C n 0 (bd_imp f₁ f₂)) (H5 : {n : ℕ} → (f : boundedFormula L (n + 2)) → C (n + 1) 0 f → C n 0 (bd_all f)) (n l : ℕ) (f : BoundedPreformula L n l) : have C' := fun (n : ℕ) => match (motive := (n l : ℕ) → BoundedPreformula L n l → Sort v) n with | 0 => fun (_l : ℕ) (_f : BoundedPreformula L 0 _l) => PUnit.{v} | k.succ => C k; C' n l f

Recursive extension of the positive-arity motive.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 0 l f = PUnit.unit
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 n_1.succ 0 NFChoice.Fol.bd_falsum = H0
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 n_1.succ 0 (NFChoice.Fol.bd_equal t₁ t₂) = H1 t₁ t₂
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 n_1.succ l (NFChoice.Fol.bd_rel R) = H2 R
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 n_1.succ l (f_1.bd_apprel t) = H3 f_1 t (NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 (n_1 + 1) (l + 1) f_1)
• NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 n_1.succ 0 f_1.bd_all = H5 f_1 (NFChoice.Fol.BoundedPreformula.rec1.key H0 H1 H2 H3 H4 H5 (n_1 + 2) 0 f_1)

def NFChoice.Fol.boundedFormula.rec1 {L : Language} {C : (n : ℕ) → boundedFormula L (n + 1) → Sort v} (hfalsum : {n : ℕ} → C n bd_falsum) (hequal : {n : ℕ} → (t₁ t₂ : boundedTerm L (n + 1)) → C n (bd_equal t₁ t₂)) (hrel : {n l : ℕ} → (R : L.relations l) → (ts : DVec (boundedTerm L (n + 1)) l) → C n (bdAppsRel (bd_rel R) ts)) (himp : {n : ℕ} → {f₁ f₂ : boundedFormula L (n + 1)} → C n f₁ → C n f₂ → C n (bd_imp f₁ f₂)) (hall : {n : ℕ} → {f : boundedFormula L (n + 2)} → C (n + 1) f → C n (bd_all f)) ⦃n : ℕ⦄ (f : boundedFormula L (n + 1)) : C n f

Recursor for bounded_formula at n+1 (fully applied).

Equations

• NFChoice.Fol.boundedFormula.rec1 hfalsum hequal hrel himp hall f = ⋯ ▸ NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall f NFChoice.DVec.nil

@[irreducible]

def NFChoice.Fol.boundedFormula.rec1.go {L : Language} {C : (n : ℕ) → boundedFormula L (n + 1) → Sort v} (hfalsum : {n : ℕ} → C n bd_falsum) (hequal : {n : ℕ} → (t₁ t₂ : boundedTerm L (n + 1)) → C n (bd_equal t₁ t₂)) (hrel : {n l : ℕ} → (R : L.relations l) → (ts : DVec (boundedTerm L (n + 1)) l) → C n (bdAppsRel (bd_rel R) ts)) (himp : {n : ℕ} → {f₁ f₂ : boundedFormula L (n + 1)} → C n f₁ → C n f₂ → C n (bd_imp f₁ f₂)) (hall : {n : ℕ} → {f : boundedFormula L (n + 2)} → C (n + 1) f → C n (bd_all f)) {n' l : ℕ} (f' : BoundedPreformula L (n' + 1) l) (ts : DVec (boundedTerm L (n' + 1)) l) : C n' (bdAppsRel f' ts)

Structural recursion accumulator.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall NFChoice.Fol.bd_falsum ts_1 = ⋯.mpr hfalsum
• NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall (NFChoice.Fol.bd_equal t₁ t₂) ts_1 = ⋯.mpr (hequal t₁ t₂)
• NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall (NFChoice.Fol.bd_rel R) ts = hrel R ts
• NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall (f'_1.bd_apprel t) ts = NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall f'_1 (NFChoice.DVec.cons t ts)
• NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall f'_1.bd_all ts_1 = ⋯.mpr (hall (NFChoice.Fol.boundedFormula.rec1.go hfalsum hequal hrel himp hall f'_1 NFChoice.DVec.nil))

def NFChoice.Fol.boundedFormula.rec {L : Language} {C : (n : ℕ) → boundedFormula L n → Sort v} (hfalsum : {n : ℕ} → C n bd_falsum) (hequal : {n : ℕ} → (t₁ t₂ : boundedTerm L n) → C n (bd_equal t₁ t₂)) (hrel : {n l : ℕ} → (R : L.relations l) → (ts : DVec (boundedTerm L n) l) → C n (bdAppsRel (bd_rel R) ts)) (himp : {n : ℕ} → {f₁ f₂ : boundedFormula L n} → C n f₁ → C n f₂ → C n (bd_imp f₁ f₂)) (hall : {n : ℕ} → {f : boundedFormula L (n + 1)} → C (n + 1) f → C n (bd_all f)) ⦃n : ℕ⦄ (f : boundedFormula L n) : C n f

Recursor for bounded_formula at any n.

Equations

• NFChoice.Fol.boundedFormula.rec hfalsum hequal hrel himp hall f = ⋯ ▸ NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall f NFChoice.DVec.nil

def NFChoice.Fol.boundedFormula.rec.go {L : Language} {C : (n : ℕ) → boundedFormula L n → Sort v} (hfalsum : {n : ℕ} → C n bd_falsum) (hequal : {n : ℕ} → (t₁ t₂ : boundedTerm L n) → C n (bd_equal t₁ t₂)) (hrel : {n l : ℕ} → (R : L.relations l) → (ts : DVec (boundedTerm L n) l) → C n (bdAppsRel (bd_rel R) ts)) (himp : {n : ℕ} → {f₁ f₂ : boundedFormula L n} → C n f₁ → C n f₂ → C n (bd_imp f₁ f₂)) (hall : {n : ℕ} → {f : boundedFormula L (n + 1)} → C (n + 1) f → C n (bd_all f)) {n l : ℕ} (f : BoundedPreformula L n l) (ts : DVec (boundedTerm L n) l) : C n (bdAppsRel f ts)

Structural recursion accumulator.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall NFChoice.Fol.bd_falsum ts_1 = ⋯.mpr hfalsum
• NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall (NFChoice.Fol.bd_equal t₁ t₂) ts_1 = ⋯.mpr (hequal t₁ t₂)
• NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall (NFChoice.Fol.bd_rel R) ts = hrel R ts
• NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall (f_1.bd_apprel t) ts = NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall f_1 (NFChoice.DVec.cons t ts)
• NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall f_1.bd_all ts_1 = ⋯.mpr (hall (NFChoice.Fol.boundedFormula.rec.go hfalsum hequal hrel himp hall f_1 NFChoice.DVec.nil))

substmax_bounded_formula — substitute the max (last)

variable

def NFChoice.Fol.substBoundedFormula {L : Language} {n n' n'' l : ℕ} (_f : BoundedPreformula L n'' l) (_s : boundedTerm L n') (_h : n + n' + 1 = n'') : BoundedPreformula L (n + n') l

Substitute variable at position n in a formula with bound n+1.

Equations

• NFChoice.Fol.substBoundedFormula NFChoice.Fol.bd_falsum x✝¹ x✝ = NFChoice.Fol.bd_falsum
• NFChoice.Fol.substBoundedFormula (NFChoice.Fol.bd_equal t₁ t₂) x✝ ⋯ = NFChoice.Fol.bd_equal (NFChoice.Fol.substBoundedTerm t₁ x✝) (NFChoice.Fol.substBoundedTerm t₂ x✝)
• NFChoice.Fol.substBoundedFormula (NFChoice.Fol.bd_rel R) x✝¹ x✝ = NFChoice.Fol.bd_rel R
• NFChoice.Fol.substBoundedFormula (f.bd_apprel t) x✝ ⋯ = (NFChoice.Fol.substBoundedFormula f x✝ ⋯).bd_apprel (NFChoice.Fol.substBoundedTerm t x✝)
• NFChoice.Fol.substBoundedFormula (f₁.bd_imp f₂) x✝ ⋯ = (NFChoice.Fol.substBoundedFormula f₁ x✝ ⋯).bd_imp (NFChoice.Fol.substBoundedFormula f₂ x✝ ⋯)
• NFChoice.Fol.substBoundedFormula f.bd_all x✝ ⋯ = (NFChoice.Fol.BoundedPreformula.castEq ⋯ (NFChoice.Fol.substBoundedFormula f x✝ ⋯)).bd_all

@[simp]

theorem NFChoice.Fol.subst_bounded_formula_fst {L : Language} {n n' n'' l : ℕ} (f : BoundedPreformula L n'' l) (s : boundedTerm L n') (h : n + n' + 1 = n'') : (substBoundedFormula f s h).fst = f.fst [BoundedPreterm.fst s // n]f

def NFChoice.Fol.substmaxBoundedFormula {L : Language} {n l : ℕ} (f : BoundedPreformula L (n + 1) l) (s : closedTerm L) : BoundedPreformula L n l

Flypitch construction substmax_bounded_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.substmaxBoundedFormula f s = NFChoice.Fol.substBoundedFormula f s ⋯

theorem NFChoice.Fol.substmax_bounded_formula_fst {L : Language} {n l : ℕ} (f : BoundedPreformula L (n + 1) l) (s : closedTerm L) : (substmaxBoundedFormula f s).fst = f.fst [BoundedPreterm.fst s // n]f

theorem NFChoice.Fol.substmax_bounded_formula_bd_all {L : Language} {n : ℕ} (f : boundedFormula L (n + 2)) (s : closedTerm L) : substmaxBoundedFormula (bd_all f) s = (substmaxBoundedFormula f s).bd_all

theorem NFChoice.Fol.substmax_bounded_formula_bd_apps_rel {L : Language} {n l : ℕ} (f : BoundedPreformula L (n + 1) l) (t : closedTerm L) (ts : DVec (boundedTerm L (n + 1)) l) : substmaxBoundedFormula (bdAppsRel f ts) t = bdAppsRel (substmaxBoundedFormula f t) (DVec.map (fun (t' : BoundedPreterm L (n + 1) 0) => substmaxBoundedTerm t' t) ts)

def NFChoice.Fol.subst0BoundedFormula {L : Language} {n l : ℕ} (f : BoundedPreformula L (n + 1) l) (s : boundedTerm L n) : BoundedPreformula L n l

Flypitch construction subst0_bounded_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.subst0BoundedFormula f s = NFChoice.Fol.BoundedPreformula.castEq ⋯ (NFChoice.Fol.substBoundedFormula f s ⋯)

@[simp]

theorem NFChoice.Fol.subst0_bounded_formula_fst {L : Language} {n l : ℕ} (f : BoundedPreformula L (n + 1) l) (s : boundedTerm L n) : (subst0BoundedFormula f s).fst = f.fst [BoundedPreterm.fst s // 0]f

theorem NFChoice.Fol.substmax_eq_subst0_formula {L : Language} {l : ℕ} (f : BoundedPreformula L 1 l) (t : closedTerm L) : subst0BoundedFormula f t = substmaxBoundedFormula f t

realize_sentence lemmas

theorem NFChoice.Fol.realize_sentence_false {L : Language} {S : Structure L} : realizeSentence S bd_falsum ↔ False

theorem NFChoice.Fol.realize_sentence_imp {L : Language} {S : Structure L} {f₁ f₂ : sentence L} : realizeSentence S (bd_imp f₁ f₂) ↔ realizeSentence S f₁ → realizeSentence S f₂

theorem NFChoice.Fol.realize_sentence_not {L : Language} {S : Structure L} {f : sentence L} : realizeSentence S (bdNot f) ↔ ¬realizeSentence S f

theorem NFChoice.Fol.realize_sentence_dne {L : Language} {S : Structure L} {f : sentence L} : realizeSentence S (bdNot (bdNot f)) ↔ realizeSentence S f

theorem NFChoice.Fol.realize_sentence_all {L : Language} {S : Structure L} {f : boundedFormula L 1} : realizeSentence S (bd_all f) ↔ ∀ (x : S.carrier), realizeBoundedFormula (DVec.cons x DVec.nil) f DVec.nil

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_imp {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {f g : boundedFormula L n} : realizeBoundedFormula v (bd_imp f g) DVec.nil ↔ realizeBoundedFormula v f DVec.nil → realizeBoundedFormula v g DVec.nil

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_and {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {f g : boundedFormula L n} : realizeBoundedFormula v (bdAnd f g) DVec.nil ↔ realizeBoundedFormula v f DVec.nil ∧ realizeBoundedFormula v g DVec.nil

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_not {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {f : boundedFormula L n} : realizeBoundedFormula v (bdNot f) DVec.nil ↔ ¬realizeBoundedFormula v f DVec.nil

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_ex {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {f : boundedFormula L (n + 1)} : realizeBoundedFormula v (bdEx f) DVec.nil ↔ ∃ (x : S.carrier), realizeBoundedFormula (DVec.cons x v) f DVec.nil

theorem NFChoice.Fol.realize_sentence_ex {L : Language} {S : Structure L} {f : boundedFormula L 1} : realizeSentence S (bdEx f) ↔ ∃ (x : S.carrier), realizeBoundedFormula (DVec.cons x DVec.nil) f DVec.nil

theorem NFChoice.Fol.realize_sentence_and {L : Language} {S : Structure L} {f₁ f₂ : sentence L} : realizeSentence S (bdAnd f₁ f₂) ↔ realizeSentence S f₁ ∧ realizeSentence S f₂

@[simp]

theorem NFChoice.Fol.realize_bounded_formula_biimp {L : Language} {S : Structure L} {n : ℕ} {v : DVec S.carrier n} {f g : boundedFormula L n} : realizeBoundedFormula v (bdBiimp f g) DVec.nil ↔ (realizeBoundedFormula v f DVec.nil ↔ realizeBoundedFormula v g DVec.nil)

theorem NFChoice.Fol.realize_sentence_biimp {L : Language} {S : Structure L} {f₁ f₂ : sentence L} : realizeSentence S (bdBiimp f₁ f₂) ↔ (realizeSentence S f₁ ↔ realizeSentence S f₂)

theorem NFChoice.Fol.realize_bounded_formula_bd_apps_rel {L : Language} {S : Structure L} {n l : ℕ} (xs : DVec S.carrier n) (f : BoundedPreformula L n l) (ts : DVec (boundedTerm L n) l) : realizeBoundedFormula xs (bdAppsRel f ts) DVec.nil ↔ realizeBoundedFormula xs f (DVec.map (fun (t : BoundedPreterm L n 0) => realizeBoundedTerm xs t DVec.nil) ts)

@[simp]

theorem NFChoice.Fol.realize_cast_bounded_formula {L : Language} {S : Structure L} {n m : ℕ} {h : n ≤ m} {f : boundedFormula L n} {v : DVec S.carrier m} : realizeBoundedFormula v (BoundedPreformula.cast h f) DVec.nil = realizeBoundedFormula (DVec.trunc n h v) f DVec.nil

theorem NFChoice.Fol.realize_sentence_bd_apps_rel' {L : Language} {S : Structure L} {l : ℕ} (f : presentence L l) (ts : DVec (closedTerm L) l) : realizeSentence S (bdAppsRel f ts) ↔ realizeBoundedFormula DVec.nil f (DVec.map (realizeClosedTerm S) ts)

theorem NFChoice.Fol.realize_bd_apps_rel {L : Language} {S : Structure L} {l : ℕ} (R : L.relations l) (ts : DVec (closedTerm L) l) : realizeSentence S (bdAppsRel (bd_rel R) ts) ↔ S.relMap R (DVec.map (realizeClosedTerm S) ts)

theorem NFChoice.Fol.realize_sentence_equal {L : Language} {S : Structure L} (t₁ t₂ : closedTerm L) : realizeSentence S (bd_equal t₁ t₂) ↔ realizeClosedTerm S t₁ = realizeClosedTerm S t₂

theorem NFChoice.Fol.realize_sentence_iff {L : Language} {S : Structure L} (v : ℕ → S.carrier) (f : sentence L) : realizeSentence S f ↔ realizeFormula v (BoundedPreformula.fst f) DVec.nil

lift_bounded_formula_at — lift bounded formulas

def NFChoice.Fol.liftBoundedFormulaAt {L : Language} {n l : ℕ} (_f : BoundedPreformula L n l) (n' _m : ℕ) : BoundedPreformula L (n + n') l

Flypitch construction lift_bounded_formula_at, retained by the first-order soundness and completeness development.

Equations

• (NFChoice.Fol.bd_falsum ↑ᶠᵇ' x✝¹ # x✝) = NFChoice.Fol.bd_falsum
• (NFChoice.Fol.bd_equal t₁ t₂ ↑ᶠᵇ' x✝¹ # x✝) = NFChoice.Fol.bd_equal (t₁ ↑ᵇ' x✝¹ # x✝) (t₂ ↑ᵇ' x✝¹ # x✝)
• (NFChoice.Fol.bd_rel R ↑ᶠᵇ' x✝¹ # x✝) = NFChoice.Fol.bd_rel R
• (f.bd_apprel t ↑ᶠᵇ' x✝¹ # x✝) = (f ↑ᶠᵇ' x✝¹ # x✝).bd_apprel (t ↑ᵇ' x✝¹ # x✝)
• (f₁.bd_imp f₂ ↑ᶠᵇ' x✝¹ # x✝) = (f₁ ↑ᶠᵇ' x✝¹ # x✝).bd_imp (f₂ ↑ᶠᵇ' x✝¹ # x✝)
• (f.bd_all ↑ᶠᵇ' x✝¹ # x✝) = (NFChoice.Fol.BoundedPreformula.castEq ⋯ (f ↑ᶠᵇ' x✝¹ # x✝ + 1)).bd_all

def NFChoice.Fol.«term_↑ᶠᵇ'_#_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

@[reducible]

def NFChoice.Fol.liftBoundedFormula {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) (n' : ℕ) : BoundedPreformula L (n + n') l

Flypitch construction lift_bounded_formula, retained by the first-order soundness and completeness development.

Equations

• f ↑ᶠᵇ n' = f ↑ᶠᵇ' n' # 0

def NFChoice.Fol.«term_↑ᶠᵇ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_↑ᶠᵇ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_↑ᶠᵇ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑ᶠᵇ ") (Lean.ParserDescr.cat `term 101))

@[reducible]

def NFChoice.Fol.liftBoundedFormula1 {L : Language} {n' l : ℕ} (f : BoundedPreformula L n' l) : BoundedPreformula L (n' + 1) l

Flypitch construction lift_bounded_formula1, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.liftBoundedFormula1 f = f ↑ᶠᵇ 1

@[simp]

theorem NFChoice.Fol.lift_bounded_formula_fst {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) (n' m : ℕ) : (f ↑ᶠᵇ' n' # m).fst = f.fst ↑f' n' # m

Sentence theories (src/fol.lean lines 2233-2759)

@[reducible, inline]

abbrev NFChoice.Fol.SentTheory (L : Language) : Type u

A SentTheory is a set of sentences (Lean 3: Theory L = set (sentence L)).

Equations

• NFChoice.Fol.SentTheory L = Set (NFChoice.Fol.sentence L)

@[reducible]

def NFChoice.Fol.SentTheory.fst {L : Language} (T : SentTheory L) : Set (formula L)

Project a sentence theory to a set of formulas

Equations

• T.fst = NFChoice.Fol.BoundedPreformula.fst '' T

theorem NFChoice.Fol.SentTheory.lift_irrel {L : Language} (T : SentTheory L) : liftFormula1 '' T.fst = T.fst

def NFChoice.Fol.SentTheory.sprf {L : Language} (T : SentTheory L) (f : sentence L) : Type u

Derivability for sentence theories: T.fst ⊢ f.fst

Equations

• T.sprf f = NFChoice.Fol.prf T.fst (NFChoice.Fol.BoundedPreformula.fst f)

def NFChoice.Fol.SentTheory.sprovable {L : Language} (T : SentTheory L) (f : sentence L) : Prop

Provability (nonempty-wrapped) for sentence theories

Equations

• T.sprovable f = NFChoice.Fol.provable T.fst (NFChoice.Fol.BoundedPreformula.fst f)

def NFChoice.Fol.«term_⊢ₛ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊢ₛ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊢ₛ_» 51 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ₛ ") (Lean.ParserDescr.cat `term 0))

def NFChoice.Fol.«term_⊢ₛ'_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊢ₛ'_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊢ₛ'_» 51 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ₛ' ") (Lean.ParserDescr.cat `term 0))

All-realize-sentence — a structure models a sentence

theory

def NFChoice.Fol.allRealizeSentence {L : Language} (S : Structure L) (T : SentTheory L) : Prop

A structure S realizes all sentences in T

Equations

• NFChoice.Fol.allRealizeSentence S T = ∀ ⦃f : NFChoice.Fol.sentence L⦄, f ∈ T → NFChoice.Fol.realizeSentence S f

def NFChoice.Fol.«term_⊨ₜ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_⊨ₜ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_⊨ₜ_» 51 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ₜ ") (Lean.ParserDescr.cat `term 0))

theorem NFChoice.Fol.all_realize_sentence_of_subset {L : Language} {S : Structure L} {T₁ T₂ : SentTheory L} (H : allRealizeSentence S T₂) (h_sub : T₁ ⊆ T₂) : allRealizeSentence S T₁

@[simp]

theorem NFChoice.Fol.all_realize_sentence_insert {L : Language} {S : Structure L} {f : sentence L} {T : SentTheory L} : allRealizeSentence S (insert f T) ↔ realizeSentence S f ∧ allRealizeSentence S T

@[simp]

theorem NFChoice.Fol.all_realize_sentence_singleton {L : Language} {S : Structure L} {f : sentence L} : allRealizeSentence S {f} ↔ realizeSentence S f

theorem NFChoice.Fol.realize_sentence_of_mem {L : Language} {S : Structure L} {T : SentTheory L} {f : sentence L} (H : allRealizeSentence S T) (h_mem : f ∈ T) : realizeSentence S f

ssatisfied — semantic consequence for sentence theories

def NFChoice.Fol.ssatisfied {L : Language} (T : SentTheory L) (f : sentence L) : Prop

T semantically entails ψ: every nonempty model of T satisfies ψ

Equations

• NFChoice.Fol.ssatisfied T f = ∀ ⦃S : NFChoice.Fol.Structure L⦄, Nonempty S.carrier → NFChoice.Fol.allRealizeSentence S T → NFChoice.Fol.realizeSentence S f

def NFChoice.Fol.allSsatisfied {L : Language} (T T' : SentTheory L) : Prop

Flypitch construction all_ssatisfied, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.allSsatisfied T T' = ∀ f ∈ T', NFChoice.Fol.ssatisfied T f

Connection between ssatisfied and satisfied

theorem NFChoice.Fol.satisfied_of_ssatisfied {L : Language} {T : SentTheory L} {f : sentence L} (H : ssatisfied T f) : satisfied T.fst (BoundedPreformula.fst f)

theorem NFChoice.Fol.ssatisfied_of_satisfied {L : Language} {T : SentTheory L} {f : sentence L} (H : satisfied T.fst (BoundedPreformula.fst f)) : ssatisfied T f

theorem NFChoice.Fol.satisfied_iff_ssatisfied {L : Language} {T : SentTheory L} {f : sentence L} : ssatisfied T f ↔ satisfied T.fst (BoundedPreformula.fst f)

theorem NFChoice.Fol.ssatisfied_snot {L : Language} {S : Structure L} {f : sentence L} (hS : ¬realizeSentence S f) : realizeSentence S (bdNot f)

Model — bundled structure satisfying a sentence theory

def NFChoice.Fol.Model {L : Language} (T : SentTheory L) : Type (u + 1)

A model of T is a structure satisfying T. Lean 3 Σ' (S : Structure L), S ⊨ T → Lean 4 {S : Structure L // all_realize_sentence S T}

Equations

• NFChoice.Fol.Model T = { S : NFChoice.Fol.Structure L // NFChoice.Fol.allRealizeSentence S T }

@[reducible, inline]

abbrev NFChoice.Fol.Model.str {L : Language} {T : SentTheory L} (M : Model T) : Structure L

The underlying structure of a model

Equations

• M.str = ↑M

theorem NFChoice.Fol.Model.sat {L : Language} {T : SentTheory L} (M : Model T) : allRealizeSentence M.str T

The model satisfies its theory

@[reducible]

def NFChoice.Fol.Model.realize {L : Language} {T : SentTheory L} (M : Model T) (ψ : sentence L) : Prop

A model realizes a sentence

Equations

• M.realize ψ = NFChoice.Fol.realizeSentence M.str ψ

@[simp]

theorem NFChoice.Fol.Model_realize_iff {L : Language} {T : SentTheory L} {M : Model T} {ψ : sentence L} : M.realize ψ ↔ realizeSentence M.str ψ

theorem NFChoice.Fol.Model_realize_of_theory {L : Language} {T : SentTheory L} (M : Model T) {ψ : sentence L} (h : ψ ∈ T) : M.realize ψ

theorem NFChoice.Fol.false_of_Model_absurd {L : Language} {T : SentTheory L} (M : Model T) {ψ : sentence L} (h : M.realize ψ) (h' : M.realize (bdNot ψ)) : False

Soundness at sentence level

theorem NFChoice.Fol.ssatisfied_soundness {L : Language} {T : SentTheory L} {A : sentence L} (H : T.sprovable A) : ssatisfied T A

theorem NFChoice.Fol.not_ssatisfied_of_model_not {L : Language} {T : SentTheory L} {ψ : sentence L} (M : Model T) (hM : M.realize (bdNot ψ)) (h_nonempty : Nonempty M.str.carrier) : ¬ssatisfied T ψ

Given a model M with M realizes ¬ψ, we have ¬ ssatisfied T ψ

Sentence-level is_consistent

def NFChoice.Fol.SentTheory.isConsistent {L : Language} (T : SentTheory L) : Prop

T is consistent if T.fst ⊬' ⊥ (at sentence/formula level)

Equations

• T.isConsistent = ¬NFChoice.Fol.provable T.fst ⊥'

Theory of a structure

def NFChoice.Fol.Th {L : Language} (S : Structure L) : SentTheory L

The theory of a structure S: all sentences true in S

Equations

• NFChoice.Fol.Th S = {f : NFChoice.Fol.sentence L | NFChoice.Fol.realizeSentence S f}

theorem NFChoice.Fol.realize_sentence_Th {L : Language} (S : Structure L) : allRealizeSentence S (Th S)

theorem NFChoice.Fol.SentTheory.is_consistent_Th {L : Language} (S : Structure L) (HS : Nonempty S.carrier) : (Th S).isConsistent

@[simp]

theorem NFChoice.Fol.in_theory_iff_satisfied {L : Language} {S : Structure L} {f : sentence L} : f ∈ Th S ↔ realizeSentence S f

eliminates_quantifiers

def NFChoice.Fol.eliminatesQuantifiers {L : Language} (T : SentTheory L) : Prop

Flypitch construction eliminates_quantifiers, retained by the first-order soundness and completeness development.

Equations

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

L_empty, T_empty, T_equality

def NFChoice.Fol.LEmpty : Language

The empty language with no functions and no relations

Equations

• NFChoice.Fol.LEmpty = { functions := fun (x : ℕ) => PEmpty.{?u.1 + 1}, relations := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

def NFChoice.Fol.TEmpty (L : Language) : SentTheory L

The empty theory over a language

Equations

• NFChoice.Fol.TEmpty L = ∅

@[reducible]

def NFChoice.Fol.TEquality : SentTheory LEmpty

The equality theory: empty theory over the empty language

Equations

• NFChoice.Fol.TEquality = NFChoice.Fol.TEmpty NFChoice.Fol.LEmpty

Section bd_alls (src/fol.lean lines 2706-2757)

def NFChoice.Fol.alls {L : Language} (_n : ℕ) : formula L → formula L

Apply ∀' n times to an unbounded formula

Equations

• NFChoice.Fol.alls 0 x✝ = x✝
• NFChoice.Fol.alls n.succ x✝ = NFChoice.Fol.preformula.all (NFChoice.Fol.alls n x✝)

def NFChoice.Fol.bdAlls' {L : Language} (k n : ℕ) : boundedFormula L (n + k) → boundedFormula L n

Apply bd_all k times, reducing the bound index from n+k to n

Equations

• NFChoice.Fol.bdAlls' 0 x✝¹ x✝ = x✝
• NFChoice.Fol.bdAlls' k.succ x✝¹ x✝ = NFChoice.Fol.bdAlls' k x✝¹ (NFChoice.Fol.bd_all x✝)

def NFChoice.Fol.bdAlls {L : Language} (n : ℕ) : boundedFormula L n → sentence L

Close off a bounded formula by universally quantifying all n free variables

Equations

• NFChoice.Fol.bdAlls 0 f = f
• NFChoice.Fol.bdAlls n.succ f = NFChoice.Fol.bdAlls n (NFChoice.Fol.bd_all f)

@[simp]

theorem NFChoice.Fol.alls'_alls {L : Language} (n : ℕ) (ψ : boundedFormula L n) : bdAlls n ψ = bdAlls' n 0 (BoundedPreformula.castEq ⋯ ψ)

@[simp]

theorem NFChoice.Fol.alls'_all_commute {L : Language} {n k : ℕ} (f : boundedFormula L (n + k + 1)) : bdAlls' k n (bd_all f) = bd_all (bdAlls' k (n + 1) (BoundedPreformula.castEq ⋯ f))

theorem NFChoice.Fol.realize_sentence_bd_alls {L : Language} {n : ℕ} {f : boundedFormula L n} {S : Structure L} : realizeSentence S (bdAlls n f) ↔ ∀ (xs : DVec S.carrier n), realizeBoundedFormula xs f DVec.nil

@[simp]

theorem NFChoice.Fol.alls_0 {L : Language} (ψ : formula L) : alls 0 ψ = ψ

@[simp]

theorem NFChoice.Fol.alls_all_commute {L : Language} (f : formula L) {k : ℕ} : alls k (preformula.all f) = preformula.all (alls k f)

@[simp]

theorem NFChoice.Fol.alls_succ_k {L : Language} (f : formula L) {k : ℕ} : alls (k + 1) f = preformula.all (alls k f)