About the “semi-classical” view of Prof. Weaver and Prof. Feferman [closed]

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:

1. 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)

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

• For question 1, aren't there basically thousands of examples? Using classical logic is the norm in mathematics. For example, almost all of contemporary set theory would be the kind of example you seek. – Joel David Hamkins Feb 16 '16 at 14:05
• Where is logic overflow when you need it? – Franz Lemmermeyer Feb 16 '16 at 17:42
• OP: I have converted your post to comments, separated by whom you wish to notify. The notification system works by using @name where 'name' means at least the first four letters of the actual user name (none of this 'Monsieur' or 'Professor' business -- use the username, please). Meanwhile, answer boxes are to be reserved for actual answers to the question, and not used to make comments (use your registered account). Finally, while a lot of comments you see on MO are throwaway comments like your "Schade, schade, schade", they are not encouraged and should be used rather sparingly. Thank you. – Todd Trimble Feb 16 '16 at 19:32
• @NikWeaver There is plenty of mathematical philosophy here on MO, and we have a successful tag in math-philosophy mathoverflow.net/questions/tagged/math-philosophy?sort=votes with almost two hundred questions, and a large group of knowledgeable and interested participants. So I don't really agree with your remark. Well-posed interesting philosophical questions can be on-topic here, particularly when they are a bit closer to actual mathematics. – Joel David Hamkins Feb 17 '16 at 2:44
• @JoelDavidHamkins: okay, fair enough. – Nik Weaver Feb 17 '16 at 3:54