Nordic Online Logic Seminar

Databases are typically assumed to have definite content so that users can pose queries and retrieve unambiguous answers. It is often the case, however, that a database may contain information that is incomplete, inconsistent, or uncertain. Possible world semantics provides meaning to logic-based queries on databases suffering from these deficiencies. Such databases are viewed as compact representations of all their possible rectifications; by definition, the certain answers are the query answers that hold true in every possible rectification of a deficient database.

The goal of this lecture is to provide an overview of some of the work on certain answers as a unifying framework for coping with incompleteness, inconsistency, and uncertainty in databases. Case studies include inconsistent databases, probabilistic databases, and election databases in social choice theory.

The idea of articulating a propositional logic that adds a relevance-sensitive implication connective to the usual truth-functional ones has been approached in many ways, e.g. using axioms and derivation rules, natural deduction systems, possible worlds or states equipped with relations or operations, algebraic structures, consecution systems etc. None are very satisfactory. In the 1970s, semantic decomposition trees (aka truth-trees, semantic tableaux, analytic tableaux) were briefly considered, but they did not get far and were swept away by the tsunami of Routley/Meyer possible worlds with ternary relations. We renew that approach using a notion of parity for the branches of a tree or, alternatively, an even more global one of sibling-parity for the entire tree. There are some nice results and, above all, some big open questions.

There is a long tradition of distinguishing finistic methods of reasoning, for both philosophical and mathematical motivations. Typically, this is made precise by reducing arguments to some theory of arithmetic – usually Peano or Heyting Arithmetic, or weaker fragments thereof. However, working directly in such systems requires encoding all objects as numbers; it is easy to get the impression that such coding is an inherent and inevitable aspect of the topic.

On the contrary, most major foundational logics – in particular, ZF-style set theory and dependent type theories – admit finitistic variants, equivalent in strength to suitable systems of arithmetic. These allow us to work rigorously in a finististic foundation, while keeping the richly expressive language we’re used to from everyday mathematics.

I will survey various finitistic systems, and then focus in more detail on the categorical Arithmetic Universes of Joyal, and type theories for these, following Maietti.

In this talk I will briefly outline Krister’s biography, focusing mainly on the early nineties onwards when I became Krister’s first PhD student. By appeal (mostly) to anecdote I will try to highlight what I take to be some of the most notable features in Krister’s approach to and views on pilosophically inspired logical research and education.