Functions, proofs, constructions

Aim of the workshop:
---------------------------
The notion of function lays at the core of constructivism. According to the intuitionistic explanation of the meaning of logical constants, a proof of an implication is understood as a function which gives proofs of the consequent when applied to proofs of the antecedent.

How this should be exactly understood is a non-trivial matter and any attempt at clarifying it requires, implicitly or explicitly, to embrace some particular view on the nature of functions. More generally, different ways of accounting for the notion of proof reflect different conceptions of functions.

Gentzen’s methods of proof-analysis depict deductive reasoning as being ultimately constituted by “atomic” operations. Via the Curry-Howard isomorphism these can be viewed as corresponding to basic ingredients of computations. Proofs are thus assumed to be linguistic entities or, at least, that it is through language that proofs are primarily accessed.

An explanation of a different kind (such as Goodman and Kreisel’s theory of constructions or the more recent research programme called ‘logic of proofs’) is one willing to grasp the notion of proof “directly”. Viewing proofs as abstract entities, the focus is not much on the internal structure of their linguistic presentations, but rather on what may be called their ‘behaviour’ (for instance how they can be combined with each other to produce new proofs).

The apparent dichotomy between proofs as constituted by inferential steps, and proofs as abstract “unstructured” entities reflects the duality of the notion of function itself. Should functions be viewed as procedures—piecewise constituted by instructions - or are functions sorts of black boxes to be identified by what they do - giving a value for each input - rather than by how they do it? Are functions primarily given as the denotation of linguistic predicates (in a Fregean manner), or are they rather an already given domain which we disclose through language?

Contact: [email protected]

Confirmed speakers:
---------------------------

• Mark van Atten
• Stefania Centrone
• Thierry Coquand
• Walter Dean
• Fritz Hamm
• Alberto Naibo
• Dag Prawitz
• Peter Schroeder-Heister
• Stewart Shapiro
• Göran Sundholm