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)

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal form and (...) monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts. (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 in place of exp given by Davenport and Roth in 1955, whereαis algebraic of degreed≥ 2 and ∣α−pq−1∣ shrink)