**KG** (the Kleene Getaway) is the name I improvised (in my answer to a [question on MO on constructive Perron-Frobenius](https://mathoverflow.net/questions/299318/constructive-proof-of-a-rational-version-of-perron-frobenius/299340#299340)) 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](https://books.google.nl/books/about/The_Foundations_of_Intuitionistic_Mathem.html?id=3AFKAAAAMAAJ&redir_esc=y)* (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.



Unorthodox constructive reasoning: The Kleene Getaway
See Michael Beeson, “Some Relations between Classical and Constructive Mathematics”, Journal of Symbolic Logic 1978, on [JStor](http://www.jstor.org/stable/2272821).


Unfortunately, he doesn’t give these principles a good name, and in my experience, people distrust this metamathematics unnecessarily.


