Reasoning without believing: On the mechanisation of presuppositions and partiality

It is well known that many relevant aspects of everyday reasoning based on natural language cannot be adequately expressed in classical first-order logic. In this paper we address two of the problems, firstly that of so-called presuppositions, expressions from which it is possible to draw implicit conclusions, which classical logic normally does not warrant, and secondly the problem of partiality and the adequate treatment of undefined expressions. In natural language, presuppositions are quite common; however, they cannot be sufficiently modelled in classical first-order logic. For instance, in the case of universal restricted quantification in natural language it is typically presupposed that these restrictions are non-empty, whereas in classical logic it is only assumed that the whole universe is non-empty. Conversely, all constants mentioned in classical logic are presupposed to denote something, while it creates no problems to speak about hypothetical objects in everyday language. Similarly, undefined expressions can be handled in natural language discourses, and utterances are not only classified into the two categories true and false. This has led to the development of various better-suited many-valued logics. By combining different approaches we can now give a static description of presuppositions and undefinedness within the same framework. Additionally, we have developed an efficient mechanisation of the induced consequence relation by combining methods from many-valued truth-functional logics and sort techniques developed for search control in automated theorem proving.