Since Goedel's famous discovery of the existence of an undecidable sentence in (first-order) Peano Arithmetic in 1931, the relevance of the incompleteness phenomena for so-called "mainstream" mathematics has been intensively debated. The question roughly was: since Goedel's undecidable propositions are mathematically meaningless, does the incompleteness phenomenon matter for "normal mathematics" at all?

A breakthrough occured in the late Seventies, with the discovery by Paris and Harrington that a seemingly innocent variant of the finite Ramsey Theorem is unprovable in Peano Arithmetic (while the finite Ramsey Theorem is provable in a much weaker system).

From then on, a large number of other (more or less) "natural" combinatorial statements have been found to be unprovable in stronger and stronger systems of arithmetic, analysis and even set-theory. Among the high points of this research is Harvery Friedman's proof that Robertson and Seymour's "Graph Minor Theorem" is unprovable from a strong (impredicative) system.

In other terms, many combinatorial theorems have been proved to be provable *only* under the assumption of some unexpectedly strong axiom of infinity.

We will give an overview of past and present research in the study of (arithmetic) unprovability. Research in this area features an interplay between proof theory, recursion theory, model theory, combinatorics, number theory etc. The basic concepts and proof techniques will be illustrated, as well as the current directions of research.

BIOGRAPHICAL SKETCH
Lorenzo Carlucci is currently affiliated with the Computer Science Department of the University of Rome "La Sapienza", as a Research Associate. He is also a Research Fellow of the "Scuola Normale Superiore di Pisa". He got his Ph.D. in Theoretical Computer Science at the "Computer and Information Sciences Department" of the University of Delaware, USA. He got his Ph.D. in Mathematics (spec. Mathematical Logic and Theoretical Computer Science) at the Mathematics Department of the University of Siena. His research interests include Mathematical independence results, proof theory, ordinal analysis and Recursion-theoretic learning theory.
http://www.cis.udel.edu/~carlucci/

We prove a strict correspondence between cut-elimination, acyclicity and denotational semantics in the framework of differential interaction nets with promotion (DIN for short). DIN is an extension of the multiplicative exponential linear logic (MELL) introducing differential operators for the exponentials.

We define the orthogonal TeX Embedding failed! of a net TeX Embedding failed! with conclusion TeX Embedding failed! as the set of all nets TeX Embedding failed! with a conclusion TeX Embedding failed! s.t. the cut between TeX Embedding failed! and TeX Embedding failed! is weak normalizable. Then, we introduce in DIN visible acyclicity, a geometric condition which in usual MELL characterizes those proof-structures which correspond to cliques in coherence spaces. Moreover, we consider finiteness spaces, a generalization of coherence spaces which are at the base of the differential extension of MELL.

Let TeX Embedding failed! be a cut-free net with conclusion TeX Embedding failed!, our results prove that the following conditions are equivalent:

1. TeX Embedding failed! contains all visible acyclic nets with a conclusion TeX Embedding failed!
2. TeX Embedding failed! is visible acyclic
3. TeX Embedding failed! is a finitary relation in the finiteness space associated with TeX Embedding failed!

These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proof-nets, namely: Bechét's theorem (TeX Embedding failed!), weak normalization theorem (TeX Embedding failed!), semantic soundness theorem (TeX Embedding failed!) and Retoré's theorem (TeX Embedding failed!). Above all, it discloses a deep unity in DIN between normalization, visible acyclicity and finiteness spaces, which was present (even if never actually remarked) only in the multiplicative fragment of linear logic.

Phase semantics (Girard 87) and its intuitionistic/noncommutative variants (Abrusci, Okada, Sambin, Troelstra, etc.) are provability semantics for linear logic and its variants. While they are sometimes considered "abstract nonsense" (or at least uninteresting from the viewpoint of computation), one cannot deny that it has a wide range of applications. For instance:

Undecidability (Lafont)
Decidability via finite model property (Lafont, Okada-Terui, Galatos-Jipsen)
Cut-elimination (Okada, Kanovitch-Okada-Scedrov, Belardinelli-Jipsen-Ono)
Denotational completeness (Girard, Streicher)
Conservativity (Kanovitch-Okada-Terui, Hamano-Takemura)
Criteria for cut-elimination (Terui, Ciabattoni-Terui)
Interpolation and amalgamation properties (Terui)
Polarity and Focalization

Thus phase semantics is a good tool for applications, and it is still useful to study it. In this talk, I will survey some uses of phase semantics and try to extract general patterns, hoping that it will lead to more applications and establishment of phase semantics as a solid, concrete and sensible tool.