# 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.

90 questions
Filter by
Sorted by
Tagged with
7 views

42 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 ...
61 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 ...
36 views

47 views

### What is the role of $n$ in a finite set (reverse maths)?

Currently I am reading Simpson's Subsystems of Second Order Arithmetic, Chapter 2, Recursive Comprehension (RCA$_0$) The author stated the following theorem at page $67.$ Theorem $2.5$ The ...
175 views

### How are sets defined in reverse mathematics?

Currently going through Simpson's "Subsystems of second order arithmetic", which I believe is the ultimate reference in reverse mathematics, after having completed (more like peeked) Stillwell's "...
41 views

30 views

### If $x\in dom(\phi),$ we can use the code $\Phi$ and minimization theorem to prove within $RCA_0$ that $\phi(x)$ exists.

Currently I am reading Simpson's Subsystem of Second Order Arithmetic. The author defined continuous function as follows: Within $RCA_0,$ let $\hat{A}$ and $\hat{B}$ be complete separable metric ...
86 views

### How much arithmetic is required to formalize quantifier elimination in Presburger arithmetic?

As we know, Presburger arithmetic can be proved decidable by demonstrating that it admits quantifier elimination, i.e. that there is an algorithm that reduces any sentence in the language to some ...
35 views

### Questions on proof of pairing map is one-to-one

Notation: Within $RCA_0,$ define pairing map $$(i,j) = (i+j)^2+i$$ In Simpson's Subsystem of Second Order Arithmetic, chapter $2,$ he stated the following theorem. Theorem II $2.2$ The following are ...
93 views

51 views

### Add non-negativity constraint to a reverse optimization function

I am working with a model for portfolio management (Black-Litterman specifically) in finance. I have problems trying to impose a constraint where I want the values of a vector ($w_i$) to be non-...
89 views

69 views

### What sort of language does the language of second-order arithmetic become if the 'numbers' are the finite ordinals?

The language of second-order arithmetic is defined as follows (the wording of this definition is due to Henry Towsner from a pdf file of "[Chapter 4], "Second Order Arithmetic and Reverse ...