NF weak partition development: NFStandard.TheoryEquivalence.

Small semantic-to-syntactic utilities used to state the equivalence between standard NF and the finite theory HailperinNF. Keeping this layer generic makes clear that the substantive work is exactly the equivalence of their models; Gödel completeness then converts that equivalence into equality of all first-order consequences.

def NFChoice.Foundation.NFStandard.DeductivelyEquivalent (T U : Fol.SentTheory LNF) : Prop

Two sentence theories have exactly the same first-order consequences.

Equations

• NFChoice.Foundation.NFStandard.DeductivelyEquivalent T U = ∀ (f : NFChoice.Fol.sentence NFChoice.Foundation.LNF), T.sprovable f ↔ U.sprovable f

theorem NFChoice.Foundation.NFStandard.consequence_of_model_inclusion {T U : Fol.SentTheory LNF} {f : Fol.sentence LNF} (hmodels : ∀ (S : Fol.Structure LNF), Fol.allRealizeSentence S U → Fol.allRealizeSentence S T) (hf : T.sprovable f) : U.sprovable f

Semantic inclusion of model classes transfers every formal consequence.

theorem NFChoice.Foundation.NFStandard.deductivelyEquivalent_of_models_iff {T U : Fol.SentTheory LNF} (hmodels : ∀ (S : Fol.Structure LNF), Fol.allRealizeSentence S T ↔ Fol.allRealizeSentence S U) : DeductivelyEquivalent T U

Theories with the same models have exactly the same formal consequences.

theorem NFChoice.Foundation.NFStandard.DeductivelyEquivalent.mp {T U : Fol.SentTheory LNF} (h : DeductivelyEquivalent T U) {f : Fol.sentence LNF} (hf : T.sprovable f) : U.sprovable f

A theorem can be transported across deductively equivalent theories.

theorem NFChoice.Foundation.NFStandard.DeductivelyEquivalent.mpr {T U : Fol.SentTheory LNF} (h : DeductivelyEquivalent T U) {f : Fol.sentence LNF} (hf : U.sprovable f) : T.sprovable f

The reverse transport across deductively equivalent theories.