A formalization of Sambins's normalization for GL

Sambin [6] proved the normalization theorem (Hauptsatz) for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45.     

A new reduction sequence for arithmetic

The main type of result in proof theory having external applications is normalization theorems: any derivation can be reduced to normal form with the help of a finite number of standard transformations (reductions). An estimate for the convergence of the process of normalization gives an estimate for the growth of provable recursive functions, which recently found application to finitary combinatorics [J. Paris and L. Harrington, A mathematical incompleteness in Peano arithmetic, in: Handbook of Mathematical Logic (1978), pp. 1133–1142]. The definition of reduction for the predicate calculus and arithmetic is due to Gentzen, who proved a normalization theorem for derivations of atomic formulas and gave an estimate for convergence with the help of an assignment to derivations d of ordinals O(d)<₀ such that O(d)>O(d) for reductions ¯d of the derivation d. Later convergence was proved for arbitrary derivations; however, the slight clarity in the choice of ¯d and the proof of decrease of ordinals impede understanding and exposition: both Takeuti (G. Takeuti, Proof Theory, North-Holland, 1975) and Schütte (Ref. Zh. Mat., 1978, 7A48K) restrict themselves to derivations of atomic formulas. In the presentpaper there is given a shorter and clearer construction of reduction ¯d and assignment of ordinals, allowing one also to simplify the proof of decrease of ordinals. The source of all the simplifications is the connection with the continuous operator of cut elimination from infinite derivations proposed by the author. In particular, the symbol O_k(d), in terms of which O(d) is defined, can be read as ordinal height of the derivation, obtained after elimination of cuts of degree k from an infinite derivation in which d is represented in a standard way. We consider the L-formulation, where there are rules of introduction of connectives in the antecedent and succedent. Extension to the natural formulation is obtained with the help of Prawitz translation.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 106–126, 1979.     

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.     

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.     

Simplification of Gentzen's reductions in classical arithmetic

The reduction of proofs of classical arithmetic applied by G. Gentzen in 1936 has not so far been used. The article offers a reduction which is a considerable simplification of that reduction. It can be used for proof normalization. The proof ordinal used is strictly monotone.     

What can be done with PRA?

Let S⁺ denote system JR _° ² + AC _° ¹ in a classical second-order arithmetic, in which the induction rule is permitted to apply only to quantifier-free formulas and to _° ² -formulas not containing functional variables, while the convolution axiom is permitted to apply only to _° ¹ -formulas without functional variables. Also postulated is the closedness of the function class being examined, relative to primitive recursive operations. System, S⁺ turns out to be sufficiently rich: in it a theory of recursions and an elementary recursive analysis can be developed, a theorem on the continuity of effective operators and a theorem on cuteliminability from -deductions can be proved, and the usual analytic proofs of many number-theoretic theorems, including the prime distribution law, can be derived (with insignificant changes). (A formalization in S⁺ of the proof of Konig's lemma on paths in binary trees and of Godel's completeness theorem is described in the note.) On the other hand, the system admits of an interpretation in primitive recursive arithmetic (PRA). In particular, quantifier-free theorems in S⁺ are deducible in PRA, while theorems of form xyR(x,y) with a quantifier-free formula R have calculi R (x,(x)) with primitive recursive function , deducible in PRA. Thus, the suppressing part of operating constructive analysis can be developed already at the finite stages of the Shanin majorant hierarchy. In addition, a purely mechanical method exists for obtaining elementary number-theoretic proofs from many analytic proofs.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akad. Nauk SSSR, Vol. 60, pp. 93–102, 1976. Results announced September 4, 1975.     

Epsilon substitution method for elementary analysis

We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.     

Theo: An interactive proof development system

This paper presents an interactive, tactic-driven, proof development system, a Theorem Prover calledTheo. Both the meta and the object levels of our theorem prover are logics presented in Typol. Typol is the programming language that implements Natural Semantics, a semantics developed at Inria and pioneered by G. Plotkin under the name Structural Operational Semantics. So Theo is written in Typol and helps the user to build proofs in an object logic also written in Typol. Tactics and tacticals are written in Typol. Other important features of Theo are the form chosen for representing proofs, and the way proofs are performed. The internal form of the proofs is very compact, expressed with combinators, that can be related to the -calculus used in Automath and its descendants. Meanwhile, Theo performs proofs by a pure calculus on proofs, using a resolution rule. Proofs may be incomplete and may contain logical variables. Theo is developed under the Centaur system, as well as Typol. This system provides a modern graphic man-machine interface that Theo uses, for the user's advantage.     

Basic Predicate Calculus is not Sound with Respect to the Strong Variant of Strictly Primitive Recursive Realizability

Mathematical Notes - It is proved that basic predicate calculus BQC is not sound with respect to the strong variant of strictly primitive recursive realizability.     

Generating the Greatest Common Divisor,and Limitations of Primitive Recursive Algorithms

The greatest common divisor of two integers cannot be generated in a uniformly bounded number of steps from those integers using arithmetic operations. The proof uses an elementary model-theoretic construction that enables us to focus on integers with transcendental ratio. This unboundedness result is part of the solution of a problem posed by Y. Moschovakis on limitations of primitive recursive algorithms for computing the greatest common divisor function.     

Three ways of recognizing inessential formulas in sequents

The first method is based on the familiar method of lowering thinnings downwards and is a further development of the lemmas on weeding of [1]. The second method is based on the use of sufficiently wide classes of sequents, for which derivability in the intuitionistic predicate calculus coincides with derivability in the classical predicate calculus and the familiar property of disjunction is true. By this method one can get, e.g., a syntactic proof of the following assertion. If the positive formula A is derivable in the theory of groups under additional assumptions of the form then A is also derivable in the theory of groups without these assumptions. As the third method there is proposed a syntactically formulated test for the conservativeness of extensions of intuitionistic axiomatic theories. With the help of this test one can get, for example, a syntactic proof of the hereditary undecidability of the intuitionistic theory of equality, with additional axioms which are the formula, all formulas of the form and all negations of formulas derivable in the classical predicate calculus.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 163–175, 1979.     

A Rigorous Proof of the Waterloo Algorithm for the Discrete Logarithm Problem

In this paper we are concerned with the Waterloo variant of the index calculus method for the discrete logarithm problem in . We provide a rigorous proof for the heuristic arguments for the running time of the Waterloo algorithm. This implies in studying the behavior of pairs of coprime smooth polynomials over finite fields. Our proof involves a double saddle point method, and it is in nature similar to the one of Odlyzko for the rigorous analysis of the basic index calculus.     

On the contrapositive of countable choice

We show that in elementary analysis (EL) the contrapositive of countable choice is equivalent to double negation elimination for ${\Sigma_{2}^{0}}$ -formulas. By also proving a recursive adaptation of this equivalence in Heyting arithmetic (HA), we give an instance of the conservativity of EL over HA with respect to recursive functions and predicates. As a complement, we prove in HA enriched with the (extended) Church thesis that every decidable predicate is recursive.     

Upper bound on the lengthening of proofs by cut elimination

In this paper there are constructed sequential calculi KGL and IGL. The calculus KGI is a version of the classical predicate calculus, and IGL is a version of constructive calculus. KGL and IGL do not contain structural rules and there are no rules in them for which in some premise more than one lateral formula would be contained. A procedure for eliminating cuts from proofs in these calculi is described. It is shown that the height of a derivation obtained by this procedure exceeds 2 ^h, where h is the height of the original derivation, is the number of sequences in the original derivation,.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 137, pp. 87–98, 1984.     

Read-Once Branching Programs, Rectangular Proofs of the Pigeonhole Principle and the Transversal Calculus

We investigate read-once branching programs for the following search problem: given a Boolean m × n matrix with m > n, nd either an all-zero row, or two 1s in some column. Our primary motivation is that this models regular resolution proofs of the pigeonhole principle , and that for m > n ² no lower bounds are known for the length of such proofs. We prove exponential lower bounds (for arbitrarily large m!) if we further restrict this model by requiring the branching program either to finish one row of queries before asking queries about another row (the row model) or put the dual column restriction (the column model).Then we investigate a special class of resolution proofs for that operate with positive clauses of rectangular shape; we call this fragment the rectangular calculus. We show that all known upper bounds on the size of resolution proofs of actually give rise to proofs in this calculus and, inspired by this fact, also give a remarkably simple rectangular reformulation of the Haken–Buss–Turán lower bound for the case m n ². Finally we show that the rectangular calculus is equivalent to the column model on the one hand, and to transversal calculus on the other hand, where the latter is a natural proof system for estimating from below the transversal size of set families. In particular, our exponential lower bound for the column model translates both to the rectangular and transversal calculi.* Part of the work was done while this author was visiting Special Year on Logic and Algorithms at DIMACS, Princeton. Also supported by Russian Basic Research Foundation grant 96-01-01222. Part of this work was done while on sabbatical leave at the Institute for Advanced Study and Princeton University, Princeton. This work was supported by USA-Israel BSF grant 92-00106 and by a Wolfson research award administered by the Israeli Academy of Sciences, as well as a Sloan Foundation grant. This work was supported in part by National Science Foundation and DARPA under grant CCR-9627819, and by USA-Israel BSF grant 92-00106.     

Epsilon substitution for $$\textit{ID}_1$$ via cut-elimination

The \(\epsilon \)-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \(\textit{ID}_1\) using a variant of the cut-elimination formalism introduced by Mints.     

Strong normalization of barrecursive terms without using infinite terms

In this paper a new proof of the strong normalization theorem (SN) for barrecursive terms is presented.The proof is based on a syntactical version of Howard's compactness of functionals of finite type (see [T, 2.8.6]). The proofs of Tait [Ta], Luckhardt [L], and Vogel [V] are all based on continuity. These proofs use infinite terms: ifT ₀,T ₁, ... is an infinite sequence of terms of type , then T ₀,T ₁, ... is an infinite term of type (0). The proof below does not make use of infinite terms.     

Randomized proofs in arithmetic

A randomized proof system for arithmetic is introduced. A proof of an arithmetical formula is defined as its derivation from the axioms of arithmetic by the standard rules of inference of arithmetic and also one more rule which we call the random substitution rule. Such proofs can be regarded as a special kind of interactive proof and, more exactly, as a special kind of the Arthur-Merlin proofs. The main result of the paper shows that a proof in arithmetic with the random substitution rule can be considerably shorter than an arithmetical proof of the same formula. Namely, there exists a set of formulas such that (i) these formulas are provable in arithmetic but, unless PSPACE=NP, do not have polynomially long proofs; (ii) these proofs have polynomially long proofs in arithmetic with random substitution (whatever random numbers appear) and the probability of error of these proofs is exponentially small. Bibliography: 10 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 49–71. Translated by E. Ya. Dantsin.     

Large step volumetric potential reduction algorithms for linear programming

We consider the construction of potential reduction algorithms using volumetric, and mixed volumetric — logarithmic, barriers. These are true large step methods, where dual updates produce constant-factor reductions in the primal-dual gap. Using a mixed volumetric — logarithmic barrier we obtain an iteration algorithm, improving on the best previously known complexity for a large step method. Our results complement those of Vaidya and Atkinson on small step volumetric, and mixed volumetric — logarithmic, barrier function algorithms. We also obtain simplified proofs of fundamental properties of the volumetric barrier, originally due to Vaidya.Research supported by a Summer Research Grant from the College of Business Administration, University of Iowa.