This paper provides an explicit description of a model for intuitionistic non-standard arithmetic, which can be formalized in a constructive metatheory without the axiom of choice.

In this paper, we give a constructive nonstandard model of intuitionistic arithmetic (Heyting arithmetic). We present two axiomatisations of the model: one finitary and one infinitary variant. Using the model these axiomatisations are proven to be conservative over ordinary intuitionistic arithmetic. The definition of the model along with the proofs of its properties may be carried out within a constructive and predicative metatheory (such as Martin-Löf's type theory). This paper gives an illustration of the use of sheaf semantics to obtain (...) effective proof-theoretic results.The axiomatisations of nonstandard intuitionistic arithmetic (to be calledHAIandHAIωrespectively) as well as their model are based on the construction in [5] of a sheaf model for arithmetic using a site of filters. In this paper we present a “minimal” version of this model, built instead on a suitable site of provable filter bases. The construction of this site can be viewed as an extension of the well-known construction of the classifying topos for a geometric theory which uses “syntactic sites”. (Such sites can in fact be used to prove semantical completeness of first order logic in a strictly constructive framework, see [6].)We should mention that for classical nonstandard arithmetics there are several nonconstructive methods of proving conservativity over arithmetic, e.g. the compactness theorem, Mac Dowell–Specker's theorem [3]. (shrink)

This paper investigates the algebraic structure of the Medvedev lattice M. We prove that M is not a Heyting algebra. We point out some relations between M and the Dyment lattice and the Mucnik lattice. Some properties of the degrees of enumerability are considered. We give also a result on embedding countable distributive lattices in the Medvedev lattice.

Simpson introduced the lattice of Π0 1 classes under Medvedev reducibility. Questions regarding completeness in are related to questions about measure and randomness. We present a solution to a question of Simpson about Medvedev degrees of Π0 1 classes of positive measure that was independently solved by Simpson and Slaman. We then proceed to discuss connections to constructive logic. In particular we show that the dual of does not allow an implication operator (i.e. that is not a Heyting algebra). We (...) also discuss properties of the class of PA-complete sets that are relevant in this context. (shrink)

We study the connection between factors of the Medvedev lattice and constructive logic. The algebraic properties of these factors determine logics lying in between intuitionistic propositional logic and the logic of the weak law of the excluded middle (also known as De Morgan, or Jankov, logic). We discuss the relation between the weak law of the excluded middle and the algebraic notion of join-reducibility. Finally we discuss autoreducible degrees.

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 Principle MP would help. Blass and Scedrov gave models of $\mathbf{HAH}$ in which this principle, which we call RP, is not valid, but their models do not satisfy either CT or MP. In this paper a realizability topos Lif is constructed in which CT and MP hold, but RP is false. (It is shown, however, that $RP$ is derivable in $\mathbf{HAH} + \mathrm{CT} + \mathrm{MP} + \mathrm{ECT}_0$, so RP holds in the effective topos.) Lif is a generalization of a realizability notion invented by V. Lifschitz. Furthermore, Lif is a subtopos of the effective topos. (shrink)