3 ms·

The thing I find really aesthetically pleasing about NF is how it adjusts the axiom of subset selection so that "the set of all sets" doesn't cause Russell's pa

The thing I find really aesthetically pleasing about NF is how it adjusts the axiom of subset selection so that "the set of all sets" doesn't cause Russell's paradox. Basically it requires that the predicates you use to select subsets must obey a certain very lightweight type system. "x is not a member of itself" is not a well-typed question under any reasonable type system, and in particular it doesn't satisfy NF's "stratifiability" requirement, so you can't use it to construct the Russell's-paradox set of all sets which do not contain themselves.

juped 2y ago
You just move the sorts around, you don't get rid of having to have sorts. I guess a rug with dirt swept under it is more aesthetically pleasing than a rug with dirt on top of it?
- epgui 2y ago
  There is no notion of types in naive set theory.
  - juped 2y ago
    No one said anything about either types or naive set theory.
psychoslave 2y ago
That sounds extremely underwhelming to my mind. Like having a programming language sold as free of any awful metaprogramming constructions (and induced headaches) through guarantees that no metaprogramming at all can be done in it. A language that forbids to talk about its own grammatical structures is doomed to see its users abandon or extend it when they will inevitably deal with a situation where exchanging about the communication tool at hand is required to appropriately deal with its possibilities, expectable behaviors and limits.
- epgui 2y ago
  Your comment doesn't make any sense. Also: > A language that forbids to talk about its own grammatical structures That's just not the case, and it's not what is being claimed here.
  - psychoslave 2y ago
    I’m not acquainted with NF, but to my perspective what the comment I was replying to was suggesting is that the structures can’t express anything about a structure of the same level of comprehension. Which, to my mind, implies that an expression should not be allowed to embed an expression. Which is roughly equivalent to disallow a code to embed code written in the same language, let alone a code aware of the language structure and able manipulate the current code base abstract syntax tree or any equivalent facility. Once again, I don’t claim this about NF, which I wasn’t aware of before this thread. I never dug into Quine’s work to be transparent on the matter.

juped 2y ago

You just move the sorts around, you don't get rid of having to have sorts. I guess a rug with dirt swept under it is more aesthetically pleasing than a rug with dirt on top of it?

epgui 2y ago
There is no notion of types in naive set theory.
- juped 2y ago
  No one said anything about either types or naive set theory.

psychoslave 2y ago

That sounds extremely underwhelming to my mind. Like having a programming language sold as free of any awful metaprogramming constructions (and induced headaches) through guarantees that no metaprogramming at all can be done in it. A language that forbids to talk about its own grammatical structures is doomed to see its users abandon or extend it when they will inevitably deal with a situation where exchanging about the communication tool at hand is required to appropriately deal with its possibilities, expectable behaviors and limits.

epgui 2y ago
Your comment doesn't make any sense. Also: > A language that forbids to talk about its own grammatical structures That's just not the case, and it's not what is being claimed here.
- psychoslave 2y ago
  I’m not acquainted with NF, but to my perspective what the comment I was replying to was suggesting is that the structures can’t express anything about a structure of the same level of comprehension. Which, to my mind, implies that an expression should not be allowed to embed an expression. Which is roughly equivalent to disallow a code to embed code written in the same language, let alone a code aware of the language structure and able manipulate the current code base abstract syntax tree or any equivalent facility. Once again, I don’t claim this about NF, which I wasn’t aware of before this thread. I never dug into Quine’s work to be transparent on the matter.