3
$\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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
2
  • 1
    $\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$
    – Franka Waaldijk
    Commented May 7, 2018 at 8:58
  • 3
    $\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$
    – Franka Waaldijk
    Commented May 7, 2018 at 9:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .