Talk:Morse–Kelley set theory

needs work

Doesn't say anything about what a "property" is (actually we want one definable by a formula in the second-order language of set theory). Doesn't mention what the other axioms are, relationship to ZFC, consistency following from an inaccessible cardinal. --Trovatore 15:05, 4 October 2005 (UTC)

redone

I have given a full account of this theory, though the form of limitation of size due to von Neumann may be viewed as eccentric. KM is not the same as second-order ZF.

Randall Holmes 16:23, 15 December 2005 (UTC)

Thanks; this article definitely needed work. I note though that you removed the point about KM being in the second-order language of set theory. I don't think that should have been removed. You're quite right of course that KM is a first-order theory, but it is expressed in second-order LST. It also should perhaps be noted that if you take exactly the same collection of axioms and give them a true second-order semantics (as opposed to the two-sorted first-order semantics that correspond to the first-order theory) you get something categorical up to the first inaccessible. --Trovatore 19:44, 15 December 2005 (UTC)

another issue in rewrite

I don't quite follow the claim that "second-order ZF" "proves the same theorems in practice" as KM. First, I'm not sure what it means for a second-order theory to "prove" something, but if it means logical implication (something is proved if true in all models of the theory), then second-order ZF proves lots of things KM doesn't (for example, Con(KM), and either CH or ¬CH, depending on which one is true). --Trovatore 06:35, 17 December 2005 (UTC)

see how you like the new language on the relationship between Morse-Kelley and second-order ZF. Randall Holmes 17:25, 17 December 2005 (UTC)

I've modified it slightly; the formulation involving definability was a little problematic. Suppose for example there were exactly five inaccessibles in the real world (of course that's nonsense, there's really proper-class many, but it's just an example). Then "the largest inaccessible" would be a definable rank of the von Neumann hierarchy. Now if we call the second inaccessible k2 and third k3, then V_k2 and V_k3 are both models of second-order ZF, but they disagree about the theory of the stage whose height is the largest inaccessible (though only because they disagree about what the largest inaccessible is). Granted, the new formulation is a little too weak, but at least it avoids this problem, which is awkward to find good language to work around.

relationship to NBG

This has now grown into a nice article.

MK can be viewed as a strengthened version of von Neumann-Bernays-Gödel’s set theory (NBG). Perhaps this relationship can be described?

the reference was already there, but not explicit enough. I have added a direct reference. Randall Holmes 19:57, 20 December 2005 (UTC)

Michael Meyling 15:56, 20 December 2005 (UTC)

second-order language???

I didn't know the phrase "second-order language". I read this as "second-order logic". Is this phrase well known? Perhaps it can be replaced or explained further after the following passage:

"Although this is a first-order theory, it is a common practice (not followed here) to use second-order language, that is, to distinguish between class variables (often capitalized) and set variables."

Perhaps something like this:

"This is can be done in the following way: $\forall x_{i}\ \phi (x_{i})$ is shorthand for $\forall X_{i}\ ({\mbox{set}}X_{i}\rightarrow \phi (X_{i}))$ and analogous for the existence quantifier."

Michael Meyling 15:55, 20 December 2005 (UTC)

It's not really my phrase, but the result of a conversation with someone else. All I'm saying is that it is the custom of some authors to use set variables and class variables, which makes the language appear like that of second-order logic (though it is not really a two-sorted theory). I don't want to clarify it because I am not actually using this convention here. Randall Holmes 19:52, 20 December 2005 (UTC)

further, I made a small change to make it clear that I'm not using some peculiar technical terminology "second-order language". Randall Holmes 19:58, 20 December 2005 (UTC)

Well, but isn't it the correct technical terminology? The set variables are intended to be interpreted by objects, and the class variables by predicates. That's second-order language. I think this nomenclature is completely standard, though I don't have any handy reference for it. (It's not second-order logic simply because that would imply some way of making inferences beyond those of first-order logic, and we aren't using any such strengthened inference rules.) --Trovatore 21:58, 20 December 2005 (UTC)

I am interested in any reference you find. --Michael Meyling 04:37, 21 December 2005 (UTC)

I'm not sure it is: second-order logic is two-sorted and KM is not. Even if it is correct it isn't universally recognized; notice also that I simply paraphrased it as "language like that of second-order logic" (though not quite the same!) so that (one hopes) it would be clear what I meant. Randall Holmes 23:45, 20 December 2005 (UTC)

I'm not very convinced by this "not two-sorted" thing. I certainly think of the sets and classes as being different sorts. I don't see any reason the sorts have to be disjoint. --Trovatore 00:03, 21 December 2005 (UTC)

They aren't disjoint in the common nomenclature. In E. Mendelson's "Introduction to Mathematical Logic" or J. D. Monk's "Introduction to Set Theory" lower case letters just indicate classes that are sets and capital letters stand for classes (see above). Being a proper class is just a predicate. Or did I miss the point? --Michael Meyling 04:37, 21 December 2005 (UTC)

I'm not saying that the domains of sets and classes in KM are or should be disjoint (they aren't and shouldn't be); the domains of objects and predicates/sets of objects in second-order logic should be disjoint (more precisely, equations between objects of different sorts do not make sense). Randall Holmes 17:25, 21 December 2005 (UTC)

There's something I didn't catch above: it is not necessarily the case that the classes of KM are to be interpreted as predicates. That seems to go better with the predicative class theory NBG. The classes of KM are more likely to be viewed realistically (as actual large collections which are not necessarily all definable as predicates). That is certainly the way I think of it. (Note that this is not a counterargument to second-order logic being applicable: second-order objects can be arbitrary collections as easily as predicates). Re the immediately preceding remark, equality between variables of different sorts is at best problematic; I prefer to think of KM as a one-sorted first order theory. But I think this is all in danger of becoming a quibble; the relationship with second order logic is clearly acknowledged at several points in the article, isn't it? Randall Holmes 00:33, 21 December 2005 (UTC)

further on equality: the basic rule for equality is that if a=b and P(a) then P(b): but this will not work well if a and b are of different sorts (and so cannot freely be substituted for one another in all contexts). Randall Holmes 00:41, 21 December 2005 (UTC)

Well, I didn't necessarily mean definable predicates. More that they shouldn't be completed totalities. If they're completed totalities, after all, why aren't they sets? But this is part of the neither-fish-nor-flesh problem with interpreting KM. So mostly I tend to think of an interpretation of KM as having some fixed inaccessible κ specified in advance; then its sets are objects of rank less than κ and its classes are subsets of V_κ. Trying to interpret it so that the individuals can be sets of arbitrary rank seems philosophically problematic. --Trovatore 01:11, 21 December 2005 (UTC)

I don't disagree with anything here... Randall Holmes 01:30, 21 December 2005 (UTC)

Kelley's original axioms

I have added the full text of Kelley's original axioms to the article. It is worth noting that Kelley does not use "second-order language"; for him the sets and classes evidently have the same status exactly. Randall Holmes 06:18, 30 December 2005 (UTC)

Having fun, Randall? I'm afraid that Kelley's axioms do imply the limitation of size in MK, but not necessarily in MKU (with urelements).

I am having fun (here, if not in relation (mathematics)). Randall Holmes 07:10, 25 January 2006 (UTC)

counterexample -- loosely, start with a model of set theory with at least 2 inaccessibles, κ₀ < κ₁. Let U be a "set" of urelements with cardinality κ₁, and construct V as the "set" of all sets which are hereditarily of cardinality < κ₀ over U. Classes are arbitrary subsets of "the universe".

As On^(V) is κ₀, while |V| is κ₁, there cannot be a bijection between On^(V) and V.

proof (in "K", that is, MK) -- again, loosely --

Lemma There is a function W on V (instead of U, for reasons which seem clear), such that for each set x, W(x) is a bijection from an ordinal onto x.

Define, by transfinite recursion,

$W(x)(\alpha )=c\left(x-\left\{W(x)(\beta )\mid \beta <\alpha \right\}\right)$

Then define, by transfinite recursion,

$V_{\alpha }=\bigcup _{\beta <\alpha }P(V_{\beta })$

For any set x, define the rank of x by:

$\rho (x)=$ the first $\alpha$ such that $x\in V_{\alpha }$.

Define R, by

x R y iff $\rho (x)<\rho (y)\lor (\rho (x)=\rho (y)\wedge (W(V_{\rho }(x))^{-1}(x)<(W(V_{\rho }(x))^{-1}(y))$

R is a well-ordering of the universe with order type On (See WE 4S in the reference below.) Finally, for any proper class X, R restricted to X is also a well-ordering of X with order type On, so that any two proper classes are equivalent.

(More detailed proofs of the implication can be found in Equivalents of the Axiom of Choice, H. Rubin & J. Rubin, with the additional note that any model of MK is also a model of NBG; Kelley's choice is approximately AC 1S in that book, while the axiom of limitations is approximately P 1S and clearly follows from WE 5S.

I don't know if this is something we want to move up to the main body, or not. Arthur Rubin | (talk) 00:41, 25 January 2006 (UTC)

Careful study shows that κ₁ need not be inaccessible, so the "counterexample" can be constructed relative to (MK+1 inaccessible), rather than (MK+2 inaccessibles). Arthur Rubin | (talk) 15:30, 25 January 2006 (UTC)

my guess would be that (the way the article is put together now) the fact that Kelley's axioms prove Limitation of Size would be of interest to the reader, but the proof can be left here. The fact that it doesn't hold with urelements is fun but perhaps too technical? Randall Holmes 17:39, 25 January 2006 (UTC)

thanks

thanks for the comments; I'll look. I didn't say anything about what could happen with urelements, and I'm not surprised if weird things happen :-) If the Kelley axioms imply Limitation of Size, I'm pleased (I don't think I say that they do or don't, do I?) Randall Holmes 01:02, 25 January 2006 (UTC)

Axiom of Pairs redundant

Is the Axiom of Pairs necessary? It seems to me that Limitation of Size, Class Comprehension, and Infinity suffice to imply it. For any sets x and y, we have from Class Comprehension a class containing only x and y; from Limitation of Size, this will be a proper class only if the universe contains no more than two sets; and from Infinity, the universe contains more than two sets. Therefore, the pair set {x, y} must exist. Just a minor piddling thing, but I was curious if I missed something here, since the article leaves out the Axiom of the Empty Set and notes why that can be done, but does not do so with regard to the Axiom of Pairs. -Chinju 15:12, 13 June 2006 (UTC)

Your argument seems correct to me. But sometimes it is better for clarity to include redundant axioms rather than try to make do with a minimalist set. Personally, I would include the axiom of empty set also rather than derive it. If a theorem is more obviously true than the "axioms" from which it is deduced, it would make sense to just declare it an axiom in its own right. JRSpriggs 03:26, 14 June 2006 (UTC)

I tend to agree with that line of thought (especially insofar as it makes for a more "modular" design; i.e., it allows us to then consider alternative systems where, say, Infinity has been removed without losing Empty set and Pairs, or such things). However, just given that the article as given seemed to be attempting a minimal axiomatization and falling clearly short, I thought I'd make sure I wasn't missing anything. -Chinju 16:43, 14 June 2006 (UTC)

This is not correct. We need axiom of pairs, to define Cartesian products, relations, function, injections that are necessary for axiom of limitation of size to work. Therefore we cannot get rid of pairing. —Preceding unsigned comment added by 72.27.119.116 (talk • contribs)

That depends on exactly how the axiom of limitation of size is worded. If the injective "function" is given by a formula of set theory with two arguments for the element being mapped and its image, then the axiom (shema) could be formulated without having an axiom of pairing as a prerequisite. JRSpriggs 08:55, 24 June 2007 (UTC)

I know of three published first order logic axiomatizations of MK: Rubin (1967), Monk (1980), and Mendelson (1997) (NBG with a 1 page supplement on MK). All three axiom sets feature Pairing, and none mentions its possible redundancy.Palnot (talk) 10:05, 21 April 2008 (UTC)

Writing Morse-Kelley

M.K can be further simplified to:

M.K is the set of sentences entailed (from first order logic with identity) by these axioms:

1) Extensionality: AxAy(x=y<->Az(zex<->zey)).

2) Regularity:Ax((Ez(zex))->Ey(yex & ~Ec(cey & cex ))).

3) Class comprehension: If P is a formula in which x doesn't occur free , then all closures of

ExAy(yex<->(P(y)&Ez(yez)))

are axioms.

Definition 1) x=V <-> Ay(yex <-> Ez(yez)).
Definition 2) x is a set <-> xeV 
Definition 3) x is a proper class <-> ~Ey(xey).
Definition 4) x=0 <-> Ay(~(yex)) 

Accordingly V is the proper class of all sets.

4) Pairing:AaeVAbeVExeVAyeV(yex<->(y=a or y=b)).

5) Union:AaeVExeVAyeV(yex<->EzeV(zea&yez)).

6) Infinity:ENeV(0eN&(Ax(xeN->xU{x}eN))).

with 'U' and {x} having the usual definitions.

7) limitation of size:

Ax((Ez(xez)) <-> x is subnumerous to V).

x is subnumerous to V <-> Af((f:x->V) ->(f is injective & ~ f is surjective)).

8)Power: AaeVExeVAyeV(yex<->AzeV(zey->zea)).

Zaljohar 03:56, 4 March 2007 (UTC)

Rubin (1967)

I thought she used NBGU, rather than MKU. (As her son and probable heir to the very small income stream from the book, I wouldn't have added it to the article, myself.) My copy doesn't seem to be here at the moment, so I can't check. — Arthur Rubin (talk) 20:58, 19 April 2008 (UTC)

I am very pleased that Jean Rubin's son is taking a close interest in this entry. I completely agree that her theory included urelements, but that alone is no reason for omitting her book from the reference section. One of us needs to check whether her class theory was NBG or MK. If the former, go ahead and remove her book from the references.

In any event, I am disappointed that in the half century since Kelley (1955), there has been at most one leisurely textbook treatment of MK. I am quite surprised that MK has yet to catch on. We all know that building up set theory and math from ZFC requires some weird contortions. Meanwhile, MK has a fine pedigree; Kelley was neither logician nor foundationalist, but an awesome working mathematician, educator, and political idealist. Morse (1965) is written in such a way that it merits a cult following. The classic text Mendelson (1997) says kind things about MK, in particular that it is friendly to the mathematician who wants to get on with his work and not wallow and set theory. And am I correct in believing that MK suffices for category theory?

Unrelated point. I can't make sense of this entry's description of Kelley's version of Class Comprehension. One more reason to trudge to the library at the first opportunity.Palnot (talk) 05:47, 20 April 2008 (UTC)

I have just confirmed that the axiomatic set theory of Rubin (1967) and Monk (1980) is indeed MK. In Rubin, this is clear only because her discussion of Class Comprehension includes a footnote describing NBG's predicativity restriction, implying that her version of the schema is impredicative. Monk, who studied at Berkeley under Kelley and Morse, is more explicit. On the other hand, I have just discovered that the library I use has no copy of Kelley (1955). Rats! Palnot (talk) 04:26, 21 April 2008 (UTC)

Thank you JR

Thanks to JRSpriggs for adding formal versions of the axioms to this entry. Would you please give a source? All axioms but Class and Comprehension are identical to those for NBG, yet the axioms you have added differ from the NBG axioms in Mendelson (1997), mainly in being more complicated. Note also that this entry is committed to a one-sorted logic (a choice I did not make), abstaining from using upper (lower) case for variables ranging over classes (sets). Either the formal axioms have to change, or the prose of this entry has to be revised to allow for a two-sorted logic. I do not object to the latter choice.

I also think that the entries for NBG and MK should have a common set of formal axioms, Class Comprehension excepted. I propose that this set of common axioms be incorporated into the entry for NBG. The MK entry would then state only one formal axiom, Class Comprehension, and refer readers desiring the other formalized axioms to the NBG entry.Palnot (talk) 20:47, 20 April 2008 (UTC)

If MK is taken to be one-sorted and NBG to be two-sorted, then merging the axiom lists would not be practical. I copied the axioms from the relevant articles on those axioms and then modified them for class theory, i.e. to agree with the English text. I did not make any distinction between upper and lower case letters. If you want to fold them all to upper case to show that they are class variables, then please feel free to do so. JRSpriggs (talk) 03:15, 21 April 2008 (UTC)

If MK can be formulated as one-sorted with a sethood predicate, then so can NBG, no? If you agree, then we can take all variables as class variables by default, writing them using lower case and freely using the Mx sethood predicated where needed. I submit that that is the best way to go, but admit that that is not the way Mendelson (1997) exposits NBG. If I understand you, you deem the natural language version of these axioms as dog and the FOL versions as the dog's tail; I think the other way.Palnot (talk) 04:38, 21 April 2008 (UTC)

The version of the axiom of power set for ZFC (sets alone) is:

$\forall a\,\exists p\,\forall b\,[b\in p\leftrightarrow \forall c\,(c\in b\rightarrow c\in a)]$

We need to modify it for a class theory. If we modify it to read like the English statement "Given a set A, if P is a class whose members are all possible subclasses of the set A, then P is a set.", then we get:

$\forall A\,\forall P\,[(MA\land \forall x\,[x\in P\leftrightarrow \forall y\,(y\in x\rightarrow y\in A)])\rightarrow MP].$

Alternatively, we could try to stick closer to the original, saying "Given any set A, there is a set P such that, given any set B, B is a member of P if and only if B is a subset of A.":

$\forall A\,(MA\rightarrow \exists P\,(MP\land \forall B\,[B\in P\leftrightarrow (MB\land \forall C\,(C\in B\rightarrow C\in A))]))$

Similarly for the axiom of union. Would you prefer this? However, this alternative is somewhat redundant with the axiom schema of comprehension because it asserts the existence of the class as well as its sethood. JRSpriggs (talk) 05:18, 21 April 2008 (UTC)

I have given the axioms my best shot; see entry. I have employed lower case throughout, except when a variable is free to range over the proper classes (because it never appears to the left of an ∈ or to the right of an M). Incidentally, I very much prefer limiting upper case to predicate letters; I share the old fashioned preference for first order theories. I took the monadic sethood predicate is from Mendelson (1997).Palnot (talk) 10:01, 21 April 2008 (UTC)

Strong axioms versus weak axioms?

There is a philosophical issue that I would like us to consider — should each separate axiom be formulated in: the strongest possible form, the weakest possible form, or some other form (simplest?)? In the strongest form, it would try to do its job without relying on help from other axioms. This would be advantageous for practical use of the axioms and for constructing sub-theories where some axioms are removed. In the weakest form, any redundant aspects (such as existence of the class for axioms other than class comprehension) would be removed. This would be useful for proving that some model satisfies certain axioms and, perhaps, establishing the independence of an axiom from the others (or the consistency of its negation with the others).

Specifically, the axioms of pairing, power set, union, and infinity each have at least two forms one of which is stronger than another. That is, they may assert the existence of the class which is the set in addition to its set-hood, or merely assert its set-hood. The axiom of infinity may also assert or not the existence of the empty class and successor classes; or merely say that if they exist and are sets, then they belong to the infinite set. JRSpriggs (talk) 14:25, 25 April 2008 (UTC)

Second order ZFC

I do not unterstand the phrase : " whatever is true in all models of second-order ZFC in which the classes are all the collections of the sets, is also provable (because the logic is second-order). "

What does "all the collections of the sets" mean ? How can we say - in second order logic - that all is true in some context is provable? Could someone enlight my lantern, and give some reference? Thank you.--Michel42 (talk) 17:16, 15 August 2008 (UTC)

It's certainly not true that anything that is true in all second-order models is provable; I removed that claim from the article. — Carl (CBM · talk) 17:52, 15 August 2008 (UTC)

Palnot (talk · contribs) changed "valid" to "provable" at

http://wiki.riteme.site/w/index.php?title=Morse%E2%80%93Kelley_set_theory&diff=206755216&oldid=206735518

JRSpriggs (talk) 09:03, 16 August 2008 (UTC)

strength

What does it mean that MK is stronger than ZFC? Are there sentences in the signature of ZFC, that are independent of ZFC but that are theorems of MK? Especially, I wonder if MK proves any arithmetic sentences that are independent of ZFC. Can something be added about this? 67.117.147.144 (talk) 06:33, 30 May 2011 (UTC)

Absolutely. KM (that's the order I'm used to seeing it — I have no idea whether Kelley or Morse actually deserves more credit) proves the consistency of ZFC, which can be represented as a Π⁰₁ statement of arithmetic ("for every n, n is not the Goedel number of a ZFC-proof of 0=1"). In fact it proves Con(ZFC+Con(ZFC)), Con(ZFC+Con(ZFC+Con(ZFC))), and so on (for some value of "and so on"). However it does not prove Con(ZFC+"there exists an inaccessible cardinal").

I am not aware, though, of any "natural" statement of arithmetic that is provable in KM but not ZFC, and I would be surprised to learn of one. --Trovatore (talk) 07:18, 30 May 2011 (UTC)

Yes, it should be possible to prove some reflection principle according to which given a bound, all sentences of complexity below that bound about sets that are true in the universal class of MK are also true in the set V_κ for some ordinal κ. From this one should be able to get that $C_{\alpha }=\operatorname {Con} ({\text{ZFC}}\land \forall \beta <\alpha \,C_{\beta })$ is provable for recursive ordinals α (such as epsilon zero) less than the proof theoretic ordinal of ZFC. JRSpriggs (talk) 11:13, 30 May 2011 (UTC)

Peculiarity?

It's a minor point, but why in 'domain f and range f denote the domain and range of the function f; this peculiarity has been carefully respected below;' is the word 'peculiarity' used? — Preceding unsigned comment added by 213.122.37.54 (talk) 20:50, 18 October 2012 (UTC)

Probably because it would be more usual to say "the domain X of the function f " in which "X" refers to the domain rather than the function. JRSpriggs (talk) 08:23, 19 October 2012 (UTC)

Axiom of Infinity can assert setness instead of existence

It is noted in the article that "p and s in Power Set and Union are universally, not existentially, quantified, as Class Comprehension suffices to establish the existence of p and s. Power Set and Union only serve to establish that p and s cannot be proper classes."

The same thing holds of the axiom of infinity - namely, that Class Comprehension suffices for the existence of an infinite class, and we need only assert that one such class is a set - and I think this should be mentioned.

This isn't quite clear from the axiom as it stands in the article, since it only asserts the existence of *an* inductive set, and not *the* set of the finite ordinals. However, it is clearly equivalent to assert the existence of ω, and there are indeed first order characterizations of the finite ordinals (see, for example, Axiom of infinity#Extracting the natural numbers from the infinite set).

By the way, this phenomenon - that most of the axioms of set theory follow from comprehension - is mentioned in Axiom schema of specification#Unrestricted comprehension. Perhaps that should be linked to? — Preceding unsigned comment added by 2607:F2C0:9437:A401:8559:59BC:5C45:B7A1 (talk) 18:03, 31 August 2016 (UTC)

Yes, one could replace the current version of the axiom of infinity by

$\forall \omega (\forall n(n\in \omega \leftrightarrow (Mn\land [n=\emptyset \,\,\lor \,\,\exists k(n=k\cup \{k\})]\,\,\land \,\,\forall m\in n[m=\emptyset \,\,\lor \,\,\exists k\in n(m=k\cup \{k\})]))\rightarrow M\omega )$

and similarly one could replace the current axiom of pairing by

$\forall x\,\forall y\,\forall z\,[(Mx\land My\land \forall s\,[s\in z\leftrightarrow (s=x\,\lor \,s=y)])\rightarrow Mz]$.

However, without a reference to support those version, I would hesitate to do so. JRSpriggs (talk) 00:42, 1 September 2016 (UTC)