Probabilistic, Quantum and Differential Reasoning


A project of SQIG at IT awaiting support.

Everybody who has worked in formal logic will confirm that it is one of the technically most refractory parts of mathematics. The reason for this is that it deals with rigid, all-or-none concepts, and has very little contact with the continuous concept of the real or of complex number, that is, with mathematical analysis. Yet analysis is the technically most successful and best-elaborated part of mathematics. Thus formal logic is, by the nature of its approach, cut off from the best cultivated portions of mathematics, and forced onto the most difficult part of the mathematical terrain, into combinatorics.

John von Neumann, The General and Logic Theory of Automata, in L. A Jeffress (ed.), Cerebral Mechanisms in Behavior: The Hixon Symposium, New York, John Whiley, 1951, pag 406.

Team Coordinators

Key publications


Mathematical logic was first developed by mathematicians concerned with the consistency of Mathematics. After some initial successes, Hilbert's program of formalizing mathematics for making sure that no such inconsistencies exist came to an abrupt end with Gödel's incompleteness theorems. However, the effort was not lost on several accounts. First, it contributed to the latest information revolution (the advent of the universal computer). Second, several useful fragments of Mathematics have been shown to be decidable (e.g. real closed fields). Third, several interesting results have been proved with the techniques of Mathematical Logic (e.g. independence theorems). Fourth, Mathematical Logic born out of pure math concerns soon became an active field of applied math (e.g. in Artificial Intelligence, Software Engineering).

In recent developments of Applied Mathematical Logic, it has become clear the need for capturing in decidable (or at least semi-decidable) formal systems knowledge about quantitative aspects of the universe of discourse at hand. For instance, one may be interested in the probability of a formula being true. More recently, the quantization drive expanded to other quantitative aspects of reality, including time and space. For instance, for verifying an air traffic control system one needs a formal system capable of reasoning about continuous variables and their derivatives over time. The interest on quantum computation triggered by Shor's algorithm put up yet another challenge to the applied logicians.

The project addresses some of the problems arising in the quantization of logic. As such, it is naturally organized into five tasks, as follows: