Definition talk:Structure (Set Theory)

From ProofWiki
Jump to navigation Jump to search

I found I was going to end up littering the page with questions and remarks, so let me collect them here:

  1. Is it intended that $R$ has anything to do with $A$? (I suspect that $R$ is a relation on $A$)
  2. The definition is situated in Category:Definitions/Set Theory but refers only to classes. Would it be better off in the Category:Class Theory?
  3. Please mind the \left, \right convention
  4. The definition for $\models$ should be on a separate (sub)page
  5. Where does $p$ live? Do we work on Definition:Propositional Logic or Definition:Predicate Logic?

That will be it for now :). --Lord_Farin 19:47, 6 August 2012 (UTC)

As to the merge suggestion by PM, I think we want to be careful to note that an ordered pair notation is misleading as one of the two components is currently a class; we are landing on the set vs. class platform again, which at this point seems to be a part of a maze which still needs to be connected to the exit called 'coherent vision'. If we all have time, I suggest brainstorming on possible solutions right now, before irritation and edit-warring become prevalent. --Lord_Farin 19:56, 6 August 2012 (UTC)
The page does not belong here. It ought to be moved somewhere else, but right now, I can't think of anything else to call it (maybe Definition:Model (Class Theory). It is also important to note that, as Lord Farin noted, $[A,R]$ is not quite a relational structure by the linked definition, since the Kuratowski ordered pair only works for sets, not proper classes. It is important that we have a definition for proper classes, because we want to be able to talk about models of, for example, inaccessible cardinals, which are not necessarily sets in ZFC. There are, however, other definitions of ordered pairs that do work with proper classes, usually by modifying the Cartesian product. Also, $[A,R]$ is not intended as a class; rather, this definition is for defining $[A,R] \models p$. And as to your second point, it should probably be changed to the class theory category. $p$ is any well-formed formula, but it doesn't have to contain free variables (but it could). --Andrew Salmon 20:17, 6 August 2012 (UTC)
A while ago I started to restructure the axiomatics section with categories like Category:Models for PropCalc: Boolean Interpretations but at the time I got bogged down on natural deduction having a very antimodular set-up. I think, for structure-technical reasons, that it would be best if we tried to fit the stuff on class models right in there, hopefully achieving a modular approach. If I interpret your approach correctly (or the small part already up) I suspect it will be (reminiscent of) the standard model theory thing for the language of set theory (LST).
Apologies for decoherence in this response but I am thinking very fast now about the structural implications of this new area being added to PW and how to ensure that everything is adequately positioned. So what we are looking at here are models for LST which are a particular case of models for PredCalc which extend models for PropCalc. This makes a page title like Definition:Model (Class Theory) inadequate, but I can't come up with a good alternative atm. --Lord_Farin 20:31, 6 August 2012 (UTC)
On the level of PropCalc the models default to boolean interpretations; as for PredCalc stuff still comes down to truth being characterised by $\in$ (thinking out loud here). I vote for Definition:Model for Axiomatic Set Theory: Universal Class and Category:Models for Axiomatic Set Theory: Universal Classes or a variant of these (like Definition:Universal Class). In some twisted way I love these philosophical, abstract considerations. --Lord_Farin 20:40, 6 August 2012 (UTC)
Noting that Definition:Universal Class already exists and grasps the desired notion, I suggest that this will be the entry point for pouring this new stuff onto the site. --Lord_Farin 20:41, 6 August 2012 (UTC)