-
19Algebraic Set Theory and the Effective ToposJournal of Symbolic Logic 70 (3). 2005.Following the book Algebraic Set Theory from André Joyal and leke Moerdijk [8], we give a characterization of the initial ZF-algebra, for Heyting pretoposes equipped with a class of small maps. Then, an application is considered (the effective topos) to show how to recover an already known model (McCarty [9])
-
17Review of: Sheaves, Games, and Model Completions (review)Bulletin of Symbolic Logic 10 (2): 216-217. 2004.
-
47Lifschitz' realizabilityJournal of Symbolic Logic 55 (2): 805-821. 1990.V. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a "q-variant" we obtain a new derived rule. We also show how to extend Lifschitz' realizability …Read more
-
16Downey, R., Gasarch, W. and Moses, M., The structureAnnals of Pure and Applied Logic 70 (1): 287. 1994.
-
REVIEWS-From sets and types to topology and analysis--Towards practicable foundations for constructive mathematicsBulletin of Symbolic Logic 12 (4): 611-612. 2006.
-
23From sets and types to topology and analysis—towards practicable foundations for constructive mathematics (review)Bulletin of Symbolic Logic 12 (4): 611-612. 2006.
-
9Extension of Lifschitz' Realizability to Higher Order Arithmetic, and a Solution to a Problem of F. RichmanJournal of Symbolic Logic 56 (3). 1991.F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic HAH: $\forall X\lbrack\forall x(x \in X \vee \neg x \in X) \wedge \forall Y(\forall x(x \in Y \vee \neg x \in Y) \rightarrow \forall x(x \in X \rightarrow x \in Y) \vee \forall x \neg(x \in X \wedge x \in Y)) \rightarrow \exists n\forall x(x \in X \rightarrow x = n)\rbrack$ , and if not, whether assuming Church's Thesis CT and Markov's Principle MP would…Read more
-
19Extensional realizabilityAnnals of Pure and Applied Logic 84 (3): 317-349. 1997.Two straightforward “extensionalisations” of Kleene's realizability are considered; denoted re and e. It is shown that these realizabilities are not equivalent. While the re-notion is a subset of Kleene's realizability, the e-notion is not. The problem of an axiomatization of e-realizability is attacked and one arrives at an axiomatization over a conservative extension of arithmetic, in a language with variables for finite sets. A derived rule for arithmetic is obtained by the use of a q-variant…Read more
-
38Relative and modified relative realizabilityAnnals of Pure and Applied Logic 118 (1-2): 115-132. 2002.The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map
-
11Axiomatizing higher-order Kleene realizabilityAnnals of Pure and Applied Logic 70 (1): 87-111. 1994.Kleene's realizability interpretation for first-order arithmetic was shown by Hyland to fit into the internal logic of an elementary topos, the “Effective topos” . In this paper it is shown, that there is an internal realizability definition in , i.e. a syntactical translation of the internal language of into itself of form “n realizes ” , which extends Kleene's definition, and such that for sentences , the equivalence [harr]n is true in . The internal realizability definition depends on finding…Read more
-
25A General Form of Relative RecursionNotre Dame Journal of Formal Logic 47 (3): 311-318. 2006.The purpose of this note is to observe a generalization of the concept "computable in..." to arbitrary partial combinatory algebras. For every partial combinatory algebra (pca) A and every partial endofunction on A, a pca A[f] is constructed such that in A[f], the function f is representable by an element; a universal property of the construction is formulated in terms of Longley's 2-category of pcas and decidable applicative morphisms. It is proved that there is always a geometric inclusion fro…Read more
-
36A semantical proof of De Jongh's theoremArchive for Mathematical Logic 31 (2): 105-114. 1991.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 Heyti…Read more
-
63Partial Combinatory Algebras of FunctionsNotre Dame Journal of Formal Logic 52 (4): 431-448. 2011.We employ the notions of "sequential function" and "interrogation" (dialogue) in order to define new partial combinatory algebra structures on sets of functions. These structures are analyzed using Longley's preorder-enriched category of partial combinatory algebras and decidable applicative structures. We also investigate total combinatory algebras of partial functions. One of the results is that every realizability topos is a geometric quotient of a realizability topos on a total combinatory a…Read more
-
61Basic subtoposes of the effective toposAnnals of Pure and Applied Logic 164 (9): 866-883. 2013.We study the lattice of local operators in Hylandʼs Effective Topos. We show that this lattice is a free completion under internal sups indexed by the natural numbers object, generated by what we call basic local operators.We produce many new local operators and we employ a new concept, sight, in order to analyze these.We show that a local operator identified by A.M. Pitts in his thesis, gives a subtopos with classical arithmetic
-
15The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013, vii + 583 pp (review)Bulletin of Symbolic Logic 20 (4): 497-500. 2014.
-
48Extension of Lifschitz' realizability to higher order arithmetic, and a solution to a problem of F. RichmanJournal of Symbolic Logic 56 (3): 964-973. 1991.F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic $\mathbf{HAH}$: $\forall X\lbrack\forall x(x \in X \vee \neg x \in X) \wedge \forall Y(\forall x(x \in Y \vee \neg x \in Y) \rightarrow \forall x(x \in X \rightarrow x \in Y) \vee \forall x \neg(x \in X \wedge x \in Y)) \rightarrow \exists n\forall x(x \in X \rightarrow x = n)\rbrack$, and if not, whether assuming Church's Thesis CT and Markov's Principl…Read more
-
Realizability: an introduction to its categorical side. Studies in Logic and the Foundations of Mathematics, vol. 152Bulletin of Symbolic Logic 16 (3): 407-409. 2010.
-
14Axioms and (counter)examples in synthetic domain theoryAnnals of Pure and Applied Logic 104 (1-3): 233-278. 2000.An axiomatic treatment of synthetic domain theory is presented, in the framework of the internal logic of an arbitrary topos. We present new proofs of known facts, new equivalences between our axioms and known principles, and proofs of new facts, such as the theorem that the regular complete objects are closed under lifting . In Sections 2–4 we investigate models, and obtain independence results. In Section 2 we look at a model in de Modified realizability Topos, where the Scott Principle fails,…Read more
-
Leiden UniversityGraduate student
Areas of Interest
Philosophy of Mind |
Philosophy of Religion |