The talk reviews some new and old developments reported in this interesting symposium.

Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the set-theoretic universe is as an indefinite (or “potential”) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a definite (“or completed”) totality, for which classical logic is appropriate; so on that view, set theory should be axiomatized on some correspondingly mixed basis. Similarly, in the case of predicative analysis, the natural numbers are conceived to form a definite totality, while the universe of sets (or functions) of natural numbers are viewed as an indefinite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. In the first part of the talk I will present ways of formulating such semi-constructive systems of analysis and set theory and survey some results characterizing their proof-theoretic strength. Interestingly, though the logic is weakened, one can usefully strengthen certain principles. In the second part of the talk I will go into the questions on that basis of what constitute definite properties of sets and definite statements about sets.

It might be hoped that a good theory of definiteness and indefiniteness would help settle the status of such statements as the Continuum Hypothesis but we are far from any such result.

Following the work of K. Gödel published in 1958, C. Spector gave in 1962 a remarkable characterization of the provably recursive functionals of full second-order arithmetic (a.k.a. analysis). Spector’s interpretation relies on a form of well-founded recursion known as bar-recursion. Spector’s interpretation is rather indirect, via the negative translation. We reprove Spector’s result avoiding the passage through intuitionistic logic, relying instead on the very simple direct interpretation of Peano arithmetic given by J. Shoenﬁeld in 1967. More speciﬁcally, ﬁnite-type Peano arithmetic, extended with the bar-recursive functionals and the quantiﬁer-free axiom of choice, proves the principle of dependent choices and, therefore, full numerical comprehension.

The bounded functional interpretation was introduced in 2005 by P. Oliva and the present author. In its version for classical arithmetic, it is an interpretation which “injects” some non set-theoretical uniformities into Peano arithmetic. The interpretation refutes extensionality as well as simple forms of comprehension for number theoretical functions. Nevertheless, due to its Soundness Theorem, the interpretation is able to extract correct uniform bounds from certain theorems of mathematics (and this opens the way to possible contributions to Proof Mining).

We recently showed that the bounded functional interpretation is compatible (via bar-recursive functionals) with full numerical comprehension.

[The above reported work is in collaboration with P. Engrácia.]

I'll review two recent papers by Yuri Manin applying Hopf algebra renormalization, a technique for taking a continuum limit that originated in quantum field theory, to the process of computation. The connection between the two fields is the notion of a string diagram, a pictorial description of a process that takes one state of a system to another.

Yuri I. Manin Renormalization and Computation I: Motivation and background, arXiv:0904.4921v2

Yuri I. Manin Renormalization and Computation II: Time Cut-off and the Halting Problem, arXiv:0908.3430v1

Category-theoretic language is used in many areas of mathematics and even physics. One of the entrances to this area for a logician is via interpretation of morphisms as proofs, more precisely as natural deductions or (almost the same) Gentzen-style sequent derivations. In particular we explain how symmetric monoidal closed categories correspond in this sense to multiplicative linear logic, that is to proofs without contraction and weakening rules. A general framework connecting categorical notions (functors, natural transformations) with proof-theoretical transformations (like cut-elimination) is presented. For example logical connectives are functors and the relation F(1_A,1_B)=1_{F(A,B)} means that axiom F(A,B)->F(A,B) can be broken into the axioms A->A and B->B. We also explain how proof theory have been used to obtain results in category theory, e.g. to derive coherence theorems from normalization theorems.

Abstract momentum in curved space

By analogy with group theory as an abstraction of symmetry,
geodesic theory can be thought of as an abstraction of momentum.
Groups are relatively complicated, having operations *xy* of
*multiplication*, *x*^{-1} of *inverse*, and a *unit*
*e*, satisfying *(xy)z = x(yz)*, *xe = ex = x*, and *xx*^{-1} = *x*^{-1}*x = e*.
A geodesic space has only the one operation *xy* of *extension*
satisfying *xx = x*, *xyy = x*, and *xyz = xz(yz)* where *xyz* abbreviates
*(xy)z*. The value of *x*_{0}*x*_{1} is the next point *x*_{2} along a
geodesic ...*x*_{-1}, *x*_{0}, *x*_{1}, *x*_{2}, *x*_{3}, ... A fourth equation
*xywz = xzwy* amounts to Euclid's Parallel Postulate in algebraic form,
characterizing the flat or affine spaces.

Many kinds of manifolds are representable as geodesic spaces,
including hyperbolic and elliptic spaces. Any group is made a geodesic
space by defining extension *xy* as the group product *yx*^{-1}*y*.
Many number systems such as integers, rationals, complex numbers, and
quaternions arise as free geodesic spaces on two generators, while
various negatively curved tilings and positively curved polyhedra
arise as quotients of the free space on three generators. A curious
3-point geodesic obtained from *Z*_{4} = {-2, -1, 0, 1} by identifying
-2 and 0 serves as an edge, allowing all undirected graphs
to be represented as geodesic spaces. Lastly, sets are definable as
those geodesic spaces satisfying *xy = x*, making geodesic theory no
less suitable than set theory as a foundation for mathematics.

The treatment of primitive recursion by J. Lambek and P. Scott employs notion of a natural number object in a category. I review application to Gödel's system T and and recent representation (by N. Yanoffsky) of primitive recursive functions as free category with a natural number object. The latter was used Yu. Manin in a paper reviewed in this seminar.

Social aspect of mathematical proofs is often used as an argument against a
possibility (even in principle) to complete any correct informal proof to a
sequence of statements beginning with axioms and proceeding by fixed
inference rules. I review very recent (November 21) talk by N. Vavilov,
chair of algebra at St. Petersburg State University. He advances such an
argument in much sharper form than it is usually done and makes the following
three claims.
Mathematical proof considered as a text proves nothing except the fact of
existence of proofs.
No *serious* mathematical proof can be completely formalized i.e., written
down according to standards advanced by mathematical logic.
The proof of classification of finite simple groups has much higher degree
of reliability than proofs of the majority of generally acknowledged
classical results in the area of topology, analysis or differential
equations.