NF weak partition development: NFStandard.Basic.

The usual graph-theoretic stratification condition for the language of NF. An equality edge preserves type and a membership edge raises type by one. At a binder, the newly bound de Bruijn variable (index zero) may be assigned an arbitrary integer type.

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

A type assignment certifies the ordinary NF stratification of a formula.

Equations

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

def NFChoice.Foundation.Formula.Stratified {n : ℕ} (p : Formula n) : Prop

A formula is stratified when it admits an integer type assignment.

Equations

• p.Stratified = ∃ (ty : Fin n → ℤ), NFChoice.Foundation.Formula.StratifiedBy ty p

@[reducible, inline]

abbrev NFChoice.Foundation.Formula.Stratification {n : ℕ} (p : Formula n) : Type

A first-class stratification certificate, useful to schema enumerators.

Equations

• p.Stratification = { ty : Fin n → ℤ // NFChoice.Foundation.Formula.StratifiedBy ty p }

@[simp]

theorem NFChoice.Foundation.Formula.stratifiedBy_falsum {n : ℕ} (ty : Fin n → ℤ) : StratifiedBy ty falsum

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem NFChoice.Foundation.Formula.stratified_neg_iff {n : ℕ} (p : Formula n) : p.neg.Stratified ↔ p.Stratified

@[simp]

theorem NFChoice.Foundation.Formula.stratified_imp_iff {n : ℕ} (p q : Formula n) : (p.imp q).Stratified ↔ ∃ (ty : Fin n → ℤ), StratifiedBy ty p ∧ StratifiedBy ty q

@[simp]

theorem NFChoice.Foundation.Formula.stratified_conj_iff {n : ℕ} (p q : Formula n) : (p.conj q).Stratified ↔ ∃ (ty : Fin n → ℤ), StratifiedBy ty p ∧ StratifiedBy ty q

@[simp]

theorem NFChoice.Foundation.Formula.stratified_disj_iff {n : ℕ} (p q : Formula n) : (p.disj q).Stratified ↔ ∃ (ty : Fin n → ℤ), StratifiedBy ty p ∧ StratifiedBy ty q

@[simp]

theorem NFChoice.Foundation.Formula.stratified_biimp_iff {n : ℕ} (p q : Formula n) : (p.biimp q).Stratified ↔ ∃ (ty : Fin n → ℤ), StratifiedBy ty p ∧ StratifiedBy ty q

@[simp]

theorem NFChoice.Foundation.Formula.stratified_all_iff {n : ℕ} (p : Formula (n + 1)) : p.all.Stratified ↔ p.Stratified

@[simp]

theorem NFChoice.Foundation.Formula.stratified_ex_iff {n : ℕ} (p : Formula (n + 1)) : p.ex.Stratified ↔ p.Stratified

theorem NFChoice.Foundation.Formula.Stratified.imp {n : ℕ} {p q : Formula n} {ty : Fin n → ℤ} (hp : StratifiedBy ty p) (hq : StratifiedBy ty q) : (p.imp q).Stratified

theorem NFChoice.Foundation.Formula.Stratified.neg {n : ℕ} {p : Formula n} (hp : p.Stratified) : p.neg.Stratified

theorem NFChoice.Foundation.Formula.Stratified.conj {n : ℕ} {p q : Formula n} {ty : Fin n → ℤ} (hp : StratifiedBy ty p) (hq : StratifiedBy ty q) : (p.conj q).Stratified

theorem NFChoice.Foundation.Formula.Stratified.disj {n : ℕ} {p q : Formula n} {ty : Fin n → ℤ} (hp : StratifiedBy ty p) (hq : StratifiedBy ty q) : (p.disj q).Stratified

theorem NFChoice.Foundation.Formula.Stratified.biimp {n : ℕ} {p q : Formula n} {ty : Fin n → ℤ} (hp : StratifiedBy ty p) (hq : StratifiedBy ty q) : (p.biimp q).Stratified

theorem NFChoice.Foundation.Formula.Stratified.all {n : ℕ} {p : Formula (n + 1)} (hp : p.Stratified) : p.all.Stratified

theorem NFChoice.Foundation.Formula.Stratified.ex {n : ℕ} {p : Formula (n + 1)} (hp : p.Stratified) : p.ex.Stratified

def NFChoice.Foundation.Formula.closeAll {n : ℕ} (p : Formula n) : Fol.sentence LNF

Universally close all free de Bruijn variables of an intrinsic formula.

Equations

• p.closeAll = NFChoice.Fol.bdAlls n p.toFlypitch

def NFChoice.Foundation.NFStandard.comprehensionBody {n : ℕ} (p : Formula (n + 1)) : Formula n

The open formula saying that some set has exactly the extension defined by p.

Equations

• NFChoice.Foundation.NFStandard.comprehensionBody p = (NFChoice.Foundation.ExactLiteralTrial.Formula.eqCandidateToPredicate p).ex

def NFChoice.Foundation.NFStandard.comprehensionInstance {n : ℕ} (p : Formula (n + 1)) : Fol.sentence LNF

The universally closed comprehension axiom associated with p.

Equations

• NFChoice.Foundation.NFStandard.comprehensionInstance p = (NFChoice.Foundation.NFStandard.comprehensionBody p).closeAll

def NFChoice.Foundation.NFStandard.StratifiedComprehension : Fol.SentTheory LNF

The ordinary NF stratified-comprehension schema.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_stratifiedComprehension_iff (f : Fol.sentence LNF) : f ∈ StratifiedComprehension ↔ ∃ (n : ℕ) (p : Formula (n + 1)), p.Stratified ∧ f = comprehensionInstance p

theorem NFChoice.Foundation.NFStandard.comprehensionInstance_mem {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) : comprehensionInstance p ∈ StratifiedComprehension

@[reducible, inline]

abbrev NFChoice.Foundation.NF : Fol.SentTheory LNF

Standard NF: extensionality plus every stratified comprehension instance.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.extensionality_mem_NF : ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axExt ∈ NF

@[simp]

theorem NFChoice.Foundation.NFStandard.comprehensionInstance_mem_NF {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) : comprehensionInstance p ∈ NF

theorem NFChoice.Foundation.NFStandard.formulaHolds_renameVars {S : Fol.Structure LNF} {n m : ℕ} (rho : Fin n → Fin m) (xs : DVec S.carrier m) (ys : DVec S.carrier n) : (∀ (i : Fin n), SemanticCore.Lowering.lookup xs (rho i) = SemanticCore.Lowering.lookup ys i) → ∀ (p : Formula n), SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.Formula.renameVars rho p) ↔ SemanticCore.Lowering.FormulaHolds S ys p

Renaming intrinsic free variables agrees with renaming their valuation.

@[simp]

theorem NFChoice.Foundation.NFStandard.formulaHolds_liftClassPredicate {S : Fol.Structure LNF} {n : ℕ} (xs : DVec S.carrier n) (a z : S.carrier) (p : Formula (n + 1)) : SemanticCore.Lowering.FormulaHolds S (DVec.cons z (DVec.cons a xs)) (ExactLiteralTrial.Formula.liftClassPredicate p) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons z xs) p

The inserted ambient set variable is semantically ignored by a lifted class predicate.

@[simp]

theorem NFChoice.Foundation.NFStandard.formulaHolds_eqCandidateToPredicate {S : Fol.Structure LNF} {n : ℕ} (xs : DVec S.carrier n) (a : S.carrier) (p : Formula (n + 1)) : SemanticCore.Lowering.FormulaHolds S (DVec.cons a xs) (ExactLiteralTrial.Formula.eqCandidateToPredicate p) ↔ ∀ (z : S.carrier), SemanticCore.Mem S z a ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons z xs) p

Direct semantics of the set-representative formula used by comprehension.

theorem NFChoice.Foundation.NFStandard.nf_extensional {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : SemanticCore.Extensional S

Every model of NF is extensional.

theorem NFChoice.Foundation.NFStandard.nf_realizes_comprehensionInstance {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) : Fol.realizeSentence S (comprehensionInstance p)

A model of NF realizes each certified closed comprehension instance.

theorem NFChoice.Foundation.NFStandard.nf_comprehension {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) (xs : DVec S.carrier n) : ∃ (a : S.carrier), ∀ (z : S.carrier), SemanticCore.Mem S z a ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons z xs) p

Semantic elimination rule for standard stratified comprehension.