A semantical proof of De Jongh's theorem

Archive for Mathematical Logic 31 (2):105-114 (1991)

Jaap Van Oosten
Leiden University
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 No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/BF01387763
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 39,545
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers.Piergiorgio Odifreddi - 1989 - Sole Distributors for the Usa and Canada, Elsevier Science Pub. Co..
The |Lambda-Calculus.H. P. Barendregt - 1988 - Philosophical Review 97 (1):132-137.

View all 6 references / Add more references

Citations of this work BETA

Relative and Modified Relative Realizability.Lars Birkedal & Jaap van Oosten - 2002 - Annals of Pure and Applied Logic 118 (1-2):115-132.
Intermediate Logics and the de Jongh Property.Dick De Jongh, Rineke Verbrugge & Albert Visser - 2011 - Archive for Mathematical Logic 50 (1-2):197-213.

View all 6 citations / Add more citations

Similar books and articles

A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Undecidability and Intuitionistic Incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
Intermediate Logics and the de Jongh Property.Dick De Jongh, Rineke Verbrugge & Albert Visser - 2011 - Archive for Mathematical Logic 50 (1-2):197-213.
A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
LEt ® , LR °[^( ~ )], LK and Cutfree Proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.


Added to PP index

Total views
18 ( #417,163 of 2,325,363 )

Recent downloads (6 months)
2 ( #694,967 of 2,325,363 )

How can I increase my downloads?


My notes

Sign in to use this feature