NF weak partition development: NFStandard.CylinderCompiler.

StratifiedByBelow cap ty p is a stratification certificate with one global normalization ceiling. In particular, the witness type chosen at every quantifier is at most cap. This is the form needed by Hailperin's uniform singleton normalization: every variable is raised exactly cap - type times, and that convention is unchanged beneath binders.

def NFChoice.Foundation.Formula.StratifiedByBelow (cap : ℤ) {n : ℕ} (ty : Fin n → ℤ) : Formula n → Prop

Stratification by ty, with every bound-variable type globally capped.

Equations

• NFChoice.Foundation.Formula.StratifiedByBelow cap ty NFChoice.Foundation.Formula.falsum = True
• NFChoice.Foundation.Formula.StratifiedByBelow cap ty (NFChoice.Foundation.Formula.equal x_1 y) = (ty x_1 = ty y)
• NFChoice.Foundation.Formula.StratifiedByBelow cap ty (NFChoice.Foundation.Formula.mem x_1 y) = (ty y = ty x_1 + 1)
• NFChoice.Foundation.Formula.StratifiedByBelow cap ty (p.imp q) = (NFChoice.Foundation.Formula.StratifiedByBelow cap ty p ∧ NFChoice.Foundation.Formula.StratifiedByBelow cap ty q)
• NFChoice.Foundation.Formula.StratifiedByBelow cap ty p.all = ∃ k ≤ cap, NFChoice.Foundation.Formula.StratifiedByBelow cap (fun (i : Fin (n + 1)) => Fin.cases k ty i) p

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedByBelow_falsum {cap : ℤ} {n : ℕ} (ty : Fin n → ℤ) : StratifiedByBelow cap ty falsum

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedByBelow_equal {cap : ℤ} {n : ℕ} (ty : Fin n → ℤ) (x y : Fin n) : StratifiedByBelow cap ty (equal x y) ↔ ty x = ty y

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedByBelow_mem {cap : ℤ} {n : ℕ} (ty : Fin n → ℤ) (x y : Fin n) : StratifiedByBelow cap ty (mem x y) ↔ ty y = ty x + 1

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedByBelow_imp {cap : ℤ} {n : ℕ} (ty : Fin n → ℤ) (p q : Formula n) : StratifiedByBelow cap ty (p.imp q) ↔ StratifiedByBelow cap ty p ∧ StratifiedByBelow cap ty q

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedByBelow_all {cap : ℤ} {n : ℕ} (ty : Fin n → ℤ) (p : Formula (n + 1)) : StratifiedByBelow cap ty p.all ↔ ∃ k ≤ cap, StratifiedByBelow cap (fun (i : Fin (n + 1)) => Fin.cases k ty i) p

theorem NFChoice.Foundation.Formula.StratifiedByBelow.mono {cap cap' : ℤ} {n : ℕ} {ty : Fin n → ℤ} {p : Formula n} : cap ≤ cap' → StratifiedByBelow cap ty p → StratifiedByBelow cap' ty p

Increasing the normalization ceiling preserves a capped certificate.

theorem NFChoice.Foundation.Formula.StratifiedByBelow.toStratifiedBy {cap : ℤ} {n : ℕ} {ty : Fin n → ℤ} {p : Formula n} : StratifiedByBelow cap ty p → StratifiedBy ty p

Forgetting the global ceiling recovers the ordinary certificate.

def NFChoice.Foundation.Formula.contextCap (n : ℕ) : (Fin n → ℤ) → ℤ

A simple upper bound for every entry of a finite type context.

Equations

• NFChoice.Foundation.Formula.contextCap 0 x_2 = 0
• NFChoice.Foundation.Formula.contextCap n.succ ty = max (ty 0) (NFChoice.Foundation.Formula.contextCap n fun (i : Fin n) => ty i.succ)

theorem NFChoice.Foundation.Formula.le_contextCap {n : ℕ} (ty : Fin n → ℤ) (i : Fin n) : ty i ≤ contextCap n ty

theorem NFChoice.Foundation.Formula.exists_stratifiedByBelow {n : ℕ} (ty : Fin n → ℤ) (p : Formula n) : StratifiedBy ty p → ∃ (cap : ℤ), (∀ (i : Fin n), ty i ≤ cap) ∧ StratifiedByBelow cap ty p

Every ordinary finite stratification admits one cap valid at all binders.

structure NFChoice.Foundation.Formula.CappedStratification {n : ℕ} (p : Formula n) : Type

A selected global cap and capped certificate for a stratified formula.

• cap : ℤ

  The cap component of the corresponding first-order structure.

• ty : Fin n → ℤ

  The ty component of the corresponding first-order structure.

• bounded (i : Fin n) : self.ty i ≤ self.cap
• certificate : StratifiedByBelow self.cap self.ty p

noncomputable def NFChoice.Foundation.Formula.cappedStratification {n : ℕ} (p : Formula n) (hp : p.Stratified) : p.CappedStratification

Package a usual stratification as a globally capped one.

Equations

• p.cappedStratification hp = { cap := Classical.choose ⋯, ty := Classical.choose hp, bounded := ⋯, certificate := ⋯ }

CylinderAlgebra is the small, typed relation-algebra interface used by the uniform Hailperin compiler. The cap is fixed for the whole formula, including all bound variables. A concrete implementation therefore raises coordinate i by Int.toNat (cap - ty i) singleton steps once and never has to rebase a tail valuation when a quantifier is crossed.

structure NFChoice.Foundation.NFStandard.CylinderAlgebra (S : Fol.Structure LNF) : Type

Operations sufficient to compile globally capped stratified formulas.

• code {n : ℕ} : ℤ → (Fin n → ℤ) → DVec S.carrier n → S.carrier

  The code operation of this NF model presentation.

• empty : ℤ → (n : ℕ) → S.carrier

  The empty operation of this NF model presentation.

• compl : ℤ → (n : ℕ) → S.carrier → S.carrier

  The compl operation of this NF model presentation.

• inter : ℤ → (n : ℕ) → S.carrier → S.carrier → S.carrier

  The inter operation of this NF model presentation.

• eqSet {n : ℕ} : ℤ → (ty : Fin n → ℤ) → (i j : Fin n) → S.carrier

  The eq Set operation of this NF model presentation.

• memSet {n : ℕ} : ℤ → (ty : Fin n → ℤ) → (i j : Fin n) → S.carrier

  The mem Set operation of this NF model presentation.

• existsSet {n : ℕ} : ℤ → (ty : Fin n → ℤ) → ℤ → S.carrier → S.carrier

  The exists Set operation of this NF model presentation.

• slice {n : ℕ} : ℤ → (ty : Fin (n + 1) → ℤ) → S.carrier → DVec S.carrier n → S.carrier

  The slice operation of this NF model presentation.

• mem_empty {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (xs : DVec S.carrier n) : ¬SemanticCore.Mem S (self.code cap ty xs) (self.empty cap n)
• mem_compl {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (A : S.carrier) (xs : DVec S.carrier n) : SemanticCore.Mem S (self.code cap ty xs) (self.compl cap n A) ↔ ¬SemanticCore.Mem S (self.code cap ty xs) A
• mem_inter {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (A B : S.carrier) (xs : DVec S.carrier n) : SemanticCore.Mem S (self.code cap ty xs) (self.inter cap n A B) ↔ SemanticCore.Mem S (self.code cap ty xs) A ∧ SemanticCore.Mem S (self.code cap ty xs) B
• mem_eqSet {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (i j : Fin n) (_h : ty i = ty j) (xs : DVec S.carrier n) : SemanticCore.Mem S (self.code cap ty xs) (self.eqSet cap ty i j) ↔ SemanticCore.Lowering.lookup xs i = SemanticCore.Lowering.lookup xs j
• mem_memSet {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (i j : Fin n) (_h : ty j = ty i + 1) (xs : DVec S.carrier n) : SemanticCore.Mem S (self.code cap ty xs) (self.memSet cap ty i j) ↔ SemanticCore.Mem S (SemanticCore.Lowering.lookup xs i) (SemanticCore.Lowering.lookup xs j)
• mem_existsSet {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (k : ℤ) (_hk : k ≤ cap) (A : S.carrier) (xs : DVec S.carrier n) : SemanticCore.Mem S (self.code cap ty xs) (self.existsSet cap ty k A) ↔ ∃ (a : S.carrier), SemanticCore.Mem S (self.code cap (fun (i : Fin (n + 1)) => Fin.cases k ty i) (DVec.cons a xs)) A
• mem_slice {n : ℕ} (cap : ℤ) (ty : Fin (n + 1) → ℤ) (_hcap : ∀ (i : Fin (n + 1)), ty i ≤ cap) (A : S.carrier) (xs : DVec S.carrier n) (z : S.carrier) : SemanticCore.Mem S z (self.slice cap ty A xs) ↔ SemanticCore.Mem S (self.code cap ty (DVec.cons z xs)) A

noncomputable def NFChoice.Foundation.NFStandard.CylinderAlgebra.compile {S : Fol.Structure LNF} (C : CylinderAlgebra S) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (p : Formula n) : Formula.StratifiedByBelow cap ty p → S.carrier

Compile a formula using one global normalization cap.

Equations

• One or more equations did not get rendered due to their size.
• C.compile x✝¹ x✝ NFChoice.Foundation.Formula.falsum x_6 = C.empty x✝¹ x✝²
• C.compile x✝¹ x✝ (NFChoice.Foundation.Formula.equal i j) x_6 = C.eqSet x✝¹ x✝ i j
• C.compile x✝¹ x✝ (NFChoice.Foundation.Formula.mem i j) x_6 = C.memSet x✝¹ x✝ i j
• C.compile x✝¹ x✝ (p.imp q) h = C.compl x✝¹ x✝² (C.inter x✝¹ x✝² (C.compile x✝¹ x✝ p ⋯) (C.compl x✝¹ x✝² (C.compile x✝¹ x✝ q ⋯)))

theorem NFChoice.Foundation.NFStandard.CylinderAlgebra.mem_compile {S : Fol.Structure LNF} (C : CylinderAlgebra S) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (p : Formula n) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (hp : Formula.StratifiedByBelow cap ty p) (xs : DVec S.carrier n) : SemanticCore.Mem S (C.code cap ty xs) (C.compile cap ty p hp) ↔ SemanticCore.Lowering.FormulaHolds S xs p

The compiler represents exactly the semantic truth set of its formula.

noncomputable def NFChoice.Foundation.NFStandard.CylinderAlgebra.comprehensionSet {S : Fol.Structure LNF} (C : CylinderAlgebra S) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) (xs : DVec S.carrier n) : S.carrier

Chosen comprehension object produced by the uniform compiler.

Equations

• C.comprehensionSet p hp xs = C.slice (p.cappedStratification hp).cap (p.cappedStratification hp).ty (C.compile (p.cappedStratification hp).cap (p.cappedStratification hp).ty p ⋯) xs

theorem NFChoice.Foundation.NFStandard.CylinderAlgebra.mem_comprehensionSet {S : Fol.Structure LNF} (C : CylinderAlgebra S) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) (xs : DVec S.carrier n) (z : S.carrier) : SemanticCore.Mem S z (C.comprehensionSet p hp xs) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons z xs) p

Every cylinder algebra validates the complete standard NF schema.