Talk:Inhabited set

"nonempty, noninhabited set"

This is confused. Do not try to prove "there is a nonempty, noninhabited set". A noninhabited set is empty! --Unzerlegbarkeit (talk) 02:40, 12 April 2010 (UTC)[reply]

It's a subtle point. A set is X is:

nonempty if X is not empty, i.e.

\lnot (\lnot \exists z(z\in X))

inhabited if there is a witness to the nonemptyness:

\exists z(z\in X)

So inhabited implies nonempty, but the converse fails in intuitionistic logic. You can see from the negations that it is plausible for it to fail, and in fact there are models in which it does. Kripke models are perfect for demonstrating this sort of thing. — Carl (CBM · talk) 02:44, 12 April 2010 (UTC)[reply]

It is unfortunate that you are distinguishing between "nonempty" ("not all sets are excluded from X")and "inhabited" ("there is a set included in X") but dismissing the distinction between "not all nonempty sets are inhabited" and "there is an nonempty set which is not inhabited." --Unzerlegbarkeit (talk) 03:18, 12 April 2010 (UTC)[reply]

I can construct a Kripke model for "there is a nonempty, noninhabited set". The language has a single predicate X, representing a set. There are two nodes in the model, and they both have the same domain {a}. The root node does not think a is in X, while the child does think a is in X. According to the root node, X is a nonempty, noninhabited set. That is, the root node forces X to be nonempty but does not force X to be inhabited.

It may be that don't understand what you are trying to tell me. — Carl (CBM · talk) 03:27, 12 April 2010 (UTC)[reply]

"Does not force P" is different from "forces not-P". The root node does NOT force "X is uninhabited". Let's write this differently. I can't think what offhand, but if you and I can't get this straight, what are our dear readers supposed to make of this? --Unzerlegbarkeit (talk) 04:51, 12 April 2010 (UTC)[reply]

OK, I see what you mean now that we can refer to an actual model to clarify terminology. I was reading "noninhabited" to mean "cannot assert it is inhabited", because I would always use "empty" for the literal negation of "inhabited". That is, I was reading "noninhabited" to mean "not forced to be inhabited", rather than "forced to be empty". I'll try to change the article, let me know if it's better. — Carl (CBM · talk) 11:35, 12 April 2010 (UTC)[reply]

I see. Well, "inhabited", "empty" and "nonempty" are predicates of set theory, but "cannot assert it is inhabited" is not. Perhaps instead we can show for instance that "all nonempty sets are inhabited" implies the limited principle of omniscience, therefore it follows from church's thesis or from intuitionistic continuity principles that "not all nonempty sets are inhabited". I'm not a big fan of introducing an ad-hoc Kripke model every time we wish to show a slight variant on the same simple failure of double negation elimination. --Unzerlegbarkeit (talk) 12:39, 12 April 2010 (UTC)[reply]

Right; on reflection, I think I only use "noninhabited" as a meta-level term, and "empty" and "inhabited" as the object-level terms. There is already an example in the article using LPO (the Riemann hypothesis), except that one has to assume some sort of Markov's principle as far as I can tell. But I think that for naive readers, a Kripke model is just as easy as anything else. — Carl (CBM · talk) 13:15, 12 April 2010 (UTC)[reply]

Your change addressed my original concern. I guess I was still unhappy because I figured it's a shallow example and could apply to a bunch of other articles. But in reality, Category:Mathematical constructivism is pretty bare, so this is appropriate. Thanks. --Unzerlegbarkeit (talk) 01:34, 14 April 2010 (UTC)[reply]