Intuitionism, Kripke’s Schema, Second-order Heyting arithmetic, Intuitionistic Real algebra, Interpretation
Miklós Erdélyi‐Szabó · Qeios · 2025
We show that in the presence of a strengthened Kripke’s schema — a plausible addition to the axiomatisation of intuitionistic analysis (see in e.g. [1] or [2]) — choice sequences can be recursively encoded in intuitionistic real algebra. Choice sequences are intuitionistically meaningful counterparts of sequences of natural numbers, and with them intuitionistic analysis can be interpreted in intuitionistic real algebra.