@user21820 Your assertion is categorically false in systems that reject the law of the excluded middle or allow for an uncountable number of truth values :p

Does Cantor's theorem hold for proper classes (and their powerclasses)?

That is, let $f$ be a (proper-class-sized) function from a class $A$ to its power class $\mathcal{P}(A)$. Can $f : A \rightarrow \mathcal{P}(A)$ be surjective?

For example, is the identity function not surjective if $A$ is the universe $V$?

@DavidReed Which assertion? I really have no idea what you're referring to.

@user2103480 That's the only way I know to be able to state the "positive" syntactic constraint. The intuitive idea is that if the defining formula makes you include some member into the set, then you never need to take it out later.

@user2103480 Yes; inductive definitions are generally like this. Yea, the idea is that we would like to extend normal specification in a uniform well-motivated manner to encompass both positive specification and inductive specification without reaching unsoundness, and the hope is that we can replace replacement by this new general specification and still get a lot of useful results that previously required replacement.

@user76284 Why not expand out into a ZFC statement and see whether the standard proof goes through? ( f : A→P(A) ) essentially means a definable f : A→(A→bool), equivalently f : A^2→bool. Let g = ( A x ↦ ¬f(x,x) ), which is a definable function of type A→bool. If f captures a definable surjection, then let c∈A such that g = ( A x ↦ f(c,x) ), and so f(c,c) ≡ g(c) ≡ ¬f(c,c). Therefore...

@user76284 Ah I see why you have this confusion. In ZFC a class is merely a property over ZFC (a 1-parameter sentence), and V of course does not have members that capture every possible class. Worse still, ( V x ↦ x ) is not even a candidate for the Cantor theorem for classes, since its signature is wrong!

The analysis carries over into class theories like NBG and MK, since every definable function over ZFC is captured by a class in NBG. So you literally have that there is no definable surjection from V to subclasses of V. But that may sound strange, especially for NBG, where the classes can really be just the definable ones, in which case there are only countably many of them, so why shouldn't there be a definable surjection from V onto classes?

This is an instance of what I call syntactic Cantor's theorem, and you can contemplate a particular instance for PA (no set theory is even needed):

@MaliceVidrine @user2103480 @LeakyNun: I'm sorry I made a slight error in my definition of positive specification. I wrote:

> If Q is a 2-parameter prenex disjunctive normal form sentence, and the sentence Q(x,S) has no atomic literal of the form "¬v∈S", we say that Q is positive in the 2nd parameter.

That's not enough; we cannot just forbid negation of membership in S; we must not allow S on the other side of "∈" too. So the correct definition is:

> If Q is a 2-parameter prenex disjunctive normal form sentence, and every atomic literal in the sentence Q(x,S) that uses "S" is of the form "v∈S" for some term v, then we say that Q is positive in the 2nd parameter.

To show that this is important, consider S = { x : x∈{0} ∧ S=∅ } which would have been allowed under the faulty definition and yields a contradiction.

Actually I'm not sure about "S∈...". My proof just doesn't work, but I can't think of a counter-example if just negated membership in S and equality with S are forbidden.

@user21820 hi

@user21820 it seems really weird to combine induction and specification, since induction generates a (possibly) larger set and specification cuts things out

@user2103480 - I'm not sure that's true. After all, in ZFC the axiom of infinity works by creating at least one set that you can cut the right inductive set out of. Cutting-out seems like a fine strategy for things defined by a minimality condition.

Ok, fair, but in an axiom that is inherently "specification" we create only subsets of some chosen set

So to get induction, we first need to obtain large enough set so that we can "cut out" the smalles inductive set

Alright, I kinda disregarded all the other axioms we have at hand, so its of course not that simple

@user21820 I was just f&*king with you....was my way of saying hello. I think it's been nearly a year since we've spoken.

heya

does anyone have a recommendation for an introductory course on modal logic?

please no philosophy books

@ShaVuklia - Check out the bibliography on this: matematikkoyu.org/docs/ModalLogicLectureNotes.pdf

At least a couple of those are math/theoretical comp sci books rather than philosophy.