Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [reverse-math]

The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them; originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", 2010).

5
votes
2answers
319 views

Cases where multiple induction steps are provably required

I am looking for references for theorems of the form: 1) Any proof of theorem $X$ requires $n$ applications of induction axioms and especially 2) Any proof of theorem $X$ requires $n$ nested ...
9
votes
0answers
349 views

Reverse Mathematics of Euclid's theorem

Euclid's theorem that there are infinitely many prime numbers has multiple proofs, ranging from Euclid's original theorem that constructs a new prime from a finite list of such, to Euler's proof that ...
5
votes
1answer
294 views

van der Waerden's theorem in Reverse Mathematics

What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem ? van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is ...
13
votes
1answer
361 views

reverse mathematics of the Lebesgue measurability of analytic sets

Can the fact that all analytic sets are Lebesgue measurable be proven in $Z_2$, or in some weak subsystem such as $\Pi^1_1\text{-CA}_0$? Conversely, can certain set existence axioms be derived from ...
3
votes
3answers
323 views

How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m ...
4
votes
0answers
109 views

Does comprehension for formulas in the analytical hierarchy imply comprehension for all formulas in second-order arithmetic?

The proof that all formulas of second-order arithmetic are $\Pi^1_n$ for some $n$ (i.e. can be written with a bloc of second-order quantifiers followed by an arithmetical formula) uses the axiom of ...
11
votes
2answers
226 views

Are all generalized Scott sets realized as generalized standard systems?

Below, I've focused on PA when lots of other theories would do. If replacing PA with a different theory leads to a more answerable question, feel free to do so. The standard system of a nonstandard ...
6
votes
1answer
232 views

Am I counting quantifiers correctly?

I think this is right but I want to check. The theory $\mathsf{WKL}^*_0$ is conservative over EFA for $\Pi^0_2$ sentences. And the first order part of $\mathsf{WKL}^*_0$ is axiomatized by EFA plus ...
3
votes
0answers
123 views

Are there amenable groups without explicit Folner sets?

This is essentially a follow-up to this previous discussion on how, in the absence of choice, the "invariant mean" and "Folner set" characterizations of amenability are no longer equivalent. Recently ...
3
votes
1answer
80 views

If one adds an inductive subset to a model of $ACA_0$, do we always get a new model of $ACA_0$?

Suppose $(M, \mathcal X) \models ACA_0$. Recall that a subset $A \subseteq M$ is $inductive$ over $M$ if $M$ satisfies all instances of induction in the expanded language with a predicate for $A$. ...
0
votes
0answers
154 views

Indirect attempts at showing that Peano Arithmetic proves Fermat's Last Theorem

So, Peano Arithmetic almost definitely proves Fermat's Last Theorem (see What is known about the relationship between Fermat's last theorem and Peano Arithmetic?). That being said, constructing an ...
11
votes
1answer
532 views

What is known about the relationship between Fermat's last theorem and Peano Arithmetic?

As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem? In particular, what is known about the arithmetic systems $PA + \...
4
votes
0answers
145 views

A forcing which can build weird models of $\neg$ADS

There is a class of forcing notions I've been playing around with recently. They have a couple nice properties, and all have the same theme, but I've found them difficult to analyze beyond the basics. ...
50
votes
8answers
7k views

What does it mean to suspect that two conjectures are logically equivalent?

Here's a familiar conversation: Me: Do you think Conjecture A and Conjecture B are equivalent? Friend: Yes, because I think they're both true. Me: [eye roll] You know what I mean... Does there ...
2
votes
0answers
64 views

Is there a connection between the subsystems of second-order arithmetic and computational complexity?

The "big five subsystems of second-order arithmetic" in reverse arithmetic reveal the stratification of the structure of mathematics. What if any is the connection of these strata with complexity ...
5
votes
1answer
226 views

A game with boldface strength

This is a problem which has been bothering me for a while now; it doesn't seem inherently too hard, but I haven't been able to make any real headway, so I'm putting it out in the open since at this ...
2
votes
2answers
449 views

Is any Cauchy sequence for completion of rational semicomputable?

For the definition of a semicomputable real, see An Introduction to Kolmogorov Complexity and its Applications by Li and Vitanyi (1997). In fact, it is not true that every Cauchy sequence for ...
5
votes
1answer
182 views

Bounded-width Konig's lemma in reverse math

We define $\mathsf{BWKL}$ as follows: Every infinite binary tree of bounded width has an infinite path. This obviously follows from $\mathsf{WKL}$. Is this principle true in $\mathsf{RCA}_0$? If not, ...
7
votes
1answer
223 views

Axiomatizations of arithmetical parts of theories

For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic ...
1
vote
1answer
174 views

How does $RCA_0$ achieve weak completeness?

Few days ago I asked about $WKL_0$ and the role of binary trees to provide for completeness for first order theories, and the question was nicely answered by Joel David Hamkins: Does $WKL_0$ plus CON(...
2
votes
1answer
98 views

Does $WKL_0$ plus CON(PA+X) give a binary tree model of PA+X?

In the context of reverse mathematics $WKL_0$ is considered equivalent to Gödel's completeness theorem over $RCA_0$. Does this mean that e.g. $WKL_0$ plus the consistency statement CON(PA+X) gives a ...
1
vote
1answer
183 views

Forcing in Second-Order Arithmetic

If I understand correctly, Stephen Simpson, in his book Subsystems of Second Order Arithmetic, deems second-order arithmetic as a two-sorted first-order theory. If this is correct, then it seems ...
84
votes
5answers
5k views

Is there a database for tracking the dependencies of mathematical theorems?

Given a proof for a result, one could denote the proof as a node on a graph, and then draw arrows to the node from axioms and previous results that the proof uses, and then draw arrows from the node ...
2
votes
1answer
242 views

Is there a model of ZF+ACC where transfer fails for the definable hyperreals?

In 2003 Kanovei and Shelah constructed a definable hyperreal field. The ultrapower used exploits a fairly large index set so that it is clear that the usual proof of Los and transfer does not go ...
2
votes
0answers
135 views

Circular reasoning in proof of bounded comprehension

Theorems II.3.7 and II.3.9 in Simpson's Subsystems of Second-Order Arithmetic appear to be circular. Specifically, theorem II.3.7 seems to make implicit use of theorem II.3.9. [Theorem II.3.9 is the ...
2
votes
1answer
200 views

Transfer with minimal choice

Let FUF postulate the existence of a Free UltraFilter on $\mathbb{N}$ and ACC the axiom of countable choice. Consider the superstructure on $\mathbb{R}$ and its inclusion in the bounded ultrapower. ...
12
votes
2answers
351 views

Can noncomputable sets be distinguishable in $RCA_0$?

Say that a set $X\subseteq\omega$ is distinguishable if there is some Turing machine $\Phi_e$ which, when given two sets exactly one of which is $X$, can determine which set is $X$. Formally, $X$ is ...
38
votes
2answers
4k views

Why is this new result such a big deal?

This popular article reports a recent result in reverse mathematics, showing that a certain theorem in Ramsey theory is provable from RCA$_0$, the base theory in SOSOA. Then there are a bunch of ...
5
votes
1answer
345 views

Constructive compactness for countable models?

The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted here, in the context of classical logic. The weak König's ...
2
votes
2answers
223 views

Compactness for countable models?

How and where is it proved that WKL$_0$ proves the compactness theorem for countable models? (This is a follow-up to a comment of F. Dorais.)
6
votes
1answer
314 views

Are there first order theories of interest to an algebraist or at least a model theorist of large cardinal consistency strength?

I am wondering if there are some first order theories of algebraic structures or structures of interest to model theorists of large cardinal consistency strength or at least unexpectedly high ...
4
votes
1answer
106 views

Proving moduli of uniform continuity in RCA_0

Simpson's Subsystems of Second Order Arithmetic (pp. 134ff.) uses RCA$_0$ to prove various theorems of analysis for all continuous functions with a suitable modulus of uniform continuity. And he ...
9
votes
1answer
334 views

Proof-theoretic ordinals after liberalizing induction to $RCA_0$

This is kind of a follow-up to this question. For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together ...
4
votes
2answers
165 views

What can be achieved by liberalizing induction for $RCA_0$?

$RCA_0$ has $\Delta_0$-comprehension and $\Sigma_1$ induction. Let $X\Sigma_{n}$ be $RCA_0$ plus $\Sigma_n$-induction and let $X\Sigma_{\omega}$-induction be $RCA_0$ plus the full induction schema. ...
6
votes
1answer
118 views

Does $WKL_0$ provide more comprehension than $RCA_0$?

$WKL_0$ extends $RCA_0$ with the statement that any infinite subset of the infinite binary tree has an infinite branch. Does $WKL_0$ Prove that there are sets which are not proven to exist by the $\...
5
votes
1answer
450 views

What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?

I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that ...
32
votes
3answers
3k views

What is the reverse mathematical strength of the fundamental theorem of algebra?

Reverse mathematics (RM) is that area that tries to pin down exactly which axioms are necessary to prove theorems, given some weak base theory. Harvey Friedman has pointed out several times (on the ...
13
votes
4answers
2k views

“Family Tree” of Theorems

Is anyone aware of any attempt to describe the dependencies of theorems (perhaps in mathematics generally, perhaps in some limited areas) in the form of a "family tree"? That is, each node on the ...
6
votes
1answer
216 views

Degree of unsolvability of finding a open approximation to a Borel set, given its Borel code

It is well known that every Borel set has the property of Baire. That is, for every Borel set $B$, there is an open set $U$ and a sequence of dense open sets $D_n$ such that for every $x\in \cap_n ...
3
votes
1answer
176 views

Formal definition of arithmetic transfinite recursion

Recently I have been trying to find the definition of the subsystem $ATR_0$ of second-order arithmetic. Only "definitions" I have found were quite vague, like informal definition on Wikipedia which ...
12
votes
1answer
731 views

What is known about the reverse mathematics of algebraic number fields?

I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...
7
votes
1answer
335 views

The definition of < in Robinson's Q

I recently had to explain how the basic axioms in Simpson's Subsystems of Second Order Arithmetic were interpretable in Robinson's Q. Most of the axioms are actually the same, except that Simpson ...
14
votes
1answer
641 views

Higher recursion theory and reverse mathematics: What is to $\Pi^1_1-CA_0$ as $RCA_0$ is to $ACA_0$?

There is an extremely rich and well-understood analogy between "recursively enumerable" and "$\Pi^1_1$" - indeed, this is the starting point of metarecursion theory, and $\alpha$-recursion theory in ...
4
votes
1answer
349 views

Necessity of omega-models in second order arithmetic

Are there examples of independence results over subsystems of true second order arithmetic that cannot be established using omega-models? To rule out trivial examples, let us assume that the base ...
10
votes
2answers
646 views

Proof complexity of two directions of equivalency?

This question is not precise, but I believe has a precise formulation. Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example: Theorem. A ...
5
votes
1answer
156 views

Attribution of an equivalence of the existence of omega-models of RCA0

There are many well-known equivalences in reverse mathematics between statements of the form "Every set is contained a countable coded $\omega$-model of $T$" and $S$, where $S, T$ are subsystems of ...
4
votes
2answers
453 views

Reverse Math of High Sets?

Is there a standard principle in reverse math that is known to be equivalent (over $RCA_0$) to the existence of a set of high (Turing) degree? I'm interested in the general case, but would be happy to ...
5
votes
1answer
695 views

Why is adopting Russell's Axiom of Reducibility as strong as eliminating the Ramified Hierarchy?

In order to respond to concerns of impredicativity, Bertrand Russell developed a system of ramified second-order logic, which is like regular second-order logic except the comprehension schema is ...
9
votes
0answers
478 views

“Hard” separation results in reverse mathematics (or similar)

This is a fairly broad question. In particular, I specify 5 questions (Q1, Q2.1, Q2.2, Q3, Q4) which for me all fall under one umbrella. Since this is unreasonably broad, I'm really interested in an ...
6
votes
1answer
170 views

Is 0' of PA degree relative to a non-low set?

Definitions: A set $X$ is of PA degree relative to a set $Y$ if every infinite $Y$-computable binary tree has an infinite $X$-computable path. A set $X$ is low if $X'$ is computable from $\emptyset'$....