Onderzoek

# The power of constructive proofs

Pagina-navigatie:

Wijzig gegevens

Titel The power of constructive proofs 06 / 2009 - 06 / 2015 Lopend OND1342424 NWO

## Samenvatting

 Directe bewijzen zijn door hun expliciete vorm informatiever dan indirecte bewijzen. Het blijkt dat zulke bewijzen nuttige, doch mysterieuze eigenschappen bezitten die niet meteen verklaarbaar zijn uit hun constructieve karakter. Deze eigenschappen willen wij onderzoeken en verklaren.

## Samenvatting (EN)

 Two mathematical proofs can differ in their computational content, even when they prove the same theorem. Consider, for example, the theorem that every number has a prime factorization. A proof of this theorem is constructive if it contains a construction which for every number produces its prime factorization, and it is nonconstructive if it does not, for example because it is a proof by contradiction. Constructive proofs are important in computer science because they provide algorithms and can thus be used for implementation. This proposal, however, is not about the applications of constructive proofs, but about the mathematical properties that they have in common. Although the notion of constructive proof may seem fairly straightforward, it is not: constructive mathematical theories, such as constructive number theory or constructive logic, share properties for which there exists no straightforward explanation. These are the properties we wish to discover and investigate. The admissible rules of a theory, which are the logical inferences that it satisfies, are an example of this. It is conjectured that for all constructive theories the admissible rules are the same, but for most strong theories, such as constructive set theory, this question is at present unsolved. In the proposal we give several other examples of this kind, and introduce methods to approach these problems. The ultimate goal is to know what are the characteristics of constructive proofs, and the aim of this proposal is to provide particular answers.

## Betrokken organisaties

Penvoerder Departement Filosofie en Religiewetenschap (UU) NWO Exacte Wetenschappen - EW (NWO)

## Betrokken personen

Projectleider Dr. R. Iemhoff