A strong multi-typed intuitionistic theory of functionals.

*(English)*Zbl 1357.03090The 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.

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.

Reviewer: Marco Benini (Buccinasco)

##### MSC:

03F55 | Intuitionistic mathematics |

03F50 | Metamathematics of constructive systems |

03F25 | Relative consistency and interpretations |

##### Keywords:

intuitionistic theory; lawless sequence; creating subject; Kripke schema; Beth model; consistency; truth predicate##### References:

[1] | Mathematical Notes 45 pp 66– (1989) |

[2] | Introduction to mathematical logic (1982) |

[3] | Proceedings of the 12th Asian Logic Conference pp 185– (2013) |

[4] | DOI: 10.2307/1971023 · Zbl 0353.02014 · doi:10.2307/1971023 |

[5] | Mathematical intuitionism. Introduction to proof theory (1987) |

[6] | DOI: 10.1007/BF02176167 · Zbl 0416.03051 · doi:10.1007/BF02176167 |

[7] | Collected works. Philosophy and foundations of mathematics 1 pp 478– (1975) |

[8] | DOI: 10.1016/0003-4843(78)90029-3 · Zbl 0399.03049 · doi:10.1016/0003-4843(78)90029-3 |

[9] | DOI: 10.1007/BF02176168 · Zbl 0416.03052 · doi:10.1007/BF02176168 |

[10] | Studia Philosophica 1 pp 261– (1935) |

[11] | DOI: 10.1007/BF02123404 · Zbl 0348.02029 · doi:10.1007/BF02123404 |

[12] | Logic, Methodology and Philos. Sci. III pp 161– (1968) |

[13] | Introduction to mathematical logic (2009) · Zbl 1173.03001 |

[14] | Some formal relative consistency proofs 18 pp 136– (1953) |

[15] | Doklady Akademii Nauk 357 pp 168– (1997) |

[16] | A strong intuitionistic theory of functionals (2014) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.