Switch to: Citations
References in:
Add references
You mustlogin to add references.
| |
We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...) generalized to relate a hierarchy of subsystems, all contained in the theory of arithmetic properties, to a corresponding hierarchy of fragments of arithmetic. The proof theoretic tools employed there are used to re-establish in a uniform, elementary way relationships between various fragments of arithmetic due to Parsons, Paris and Kirby, and Friedman. (shrink) | |
A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs of Σ 2 -finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due (...) to Roth himself and to Esnault and Viehweg. The analysis of the former yields an exponential bound of order exp(70ε -2 d 2 ) in place of exp(285ε -2 d 2 ) given by Davenport and Roth in 1955, where α is (real) algebraic of degree d ≥ 2 and $|\alpha - pq^{-1}| . (Thus the new bound is less than the fourth root of the old one.) The new bounds extracted from the other proof are polynomial of low degree (in ε -1 and log d). Corollaries: Apart from a new bound for the number of solutions of the corresponding Diophantine equations and inequalities (among them Thue's inequality), $\log \log q_\nu , where q ν are the denominators of the convergents to the continued fraction of α. (shrink) | |
We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...) sub-classical logic Limit Computable Mathematics [6], Hayashi and Nakata [7]). (shrink) | |
We consider the extent to which one can compute bounds on the rate of convergence of a sequence of ergodic averages. It is not difficult to construct an example of a computable Lebesgue measure preserving transformation of [0, 1] and a characteristic function f = χA such that the ergodic averages Anf do not converge to a computable element of L2([0, 1]). In particular, there is no computable bound on the rate of convergence for that sequence. On the other hand, (...) we show that, for any nonexpansive linear operator T on a separable Hilbert space and any element f , it is possible to compute a bound on the rate of convergence of Anf from T , f , and the norm f ∗ of the limit. In particular, if T is the Koopman operator arising from a computable ergodic measure preserving transformation of a probability space X and f is any computable element of L2 (X ), then there is a computable bound on the rate of convergence of the sequence Anf. (shrink) | |
In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems which (...) allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink) | |
We prove a soundness and completeness result for Aschieri and Berardiʼs learning based realizability for Heyting Arithmetic plus Excluded Middle over semi-decidable statements with respect to 1-Backtracking Coquand game semantics. First, we prove that learning based realizability is sound with respect to 1-Backtracking Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizers and winning strategy extraction for some classical proofs. (...) Secondly, we extend our notion of realizability to a total recursive learning based realizability and show that the notion is complete with respect to 1-Backtracking Coquand game semantics. (shrink) | |
We give a constructive analysis of learning as it arises in various computational interpretations of classical Peano Arithmetic, such as Aschieri and Berardi learning based realizability, Avigad’s update procedures and epsilon substitution method. In particular, we show how to compute in Gödel’s system T upper bounds on the length of learning processes, which are themselves represented in T through learning based realizability. The result is achieved by the introduction of a new non standard model of Gödel’s T, whose new basic (...) objects are pairs of non standard natural numbers and moduli of convergence, where the latter are objects giving constructive information about the former. As a foundational corollary, we obtain that that learning based realizability is a constructive interpretation of Heyting Arithmetic plus excluded middle over Σ10 formulas and of all Peano Arithmetic when combined with Gödel’s double negation translation. As a byproduct of our approach, we also obtain a new proof of Avigad’s theorem for update procedures and thus of the termination of the epsilon substitution method for PA. (shrink) | |
Home |New books and articles |Bibliographies |Philosophy journals |About PhilPapers |API |Contact us |Code of conduct
PhilPapers logo byAndrea Andrews andMeghan Driscoll.
This site uses cookies and Google Analytics (see ourterms & conditions for details regarding the privacy implications).Use of this site is subject toterms & conditions.
All rights reserved byThe PhilPapers Foundation
Server: philpapers-web-5b9ff6f457-q9rxf uwo