Questions tagged [new-foundations]

New Foundations is the axiomatic set theory in Quine's 1937 article "New Foundations for Mathematical Logic"; it simplifies the theory of types of Principia Mathematica.

Filter by
Sorted by
Tagged with
25 votes
1 answer
2k views

Can you have a type theory where there is type of all types?

Normally in a type theory, you can not have a type of all types, due to Girard's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets. Therefore, usually you just ...
Christopher King's user avatar
21 votes
5 answers
4k views

How much of ZFC does Quine's New Foundations prove?

Main Question: Does anyone know of a reference that can tell me which axioms of ZFC Quine's New Foundations prove, disprove, and leave undecided? Secondary Question: I've read that diagonal ...
Amit Kumar Gupta's user avatar
18 votes
10 answers
7k views

Set theory and alternative foundations

Every foundational system for mathematics I have ever read about has been a set theory, from ETCS to ZFC to NF. Are there any proposals for a foundational system which is not, in any sense, a set ...
psihodelia's user avatar
17 votes
7 answers
2k views

Understanding Specker's disproof of the axiom of choice in New Foundations

Hi all! I am trying to understand Specker (1953)'s proof (found here) that the axiom of choice is false in New Foundations. I am stuck on the following point. At 3.5 Specker writes: 3.5. The cardinal ...
Nick Thomas's user avatar
17 votes
0 answers
434 views

The free complete lattice on three generators, beyond ZF

This was originally asked at MSE; although it is still under bounty it seems unlikely to be answered there. $\mathsf{ZF}$ proves that there is no free complete lattice on three generators since any ...
Noah Schweber's user avatar
14 votes
4 answers
2k views

Where is the end of universe?

In some sense the empty set ($\emptyset$) and the global set of all sets ($G$) are the ends of the universe of mathematical objects. The world which $ZFC$ describes has an end from the bottom and is ...
user avatar
13 votes
1 answer
380 views

What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?

On the Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories, it is stated without reference that bare $\mathsf{NFU}$ (i.e., $\mathsf{NFU}$ without the axiom of infinity) ...
James Hanson's user avatar
  • 10.3k
13 votes
0 answers
519 views

Large cardinals arising from alternate set theories

My question is whether there are model-theoretic large cardinal axioms associated with $NFU$ - or more generally, with set theories other than $ZFC$. Large cardinal properties generally come in one ...
Noah Schweber's user avatar
10 votes
2 answers
690 views

Constructible models of New Foundations?

Hi all! Is there anything like Gödel's constructible universe for New Foundations? More precisely, I would like a process for taking a model $M$ of NF, and using it to build a model $L \subseteq M$ ...
Nick Thomas's user avatar
10 votes
2 answers
650 views

New Foundations and weaker forms of choice

New Foundations (introduced by Quine) proves that $AC$ is false. Out of curiosity, is $NF$ consistent with countable choice or dependent choice? What's the strongest consequence of choice still ...
Rachid Atmai's user avatar
  • 3,756
9 votes
2 answers
547 views

Definitions of ordinal besides von Neumann & Frege-Russel?

So my Google-fu didn't show any references on this. I'm studying an obscure set theory (ML, a variation on NF with proper classes) and it seems to not deal well with the standard definitions of ...
Malice Vidrine's user avatar
8 votes
1 answer
773 views

A question about Quine's set theory NF.

This question might not really be considered appropriate for mathoverflow.net but I'll risk asking it and apologize in advance if I have commited a booboo. It is often said that in NF one can prove ...
Garabed Gulbenkian's user avatar
7 votes
0 answers
233 views

New Foundations in a Homotopy/Intuitionistic Type Theory form?

New Foundations is a famously odd set theory suggested by Quine in the 1930s which: Features a universal set. Disproves the axiom of choice. Proves the existence of an infinite set by a trivial ...
wlad's user avatar
  • 4,823
6 votes
1 answer
363 views

What drawbacks are there to using NF(U) for category theory?

In category theory, you often run into what is known as "size" issues. That is, you run into the issue that the categories you try to define are too "big" to be sets, and so you need to use classes or ...
Christopher King's user avatar
6 votes
1 answer
227 views

Strengthening Quine's New Foundations with a more flexible stratification criterion?

Let's say that a formula in the language of set theory is flexibly stratified iff there exists a function $f$ from variable symbols to $\omega$ such that if $x=y$ appears in the formula, then $f(x)=f(...
Dylan Pizzo's user avatar
6 votes
1 answer
513 views

Intersection of iterated powerset in NFU

I am interested in the existence of the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ for any given set $x$, in the context of NFU (New Foundations with Urelements). It seems to me that the ...
Marcos Cramer's user avatar
5 votes
1 answer
417 views

In search of a set theory with specific properties

I'm in search of a set theory that satisfies the following requirements. There is a universal set $V$ such that $\forall x(x \in V)$. So for example, $V \in V$. Sets whose elements are 'large' exist. ...
goblin GONE's user avatar
  • 3,693
5 votes
1 answer
884 views

New foundation in homotopy type theory

Is there any model of NF (New Foundations) on HoTT (homotopy type theory)? Because there is a model of ZF(C) on HoTT (The HoTT book, Section 10.5) and NF on ZFC (by this Wikipedia articile), I think ...
H Koba's user avatar
  • 369
4 votes
2 answers
506 views

Anti-foundational set theory with a universal set

There are alternative set theories that allow for a universal set, e.g. NF(U), positive set theory and and topological set theory. There are also alternative set theories like ZFA that allow for the ...
Marcos Cramer's user avatar
4 votes
1 answer
645 views

Does Tarski's squaring theorem imply Axiom of Choice in NFU?

I'm trying to see which results from mainstream set theory (ZF) about Axiom of Choice can be proved in New Foundations with Urelements (U is added simply because ...
Veky's user avatar
  • 341
3 votes
2 answers
492 views

Can we write Tangled Type Theory without reference to type sequences?

I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the ...
Zuhair Al-Johar's user avatar
3 votes
0 answers
115 views

If NF is consistent, then is this form of Extensionality consistent with Stratified Comprehension?

Let's work in Quine's $\sf ML$, we can define classes after nonstratified formulas. Now for every set $X$ we can define the membership graph $\operatorname {MG}(X)$ on its transitive closure, that is ...
Zuhair Al-Johar's user avatar
2 votes
1 answer
501 views

Is there anything against this function j being injective?

Language (first order logic with equality "$=$" and membership "$\in$", and constant symbol "$j$") Axiom: ID axioms + There exists a set $A$, such that: Field: $\forall x \in j \ \exists a \in A \ \...
Zuhair Al-Johar's user avatar
2 votes
0 answers
48 views

Is $\sf NF(U)$ interpretable in $\sf NF(U)-0$?

It is known that in $\sf ZFC$ related theories one can remove the the empty set axiom and foundation, stipulate that all sets are nonempty, axiomatize replacement and separation in such a manner that ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
122 views

Does the consistency of $\sf NF$ enable us to transfer its cardinal comparisons to the inside of $\sf Z$?

I think that stratified comprehension has the potential to breach Cantor's arguments about the relative size of sets and their powers, this has been done to an extent in $\sf NFU$ and the known ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
120 views

Can the well founded world of NFU be itself the hereditarily Cantorian world and also satisfy ZFC?

Is it possible to squeeze the hereditarily Cantorian world "$\sf H_{Cant}$" of $\sf NFU$ be the well founded world $\sf WF$ of $\sf NFU$. Moreover, can we have $\sf WF$ of $\sf NFU$ to ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
299 views

Is there a clear inconsistency with this system that would interpret NF?

This is a first order set theory, with the purpose of interpreting $\sf NF$ set theory: Extensionality: $\forall X \forall Y: \forall z (z \in X \leftrightarrow z \in Y) \implies X=Y$ Pairing: $\...
Zuhair Al-Johar's user avatar
2 votes
0 answers
305 views

Can this external injection into a set from its power set, be not isomorphic on membership?

Add a primitive partial unary function symbol $F$ to the first order language of set theory. Working in Zermelo (Separation restricted to the language of set theory), add the following axioms: $F$ ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
154 views

Can we add $NF$ to Ackermann's set theory?

Can we simply add stratified comprehension $SF$ to axioms of Ackermann's set theory $Ack$? Is there a clear argument of inconsistency involved with such addition? supposing that $NF$ and $Ack$ are ...
Zuhair Al-Johar's user avatar
2 votes
0 answers
230 views

Can we have the well founded world of NF obeying ZF?

The following question is about the possibility of having a world of sets obeying new foundations "NF" with their well founded sets obeying rules of ZF. It uses the revised version of Quines ...
Zuhair Al-Johar's user avatar
1 vote
1 answer
398 views

NF and incompleteness

Are there any well-known statements independent of NF? And also, are there prerequisites suggesting that NF in any way, to one extent or another, are not covered by the incompleteness theorem?
PaleChaos's user avatar
1 vote
1 answer
222 views

Can $\mathsf{TNT}$ be modeled in non-well-founded models of $\mathsf{ZF}$?

The theory $\mathsf{TNT}$, introduced by Hao Wang in 1952, adds negative types to simple Type Set Theory $\mathsf{TST}$, so it's written exactly as $\mathsf{TST}$ but with the type indices ranging ...
Zuhair Al-Johar's user avatar
1 vote
0 answers
42 views

Is stratified sorted rendering of naive set theory equivalent to tangled type theory?

I think the most important point in stratification is to have what may be called a fixed membership type distance per variable. What I mean is that if a variable $x_i$ occurs in a stratified formula $\...
Zuhair Al-Johar's user avatar
1 vote
0 answers
46 views

Can we add the singleton map to $\sf NFP$?

In $\sf NF(U)$ it is known that the singleton map $(x \mapsto \{x\})$ is not a set, which is a source of a lot of extremely counter-intuitive results in $\sf NF(U)$. However, a weakening of the ...
Zuhair Al-Johar's user avatar
1 vote
0 answers
113 views

Can all relations and functions be implemented as sets in some fragments of set theory?

Define wholly stratified $\sf NF$ to be $\sf NF$ with its language restricted to stratified expressions. In this theory we can arrive at a general implementation of tuples, that is: $\langle x_1,..,...
Zuhair Al-Johar's user avatar
1 vote
0 answers
65 views

Is existence of external rank shifting automorphism proves moving of infinitely ranked stratified power stages of this theory?

In this posting, I've define stratified power sets $\mathcal P^\equiv$ operator. Now we define $V^\equiv_\alpha$ as the iterative stratified power sets of $V_\omega$ as: $$V^\equiv_0 = V_\omega \\ V^\...
Zuhair Al-Johar's user avatar
1 vote
0 answers
41 views

What is the proof in NFU+|Ur|>|Set| of having less sets of sets than sets of Ur-elements?

Working in $\text{NFU}$, let $Ur$ be the set of all empty objects except a specific empty object $\emptyset$ that stands as the empty set, let $Set$ be the set of all non empty objects and $\emptyset$....
Zuhair Al-Johar's user avatar
1 vote
0 answers
254 views

Is there a non-trivial consistency preserving transformation?

In ‎set ‎theory ‎"equiconsistency" (and not "consistency") ‎of ‎the ‎theories ‎is the‎ ‎main ‎part ‎of ‎researches. ‎So ‎we ‎usually ‎try ‎to ‎construct a‎ ‎new model ‎using a‎ ‎given ‎one. ‎In ‎the ‎...
user avatar
0 votes
1 answer
566 views

Can Godel's incompleteness theorems be in some sense circumvented this way?

New foundations "NF" (formulated in the language of $\small \sf FOL(\in)$), can define a kind of ordered pair relation $``\rho"$ such that we can have a set $E$ of those pairs where NF proves the ...
Zuhair Al-Johar's user avatar
0 votes
1 answer
241 views

Is Cantor-Bernstein-Schroeder theorem for skew cardinality, consistent with NF?

Define: $n$-skew pair of $x,y$, denoted by $\langle x,y \rangle^n$, as: $(singleton^n(x), y)$ Define: $(-n)$-skew pair of $x,y$, denoted by $\langle x,y \rangle^{-n}$, as: $(x, singleton^n(y))$ ...
Zuhair Al-Johar's user avatar
0 votes
1 answer
277 views

Is this theory equivalent to Tangled Type Theory?

Language: Multi-sorted first order logic with equality and membership, where for each natural $n$ we have variables $x_i^n$ of sort $n$, and for each decidable monotonic strictly increasing sequence ...
Zuhair Al-Johar's user avatar
0 votes
1 answer
82 views

Can global failure of Extensionality in fragments of NFU permit existence of singleton relation set?

Let $SF$ be the schema of stratified comprehension. Take the theory $SF + Infinity + Choice + \text {Extensionality fails everywhere}$ Is the following consistent with this theory? $\exists \iota \...
Zuhair Al-Johar's user avatar
0 votes
4 answers
531 views

Consistency of the concept of the collection of all collection

By Russel's paradox, we know that the concept of the set of all sets is inconsistent. Similarly, if classes have only sets as members, the concept of the class of all classes is inconsistent because ...
Gérard Lang's user avatar
  • 2,617
0 votes
2 answers
557 views

Limiting set theory using symmetry

[Cross-posted from here] If my understanding is correct, naive set theory needs to be restricted in order to avoid paradoxes including the Russell paradox. Typically, the restriction is expressed in ...
Muhammad Alkarouri's user avatar
0 votes
0 answers
105 views

Is there a clear inconsistency with this general assertion about n-internalizations of external bijections?

Define: $j^1[x]= j(x) \\ j^{n+1}[x] = \{j^n[y]: y \in x\} \\ j^{-n}[x] = \{y : j^n[y] \in x\}$ Define: $n=1,2,3,...\\ _n\mathsf{Forth}_j(S)=\{j^n[x] : x \in S\} \\ _n\mathsf{Back}_j(S)=\{j^{-n}[x] : ...
Zuhair Al-Johar's user avatar
0 votes
0 answers
189 views

What known paradoxes are associated with having a type-level tuple indexed by all ordinal numbers?

By a type-level tuple $t(f)$ that captures a function $f$, it is meant a relation that is definable by a stratified formula that assigns to $t(f)$ the same type it assigns to each element of the ...
Zuhair Al-Johar's user avatar
0 votes
1 answer
119 views

Can removal of extensionality avoid cardinality errors in stratified theories?

Let $SF$ be the schema of stratified comprehension. Take the theory $SF + Infinity + Choice + \text {Extensionality fails everywhere}$. Are the following consistent with this theory? $\forall X (|...
Zuhair Al-Johar's user avatar
0 votes
0 answers
166 views

Is this fragment of NF known to be consistent?

The following theory is a fragment of $\small \sf NF$. My question is about if it is known to be consistent without assuming the consistency of $\small\sf NF$. The language is of first order logic ...
Zuhair Al-Johar's user avatar
0 votes
0 answers
369 views

Is there a known shorter axiomatization of NF than this?

Is there an already known axiomtization of $NF$ that is shorter than the following axiomatic system in first order logic with equality $``="$ and membership $``\in"$? And what is exactly meant by ...
Zuhair Al-Johar's user avatar
-1 votes
1 answer
172 views

Is there an obvious inconsistency with this extension of Tangled Type Theory?

This posting is a follow up of this Language multi-sorted FOL, with sorts (types) indexed by the naturals, equality symbol restricted to same type, while membership symbol restricted from lower to ...
Zuhair Al-Johar's user avatar