Infinitely many numbers, infinitely large quantities, infinitely many steps: In mathematics, one has to deal a lot with infinity. Nevertheless, mathematical books have a finite number of pages. How can one talk about infinity using finite expressions? For that reason, the mathematician Stefan Hetzl from the Technical University of Vienna (Institute of Discrete Mathematics and Geometry) wants to connect proof theory, a branch of logic, together with formal language theory. It is anticipated that important new results will be obtained for computer sciences from this link - because infinity lurks within this subject, for instance if you wish to determine whether a computer program will be able to cope with any input taken from an infinite number of possibilities.

The Vienna Science, Research and Technology Fund (WWTF) is supporting Stefan Hetzl’s research project as part of the "Vienna Research Groups for Young Investigators" program with a total of 1.5 million euros. Hetzl will use this money over the next few years to establish his own research group at the Technical University of Vienna.

An infinite number of leap years
Even in everyday life we are dealing with finite descriptions of infinite things, "There are an infinite number of leap years," explains Stefan Hetzl, "but they can be defined by finite rules." The first rule of thumb is that every year that can be divided by four is regarded as a leap year. If the year is also divisible by one hundred, then it is not a leap year - but every four hundred years it is again. So by using variously complicated descriptions, you can describe different classes of years; and with enough rules one can fully define the infinite set of all leap years.

Mathematics always remains incomplete
"It is similar in proof theory," says Stefan Hetzl. "The more powerful the theory of logical rules is, so the more mathematically true statements can be derived from it." You will never reach its boundaries of course, as the great Viennese logician Kurt Goedel proved at the beginning of the Thirties: No logical system can simultaneously include - without exception- all logical truths, while internally being fully consistent. "Theories are always an approximation of the truth, one never reaches the whole truth" said Stefan Hetzl.

Similar to how proof theory is concerned with the way mathematical statements are related to each other and from what they can be derived, formal language theory deals with the rules of grammar, language and statements. "The term 'language' summarizes it quite well," said Stefan Hetzl. "This may be a natural language like English or German, or a computer language; or the set of all mathematical expressions that are formed according to certain rules can also be interpreted as a language". In logic, one works systems of rules with different degrees of power, which allow different statements to be formulated. In formal language theory, one can describe different types of grammar that different languages yield.

Mathematical induction: domino-effect evidence
A particularly powerful instrument of mathematical argumentation (reasoning) is induction. With this, one can prove statements about infinite sets of numbers: the summing up of all odd numbers up to a random maximum number forms a square number; for example: 1 +3 +5 = 9, which is three squared. One proves that by first checking whether it is true for the very first step. After that, one has to show that the statement - if it is valid for an arbitrary step - can always be transferred to the next step (see box below). If that succeeds, then you have proved the statement for an infinite number of possible steps; just like managing to topple an infinitely long chain of Domino stones sequentially by just pushing over the first one and ensuring that each one knocks the next one over.

"This method of induction is very important especially in computer science," says Stefan Hetzl. "When computer programs go through loops, when variables are recursively defined, then induction is the proof-tool of choice." But is it really always useful and relevant? Hetzl hopes to gain new insights into the theoretical foundations of such proof reasoning by linking proof theory with formal language theory.

Demonstrably correct computer programs
A field of work in which such research is of great significance, is software verification: "One wants to have computer programs that run as stable as possible and that behave correctly, no matter what inputs they get," says Hetzl. There are typically an infinite number of different possible inputs - so you can never fully test a computer program through simple trial & error testing. In order to demonstrate that a computer program really functions correctly, one must proceed in a proof-theoretically smart manner so as to cover an infinite number of possibilities using only a finite number of steps.

Stefan Hetzl sees himself primarily as a mathematician, but he has also studied computer science - and so he doesn’t find it difficult to build bridges between these disciplines. The "Vienna Center for Logic and Algorithms", an initiative of the Technical University of Vienna’s Faculty of Informatics existing since 2012, is doing research in the field of logic in a similar manner. "My group will probably work mainly with paper and pencil over the next few years. Then, utilizing the results from this, we will move in the direction of its application", Hetzl announced.

<link http: www.tuwien.ac.at dle pr aktuelles downloads unendlich link_extern> Photo Download

Further information:
Dr. Stefan Hetzl
Institut für Diskrete Mathematik und Geometrie
Technische Universität Wien
Wiedner Hauptstraße 8-10
T: +43-1-58801-104262
<link>stefan.hetzl@tuwien.ac.at