Definition talk:Class (Class Theory)/Zermelo-Fraenkel

From ProofWiki
Jump to navigation Jump to search

This might turn out to be a much bigger problem than I had initially anticipated. There are lots of pages that use proper classes, and unless there's a way to allow proper classes into ZFC (which I don't think there is), all of those pages may have to be reworked, or get tagged with {{NotZFC}}. --HumblePi (talk) 20:03, 26 April 2017 (EDT)

The enormity of the task that you see ahead is one big reason why nobody has got round to attempting it yet.
For now, attach your <code>{{NotZFC}}</code> tag to everything you see as needs it -- I have made it so that all such pages get included in the new Category:Class Theory Work in Progress.
This should then allow us to see the prospect before us. --prime mover (talk) 04:25, 27 April 2017 (EDT)
Okay, I'll do that then. Once I've finished tagging all of those pages we can figure out what should be done with them. --HumblePi (talk) 18:18, 27 April 2017 (EDT)
Also bear in mind that the treatment as provided by the contributor who posted up the contents of the Takeuti and Zaring book was called into question for its lack of cohesion and imprecision. I can't comment on that because I was not in the position to be able to comment adequately on it (it's out of my area of expertise). So when all this is done, tread carefully where those pages are concerned. --prime mover (talk) 18:58, 27 April 2017 (EDT)
Takeuti and Zaring? I've never heard of it. I'm curious to see how it handles classes, so I'll try to get my hands on it and see how I can sort this all out. --HumblePi (talk) 19:17, 27 April 2017 (EDT)
It's cited at the bottom of most of the pages you are in the process of adding your template to. Feel free to explore. --prime mover (talk) 19:20, 27 April 2017 (EDT)
Proper classes don't exist in ZFC, but that doesn't mean the proofs are incorrect. Just as the Axiom of Specification is an infinite collection of axioms, a "theorem" proved using classes is actually an infinite collection of theorems, corresponding to every possible WFF we could input into it. Alternatively, we are trying to demonstrate that we can prove the theorem no matter what specific formula is chosen to instantiate the $\map P x$. As long as the warning at the bottom of the page is heeded, and we never quantify over classes (as that would correspond to second-order logic), then there is no problem. Still, it's probably worth proving the emergent properties of classes defined in this way before they are used in theorems. CircuitCraft (talk) 05:05, 11 January 2023 (UTC)