Mathematical Logic Seminar Abstracts Autumn 2009

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. Shoenfield in 1967. More specifically, finite-type Peano arithmetic, extended with the bar-recursive functionals and the quantifier-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

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^-1x = 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₀x₁ is the next point x₂ along a geodesic ...x_-1, x₀, x₁, x₂, x₃, ... 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^-1y. 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₄ = {-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.