The article describes an intuitionistic theory, SLP, which aims at being a sort of universal theory, since it contains arithmetic and a type theory with axioms to model functionals and choice. The SLP theory is proved to be consistent by constructing Beth models for all the fragments with types of limited height in the type hierarchy. Moreover, the SLP theory is shown to be equiconsistent with TI, a classical typed set theory having an impredicative restricted comprehension axiom. Thus, the universal character of TI and SLP stems from the fact that many parts of classical mathematics can be developed inside TI and, thus, interpreted in SLP, so receiving an intuitionistic interpretation.
It is worth remarking that both TI and SLP are stronger than second-order arithmetic thus justifying the claim that SLP provides a reasonable intuitionistic counterpart to classical mathematics, as far as it can be developed inside the rather powerful framework of TI.
The article is very well written and clear also for the non-expert, although some key proofs are missing from the paper, but referenced in literature. The purist will be disappointed since SLP proves some principles, like weak continuity or the Kripke’s schema which are debatable in a predicative setting; also, the formal Church’s thesis is inconsistent with SLP.
But, purists apart, the results shows how to proficiently use the semantics of Beth models to interpret in an intuitionistic framework a few notoriously difficult aspects of classical mathematics, and this makes the paper worth reading for a general audience.