Curry-Howard, Game Semantics and Herbrand´s Theorem

The famous Herbrand Theorem says that from any first-order classical proof of existence of an element satisfying some propositional property, we can extract a Herbrand disjunction: a complete finite list of possible witnesses -- elements satisfying the property. Herbrand`s Theorem tells us what is the immediate computational content of classical first-order logic: the list of witnesses contained in any Herbrand disjunction. What is of great interest, in the light of this result, is to automatically transform proofs into computer programs in order to compute from any first-order proof of any existential statement a suitable list of witnesses. Indeed, it is one of the most remarkable discoveries in the whole history of logic that logical proofs can be seen as, and actually are, certified computer programs. Each logical inference corresponds to a natural construct of a functional programming language. This was first discovered for constructive proofs, which seems fairly reasonable, but is not at all trivial to establish. The result was then extended to classical proofs, i.e. proofs that may use ineffective principles such as the excluded middle. This correspondence between proofs and programs is known as Curry-Howard isomorphism. Recently, the applicant introduced a Curry-Howard interpretation of classical first-order logic capable of giving an elegant and natural proof of Herbrand`s Theorem. It describes classical proofs as learning-based computer programs, which implement in a logically sound way an efficient process of trial and error: they make hypotheses, test and correct them when they are learned to be wrong. This constructive interpretation is inspired by and has been shown to be tightly connected with Coquand`s game semantics: a program yields a computable winning backtracking strategy for a class of simple games, where two players debate about the truth of a formula. The goal of this project is to obtain new results about Herbrand`s Theorem, using the tools of Curry-Howard correspondence and game semantics. We want to show that the process of cut-elimination in the framework of expansion trees with cut always terminates, by using games semantics. We want to state and prove a confluence result about the Herbrand disjunctions produced by our Curry-Howard correspondence: this is particularly significant because in general classical calculi are non-confluent. We want to prove that our calculus can also interpret a semi-intuitionistic logical system which proves a classically strong form of Markov`s principle and enjoys a computationally richer version of Herbrand`s Theorem, where the witnesses in Herbrand disjunctions are closed terms even for arbitrary complex existentially quantified formulas. Finally, we would like to extend our Curry-Howard interpretation to second-order logic and take the first step towards its implementation.

In the modern world, computing devices are everywhere and not only can operate in parallel, but also communicate with each other by sending and receiving messages. This computing paradigm is known as concurrency. With this project we have connected in a new way logic to concurrent computation. We have obtained concurrent functional programming languages which corresponds to logical proofs. Thanks to this correspondence, known in general as Curry-Howard isomorphism, one can study more easily their complicated computational properties. In particular, we have found that Gödel propositional logic, Dummetts first-order logic, Markovs logic can give type systems for concurrent programs. We also used in a new way game semantics to estimate the cost of running functional programs. Thanks to famous results in logic, evaluation of simply typed functional programs can be seen as a game-like interaction of strategies for certain games. Proving general results about lengths of two-players games brings therefore automatically complexity bounds on the execution of programs. We focused on a very general mathematical definition of game that includes standard games like chess. We obtained refined results about interaction between strategies that can revise and change their previous moves and found a method to measure strategy-complexity. As a consequence, one can compute new, more tight bounds about the complexity of evaluating typed functional programs.