# Unorthodox constructive reasoning: The Kleene Getaway

KG (the Kleene Getaway) is the name I improvised (in my answer to a question on MO on constructive Perron-Frobenius) for a constructive principle which enables the direct constructive use of a classical result in the following situation:

Suppose T is a classical theorem of analysis/topology/... provable in a formal system $\mbox{F}$ which is constructively 'sound' in the sense that $\mbox{F}$ is constructively equiconsistent with its constructive subsystem $\mbox{F}$$_\mbox{c}, obtained by leaving out LEM. Now suppose that we have an x and a property P such that: a) P(x) is constructively decidable (so we can decide P(x) or \neg(P(x)) b) P(x) holds classically by T Then KG states that P(x) holds constructively as well. Proof: The proof is actually quite simple, on the proof-level of the formal system, since \neg (P(x)) is impossible by b) and the equiconsistency of \mbox{F} and \mbox{F}$$_\mbox{c}$

Question 1: does anyone know of a publication where this principle is mentioned explicitly, and (hopefully) given a name?

So far I seem to be the only one using it, especially as a shortcut in online discussions (see the MO-question I mentioned above) to quickly establish that something can be proved constructively.

Question 2: Almost always when I use it, it is met with a mixture of disbelief or disapproval. Is there a better way of presenting it, to overcome what I believe to be miscommunication?

Some background:

One of Kleene's highest achievements in my opinion is one of the least known: his seminal work The Foundations of Intuitionistic Mathematics - especially in relation to recursive functions (usually abbreviated FIM).

In FIM Kleene developed a formal system (also called FIM...) and 4 years later, through function realizability methods, he showed equiconsistency of the classical extension of a basis theory of FIM and the intuitionistic extension of that basic system.

So, unnoticed by many: intuitionistic mathematics is as sound as classical mathematics, in the comparative realm of say separable analysis, topology, etc.