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