Room P3.10, Mathematics Building

Luís Cruz-Filipe, U Nijmegen, Netherlands

Completeness of first-order logic with partial functions

In most branches of mathematics, total functions are the exception rather than the rule. But representing partiality in formal systems like first-order logic (FOL) or type theory is quite tricky, since by their own nature these systems deal only with total objects. With this in mind, Wiedijk and Zwanenburg introduced an extension of FOL where functions are allowed to be partial and showed that their system was equivalent to FOL with so-called “domain conditions”. In this talk we look at the model theory for their system, which has some unexpected differences from the model theory for FOL, and show that the equivalence they showed also holds at the semantic level. As a consequence, we obtain completess of this system.