Contents

Contents

Idea

Kripke’s schema is a principle first found implicitly in the school of Brouwer, going beyond base constructive logic. It ties propositions (or, in some formulations, membership of subsets of the naturals) to the values of infinite sequences in $\{0, 1\}$.

Formulation

KS: For every statement $\phi$ holds: There exists a binary sequence $a$, such that $\phi$ holds iff there is some $n$ such that $a_n=1$.

In the formalization of evolving choice sequences by Saul Kripke, this may be motivated by the idea that, roughly speaking, for any proposition there would be a sequence capturing its proof search, so that, thus, if and only if the proposition is provable, that search eventually terminates.

Weaker variants

KS implies, for example, the following Weak Principle of Finite Possibility, which can be stated just in terms of sequences:

WPFP: For every binary sequence $b$, there exists a binary sequence $a$, such that $b$ is the zero sequence iff $a$ is not the zero sequence.

This is to say, to any sequence there is a certain sort of value-inverted sequence. Classically, of course, the value $1 - {\mathrm{max}}({\mathrm{range}}(b))$ exactly determines whether $b$ is the zero sequence and thus the constant sequence $a$ with that value does the job. But constructively one generally cannot inspect all, infinitely many return values of a sequence $b$.

Implications

Binary sequences are nicely behaved objects and, in turn, KS can be shown to be equivalent to the claim that every inhabited subset of the naturals is countable.

The principles also has implications for metric spaces.

It can be shown that (WPFP + MP) iff LPO. Those principles are thus not provable in Russian constructivism (adopting MP but not LPO). Indeed, formulations of KS contradict the so called Constructive Church’s Thesis.

References

Last revised on August 22, 2021 at 14:45:17. See the history of this page for a list of all contributions to it.