Seminar Formale Mathematik
Dozenten
- Prof. Dr. Peter Koepke
- Prof. Dr. Bernhard Schröder
Zeit und Ort
Freitags 10-12 im Zimmer 006.
Inhalt
Vorträge von internen und externen Referenten über Formale Mathematik, d.h., über die axiomatische Durchführung von Mathematik in strikt formalen Sprachen mit strikt formalen Ableitungsregeln. Im Zusammenhang mit dem lokalen Projekt NaProChe (Natural language Proof Checking) wird besonders die Frage diskutiert, inwieweit durch den Einsatz von Softwaresystemen strikt formale Systeme aufgebaut werden können, die für den Benutzer "natürlich" im Sinne des gewöhnlichen mathematischen Arbeitens sind. Das bezieht sich auf Benutzerschnittstellen, verwendete Sprache, Theorien und Beweismethoden.
Die Vorträge finden etwa 14-tägig statt.
Friday, April 15, 11:15-13:00 (one hour later than usual!), EA 60, Room 1.007
Marco Caminati, Classical model theory in Mizar
Abstract:
I have formalized Lindenbaum lemma, satisfiability, Godel's completeness
and Lowenheim-Skolem theorems in Mizar, using a simplified, unified and
coherent framework to encode model theory.
I will describe this framework, focusing in particular on the simplified
syntax for first-order languages (only two special symbols, and no need
for constant symbols) and on the sequent derivation rules adopted (not
requiring to define the concept of free occurrence).
Then I will show how those constructions were used for a new, Henkin-like,
scheme to prove the results hinted above, with emphasis on the role of
each single derivation rule, and on when some standard definitions
(consistency, maximality, rule correctness) of model theory actually need
to come into play.
If time permits, I will also discuss some aspects of the Mizar
implementation of the aforementioned syntax and sequent calculus."
Former Terms