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.