A semantical proof of De Jongh's theorem |
| |
Authors: | Jaap van Oosten |
| |
Institution: | (1) Faculteit Wiskunde en Informatica, Universiteit van Amsterdam, Plantage Muidergracht 24, NL-1018 TV Amsterdam, The Netherlands |
| |
Abstract: | Summary In 1969, De Jongh proved the maximality of a fragment of intuitionistic predicate calculus forHA. Leivant strengthened the theorem in 1975, using proof-theoretical tools (normalisation of infinitary sequent calculi). By a refinement of De Jongh's original method (using Beth models instead of Kripke models and sheafs of partial combinatory algebras), a semantical proof is given of a result that is almost as good as Leivant's. Furthermore, it is shown thatHA can be extended to Higher Order Heyting Arithmetic+all true
2
0
-sentences + transfinite induction over primitive recursive well-orderings. As a corollary of the proof, maximality of intuitionistic predicate calculus is established wrt. an abstract realisability notion defined over a suitable expansion ofHA. |
| |
Keywords: | 03F50 |
本文献已被 SpringerLink 等数据库收录! |
|