A model for intuitionistic non-standard arithmetic
From MaRDI portal
Publication:1891250
DOI10.1016/0168-0072(93)E0071-UzbMath0829.03040MaRDI QIDQ1891250
Publication date: 21 January 1996
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Baire spacetopossheavesfirst-order arithmetictrue arithmeticGrothendieck topologycategory of filtershigher-order Heyting arithmeticKripke-Joyal forcing relation
Categorical logic, topoi (03G30) Nonstandard models of arithmetic (03H15) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90)
Related Items (22)
Insight in discrete geometry and computational content of a discrete model of the continuum ⋮ Saturated models of intuitionistic theories ⋮ A sheaf-theoretic foundation for nonstandard analysis ⋮ Implication via spacetime ⋮ Asymptotic linear -- nonlinear duality, indeterminism and mathematical intelligence ⋮ Basic subtoposes of the effective topos ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Nonstandard proof methods in toposes ⋮ Intuitionistic nonstandard bounded modified realisability and functional interpretation ⋮ Minimal models of Heyting arithmetic ⋮ Realizability with a local operator of A. M. Pitts ⋮ Ultrafilters, finite coproducts and locally connected classifying toposes ⋮ Ultrapowers as sheaves on a category of ultrafilters ⋮ Constructive nonstandard representations of generalized functions ⋮ Real numbers in the topos of sheaves over the category of filters ⋮ Ultrasheaves and double negation ⋮ A functional interpretation for nonstandard arithmetic ⋮ Forcing in Proof Theory ⋮ 2002 Annual Meeting of the Association for Symbolic Logic ⋮ The monotonic sequence theorem and measurement of lengths and areas in axiomatic non-standard hyperrational analysis ⋮ Developments in Constructive Nonstandard Analysis ⋮ Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
Cites Work
This page was built for publication: A model for intuitionistic non-standard arithmetic