Merlin Carl
Mathematisches Institut
Rheinische Friedrich-Wilhelms-Universität Bonn
Beringstraße 1
D-53115 Bonn
Germany
Office: Beringstraße 4, Room 16
Phone: + 49-228-73-3791
E-mail : carl (at math.uni-bonn.de)
Currently, I am primarily concerned with an approach to simplify fine structure and core model theory. The fine hierarchy, as defined in a paper of Peter Koepke, is built by iterating quantifier-free definability relative to some predicate and considerably refines Jensens J-hierarchy in such a way that the intermediate stages still satisfy a version of the condensation lemma. In Peter Koepkes paper
"A new finestructural hierarchy for the constructible universe", the power of this theory is demonstrated by a comparably short proof of the covering lemma. It is natural to ask whether other important parts of constructible combinatorics like the square principle or morasses as well as the construction of core models based on linear iteration techniques can be carried out in the new theory with a similar effect. It turns out that, to a certain extend, this can indeed be achieved. The same question arises for the construction and proof of the basic properties of core models.
Another occupation of mine is the Naproche project (for a brief description, see below).
I'm also involved in research concerning ordinal computability on "Infinite Time Register Machines"; here is a joint paper with Peter Koepke, Miriam Nasfi, Tim Fischbacher and
Gregor Weckbecker "Infinite Time Register Machines" summarizing our results. (To appear in Archive for Mathematical Logic soon.)
In my Diplomarbeit, I constructed a diophantine equation which is solvable iff ZFC is inconsistent.
There's also a joint work with Prof. Moroz from the Max Planck Institute
"On a diophantine representation of the predicate of provability" about this subject.
Teaching
In the "Bonner Matheclub" , I try to foster interest and skills of mathematically talented pupils by posing challenging problems and teaching ways how to solve them.
In WS 2008/2009, Prof. Koepke and me have organized a seminar on the application of modal logic in the study of number-theoretical provability. The seminar page can be found here:
"Hauptseminar mathematische Logik 08/09" .
In WS 2009/2010, I was the co-organizer of a Hauptseminar on the methods from logic and formal linguistics involved in the Naproche project. See here for more information:
"Hauptseminar mathematische Logik 09/10"
In the current semester, Bernhard Irrgang and me are giving a seminar on recursion theory:
Seminar mathematische Logik 2010
NAPROCHE
It is a striking consequence of Gödel's completeness theorem that all mathematical proofs can in principle be carried out in a formal language that allows a purely syntactical correctness check. The former makes it possible in principle, the latter desirable to have formalizations for most, if not all, proofs. However, these formal languages appear to be ill-adapted to the natural way of thinking and communicating about mathematics; mathematicians tend to use a special kind of natural language with special formulations, vocabulary and abbreviations, enriched with formulas from predicate calculus and logical figures different from and more advanced than the rules of "natural deduction". This form is easier to produce, be read and understand, but forces the proof-check to be done by humans. The "Naproche" (which is short for NAtural language PRoof CHEcker) project is meant as an attempt to shrink this gap between formal and natural language representation of a proof by examining the latter and developping a controlled but rich fragment that can automatically be translated in a form accepted by proof-checking tools like Mizar or Coq.
So far, a software has been written which converts mathematical arguments in a very restricted natural language written in TeXmacs into a linguistic format invented for this purpose, the Proof Representation Structures (PRS). These resemble the well-known Discourse Representation Structures (DRS) from formal linguistics in that they allow similar techniques for anaphorical resolution while at the same time being adapted to mirror the logical architecture of a proof - for example, by representing discourse conditions as lists rather then sets to account for the importance of the order in which sentences appear in a deductive argument. This structures can be exploited by a recursive PRS-checking algorithm which in principle can use any standard proof-checking software as a module.
Further steps will include using a dynamic rather than a static language that can be expanded by definitions, deriving a format for proof-plans, enriching the accepted language and formalizing interesting theories to approach the level of textbook proofs on set theory, logic or linear algebra.