# Tagged Questions

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", ...

223 views

2k views

### Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?

I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...
259 views

435 views

### Z_2 versus second-order PA

These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the ...
710 views

### Applicability of Deduction theorem to Primitive recursive arithmetic [closed]

Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing ...
311 views

### How do you restrict the induction axiom in second (or higher) order logic?

Dear all, I am interested in reverse mathematics. The theory is that most of mathematics can be expressed and proven in ACA0, that is second order logic, with the induction axiom restricted. However,...
212 views

### Non-Computational classical subterms

Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term ...
728 views

### reverse mathematics strength of “Lipschitz functions are somewhere differentiable”

What is the reverse mathematics strength of "For all Lipschitz functions $\; f : \mathbb{R} \to \mathbb{R} \;$, $\;$ there exists a real number $x$ such that $f$ is differentiable at $x$." ? (...
779 views

2k views

### Consistency strength needed for applied mathematics

Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC ...
687 views

### Soundness Theorem in reverse mathematics

STPL := soundness theorem for predicate logic (see this) When trying to figure out the strength of the STPL in reverse mathematics, I managed to convince myself of the following: a) ACA0 has a (...
2k views

### Is finitism an extreme form of constructivism?

I hope this question is not too soft for MO. The Wikipedia says about finitism that it is an extreme form of constructivism. See http://en.wikipedia.org/wiki/Finitism. I doubt that this is correct. ...
300 views

### Strength of Transfinite Induction on the Difference Hierarchy

I'm wondering if a particular theory of second order arithmetic has been studied or is known to be equivalent to some other theory. Consider the formulas generated by $\Pi^1_1$ and $\Sigma^1_1$ ...
1k views

### Reverse mathematics strength of identically zero polynomials are the zero polynomial

According to wikipedia, the statement "every polynomial over a countable field that is not the zero polynomial has only finitely many roots" is equivalent to RCA0 over RCA0* (which is called ERCA-0 in ...
221 views

### Proving boundedness of continuous images of [0,1] in WKL0

I've been reading about reverse mathematics (mostly on wikipedia), and I had been thinking that I understood how to prove the equivalences to WKL0 and ACA0 mentioned in the its article. However, I ...
908 views

### Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?

Transfinite induction requires a second order induction hypothesis. So, that can not be defined as axiom scheme in FOL. However, if I look to Goodstein's theorem en the Hydra games, then they have to ...
605 views

### Weakest subsystems of second order arithmetic for mathematical logic

It is known that to prove completeness of first-order logic for countable languages WKL0 is enough. But, is it the weakest subsystem where one can prove it? What about the incompleteness theorems? Is ...
884 views

### Can Goodstein's theorem been proven with first order PA + Constructive Omega Rule?

I am trying to understand transfinite induction and Gentzen's theories. But I was wondering, if there is any connection with the Constructive Omega Rule (COR). With COR I mean that if you can proof: ...
2k views

### What is the reverse mathematics of first-order logic and propositional logic?

Suppose one tries to formalize first-order logic. How much "strength" is required to do this? Strength can mean in various senses: The fragment of ZFC needed to codify first-order logic. Which ...
Background Exercise 2.1.16b in Hartshorne (homework!) asks you to prove that if $0 \rightarrow F \rightarrow G \rightarrow H \rightarrow 0$ is an exact sequence of sheaves, and F is flasque, then \$0 \...