Questions tagged [reverse-math]

Reverse mathematics is the study of which axioms are required to prove mathematical theorems. This study is carried out by using formal theories of arithmetic, particularly subsystems of second-order arithmetic. Similar results in the context of set theory, for example those related to the axiom of choice and ZF set theory, should use the set-theory tag instead, possibly in combination with the axiom-of-choice tag.

Filter by
Sorted by
Tagged with
1 vote
1 answer
60 views

Why doesn't $RCA_0$ prove $\Sigma^0_1$-comprehension?

Answer: because that's $ACA_0$, alright, but: Friedman et al.'s 1983 "Countable algebra and set existence axioms" has [verbatim, including old terminology and dubious notation]: Lemma 1.6 ($...
ac15's user avatar
  • 1,024
3 votes
1 answer
135 views

Is the empty set always an 'implicit member' of all sets under a pure set theory?

Pure set theory, wherein all objects considered are sets —whose elements are themselves sets, and so forth— is usually thought of as building itself up in an ex nihilo fashion off the empty set $\...
Sho's user avatar
  • 334
2 votes
0 answers
32 views

Simpson's proof of the Gandy Kreisel Tait theorem in $\textbf{ATR}_0$

I believe there is an error in Simpson's book "Subsystems of Second Order Arithmetic". Theorem VIII.6.4 states: $\textbf{ATR}_0$ proves that any $Y$ such that $Y_i=\{(n,i)\in y:n\in\mathbb{N}...
Giorgio Genovesi's user avatar
4 votes
0 answers
38 views

Simpson's proof that $\textbf{WKL}_0$ proves existence of recursively saturated models.

Lemma IX.4.2 of Subsystem's of second order arithmetic Simpson claims that $\textbf{WKL}_0$ is sufficient to prove that every consistent theory has a saturated model. I will summarize the proof: Let $...
Giorgio Genovesi's user avatar
1 vote
0 answers
79 views

What is the significance of the difference between I$\Sigma_3$, I$\Sigma_{30}$ and I$\Sigma_{3000000}$ and $PA$?

There is of course a difference for logicians, but from a non-logician-mathematician's perspective, what is the real significance of arbitrarily complex induction predicates? Are there perhaps ...
10012511's user avatar
  • 682
2 votes
2 answers
573 views

Is the set of all algorithms computable?

Informally, I am basically asking if there is an algorithm that checks if the input is an algorithm or not. In Proofs From the Inside Out by John Stillwell, the author sometimes talks about an ...
Lucas Salim's user avatar
1 vote
0 answers
60 views

Is $\mathsf{I}\Sigma_n^0$ is the first-order part of $\Sigma_n^0$-$\mathsf{CA}_0$?

This seems obvious in view of the relation of $\mathsf{PA}$ and $\mathsf{ACA}_0$, but I just want to make sure that I'm not overlooking something important. Edit: This is false in view of the fact ...
10012511's user avatar
  • 682
3 votes
1 answer
61 views

Reverse mathematics of characterization of compact spaces

It is known that, over $\text{RCA}_0$, the Heine-Borel theorem is equivalent to $\text{WKL}_0$ and that the Bolzano-Weierstrass theorem is equivalent to $\text{ACA}_0$. In general, a topological space ...
Gavin Dooley's user avatar
  • 1,055
0 votes
0 answers
104 views

$t(x) - t(x/2) + t(x/3) - t(x/4) + ... = 0$ implies $t(x) + t(x/2)+t(x/3)+t(x/4) = C x$?

Inspired by this mysterious function : $f(x) + f(x/2) + f(x/3) + f(x/4) + ... = x$ and $\lim_{n \to \infty} \frac{f(n)}{\pi(n)} = 1$? I started to wonder since the alternating sum equals zero : $$f(x) ...
mick's user avatar
  • 16k
2 votes
1 answer
67 views

Is the range of a total $\Pi^1_1$ function $\Delta^1_1$?

Let $f:\mathbb{N}\rightarrow\mathbb{N}$ be a total function whose graph is definable via a $\Pi^1_1$ formula. Then is the range of $f$ a $\Delta^1_1$ set? Clearly the range is $\Pi^1_1$, but is it $\...
Keshav Srinivasan's user avatar
2 votes
0 answers
38 views

represent polynomials as linear combinations of a kind of radial basis functions

Recently, I'm reading a paper Riesz representation theorem, Borel measures and subsystems of second-order arithmetic. In page 2, the author said that polynomials are linear combinations of basic ...
ZyS's user avatar
  • 31
2 votes
0 answers
69 views

Understanding the system $\textbf{ACA}_0'$ and and exercise $6.26$ of Hirschfeldt

The system $\textbf{ACA}_0' $ is the theory $ \textbf{ACA}_0 $ plus the statement $\forall n\,\forall X \,\exists X^{(n)}$. I'm not entirely sure what the proper way to express this as a second order ...
MIO's user avatar
  • 1,916
1 vote
1 answer
134 views

Reverse mathematics and determinacy theorems

I recently learned about three determinacy theorems, and I am curious about the reverse mathematical-strength of (the countable analogs of) these theorems. These theorems are Zermelo's Theorem (...
Gavin Dooley's user avatar
  • 1,055
0 votes
1 answer
149 views

Real numbers cannot be constructed?

Sorry if this is another crank finitism question, I am bit confused. According to wikipedia: Constructivism asserts that it is necessary to find (or "construct") a specific example of a ...
confusedscreaming's user avatar
3 votes
0 answers
73 views

Why does $\mathsf{WKL}_{0}$ not prove Ramsey's Theorem for singletons?

Consider the satement $\mathsf{RT}^{p}$ (Infinite Ramsey's Theorem for exponent $p\in\mathbb{N}$): For any $r\in\mathbb{N}$, and for any function $c:[\mathbb{N}]^{p}\rightarrow [r]$, there exists an ...
John's user avatar
  • 4,330
1 vote
1 answer
107 views

What is the proof theoretic ordinal of $\mathsf{B\Sigma}_{2}^{0}$?

The proof-theoretic strength of a theory is measured by the $\mathsf{\Pi}_{1}^{1}$-ordinal of the theory and it is called the proof-theoretic ordinal (PTO) of the theory (there are other ordinal ...
John's user avatar
  • 4,330
5 votes
1 answer
199 views

What are the proof-theoretic strengths of Ramsey's theorems?

The proof-theoretic strength of a theory is measured by the $\mathsf{\Pi}_{1}^{1}$-ordinal of the theory (indeed, there are other ordinal analyses, like the $\Pi_{2}^{0}$-ordinal of the theory). ...
John's user avatar
  • 4,330
0 votes
2 answers
73 views

Is it possible to prove the reversibility exponent math? [duplicate]

TL;DR: How do I prove x0=1 without proving by division of x? I'm somewhat new to calculus, so I don't have much experience with complex proofs. That being said, I ran into someone recently who argues ...
EvanderIV's user avatar
5 votes
0 answers
70 views

What modifications to the axioms of primitive recursion would restrict its expressivity to that of Presburger arithmetic?

Inspired by reading through this page: https://golem.ph.utexas.edu/category/2019/08/turing_categories.html https://en.wikipedia.org/wiki/Primitive_recursive_function Among the primitive recursive ...
jpt4's user avatar
  • 51
1 vote
0 answers
59 views

Order types of modified gap-embedding relations on finite trees

Kruskal's tree theorem states that finite trees are well-quasi-ordered under homeomorphic embedding (i.e. inf-preserving injections). In order to prove the Robertson-Seymour theorem, the "...
C7X's user avatar
  • 1,207
1 vote
0 answers
46 views

Axiomization of constructive primitive recursive arithmetic without induction

I want to play with a fragment of constructive primitive recursive arithmetic lacking induction kind of like Robinson arithmetic. Basically the intent is to axiomize a sort of "weak natural ...
Molly Stewart-Gallus's user avatar
0 votes
0 answers
123 views

A tree with a lexicographic order is a linear ordered structure

Let T be a binary tree. In RCA0, I wanted to show that (T,<) is a linear ordered structure where < means the lexicographic ordering on T. I tried to prove it, and I did. I think my proof works; ...
Mohammad tahmasbi zade's user avatar
2 votes
0 answers
55 views

A Peano system with an infinite initial segment

Let $T$ be a binary tree with the lexicographic order. And $f:T→T$ be the successor operation. We denote the empty sequence in $T$ by $i$. Also Suppose that: For all $X⊂T$ if these two conditions hold:...
Mohammad tahmasbi zade's user avatar
0 votes
0 answers
58 views

The set of all finite sequences in RCA0

In the book "subsystems of second order arithmetic", page 68, Simpson claimed that the set of all codes of finite sequences (denoted by "Seq") exists by sigma 0-0 comprehension. I ...
Mohammad tahmasbi zade's user avatar
3 votes
0 answers
44 views

In RCA0, Prove that for all n, fⁿ(i) exists

I wanted to prove in RCA0 that: If f:A→A be a function and i∈A, then for all n, fⁿ(i) exists. To reach that, I proved another theorem. I wrote my proof but I'm not sure it's rigorous. If you read it, ...
Mohammad tahmasbi zade's user avatar
0 votes
1 answer
60 views

Does Z₂ Prove the iteration theorem?

iteration theorem: Let (ℕ,0,S) be the structure of natural numbers. And let W be an arbitrary set and c be an arbitrary member of W and g be a function from W into W. Then, there is a unique function ...
Mohammad tahmasbi zade's user avatar
1 vote
0 answers
92 views

What is the importance of Peano categoricity?

We know that Dedekind in 1888 proved that second order peano arithmetic(PA2) is categorical. My question is, why is it important? Does it have any mathematical, philosophical or foundamental ...
Mohammad tahmasbi zade's user avatar
1 vote
0 answers
38 views

Peano categoricity is equivalent to weak konig lemma

Peano categoricity (PC) says that: Every model for second order peano system is isomorphic to standard model. i.e PC says that every peano system such as (A, f, i) is isomorphic to (N, S, 0). Simpson ...
Mohammad tahmasbi zade's user avatar
2 votes
0 answers
32 views

Strength and conservativity of $\Sigma^1_n \textrm{-DC}_0$

How strong is $\Sigma^1_n \textrm{-DC}_0$ in terms of consistency strength? I know it is conservative to $\Pi^1_n \textrm{-TI}_0$, but I don't know its relation to other subsystems. Are there any ...
Binary198's user avatar
  • 269
0 votes
1 answer
82 views

Second-order arithmetic subsystems

I've been surfing the internet, and have found some subsystems or additional axioms of second-order arithmetic whose definitions I could not find. Does anyone know what the following axioms/subsystems ...
Binary198's user avatar
  • 269
2 votes
1 answer
142 views

A bit of reverse math fun: how to ensure the existence of the ordinal $\omega^\omega$?

Lately I was having some fun with axiomatizing the ordinals. This isn't a research project or anything, just a casual little side task to keep myself busy during the winter holidays. I started out ...
Michał Zapała's user avatar
5 votes
1 answer
440 views

What is the difference between "Peano arithmetic," "second-order arithmetic," and "second-order Peano arithmetic?"

I think this needs to be clarified, so it would be helpful to see an answer to this somewhere. I've seen the following terms: Peano arithmetic. Second-order arithmetic. Second-order Peano arithmetic. ...
Maximal Ideal's user avatar
1 vote
0 answers
45 views

Proof of that there is no uniform proof of the Effective Dushnik-Miller conjecture.

I'm a little confused by Theorem 5.23 in Rod Downey's "Computability Theory and Linear Orderings." Specifically, I'm not sure how he constructs such an A (meeting the requirements $R_e$ ...
Will Asness's user avatar
0 votes
1 answer
35 views

getting the initial number from the end total [closed]

i would need some advice if it is possible to get the initial number from a total number. I am trying to create a level system in my application and i need from the total experience to find the ...
Mireille28's user avatar
1 vote
0 answers
114 views

Reverse Mathematics of Well-Founded Induction in Primitive Recursive Arithmetic

I have another question about Primitive Recursive Arithmetic, and I'll borrow it's axiomatization from my other question Does the Deduction Theorem fail for Primitive Recursive Arithmetic?. Consider ...
noname_lonestar's user avatar
2 votes
2 answers
3k views

How to get an original function from the limit definition of a derivative?

Say I have $$\lim_{h\to0} \frac{e^h-1}{h}$$ If $$\frac{d}{dx}(e^x)|_{x=0} = \lim_{h\to0} \frac{e^{0+h}-e^0}{h},$$ how would I “back engineer” the derivative limit definition to satisfy the expression ...
Canadian Bacon's user avatar
2 votes
1 answer
151 views

What is the Turing degree of truth in the second-order theory of real numbers?

Let $X$ be the set of Godel numbers of sentences in the second-order language of ordered fields which are true in $\mathbb{R}$. Then my question is, what is the Turing degree of $X$? In particular, ...
Keshav Srinivasan's user avatar
1 vote
2 answers
83 views

Is it possible to calculate the input variable of a specific encryption function without brute-forcing it?

I didn't know where to post this question, here or SO but I feel it's more of a math problem. Lately I have been reverse engineering a game, and figured out how it takes user input, encodes it, and ...
Panos Paschalis's user avatar
1 vote
1 answer
146 views

Weak Konig's Lemma and Sequential Compactness

May I ask how is "Sequential Compactness" related to "Weal Konig's Lemma"? If we have a bounded set in real number space, how do we prove that every infinite sequence in this set ...
PassingBy's user avatar
  • 237
4 votes
0 answers
157 views

Geometry of typical sets

A common construction in statistics is the distribution of $n$ iid random variables, for $n$ arbitrarily large. For large enough $n$ the distribution is approximately uniform over a highly regular ...
Christian Chapman's user avatar
1 vote
0 answers
59 views

What subsystem of second-order arithmetic proves the weak Godel’s Theorem?

Godel’s Incompleteness Theorem states that any omega-consistent recursive theory in the language of first-order arithmetic is incomplete. But there is a weaker version of Godel’s Theorem that is ...
Keshav Srinivasan's user avatar
-1 votes
1 answer
91 views

How can i figure out an algorithm by comparing input and output? [closed]

I have a bunch of input numbers and output numbers that were run through an algorithm that I don't know. What is the approach for discovering the algorithm that generated the outputs? I assume this is ...
rogerpark's user avatar
3 votes
0 answers
90 views

Reducing the strength of a category theoretic proof

The motivation for this question is the following: Say we have a formula $\phi$ in peano arithmetic, and we have proof $\pi$ of $\phi$ using possibly higher order arithmetic or category theory (that ...
Couchy's user avatar
  • 2,722
2 votes
1 answer
105 views

How much choice is needed to prove that every compact metric space is a continuous image of the Cantor set?

Having inspected the proof of the fact that for every compact metric space $X$ there exists a continuous surjection from $\{0,1\}^{\mathbb N}$ onto $X$, it looks to me it is a theorem of ZF + DC (...
Tomasz Kania's user avatar
  • 16.4k
1 vote
0 answers
91 views

What is the Turing degree of the set of True formula of Arithmetic whose order is an infinite ordinal

This question was originally posted as a part of this other question, but I was suggested to make a new question for this part. In the first question I asked about the Turing degree of the set of ...
holmes's user avatar
  • 413
3 votes
1 answer
306 views

What is the Turing degree of the set of true formula of Second Order Arithmetic?

The set of true formula of First Order Arithmetic is not arithmetical (by Tarski's undefinability theorem) and it has Turing degree $\emptyset^{(\omega)}$. What about the set of true formula of ...
holmes's user avatar
  • 413
5 votes
1 answer
554 views

Why does the Cantor-Bendixson cupcake theorem need transfinite induction?

Recall the Cantor-Bendixson theorem: Let $X$ be a Polish space. For every closed subset $K \subseteq X$, there is a unique disjoint sum decomposition $C \cup P = K$ where $C$ is countable and $P$ ...
Aidan Backus's user avatar
7 votes
0 answers
100 views

What is the "validity logic(s)" of moderate theories?

This question is motivated by this old answer of mine. Below, by "appropriate theory" I mean any consistent finitely axiomatizable theory in the language $L_2$ of second-order arithmetic containing $...
Noah Schweber's user avatar
2 votes
0 answers
63 views

Automated discovery of interesting theorems by searching motifs in words (e.g. Coq lambda calculus) - grammatical notion of reverse mathematics?

Proof assistant Coq allows to represent any theorem as the lambda type (whose proof is the lambda term) (there are other proof assistants like Isabelle/HOL, Lean, etc. that allows similar grammatical ...
TomR's user avatar
  • 1,313
0 votes
1 answer
115 views

Constructive mathematics plus existence of discontinuous functions

Bishop's constructive mathematics (BISH) is meant to be the intersection of the theories of Brouwer, early Recursion Theory, and classical mathematics, and so it can be modelled by any model for the ...
William Bell's user avatar