Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-28T13:54:11.876Z Has data issue: false hasContentIssue false
  • English
  • Français

The Herbrand topos

Published online by Cambridge University Press:  04 June 2013

BENNO VAN DEN BERG
BENNO VAN DEN BERG*
Affiliation:
Mathematisch Instituut, Utrecht University, PO. Box 80010, 3508 TA Utrecht, The Netherlands. e-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We define a new topos, the Herbrand topos, inspired by the modified realizability topos and our earlier work on Herbrand realizability. We also introduce the category of Herbrand assemblies and characterise these as the ¬¬-separated objects in the Herbrand topos. In addition, we show that the category of sets is included as the category of ¬¬-sheaves and prove that the inclusion functor preserves and reflects validity of first-order formulas.

Type
Research Article
Information
Mathematical Proceedings of the Cambridge Philosophical Society , Volume 155 , Issue 2 , September 2013 , pp. 361 - 374
Copyright
Copyright © Cambridge Philosophical Society 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]van den Berg, B. A topos for a nonstandard functional interpretation. arXiv:1301.3679 (2013).Google Scholar
[2]van den Berg, B., Briseid, E. and Safarik, P.A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic 163 (12) (2012), 1962–1994.CrossRefGoogle Scholar
[3]Biering, B.Dialectica interpretations: a categorical analysis. PhD. thesis (2008). Available from the homepage of Lars Birkedal.Google Scholar
[4]Carboni, A.Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103 (1995), 117–148.CrossRefGoogle Scholar
[5]Ferreira, F. and Nunes, A.Bounded modified realizability. J. Symbolic Logic 71 (1) (2006), 329–346.CrossRefGoogle Scholar
[6]Grayson, R. J.Modified realisability toposes. Handwritten notes from Münster University (1981).Google Scholar
[7]Hyland, J. M. E.The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165–216. North-Holland, Amsterdam, 1982.Google Scholar
[8]Johnstone, P. T.Sketches of an Elephant: a Topos Theory Compendium. Vol. 1. Oxf. Logic Guides, vol. 43 (Oxford University Press, New York, 2002).Google Scholar
[9]Johnstone, P. T.Sketches of an Elephant: a Topos Theory Compendium. Vol. 2. Oxf. Logic Guides, vol. 44 (Oxford University Press, Oxford, 2002).Google Scholar
[10]Johnstone, P. T. The Gleason cover of a realizability topos. Unpublished manuscript (2013).Google Scholar
[11]Kreisel, G.Interpretation of analysis by means of constructive functionals of finite types. In Constructivity in Mathematics: Proceedings of the colloquium held at Amsterdam, 1957 (ed. by Heyting, A.). Studies in Logic and the Foundations of Mathematics (North-Holland Publishing Co., Amsterdam, 1959), pp. 101–128.Google Scholar
[12]Mac Lane, S. and Moerdijk, I.Sheaves in Geometry and Logic – A First Introduction to Topos Theory. Universitext (Springer-Verlag, New York, 1992).Google Scholar
[13]McCarty, D. C.Variations on a thesis: intuitionism and computability. Notre Dame J. Formal Logic 28 (4) (1987), 536–580.CrossRefGoogle Scholar
[14]van Oosten, J.The modified realizability topos. J. Pure Appl. Algebra 116 (1–3) (1997), 273–289.CrossRefGoogle Scholar
[15]van Oosten, J.Realizability – An Introduction to its Categorical Side, Studies in Logic, vol. 152 (Elsevier, Amsterdam, 2008).Google Scholar
[16]Streicher, T. A semantic version of the Diller–Nahm variant of Gödel's Dialectica interpretation. Unpublished note available from the author's homepage (2006).Google Scholar
[17]Troelstra, A. S. and van Dalen, D.Constructivism in mathematics. Vol. I. Studies in Logic and the Foundations of Mathematics, vol. 121 (North-Holland Publishing Co., Amsterdam, 1988).Google Scholar