We describe a short model-theoretic proof of an extended normal form theorem for derivations in predicate logic which implies in PRA a normal form theorem for the arithmetic derivations . Consider the Gentzen-type formulation of predicate logic with invertible rules. A derivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is () or () and b is its eigenvariable. Free (...) variables of such derivation are eigenvariables and free variables of its last sequent. Then any sequent derivable in predicate logic has a cut-free derivation with proper variables where the main formula of any antecedent rule is underivable. The proof is by a simple modification of the construction of a countermodel of the formula from the open branch of its canonical proof-search tree. It extends to intuitionistic and higher order systems. The proof of the corresponding normalization theorem outlined in [8] uses the passage to the infinitary derivations enriched by finitary derivations. The normal form after a modification to make it decidable can be considered as a realization of Gentzen's idea stated at the end of [2], that his notion of reduction for arithmetic can be extended to other fields of mathematics. (shrink)

This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...) . In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical assumptions x (...) εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)

Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology composed of instances of (...) the end-sequent and the cut formulas. This tautology describes the proof in the following way: Each cut induces a formula stating that a disjunction of instances of the cut formula implies a conjunction of instances of the cut formula. All these cut-implications together then imply the already existing instances of the end-sequent. The proof that this formula is a tautology is carried out by transforming the instances in the proof to normal forms and using characteristic clause sets to relate them. These clause sets have first been studied in the context of cut-elimination.This extended Herbrand theorem is then applied to cut-elimination sequences in order to show that, for the computation of an Herbrand-disjunction, the knowledge of only the term substitutions performed during cut-elimination is already sufficient. (shrink)