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.
62 questions
2
votes
0
answers
116
views
Can we have the set world obeying Quine's New Foundations with its well-founded realm obeying $\sf ZFC$?
Is this theory consistent?
Language: first order language of set theory,
Extra-logical axioms:
1. Extensionality: as in $\sf NF$.
2. Stratified Comprehension: as in $\sf NF$.
Define: a set is said ...
- 11.3k
2
votes
2
answers
172
views
Can the Category of that kind of small sets in $\sf NFU$ be Cartesian closed?
Working in Quine's $\sf NFU$, with urelements being at least as many as sets. Formally the latter is: $|Ur| \geq |Set|$.
Where $Ur$ is the set of all urelements and $Set$ is the set of all sets. We ...
- 11.3k
6
votes
1
answer
162
views
Can there exist a set of all transitive sets in a model of NF or NFU?
Is it consistent with $\sf NF$ or $\sf NFU$ to have a set of all transitive sets? Formally:
$\exists t \forall x (x \in t \leftrightarrow x \text { is transitive})$
Where "$x$ is transitive" ...
- 11.3k
-4
votes
1
answer
139
views
About the definitions of well-foundedness in this extension of NFU that interprets ZFC?
Lets see how the world of sets could look like from the perspective of $\sf NFU$. So, here we work within the first order language of set theory, with the following extra-logical axioms:
1. Quine atom:...
- 11.3k
-3
votes
1
answer
117
views
Can stratification be used to internalize functions on models of $\sf Z$?
Suppose $M$ is a model of $\sf Z +\neg AC$ that is externally bijective to an element $k \in M$. Obviously if $j$ denotes such an external bijection, then it cannot be used in Separation within $M$, ...
- 11.3k
-1
votes
1
answer
141
views
Can stratification be used to internalize external functions inside models of $\sf ZF$?
Suppose $M$ is a model of $\sf ZF+\neg AC$ that is externally bijective to an element $k \in M$. Obviously if $j$ denotes such an external bijection, then it cannot be used in Separation and ...
- 11.3k
3
votes
0
answers
130
views
Is Quine's Mathematical Logic "ML" consistent with Azcel's Extensionality?
Now that Holmes had proven the consistency of adding Extensionality to Stratified Comprehension (i.e. $\sf NF$), a question along the same vein presents itself:
Is Aczel's Extensionality axiom ...
- 11.3k
0
votes
0
answers
70
views
Is Acyclic ZF consistent with downshifting automorphisms?
Recall the criterion of acyclic comprehension. This is shown to be equivalent to stratified comprehension for language $\sf FOL(=, \in)$, given minimal assumptions. [See here, and here].
Let Acyclic ...
- 11.3k
1
vote
0
answers
53
views
Can MLU prove symmetric comprehension?
Working in $\sf ML$$\sf U$:
Define: $x \in^f y \iff f(x) \in y$
by $\varphi^f$ we mean the formula obtained by merely replacing each "$\in$" symbol in formula $\varphi$ by the symbol "...
- 11.3k
11
votes
3
answers
2k
views
What governs our "perception?" about the platonic realm of sets?
Here, I want to delve into what do we exactly feel about what constitutes a platonic existence of a set? Or what makes us think or actually a kind of feel or sense the existence of a set in the ...
- 11.3k
0
votes
0
answers
62
views
Is stratified Z - Infinity + there is a set as big as its powerset, consistent if NF is consistent?
The question of consistency of $\sf NF$ can be seen to be equivalent to the question of whether the theory "Stratified $\sf Z$ - Regularity - Infinity + There exists a set as big as its powerset&...
- 11.3k
-3
votes
1
answer
241
views
Can we have a hybrid comprehension between Z and NF?
Hybrid Comprehension: if $\phi,\varphi$ are formulas in which $x$ doesn't occur, and $\varphi$ is stratified; then: $$ \forall A \exists x \forall y \, (y \in x \leftrightarrow \varphi \land [wf(A) \...
- 11.3k
2
votes
0
answers
60
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 ...
- 11.3k
1
vote
0
answers
57
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 $\...
- 11.3k
7
votes
0
answers
266
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 ...
- 4,943
6
votes
1
answer
276
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(...
- 395
2
votes
0
answers
134
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 ...
- 11.3k
0
votes
0
answers
106
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] : ...
- 11.3k
-1
votes
1
answer
189
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 ...
- 11.3k
3
votes
2
answers
568
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 ...
- 11.3k
1
vote
1
answer
240
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 ...
- 11.3k
4
votes
1
answer
678
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 ...
- 351
0
votes
1
answer
322
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 ...
- 11.3k
1
vote
0
answers
54
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 ...
- 11.3k
1
vote
0
answers
119
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,..,...
- 11.3k
3
votes
0
answers
125
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 ...
- 11.3k
2
votes
0
answers
123
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 ...
- 11.3k
17
votes
0
answers
509
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 ...
- 21.1k
13
votes
1
answer
436
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) ...
- 12.4k
1
vote
0
answers
66
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^\...
- 11.3k
2
votes
0
answers
305
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: $\...
- 11.3k
2
votes
0
answers
306
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$ ...
- 11.3k
2
votes
0
answers
157
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 ...
- 11.3k
1
vote
1
answer
428
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?
- 77
2
votes
0
answers
247
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 ...
- 11.3k
0
votes
0
answers
194
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 ...
- 11.3k
0
votes
1
answer
598
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 ...
- 11.3k
0
votes
1
answer
246
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))$
...
- 11.3k
0
votes
1
answer
122
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 (|...
- 11.3k
0
votes
1
answer
88
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 \...
- 11.3k
0
votes
0
answers
172
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 ...
- 11.3k
0
votes
0
answers
387
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 ...
- 11.3k
2
votes
1
answer
506
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 \ \...
- 11.3k
1
vote
0
answers
43
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$....
- 11.3k
6
votes
1
answer
530
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 ...
- 1,228
6
votes
1
answer
375
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 ...
- 6,353
27
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 ...
- 6,353
4
votes
2
answers
548
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 ...
- 1,228
5
votes
1
answer
926
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 ...
- 369
13
votes
0
answers
530
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 ...
- 21.1k