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", ...
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 ...
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 ...
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 ...
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: ...
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 ...
According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA. http://en.wikipedia.org/wiki/Reverse_Mathematics First of all I have a few questions about the proof: a - What ...
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 ...