# ProjectFalschheit und Widerlegungen: Zur negativen Seite der Logik

## Basic data

Title:

Falschheit und Widerlegungen: Zur negativen Seite der Logik

Duration:

3/1/2018 to 2/1/2021

Abstract / short description:

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.

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.

Keywords:

logic

Logik

proof theory

Beweistheorie

Negation

Widerlegung

Falschheit

## Involved staff

### Managers

Wilhelm Schickard Institute of Computer Science (WSI)

Department of Informatics, Faculty of Science

Department of Informatics, Faculty of Science

## Local organizational units

Wilhelm Schickard Institute of Computer Science (WSI)

Department of Informatics

Faculty of Science

Faculty of Science

## Funders

Bonn, Nordrhein-Westfalen, Germany