The weak pigeonhole principle for function classes in S 12

It is well known that S ¹₂ cannot prove the injective weak pigeonhole principle for polynomial time functions unless RSA is insecure. In this note we investigate the provability of the surjective (dual) weak pigeonhole principle in S ¹₂ for provably weaker function classes. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Abelian groups and quadratic residues in weak arithmetic

We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S₂² + iWPHP(Σ₁^b), and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in S₂² + iWPHP(PV) extended by the pigeonhole principle PHP(PV). We prove the quadratic reciprocity theorem (including the supplementary laws) in the arithmetic theories T₂⁰ + Count₂(PV) and I Δ₀ + Count₂(Δ₀) with modulo‐2 counting principles (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Ordinal notations and well-orderings in bounded arithmetic

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T₂¹ and S₂² can prove the well-foundedness on bounded domains of the ordinal notations below ₀ and Γ₀. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below ₀ and Γ₀ without increasing the class PLS.     

On the correspondence between arithmetic theories and propositional proof systems – a survey

The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11]. Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krají?ek and Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A note on parameter free Π1‐induction and restricted exponentiation

We characterize the sets of all Π₂ and all $\mathcal {B}(\Sigma _{1})We characterize the sets of all Π₂ and all $\mathcal {B}(\Sigma _{1})$ (= Boolean combinations of Σ₁) theorems of IΠ^?₁ in terms of restricted exponentiation, and use these characterizations to prove that both sets are not deductively equivalent. We also discuss how these results generalize to n > 0. As an application, we prove that a conservation theorem of Beklemishev stating that IΠ^?_{n + 1} is conservative over IΣ^?_n with respect to $\mathcal {B}(\Sigma _{n+1})$ sentences cannot be extended to Π_{n + 2} sentences. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim     

Separations of first and second order theories in bounded arithmetic

We prove that PTC_N(n) (the polynomial time closure of the nonstandard natural number n in the model N of S₂.) cannot be a model of U¹₂. This implies that there exists a first order sentence of bounded arithmetic which is provable in U¹₂ but does not hold in PTC_N(n).     

A note on the existence of positive bounded solutions for an epidemic model

In this short note, we establish an existence and uniqueness theorem about a positive bounded solution for a nonlinear infinite delay integral equation, which arises in some epidemic problems. As one can see, our main result can deal with some cases, to which many previous results cannot be applied. In addition, we show that our main result can also be applied to a Lasota–Wazewska model.     

Independence results for weak systems of intuitionistic arithmetic

This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a two‐node PA‐normal Kripke structure which does not force iΣ₂. We prove i?₁ ? i?₁, i?₁ ? i?₁, iΠ₂ ? iΣ₂ and iΣ₂ ? iΠ₂. We use Smorynski's operation Σ′ to show HA ? lΠ₁.     

A note on complete bounded trajectories and attractors for compressible self-gravitating fluids

In this paper we prove the boundedness for energy of weak solutions to the Navier-Stokes equations for compressible self-gravitating fluids in time in bounded domains with arbitrary forces and the adiabatic constant γ∈(3/2,5/3]. Thus the results on the existence of complete bounded trajectories and attractors for compressible self-gravitating fluids can be generalized up to γ>3/2.     

A note on effective ultrapowers: Uniform failure of bounded collection

By suitably adapting an argument of Hirschfeld (see [2, Chapter 9]), we show that there is a single Δ₁ formula that defeats “bounded collection” for any model of II₂ Arithmetic that is either a recursive ultrapower or an existentially complete model. Some related facts are noted. MSC: 03F30, 03C62.     

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.     

On End-Extensions of Models of ¬exp

Every model of IΔ₀ is the tally part of a model of the stringlanguage theory Th-FO (a main feature of which consists in having induction on notation restricted to certain AC⁰. sets). We show how to “smoothly” introduce in Th-FO the binary length function, whereby it is possible to make exponential assumptions in models of Th-FO. These considerations entail that every model of IΔ₀ + ¬exp is a proper initial segment of a model of Th-FO and that a modicum of bounded collection is true in these models. Mathematics Subject Classification: 03F30, 03C62, 68Q15.     

A note on a theorem of Kanovei

We give a short proof of a theorem of Kanovei on separating induction and collection schemes for _n formulas using families of subsets of countable models of arithmetic coded in elementary end extensions.Mathematics Subject Classification (2000): 03C62     

A note on the minimum bounded edge-partition of a tree

Minimum bounded edge-partition divides the edge set of a tree into the minimum number of disjoint connected components given a maximum weight for any component. It is an adaptation of the uniform edge-partition of a tree. An optimization algorithm is developed for this NP-hard problem, based on repeated bin packing of inter-related instances. The algorithm has linear running time for the class of ‘balanced trees’ common for the stochastic programming application which motivated investigation of this problem.Fast 2-approximation algorithms are formed for general instances by replacing the optimal bin packing with almost any bin packing heuristic. The asymptotic worst-case ratio of these approximation algorithms is never better than the absolute worst-case ratio of the bin packing heuristic used.     

A note on the arithmetic of differential equations

In this note we give a method for computing the differential Galois group of some linear second-order ordinary differential equations using arithmetic information, namely the p-curvatures.     

On a class of bounded trajectories for some non‐autonomous systems

We prove, by variational arguments, the existence of a solution to the boundary value problem in the half line ((0.1)) where c ≥ 0 and a belongs to a certain class of positive functions. The existence of such a solution in the case c = 0 means that the system (0.1) behaves in significantly different way from its autonomous counterpart. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A note on the schemes of replacement and collection

We derive the schemes of from certain weak forms of the same.