All Questions
6,026 questions
7
votes
1
answer
290
views
Equivalence of omniscience principles for natural numbers and analytic omniscience principles for Cauchy real numbers
In constructive mathematics, a proposition $P$ is decidable if $P \vee \neg P$, and a proposition is stable if $\neg \neg P \implies P$. We have the following principles of omniscience for the natural ...
- 32.5k
1
vote
1
answer
276
views
About having one axiom schema for ZFC motivated after the iterative conception of sets?
This posting is related to this posting, and builds its motivation from this answer to it.
Define: $\operatorname {History}(x) \iff \\\forall y \in x: y=\{c \mid \exists z : z \in y \cap x \land (c \...
- 11.3k
1
vote
2
answers
338
views
Heuristic interpretations of the PA-unprovability of Goodstein's Theorem
I've relatively recently learned about Goodstein's Theorem and its unprovability in Peano arithmetic (the Kirby-Paris Theorem). I do not have any real knowledge of formal logic; but I think I've seen ...
- 708
22
votes
3
answers
2k
views
Algebraization of second-order logic
Is there an algebraization of second-order logic, analogous to Boolean algebras for propositional logic and cylindric and polyadic algebras for first-order logic?
- 4,713
6
votes
0
answers
290
views
Bounding proofs of transfinite induction
Let $\phi$ be a "reasonable" formula in the language of first-order arithmetic expressing some amount of transfinite induction along a given (index for a) computable linear order; my default ...
- 12.9k
2
votes
0
answers
76
views
Defining fields of characteristic zero in existential second-order logic
Is it possible to define in existential second-order logic (ESO) the class of fields of characteristic zero? An easy compactness argument shows that the class of fields of positive characteristic is ...
- 135
1
vote
1
answer
143
views
What determines non-finite axiomatizability of a class extension of a set theory?
Suppose $T$ is a set theory, i.e. doesn't have proper classes. And $T$ can interpret $\sf PA$, and $T$ is an effectively generated consistent first order set theory. Now, let $T^+$ be a class theory ...
- 47.4k
6
votes
1
answer
742
views
Which part(s) of this proof of Goodstein's Theorem are not expressible in Peano arithmetic?
EDIT: Noah Schweber helpfully points out that $\mathsf{ACA}_0$ is a conservative extension of Peano arithmetic in which certain aspects of my proof not expressible in Peano arithmetic are expressible. ...
- 236k
9
votes
0
answers
168
views
Algebraic structures on spaces of ultrafilters
The space of ultrafilters on $\omega$ has a natural semigroup structure, and ultrafilters that are idempotent in that algebra have seen applications in combinatorics on the natural numbers, for ...
- 18.6k
19
votes
6
answers
2k
views
Variable-centric logical foundation of calculus
Since calculus originated long before our modern function concept, much of our language of calculus still focuses on variables and their interrelationships rather than explicitly on functions. For ...
- 2,203
5
votes
0
answers
101
views
Computational view of subsystems of second-order arithmetic
If System T "corresponds" to full first-order arithmetic, and System F (λ2) corresponds to full second-order arithmetic, what type systems would be associated with weaker fragments, ...
CommunityBot
- 1
1
vote
0
answers
119
views
What is the minimal length of an undecidable sentence in those ZFC related theories?
If we measure the length of a sentence by the number of occurrences of atomic subformulas in it. So, for example in set theory written in $\sf FOL(\in)$, the length of a sentence is the number of ...
- 11.3k
12
votes
2
answers
1k
views
Am I doing a forcing argument here?
I have an argument of the following form:
Executive Summary:
We have a $\mathbb R$-valued function $L$ which we want to show is $\mathbb Z$-valued. We approximate it by $\mathbb Q$-valued functions $\...
- 44.4k
13
votes
3
answers
1k
views
Which ordinals can be proof-theoretic ordinals of a reasonable theory?
When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended ...
- 2,031
12
votes
1
answer
500
views
How strong is the Schröder–Bernstein theorem where one set is the natural numbers?
The full Schröder–Bernstein theorem states that given an injection from A to B and also one from B to A, there is a bijection between A and B. It is equivalent to excluded middle, as shown in the ...
- 12.9k
1
vote
1
answer
131
views
How can we define non-finitely axiomatizable extensions of set theories?
Suppose we have a first order set theory $T$ that is finitely axiomatizable. Is there a general way to formalize a set theory $T^+$ that extends $T$ and that is slightly stronger than $T$ and that is ...
- 20.5k
2
votes
0
answers
143
views
Constructively, when do functions that agree on $[a, b] \cup [b, c]$ also agree on $[a,c]$?
Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be ...
- 6,353
5
votes
1
answer
345
views
A question on the size of an admissible ordinal
Let $\mathbf{L}_{\varsigma}$ be the level of ordinal $\varsigma$ of Gödel's constructible universe $\mathbf{L}$. Let $\Sigma_{3}$-KP be Kripke-Platek set theory with infinity and $\Sigma_{3}$-$...
- 2,031
17
votes
2
answers
1k
views
Is it consistent with ZFC that the real line is approachable by sets with no accumulation points?
Let $P$ denote the following proposition:
There exists a set $S$ of subsets of $\mathbb{R}$ such that
$S$ is totally ordered by inclusion;
each member of $S$ has no accumulation points;
the union of ...
- 7,817
11
votes
6
answers
1k
views
When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?
Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f : [a, b] \cup [b, c] \to S$ be a function. When can we find a function $g : [a, c] \to S$ that meets the following ...
- 6,353
10
votes
0
answers
274
views
Open problems in complete theories
It is well-known that every complete recursively enumerable first-order theory is decidable. Does that mean that such theories are "trivial", or are there still interesting open problems ...
- 6,353
10
votes
1
answer
1k
views
What gets to be called a "proper class?"
ZFC has no formal notion of "proper class," but informally, everyone uses the term anyway. $V$, $Ord$, etc are said to be proper classes. Similarly, although in ZFC, one can only take the &...
- 236k
13
votes
2
answers
522
views
Computability-theoretic results relevant to realizability
This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of ...
- 20.5k
2
votes
1
answer
173
views
Chromatic number and taking duals of hypergraphs
If $H=(V,E)$ is a hypergraph and $\kappa\neq \emptyset$ is a cardinal, then a map $c:V\to \kappa$ is said to be a colouring if for every edge $e\in E$ with $|e|\geq 2$ the restriction $c\restriction_e:...
- 13.4k
2
votes
0
answers
46
views
Chromatic number of the dual hypergraph [duplicate]
Let $H = (V,E)$ be a hypergraph. For $v\in V$ we set $E_v = \{e\in E: v\in E\}$. The dual of $H$ is defined by $H^* =(E, V^*)$ is, where $V^* = \{E_v:v\in V\}$.
If $\kappa>0$ is a cardinal, a map $...
- 48.9k
60
votes
8
answers
10k
views
Why should we believe in the axiom of regularity?
Today I started reading Maddy's Believing the axioms. As I knew beforehand, it includes some discussion of ZFC axioms. However, I really hoped for a more extensive discussion of axiom of foundation/...
- 4,713
13
votes
4
answers
843
views
What is a "general" relation algebra?
I'm trying to understand why (or if) the axioms of relation algebras are "the right ones." For example, we can back up the idea that the group axioms exactly capture the notion of "...
CommunityBot
- 1
9
votes
1
answer
578
views
Are there ill-founded "maximally wide" models of $\mathsf{ZFC}$?
Throughout assume $\mathsf{ZFC}$ + "There is a proper class of inaccessible cardinals." I'm also happy to strengthen the large cardinal hypothesis if that would help.
Say that a model $M\...
- 17.7k
15
votes
2
answers
919
views
Which are the hereditarily computably enumerable sets?
My question is about sets that are computably enumerable with respect to their hereditary membership structure. Specifically, let me define that a hereditarily computably enumerable (h.c.e.) set is ...
- 7,545
3
votes
0
answers
170
views
Is the Tarski–Seidenberg theorem constructively provable?
The Tarski–Seidenberg theorem asserts that the projection of a semialgebraic set is also a semialgebraic set. My question is whether this is provable in constructive mathematics.
First, let me ...
- 6,353
10
votes
0
answers
159
views
Closed sets versus closed sublocales in general topology in constructive math
This question is set in constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF.
Short version of the question: if $X$ is a sober ...
- 32.5k
2
votes
1
answer
57
views
Are simplicial commutative inverse semigroups fibrant?
Let $X$ be a simplicial object in the category of commutative inverse semigroups (or monoids, if needed). Is the underlying simplicial set of $X$ always a Kan complex? If so, are there some nice ...
- 37.8k
7
votes
2
answers
727
views
What goes wrong in Easton forcing if we don't just use regular cardinals?
Recall that Easton forcing was introduced to show that the continuum function at regular cardinals could be anything subject to 'the obvious constraints' (monotonicity etc). However, it is a handy ...
- 1,097
10
votes
1
answer
644
views
Infinitary logics and the axiom of choice
Suppose we want to enhance ZF by allowing for infinitary formulas instead of just first-order ones in our axiom schema of separation and/or replacement. It seems that we don't need much power in our ...
- 20.5k
11
votes
3
answers
1k
views
How to handle sums in Tait's reducibility proof of strong normalisation?
I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
- 1,094
4
votes
0
answers
193
views
Examples of Grothendieck ($\infty$-)topoi which do / do not satisfy the law of excluded middle
I would like to create a big list of Grothendieck topoi (or Grothendieck $\infty$-topoi) which do / do not satisfy the law of excluded middle. That is, let’s list some examples of topoi whose internal ...
- 64k
3
votes
1
answer
125
views
Is existence of this function on nonempty sets of Quine atoms consistent with ZF-Regularity?
Working in $\sf ZF \text { - Regularity}$
Let $A $ be the set of all Quine atoms.
Let $f$ be a partial injective function from $\mathcal P(A)\setminus \{\emptyset\}$ to $A$.
Lets postulate the ...
- 236k
2
votes
0
answers
48
views
Is the class of strongly Kripke complete normal modal logics closed under sums?
Given an arbitrary set of normal modal logics $\mathcal{L}$, one can define their sum $\bigoplus \mathcal{L}$ (or $\bigoplus_{L \in \mathcal{L}} L$ if you prefer) to be the least normal modal logic ...
- 21
8
votes
0
answers
152
views
Which sentences are "strategically preserved"?
Below, everything is first-order.
Say that a sentence $\varphi$ is strategically preserved iff player 2 has a winning strategy in the following game:
Players 1 and 2 alternately build a sequence of ...
- 4,713
3
votes
1
answer
174
views
Is it consistent to have $\kappa$-Kurepa trees for some $\kappa$, but no Kurepa trees of other heights?
Definitions A tree means a set-theoretic tree, that is a poset $(T,<)$ so that for each $x\in T$, the set $\{y\in T\mid y<x\}$ is well-ordered.
A $\kappa$-Kurepa tree is a tree of height $\kappa$...
- 236k
2
votes
0
answers
235
views
Is there a computable model of HoTT?
Among the various models of homotopy type theory (simplicial sets, cubical sets, etc.), is there a computable one?
Can the negative follow from the Gödel-Rosser incompleteness theorem?
If there is no ...
CommunityBot
- 1
5
votes
0
answers
109
views
Computational complexity of arithmetic sentences over classical theories
Below, I use the term "tracker" rather than "realizer" since I'm not requiring the relevant objects to be computable.
Define the relation "$f$ tracks $\varphi$" for $f:\...
- 20.5k
7
votes
1
answer
561
views
How are real numbers defined in elementary recursive arithmetic?
I am currently reading about elementary function arithmetic and Harvey Friedman's grand conjecture.
In Number theory and elementary arithmetic, Jeremy Avigad expressed Fermat's last theorem, ...
- 20.5k
19
votes
6
answers
2k
views
Book recommendation introduction to model theory
Next semester I will be teaching model theory to master students. The course is designed to be "soft", with no ambition of getting to the very hardcore stuff. Currently, this is the syllabus....
- 5,031
-2
votes
1
answer
169
views
Is discriminative choice provable in ZFC?
Let $\phi$ be a formula defining an equivalence relation.
Definitions:
The $\phi$-cardinality of a set $X$ be the cardinality of $X/\phi$. That is, the cardinality of the set of all equivalence ...
- 18.6k
32
votes
5
answers
3k
views
What is the status of the Hilbert 6th problem?
As you know, the Hilbert sixth problem was to axiomatize physics. According to the Wikipedia article, there is some partial succes in this field. For example, Classical mechanics, I believe, can be ...
- 7,426
20
votes
5
answers
2k
views
Does formalizing math require search and creativity, or is it near-mechanical?
I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...
- 1,667
4
votes
1
answer
269
views
Does Peano's axioms prove $\alpha$-induction for primitive recursive sequences for every concrete $\alpha < \varepsilon_0$?
It is well-known that Peano's axioms (PA) cannot prove $\varepsilon_0$-induction for primitive recursive sequences (PRWO($\varepsilon_0$)), because PA + PRWO($\varepsilon_0$) proves the consistency of ...
- 3,042
8
votes
2
answers
510
views
Condition to guarantee that an inhabited and bounded set of reals has a supremum
This question is about constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the symbol $\mathbb{R}$) refer to ...
- 35.5k
6
votes
1
answer
414
views
Constructive treatment of Jacobson rings
Which result is closest to the classical
General Hilbert's Nullstellensatz: Finite type algebras over Jacobson rings are Jacobson.
and constructively true at the same time? And where can I find a ...
- 76