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&rsquo\;s methods of proof-analysis depict deductive reasoning as \;being ultimately constituted by &ldquo\;atomic&rdquo\; 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&rsquo\;s \;theory of constructions or the more recent research programme called \;&lsquo\;logic of proofs&rsquo\;) is one willing to grasp the notion of proof \;&ldquo\;directly&rdquo\;. 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 &lsquo\;behaviour&rsquo\; (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 &ldquo\;unstructured&rdquo\; entities reflects the \;duality of the notion of function itself. Should functions be viewed \;as procedures&mdash\;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: \;fun.pro.con@gmail.com
Confirmed speakers:
---------------------------