# 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