Contemporary logic is pursued almost exclusively in a metamathematical mode. The formalized languages so closely associated, both historically and topically, with modern logic are then systems of formal objects, not systems of expressions. If we want a formalized language to be a language in the proper sense, it has to be equipped with carefully crafted meaning explanations. The topic of this workshop is the contrast between meaningful and merely formal formalized languages. Special attention will be paid to the meaning explanations of Per Martin-Löf's type theory.
11.00 — 12.30. Peter Dybjer (Chalmers University of Technology): Generalised predicativity, tests, and Martin-Löf’s meaning explanations for Intuitionistic Type Theory.
14.00 — 15.30. Ansten Klev (Czech Academy of Sciences): Martin-Löf's dialogue rules.
15.30 — 17.00 Göran Sundholm (Leiden University): The Completeness Theorem? So what!