Intuitionistic nonstandard bounded modified realisability and functional interpretation

We present a bounded modified realisability and a bounded functional interpretation of intuitionistic nonstandard arithmetic with nonstandard principles.The functional interpretation is the intuitionistic counterpart of Ferreira and Gaspar's functional interpretation and has similarities with Van den Berg, Briseid and Safarik's functional interpretation but replacing finiteness by majorisability.We give a threefold contribution: constructive content and proof-theoretical properties of nonstandard arithmetic; filling a gap in the literature; being in line with nonstandard methods to analyse compactness arguments.     

Intuitionistically provable recursive well-orderings

We consider intuitionistic number theory with recursive infinitary rules (HA^*). Any primitive recursive binary relation for which transfinite induction schema is provable is in fact well founded. Its ordinal is less than ε⁰ if the transfinite induction schema is intuitionistically provable in elementary number theory. These results are provable intuitionistically. In fact, it suffices to consider transfinite induction with respect to one particular number-theoretic property.     

ℋ-theories, fragments of HA and PA-normality

For a classical theory T, ℋ(T) denotes the intuitionistic theory of T-normal (i.e. locally T) Kripke structures. S. Buss has asked for a characterization of the theories in the range of ℋ and raised the particular question of whether HA is an ℋ-theory. We show that T ⁱ ∈ range(ℋ) iff T ⁱ = ℋ(T). As a corollary, no fragment of HA extending iΠ ₁ belongs to the range of ℋ. A. Visser has already proved that HA is not in the range of H by different methods. We provide more examples of theories not in the range of ℋ. We show PA-normality of once-branching Kripke models of HA + MP, where it is not known whether the same holds if MP is dropped. Received: 15 August 1999 / Published online: 3 October 2001     

An Effective Conservation Result for Nonstandard Arithmetic

We prove that a nonstandard extension of arithmetic is effectively conservative over Peano arithmetic by using an internal version of a definable ultrapower. By the same method we show that a certain extension of the nonstandard theory with a saturation principle has the same proof‐theoretic strength as second order arithmetic, where comprehension is restricted to arithmetical formulas.     

Finite investigations of transfinite derivations

-derivations of arithmetic formulas are analyzed. A primitive recursive normalization operator E is constructed in the first part. It cut-eliminates not only recursively described derivations (i.e., well-founded proof-figures) but also arbitrary (not necessarily well-founded) proof-figures constructed from an axiom by derivation rules. This permits us to apply E in the theory of models, Its application in the theory of proofs is based on the formalizability of the fundamental properties of E in a primitive recursive arithmetic. Cut-eliminability in the Heyting arithmetic HA+AC with the axiom of choice of all finite types is proved in the second part. The formulation allowing cut-elimination uses terms associated with the derivations by a method due to Carry, Howard, Girard, and Martin-Löf. These terms are included in the very formulation of the rules. The conservativity of HA+AC over HA is obtained as one of the corollaries.Results announced on April 29, May 4, and September 21, 1972.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 49, pp. 67–121, 1975.     

Loeb measure, finitely additive measures, and a theorem of Banach

The Loeb measure construction from nonstandard analysis is applied to two theorems in standard measure theory. In both cases the essential simplification offered by the approach is the ability to work with a σ-additive measure space, even if the hypotheses only guarantee finite additivity. The key to this simplification is the property of à₁{\aleph_1}-saturated nonstandard models, that any finitely additive measure on an internal algebra extends immediately to a σ-additive measure.     

Measures and forking

Shelah's theory of forking (or stability theory) is generalized in a way which deals with measures instead of complete types. This allows us to extend the method of forking from the class of stable theories to the larger class of theories which do not have the independence property. When restricted to the special case of stable theories, this paper reduces to a reformulation of the classical approach. However, it goes beyond the classical approach in the case of unstable theories. Methods from ordinary forking theory and the Loeb measure construction from nonstandard analysis are used.     

Computational adequacy for recursive types in models of intuitionistic set theory

This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo–Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an “internal” computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine “external” computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC. In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models.     

Nonstandard extensions of uniform algebraic systems

Important applications of nonstandard analysis to the theory of Banach spaces are based on the construction of the nonstandard hull of a normed linear space [1,2]. By making use of the iterated nonstandard enlargements [3], in the present article we propose a universal construction for arbitrary uniform algebraic systems which allows one to study the nonstandard hulls and completions of such systems.In Section 1 we give necessary information about nonstandard enlargements and prove a number of important results in the general theory of monads. In Section 2 we present basic facts on nonstandard topologies and uniform algebraic systems. In Section 3 we describe a general algebraic construction with the help of which we study the question of completing uniform algebraic systems. Conditions for existence of nonstandard hulls for such systems are obtained in Section 4.Translated fromSibirskiî Matematicheskiî Zhurnal, Vol. 35, No. 5, pp. 1094–1105, September–October, 1994.     

Loeb measure,finitely additive measures,and a theorem of Banach

The Loeb measure construction from nonstandard analysis is applied to two theorems in standard measure theory. In both cases the essential simplification offered by the approach is the ability to work with a σ-additive measure space, even if the hypotheses only guarantee finite additivity. The key to this simplification is the property of -saturated nonstandard models, that any finitely additive measure on an internal algebra extends immediately to a σ-additive measure.      

A semantical proof of De Jongh's theorem

Summary 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 ₂ ⁰ -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.     

Extracting Algorithms from Intuitionistic Proofs

This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory S, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ₁.     

Certain Partial Conservativeness Properties of Intuitionistic Set Theory with the Principle of Double Complement of Sets

The Zermelo–Fraenkel set theory with the underlying intuitionistic logic (for brevity, we refer to it as the intuitionistic Zermelo–Fraenkel set theory) in a two-sorted language (where the sort 0 is assigned to numbers and the sort 1, to sets) with the collection scheme used as the replacement scheme of axioms (the ZFI2C theory) is considered. Some partial conservativeness properties of the intuitionistic Zermelo–Fraenkel set theory with the principle of double complement of sets (DCS) with respect to a certain class of arithmetic formulas (the class all so-called AEN formulas) are proved. Namely, let T be one of the theories ZFI2C and ZFI2C + DCS. Then (1) the theory T+ECT is conservative over T with respect to the class of AEN formulas; (2) the theory T+ECT+M is conservative over T+M{su?} with respect to the class of AEN formulas. Here ECT stands for the extended Church’s thesis, Mis the strong Markov principle, and M{su?} is the weak Markov principle. The following partial conservativeness properties are also proved: (3) T+ECT+M is conservative over T with respect to the class of negative arithmetic formulas; (4) the classical theory ZF2 is conservative over ZFI2C with respect to the class of negative arithmetic formulas.     

Computability in structures representing a Scott set

Continuing work begun in [10], we utilize a notion of forcing for which the generic objects are structures and which allows us to determine whether these “generic” structures compute certain sets and enumerations. The forcing conditions are bounded complexity types which are consistent with a given theory and are elements of a given Scott set. These generic structures will “represent” this given Scott set, in the sense that the structure has a certain weak saturation property with respect to bounded complexity types in the Scott set. For example, if ? is a nonstandard model of PA, then ? represents the Scott set ? = n∈ω | ?⊧“the nth prime divides a” | a∈?. The notion of forcing yields two main results. The first characterizes the sets of natural numbers computable in all models of a given theory representing a given Scott set. We show that the characteristic function of such a set must be enumeration reducible to a complete existential type which is consistent with the given theory and is an element of the given Scott set. The second provides a sufficient condition for the existence of a structure ? such that ? represents a countable jump ideal and ? does not compute an enumeration of a given family of sets ?. This second result is of particular interest when the family of sets which cannot be enumerated is ? = Rep[Th(?)]. Under this additional assumption, the second result generalizes a result on TA [6] and on certain other completions of PA [10]. For example, we show that there also exist models of completions of ZF from which one cannot enumerate the family of sets represented by the theory. Received: 8 October 1997 / Published online: 25 January 2001     

Preservation theorems for bounded formulas

In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV₁. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction on strict formulas proves decidability of formulas, then P=NP. We also prove that, if the mentioned intuitionistic theory proves , then P=NP.     

Sequent calculus proof theory of intuitionistic apartness and order relations

Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over the usual theories of order. Received: 4 December 1997     

Intuitionistic Frege systems are polynomially equivalent

In a paper by Cook and Reckhow (1979), it is shown that any two classical Frege systems polynomially simulate each other. The same proof does not work for intuitionistic Frege systems, since they can have nonderivable admissible rules. (The rule A/B is derivable if the formula A → B is derivable. The rule A/B is admissible if for all substitutions σ, if σ(A) is derivable, then σ(B) is derivable.) In this paper, we polynomially simulate a single admissible rule. Therefore any two intuitionistic Frege systems polynomially simulate each other. Bibliography: 20 titles. Published in Zapiski Nauchnykh Seminarov POMI, Vol. 316, 2004, pp. 129–146.     

Persistency of linear programming relaxations for the stable set problem

The Nemhauser–Trotter theorem states that the standard linear programming (LP) formulation for the stable set problem has a remarkable property, also known as (weak) persistency: for every optimal LP solution that assigns integer values to some variables, there exists an optimal integer solution in which these variables retain the same values. While the standard LP is defined by only non-negativity and edge constraints, a variety of other LP formulations have been studied and one may wonder whether any of them has this property as well. We show that any other formulation that satisfies mild conditions cannot have the persistency property on all graphs, unless it is always equal to the stable set polytope.

     

The strength of Martin-Löf type theory with a superuniverse. Part I

Universes of types were introduced into constructive type theory by Martin-L?f [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say . The universe then “reflects”. This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]). It is proved that Martin-L?f type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal but well below the Bachmann-Howard ordinal. Not many theories of strength between and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. Received: 14 October 1997