6 ms·
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, foral
by Smaug123 27d ago
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
- andriy_koval 27d ago> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example. I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?
- Smaug123 27d agoBecause you wrote: > what are exactly rules, which could be separate topic of research, this detail is skipped I am now confident you’re a troll, though, so I am going to bow out.
- andriy_koval 27d agoI referred to specific definition in wikipedia. Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.