Falschheit und Widerlegungen: Zur negativen Seite der Logik

01/03/2018 to 01/02/2021

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 implicationexpresses 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.