In the thread "Is platonism regarding arithmetic consistent with the multiverse view in set theory?", Prof. Hamkins writes:
The view you are suggesting is something close to what is held by Solomon Feferman, who holds that the objects and truths of arithmetic have a definite nature that is not shared when one moves up to higher-order objects, such as the collection of all sets of natural numbers. Feferman has long been known for the view that the continuum hypothesis is inherently vague, in a way that arithmetic is not, and this seems to be basically what you are talking about. See for example his article
- Solomon Feferman, Is the continuum hypothesis a definite mathematical problem? Exploring the Frontiers of Incompleteness (EFI) Project, Harvard 2011-2012.
[...]
One interesting aspect of the view is the idea of using classical logic in the lower more-definite realm, and intuitionistic logic in the higher realm, where assertions such as the continuum hypothesis may have a less definite meaning. Nik Weaver has pointed out in the comments below that he had first proposed this dichotomizing idea in his 2005 article:
- Nik Weaver, Predicativity beyond Γ_0, 2005.
So, in this view, one is only allowed to use classical logic when proving (say) arithmetical statements. Let us call a proof that only uses classical logic when proving arithmetical statements a "semi-classical proof". A "semi-classical proof" is not allowed to use classical logic in the non-definite realm.
QUESTIONS:
Can you please give 'real-life' examples of non-semi-classical proofs? That is, examples of proofs that use classical logic in the less definite realm. (community wiki)
Here a vague question (that nevertheless can be made precise): If an arithmetical statement has a classical proof, does it also have a "semi-classical" proof?
EDIT: The second question can be made precise as follows: One considers the axiom system ZFC. Call a ZFC-formula arithmetical if it is a translation of a formula of peano-arithmetic (to every formula of peano-arithmetic one can assign a ZFC-formula that expresses the same). Now, one considers a proof system that is only allowed to use "p or not p" as an axiom if p is an arithmetical formula. Since axiom of choice implies LEM, one restricts the comprehension schema as follows: usually, given a set A and a formula P(x) one can construct the set {x in A : P(x)}, but in our system, the idea is that this should only be allowed when P(x) is arithmetical or harmless, that is, one cant construct sets
U = {x in {0, 1} : (x=0) or CH},
V = {x in {0, 1} : (x=1) or CH}. Therefore, in our proof system, the axiom of choice does not imply "CH or not CH" because the proof of Diaconescu's theorem does not work.