2
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

See Michael Beeson, “Some Relations between Classical and Constructive Mathematics”, Journal of Symbolic Logic 1978, on JStor.

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

$\endgroup$
  • $\begingroup$ I've accepted your answer because it obviously is what I'm looking for :-). Unfortunately I can't login to my JSTORaccount because their loginservice is down, pff. So I can't really comment more, please have some patience. Thanks again, cheers Frank. $\endgroup$ – Frank'a Waaldijk May 7 '18 at 8:58
  • 1
    $\begingroup$ The login finally succeeded... Wow, this is precisely what I was hoping for. What a wonderful article!! Finally I can use KG with a reference, this is very helpful Matt! $\endgroup$ – Frank'a Waaldijk May 7 '18 at 9:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.