Falsity and refutations: Understanding the negative side of logic

点击翻译按钮获取中文摘要

In spite of the central role played by the notions of falsity and refutation, as of today there is no agreement on which should be their correct understanding in logic. On the most common view, falsity, refutation and denial play a merely ancillary role compared to their positive counterparts, truth, proof and assertion. Such a view has been opposed by some authors , who called for treating positive and negative notions on a par. How this should be done, however, is still the object of controversies. The goal of the project is to propose a novel picture of logic that does justice to its negative side. Its major contribution will be an analysis of the notion of refutation on its own, i.e. independently of the notion of proof. The project will begin by criticising the traditional view, on which negative notions are subordinated to positive ones, and by proposing to identify the source of this view in a realist conception of meaning. On such a conception, whereas portions of reality - i.e. facts - correspond to true sentences, nothing corresponds to false ones. On current alternative views, which rather rely on a `constructive' conception of meaning, the assertion of a proposition is justified by the possession of a proof of it, and the denial of a proposition is justified by the possession of a refutation of it. The common weakness of both the traditional conception and these alternative views is that, although implication expresses the most important kind of relation between propositions in logic, the conditions at which an implication `if A then B' is false (refuted) are formulated by making reference to the notion of truth (proof): `if A then B' is false (refuted) whenever A is true (proved) and B is false (refuted).The main part of the project will consists in delivering a novel operational understanding of refutations, analogous to the operational understanding of proofs underlying intuitionism. The operative conception of proofs is based on the `Curry-Howard correspondence', that establishes a close connection between logic and computer science, in that a formal derivation can be seen as encoding an algorithm, i.e. the abstract representation of a computer program, that taken a proof of the assumptions as input yields a proof of the conclusion as output. In order to make the notion of refutation precise in this context, we will show how to associate `dual programs' to formal derivations, i.e. programs that take a refutation of the conclusions as input and yield a (collective) refutation of the assumptions as output.On the basis of the proposed understanding of refutations, we will investigate the conditions at which a logical system lends itself to be understood as a ``logic of proof'', as a ``logic of refutation'', or as a synthesis of the two. Moreover, we will introduce tools for developing new logical systems in which proofs and refutations are encoded in different ways and connected by different kinds of negation operators.