**Financial support through the following projects:**

UID/MAT/00297/2019

UID/MAT/00297/2013

PEst-OE/MAT/UI0297/2014

PEst-OE/MAT/UI0297/2011

Tuesday, 23 February 2016, 2:00 p.m.

Lecturer: Reinhard Kahle (CMA e DM, FCT-UNL)

Title: "Is there a "Hilbert thesis"?"

Local: Sala de seminários, Edifício VII

Faculdade de Ciências e Tecnologia, Quinta da Torre, Caparica

Abstract: In his introductory paper to first-order logic, Jon Barwise writes in the Handbook of Mathematical Logic (1977):

"... the informal notion of provable used in mathematics is made precise by the formal notion provable in first-order logic. Following a sug[g]estion of Martin Davis, we refer to this view as Hilbert's Thesis."

The relation of informal and formal notion(s) of proof is currently under discussion due to the challenges which modern computer provers issue to mathematics, and one can assume that some kind of "Hilbert's Thesis" is widely accepted by the scientific community.

In the first part of our talk we discuss the nature of the thesis advocated by Barwise (including its attribution to Hilbert). We will compare it, in particular, with Church's Thesis about computability. While Church's Thesis refers to one particular model of computation, Hilbert's Thesis is open to arbitrary axiomatic implementations. We will draw some first conclusions from this difference, in particular, concerning the question, how a "Hilbert thesis" could be formulated more specifically.

Church's Thesis receives some evidence from the fact that it blocks any diagonalization argument by the use of partial functions. In the second part of the talk, we pose the question whether there could be something like a partial proof, giving a formal counterpart to a partial function. The relation would arise from an extension of the Curry-Howard isomorphism to untyped λ terms.