All Questions
1,136 questions
19
votes
2
answers
2k
views
Which kind of foundation are mathematicians using when proving metatheorems?
Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not....
user103598
19
votes
1
answer
1k
views
Goodstein's theorem without transfinite induction
Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the ...
user10891
19
votes
0
answers
563
views
What algebraic properties are preserved by $\mathbb{N}\leadsto\beta\mathbb{N}$?
Given a binary operation $\star$ on $\mathbb{N}$, we can naturally extend $\star$ to a semicontinuous operation $\widehat{\star}$ on the set $\beta\mathbb{N}$ of ultrafilters on $\mathbb{N}$ as ...
- 20.5k
18
votes
2
answers
3k
views
(Fictive) story of a time where people reasoned only up to isomorphism
I seem to remember reading once a story that some mathematician had written to justify the use of categories, or isomorphisms or equivalences, or something like that. The story goes something like ...
- 796
18
votes
3
answers
1k
views
Are there examples of nonconstructive metaproofs?
This came up in a question on the xkcd forums. Is it possible to have a nonconstructive metaproof, i.e. a proof that there exists a proof in some formal system which does not construct said proof? Are ...
18
votes
2
answers
1k
views
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
There have been a couple of recent questions, here and here, regarding the role of the axiom of choice in real-analytic results with applicability to general relativity. This lead me to look at some ...
- 13.1k
18
votes
3
answers
1k
views
Computable nonstandard models for weak systems of arithmetic
By Tennenbaum's theorem, PA itself does not have any computable nonstandard models. The integer polynomials which are 0 or have a positive leading coefficient form a computable nonstandard model of ...
user5810
18
votes
3
answers
2k
views
Scott-Solovay unpublished paper on ``Boolean valued models of set theory''
I have read some papers from 1970$^{th}$, and in some of them, the paper of Scott and Solovay on ``Boolean valued models of set theory'' is given as a main reference, with many references to the ...
- 32.2k
18
votes
1
answer
2k
views
Lawvere's fixed point theorem and the Recursion Theorem
Building off of Qiaochu's comment on my answer to a previous mathoverflow question, I would like to know: can the Recursion Theorem, $$\forall e\exists k[\Phi_e\text{ is total }\implies \Phi_{\Phi_e(k)...
- 20.5k
18
votes
1
answer
2k
views
What is the modal logic of outer multiverse?
The mathematical multiverse could be viewed as a gigantic Kripke model with models of $ZFC$ as possible worlds connected to each other via a certain accessibility relation.
The modal logic associated ...
18
votes
3
answers
3k
views
What's the earliest result (outside of logic) that cannot be proven constructively?
Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't).
An obvious counter-example is the law ...
- 6,353
18
votes
3
answers
1k
views
How badly does compactness fail in $\mathcal{L}_{\omega_1\omega}$?
I would like to get a better idea of how badly compactness fails in $\mathcal{L}_{\omega_1\omega}$.
Let $\Gamma$ be an arbitrary set of sentences from $\mathcal{L}_{\omega_1\omega}$. Let the ...
- 1,142
18
votes
1
answer
1k
views
Can Vopenka's principle be violated definably?
One form of Vopenka's principle (a large cardinal axiom) states that no locally presentable category contains a full subcategory which is large (= a proper class) and discrete (= contains no ...
- 66.8k
18
votes
2
answers
1k
views
Comparing "axiomatized function spaces"
This was previously asked and bountied at math.stackexchange with no response. I've also tweaked the language for clarity; see the edit history for the broader context, and note that the existing ...
- 20.5k
18
votes
1
answer
772
views
Two strengthenings of "strong measure zero"
A set $X\subseteq\mathbb{R}$ is strong measure zero if, for every sequence $(\epsilon_i)_{i\in\mathbb{N}}$ of positive reals, there is a sequence $(I_i)_{i\in\mathbb{N}}$ of open intervals covering $X$...
- 20.5k
17
votes
1
answer
960
views
Polynomial-time algorithm to compare numbers in Conway chained arrow notation
I am looking for a polynomial-time algorithm which, given a character string containing two numbers in Conway's chained arrow notation for large numbers, indicates whether the first number is less ...
- 171
17
votes
1
answer
1k
views
Are integers conservatively embedded in the field of complex numbers?
I am looking for a reference to the fact that $\mathbb{Z}$ is conservatively embedded into the field $\mathbb{C}$ of complex numbers, that is anything in $\mathbb{Z}$ which is definable in $(\mathbb{C}...
- 301
17
votes
7
answers
2k
views
Non-constructive proofs of decidability?
Are there examples of sets of natural numbers that are proven to be decidable but by non-constructive proofs only?
16
votes
1
answer
841
views
Do all countable $\omega$-standard models of ZF with an amorphous set have the same inclusion relation up to isomorphism?
In my recent paper with Makoto Kikuchi,
J. D. Hamkins and M. Kikuchi, The inclusion relations of the countable models of set theory are all isomorphic. manuscript under review. (arχiv)
we proved ...
- 236k
17
votes
2
answers
2k
views
Do the surreal numbers enjoy the transfer principle in ZFC?
The surreal field $\newcommand\No{№}\No$ is definable in ZFC, and it is easy to see that the surreal order is $\kappa$-saturated for every cardinal $\kappa$, precisely because we fill any specified ...
- 236k
17
votes
1
answer
964
views
Examples of vector spaces with bases of different cardinalities
In this question Sizes of bases of vector spaces without the axiom of choice it is said that "It is consistent [with ZF] that there are vector spaces that have two bases with completely different ...
- 173
17
votes
1
answer
641
views
How hard is it to say "not exactly $p$" with a Horn sentence?
EDIT: immediately after bountying the question (whoops ...) I found, while looking for something else entirely, that Sauro Tulipani gave an explicit algorithm for producing a Horn sentence $\varphi_p$ ...
- 20.5k
17
votes
1
answer
3k
views
Forcing in Homotopy Type Theory
I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...
- 10.5k
17
votes
2
answers
2k
views
Why are model theorists so fond of definable groups?
My PhD was on so called "pure" model theory, and my advisor was not very much interested in applications of model theory to algebra. Now I feel the need to fill in the gap, and I'd like to educate ...
- 1,031
17
votes
3
answers
3k
views
Gödel's Incompleteness Theorem and the complexity of arithmetic
In How complicated can structures be? Jouko Väänänen says:
The guiding result of mathematical logic is the Incompleteness Theorem of Gödel,
which says that the logical structure of number theory ...
- 9,720
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 ...
- 413
17
votes
2
answers
2k
views
Why is Kleene's notion of computability better than Banach-Mazur's?
In this post about the difference between the recursive and effective topos, Andrej Bauer said:
If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos ...
- 9,201
17
votes
3
answers
3k
views
What is the history of the Y-combinator?
Inspired by the comments to this question, I wonder if someone can explain the history of the fixed point combinator (often called the Y combinator) in lambda calculus.
Where did it first appear? ...
- 8,803
16
votes
2
answers
2k
views
Two versions of "absolutely ccc"
I have recently been slogging my way through Shelah's "Large continuum, oracles". Essentially from the start there has been a question needling me which I cannot seem to answer.
In the paper, Shelah ...
- 666
16
votes
1
answer
2k
views
Sneaky Recursive Non-Well-Orders
Background
An ordinal $\alpha$ is called a recursive ordinal if there is a recursive well-order $R$ on $\mathbb{N}$ such that ordertype($\mathbb{N},R) = \alpha$. For example, $\omega\cdot 2$ is a ...
- 1,601
16
votes
1
answer
846
views
Are the rationals definable in any number field?
Let $K$ be a number field. Is it necessarily true that $\mathbb{Q}$ is a first-order definable subset of $K$? Equivalently (since in any number field, its ring of integers is a definable subset), is $\...
- 2,130
16
votes
1
answer
2k
views
Does ZF prove that all PIDs are UFDs?
Main Question:
Does ZF (no axiom of choice) prove that every Principal Ideal Domain is a Unique Factorization Domain?
The proofs I've seen all use dependent choice.
Minor Questions:
Does ZF + ...
user5810
16
votes
2
answers
1k
views
How special is first-order $\mathsf{PA}$?
This is a modified version of a question which was asked and bountied at MSE without success.
Below, "$\mathsf{PA}$" refers to first-order Peano arithmetic.
There are various "...
- 20.5k
16
votes
1
answer
1k
views
Proving that ZF is Artemov-consistent
As discussed in another MO question, Sergei Artemov has proposed that the standard formalization Con(PA) of "PA is consistent" is flawed, and has proposed a different way to formalize "...
- 82.7k
16
votes
2
answers
1k
views
Ultrafilters arising from Keisler-Shelah ultrapower characterisation of elementary equivalence
In model theory, two structures $\mathfrak{A}, \mathfrak{B}$ of identical signature $\Sigma$ are said to be elementarily equivalent ($\mathfrak{A} \equiv \mathfrak{B}$) if they satisfy exactly the ...
16
votes
3
answers
1k
views
Finite versions of Godel' s incompleteness
Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...
- 7,853
16
votes
2
answers
1k
views
Von Neumann's consistency proof
In the paper Zur Hilbertschen Beweistheorie, John Von Neumann has proposed a consistency proof for
a fragment of first-order arithmetic (the fragment without induction and with
the successor axioms ...
- 32.2k
16
votes
1
answer
1k
views
Does Urysohn's Lemma imply Dependent Choice?
It's widely known$^{1}$ that in the proof of Urysohn's Lemma (UL) one uses the Principle of Dependent Choice (DC). Inspired by the equivalence between DC and Baire's Category Theorem$^{2}$, I'd like ...
- 405
16
votes
1
answer
834
views
Can $Ord$ have nontrivial second-order elementary self-embeddings?
I forgot to mention originally: this was motivated by this old MSE question.
It's not hard to show in $\mathsf{ZFC}$ that there are nontrivial elementary embeddings from $(Ord; \in)$ to itself - or ...
- 20.5k
16
votes
1
answer
1k
views
Can there be a global linear ordering of the universe without a global well-ordering of the universe?
This question arose in the answers to Asaf Karagila's
question Does ZFC prove that the universe is linearly orderable?. The answer there was that one can have a ZFC model with no global linear ...
- 236k
16
votes
1
answer
2k
views
Characterization of Stone-Cech compactifications
Suppose I have an infinite discrete topological space $X$ of cardinality $\kappa$. Then I know some things about the Stone-Cech compactification, $\beta X$: it is Hausdorff and compact but not ...
- 20.5k
16
votes
4
answers
4k
views
How are Modal Logic and Graph Theory related?
I am currently taking a graduate logic course on Modal Logic and I can't help notice that there are a certain class of graphs characterized by the modal axioms such as (4) $\Box p \rightarrow \Box \...
- 1,441
16
votes
1
answer
751
views
Is it consistent with ZFC that no nontrivial forcing notion has automatic mutual genericity?
A nontrivial forcing notion $\newcommand\Q{\mathbb{Q}}\Q$ exhibits
automatic mutual genericity, if whenever $G,H\subseteq\Q$ are
distinct $V$-generic filters (existing, say, in some forcing
extension ...
- 236k
16
votes
1
answer
462
views
What sets of primes can we pick out with first-order statements?
For each prime $p$, we have the algebraically closed field $\bar{\mathbb F}_p$ with the Frobenius automorphism.
Given any first-order statement with no free variables using the symbols $0,1, +, \...
- 149k
16
votes
3
answers
2k
views
Ackermann's function over the reals
Ackermann's function is defined over integers $x$, $y$, $A(x,y)$,
with conditions for when $x=0$ or $y=0$, and otherwise uses recursive
definitions involving arguments $x-1$ and $y-1$.
Is there a ...
- 151k
16
votes
0
answers
646
views
Consistency strength of $j:L_δ→L_δ$ for some δ
What is the consistency strength of existence of a nontrivial elementary embedding $j:L_δ→L_δ$ for some ordinal $δ$?
The consistency strength is strictly between totally ineffable and $ω$-Erdős ...
- 7,545
16
votes
1
answer
2k
views
Axioms of Choice in constructive mathematics
There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC)
$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...
- 791
16
votes
2
answers
1k
views
Major applications of the internal language of toposes
What are the major applications of the internal language of toposes?
Here are a few applications I know:
Mulvey's proof of the Serre–Swan theorem in which he interprets the intuitionistically valid ...
16
votes
3
answers
1k
views
Vopěnka's Principle for non-first-order logics
(For simplicity, the background theory for this post is NBG, a set theory directly treating proper classes which is a conservative extension of ZFC.)
Vopěnka's Principle ($VP$) states that, given any ...
- 20.5k
16
votes
1
answer
695
views
Is every class that does not add sets necessarily added by forcing?
We know there are many situations in which we can force over a model $M$ of GBC to add a class $G$ without adding any sets. That is, the extension $M[G]$ satisfies GBC and has the same sets as $M$. ...
- 1,146