SummaryLooking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to analyse the (...) role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory.RésuméSi on considère la théorie de la démonstration comme une tentative de ‘codifier’ les pas logiques d'une démonstration mathématique, on se rendra compte qu'on n'a pas répondu de façon satisfaisante à la question suivante: quelles sont les règies qui rendent complètement explicite le sens d'un connecteur logique? Le lambda‐calcul a été apparemment plus cohérent, tout simplement parce que l'utilisation du‘λ’ avec sa projection 'apply' est spécifiée par une regie de 'réduction': β‐conversion. Nous essayons d'analyser le rôle des règies de démonstration, en utilisant un système formel de règies conçu pour englober à la fois les notions de la théorie de la démonstration et celles du lambda‐calcul: la Théorie Intuitionniste des Types de Martin‐Löf.ZusammenfassungWenn man Beweistheorie als einen Versuch, ein allgemeines Muster der logischen Schritte in einem mathematischen Beweis zu kodifizieren, betrachtet, so scheint die Frage nach der Art von Regeln , die die Bedeutung von logischen Operatoren vollständig beschreiben, nicht zufriedenstellend beantwortet. Der Lambda‐Kalkül erscheint, kohärenter, einfach deshalb weil der Gebrauch von ‘λ’ zusammen mit dessen Projektion 'apply' durch Regeln bestimmt wird, die man 'Reduktions'‐Regeln nennen kann: β‐Konversion. Wir versuchen, die Rolle von Beweisregeln zu analysieren, indem wir ein Regelsystem verwenden, das sowohl die Begriffe der Beweistheorie als auch diejenigen des Lambda‐Kalküls erfasst, nämlich die Martin‐Löfsche Typentheorie. (shrink)

The intention here is that of giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett–Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i.e. the so-called reduction rules. For that we suggest an extension (...) to the Curry– Howard interpretation which draws on the idea of labelled deduction, and brings back Frege’s device of variable-abstraction to operate on the labels (i.e., proof-terms) alongside formulas of predicate logic. (shrink)

We are concerned with showing how ‘labelled’ Natural Deduction presentation systems based on an extension of the so-called Curry-Howard functional interpretation can help us understand and generalise most of the deduction calculi designed to deal with the logical notion of existential quantification. We present the labelling mechanism for ‘’ using what we call ‘ɛ-terms’, which have the form of ‘a’) in a dual form to the ‘Ax.f’ terms of in the sense that the ‘witness’ is chosen at the time of (...) assertion/introduction.With the intention of demonstrating the generality of our framework, we provide a brief comparison with some other calculi of existentials, including the model-theoretic interpretations of Skolem and Herbrand, indicating the way in which some of the classical results on prenex normal forms can be extended to a wide range of logics. The essential ingredient is to look at the conceptual framework of labelled natural deduction as an attempted reconstruction of Frege's functional calculus where the devices of the Begriffsschrift work separately from, yet in harmony with, those of the Grundgesetze 1. (shrink)

Further to the connections between meaning and use, it seems useful to consider the consequences one is allowed to draw from a proposition as something directly related to its meaning/use. And indeed, Wittgenstein's references to the connections between meaning and the consequences, as well as between use and consequences are sometimes as explicit as his celebrated ‘definition’ of meaning as use given in the Investigations. Here we attempt to collect some of these references, discussing how an intuitive basis for the (...) construction of a more convincing proof-theoretic semantics for the mathematical language can arise out of this connection meaning/use/ consequences. (shrink)

As a celebration of theTractatus100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that “everyone is aware of the holistic character of Wittgenstein’s later philosophy, but it is not so well known that it was already beginning to establish itself in theTractatus” (The False Prison, 1987). From the latter to the former, Stephen Hilmy’s (The Later Wittgenstein, 1987) extensive study of theNachlasshas helped removing classical misconceptions such as (...) Hintikka’s claim that “Wittgenstein in thePhilosophical Investigationsalmost completely gave up the calculus analogy.” Hilmy points out that even in theInvestigationsone finds the use of the calculus/game paradigm to the understanding of language, such as “in operating with the word” (Part I, §559) and “it plays a different part in the calculus”. Hilmy also quotes from a late (1946) unpublished manuscript (MS 130) “this sentence has use in the calculus of language”, which seems to be compatible with “asking whether and how a proposition can be verified is only a particular way of asking ‘How do you mean?’” Central in this back and forth there is an aspect which seems to deserve attention in the discussion of a semantics for the language of mathematics which might be based on (normalisation of) proofs and/or Hintikka/Lorenzen game-dialogue: the explication of consequences. Such a discussion is substantially supported by the use of the open and searchableThe Wittgenstein Archives at the University of Bergen. These findings are framed within the discussion of the meaning of logical constants in the context of natural deduction style rules of inference. (shrink)

The intention here is that of giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett-Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i. e. the so-called reduction rules. For that we suggest an (...) extension to the Curry-Howard interpretation which draws on the idea of labelled deduction, and brings back Frege's device of variable-abstraction to operate on the labels (i. e., proof-terms) alongside formulas of predicate logic. (shrink)

One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.

The intention here is that of giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett–Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i.e. the so-called reduction rules. For that we suggest an extension (...) to the Curry– Howard interpretation which draws on the idea of labelled deduction, and brings back Frege’s device of variable-abstraction to operate on the labels (i.e., proof-terms) alongside formulas of predicate logic. (shrink)

The question of finding a suitable formal account of meaning for the logical signs has troubled many philosophers and logicians since the early days of formal logic, whenever it is even recognised as a problem. Here I attempt to show how two operational approaches to the problem can still be shown to be ‘technically’ equivalent, despite having emerged from two different readings of a single philosophical account, and being essentially distinct with respect to the rôle of ‘will’ in the mathematical (...) activity: on the one hand, the ‘semantics of use’, my own reformulation of P. Martin‐Löf's Intuitionistic Type Theory canonical‐values based semantics by taking the normalisation rules as the key semantical device; and, on the other hand, J. Hintikka's Game‐Theoretical Semantics, where the meaning of logical signs is given via semantical games. The philosophical account from which both emerge is precisely Wittgenstein's later account of propositions, where the notion of ‘language‐games’ is introduced as a key semantical device. Observing that the normalisation rules seem to be able to formalise the explanation of the consequences one can draw from a proposition,3 thus showing the function/purpose/usefulness of its main connective in the calculus of language, it seems reasonable to advocate that such a meta‐mathematical device can be a semantically useful notion which would lead to a more reasonable account of the problem of formulating the meaning of logical constants. (shrink)