nLab Kripke's schema





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



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}\{0, 1\}.


KS: For every statement ϕ\phi holds: There exists a binary sequence aa, such that ϕ\phi holds iff there is some nn such that a n=1a_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 bb, there exists a binary sequence aa, such that bb is the zero sequence iff aa 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 1max(range(b))1 - {\mathrm{max}}({\mathrm{range}}(b)) exactly determines whether bb is the zero sequence and thus the constant sequence aa with that value does the job. But constructively one generally cannot inspect all, infinitely many return values of a sequence bb.


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.


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