Published: 27th January 2011
DOI: 10.4204/EPTCS.47
ISSN: 2075-2180

EPTCS 47

Proceedings Third International Workshop on
Classical Logic and Computation
Brno, Czech Republic, 21-22 August 2010

Edited by: Steffen van Bakel, Stefano Berardi and Ulrich Berger

Invited Presentation: Analyzing proofs based on weak sequential compactness Ulrich Kohlenbach	1
Invited Presentation: Epsilon Substitution for Predicate Logic Grigori Mints	3
Interactive Learning Based Realizability and 1-Backtracking Games Federico Aschieri	6
On Various Negative Translations Gilda Ferreira and Paulo Oliva	21
Superdeduction in Lambda-Bar-Mu-Mu-Tilde Clément Houtmann	34
An applicative theory for FPH Reinhard Kahle and Isabel Oitavem	44
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic Luís Pinto and Tarmo Uustalu	57
Dialectica Interpretation with Marked Counterexamples Trifon Trifonov	73

Analyzing proofs based on weak sequential compactness

Ulrich Kohlenbach (Darmstadt)

Recent work in the 'proof mining' program of extracting effective uniform bounds from proofs in nonlinear analysis ([5]) has started to address proofs that are based on uses of weak sequential compactness in Hilbert space in an abstract setting without any use of separability ([6, 7, 8]). In this talk

we extract explicit uniform rates of metastability (in the sense of T. Tao [9]) from a proof due to F.E. Browder ([3]) on the convergence of approximants to fixed points of nonexpansive mappings that is based on an application of weak sequential compactness and show how the analysis eliminates the use of weak compactness ([7]);
we then extract another rate of metastability (of similar nature) from an alternative proof of Browder's theorem essentially due to Halpern ([4]) that already avoids any use of weak compactness;
finally, obtain an effective uniform rate of metastability for Baillon's ([1]) famous nonlinear ergodic theorem in Hilbert space. In fact, we analyze a proof due to Brezis and Browder ([2]) of Baillon's theorem relative to the use of weak sequential compactness ([8]) This time weak compactness does not seem to be eliminable (Baillon's theorem itself states a weak convergence result) but requires a full treatment of the (monotone) functional interpretation of the weak sequential compactness of bounded closed convex subsets in abstract Hilbert spaces by means of bar recursion (of lowest type). The final result, nevertheless, can be recasted in terms of Gödel's T.

References

[1]	Baillon, J.B., Un théorème de type ergodique pour les contractions non linéaires dans un espace de Hilbert. C.R. Acad. Sci. Paris Sèr. A-B 280, pp. 1511-1514 (1975).
[2]	Brézis, H., Browder, F.E., Nonlinear ergodic theorems. Bull. Amer. Math. Soc. 82, pp. 959-961 (1976).
[3]	Browder, F.E., Convergence of approximants to fixed points of nonexpansive nonlinear mappings in Banach spaces. Arch. Rational Mech. Anal. 24, pp. 82-90 (1967).
[4]	Halpern, B., Fixed points of nonexpanding maps. Bull. Amer. Math. Soc. 73, pp., 957-961 (1967).
[5]	Kohlenbach, U., Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. xx+536pp., Springer Heidelberg-Berlin, 2008.
[6]	Kohlenbach, U., On the logical analysis of proofs based on nonseparable Hilbert space theory. In: Feferman, S., Sieg, W. (eds.), Proofs, Categories and Computations. Essays in Honor of Grigori Mints. College Publications, pp. 131-143 (2010)
[7]	Kohlenbach, U., On quantitative versions of theorems due to F.E. Browder and R. Wittmann. To appear in: Advances in Mathematics.
[8]	Kohlenbach, U., A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Preprint, 18pp., 2010.
[9]	Tao, T., Soft analysis, hard analysis, and the finite convergence principle. Essay posted May 23, 2007. Appeared in: 'T. Tao, Structure and Randomness: Pages from Year One of a Mathematical Blog. AMS, 298pp., 2008'.

Epsilon Substitution for Predicate Logic

Grigori Mints (Stanford)

An epsilon substitution method for first order predicate logic had been described and proved to terminate in the monograph "Grundlagen der Mathematik". We discuss obstacles to extension of this proof to second order logic.

Preliminaries

In the preface to volume 2 of [1] in 1939 P. Bernays wrote:
"At present W. Ackermann is transforming his previous proof presented in the Chapter two of this volume to employ transfinite induction in the form used by Gentzen and cover the whole arithmetical formalism.
When this succeeds - as there are all grounds to expect - then the efficacy of the original Hilbert's Ansatz will be vindicated. In any case already on the base of the Gentzen's proof one can be convinced that the temporary fiasko of the proof theory was caused merely by too high methodological requirements imposed on that theory. Of course the decisive verdict about the fate of proof theory depends on the problem of proving the consistency of the Analysis." [English translation by G. Mints].

Hilbert's Ansatz here refers to the epsilon substitution method introduced by D. Hilbert for a formulation where quantifiers are defined in terms of the ε-symbol ε x F[x] read "some x satisfying F[x] ".

∃ xF[x] ↔ F[ε xF[x]]. Corresponding axioms are critical formulas F[t] → F[ε xF[x]]. Other axioms are tautologies in the case of predicate logic. For arithmetic one adds εe xF[x] ≠ 0 ↔ ¬ F[pd(ε xF(x)] where pd is the predecessor function, plus arithmetic axioms different from mathematical induction.

The principal part of a proof (derivation) in a system based on ε-symbol is a

finite system E of critical formulas.

Substitution method from "Grundlagen der Mathematik"

The goal of the epsilon substitution process for first order logic introduced in this form by W. Ackermann and described in "Grundlagen der Mathematik" [1] is to find a series of substitutions of ε-terms by other terms

S ≡ (e₁,t₁),…,(e_k,t_k) making true some disjunction of instances of E: |E|_S∨…∨|E|_S' is a tautology.

It is instructive to compare this to Herbrand disjunction.
The principal step. Take the ε-term

ε xF[x] of maximal complexity and write given system E of critical formulas as E ≡ E'[ε xF[x]] ∪ { (F[t₁] ≠ F[ε xF[x]]),…,(F[t_k] ≠ F[ε xF[x]]) }. Then replace given system E by the union E'[ε xF] ∪ E'[t₁] ∪ … ∪ E'[t_k] which
1 consists of critical formulas and
2 has smaller complexity.
Hence this substitution process terminates producing required tautological disjunction.

Extension to Second Order Logic

For the Second Order Logic the language is extended by the second order ε-symbols ε XF[X] with the critical formulas

F[T] ≠ F[ε XF[X]], T ≡ λ xG[x]. Quantifiers are defined as before: ∃ XF[X] ≡ F[ε xF[X]].

It is still possible to make one step of the previous method:
Take the ε-term

ε XF[X] of maximal complexity and write given system E of critical formulas as E ≡ E'[ε XF[X]] ∪ { (F[T₁] ≠ F[ε XF[x]]),…,(F[T_k] ≠ F[ε XF[X]]) }. Then replace given system E by the union E'[ε XF] ∪ E'[T₁] ∪ … ∪ E'[T_k] which again consists of critical formulas.
But now because of impredicativity the new system of critical formulas can have higher complexity.

An open Problem. Extend termination proof to second order case.

Difficulties

Even if this substitution process terminates, the proof of termination should use different ideas, most probably from Girard's computability proof.

However there is no Tait-Girard-style computability proof in the literature even for the first order case.
Even in the first order case strong termination fails.
First, as noticed already by Ackermann, the attempt to substitute ε-terms of a non-maximal rank first can destroy some critical formulas.
Second, even for maximal rank, the attempt to substitute for a term of non-maximal degree can lead to a loop even for the first order. Define

e₀ := ε xP(x,0) and consider the following system of critical formulas: P(ε xP(x,0),e₀) ≠ P(ε xP(x,0),0) P(ε xP(x,ε xP(x,e₀)),e₀) ≠ P(ε xP(x,e₀),e₀) Write it as P(e₁,0) ≠ P(e₀,0), P(e₂,e₀) ≠ P(e₁,e₀). If the first critical formula (for the ε-term e₀) is eliminated first, the result is P(e₂,e₀) ≠ P(e₁,e₀), P(e₃,e₁) ≠ P(e₂,e₁) At the n-th step we get P(e_n+2,e_n) ≠ P(e_n+1,e_n), P(e_n+3,e_n+1) ≠ P(e_n+2,e_n+1), so the process loops.

[1] D. Hilbert, and P. Bernays, "Grundlagen der Mathematik", Bd.1,2, Springer 1934, 1939