This is a purely conceptual paper. It aims at presenting and putting into perspective the idea of a proof-theoretic semantics of the logical operations. The first section briefly surveys various semantic paradigms, and Section 2 focuses on one particular paradigm, namely the proof-theoretic semantics of the logical operations.

According to a main idea of Gentzen the meanings of the logical constants are reflected by the introduction rules in his system of natural deduction. This idea is here understood as saying roughly that a closed argument ending with an introduction is valid provided that its immediate subarguments are valid and that other closed arguments are justified to the extent that they can be brought to introduction form. One main part of the paper is devoted to the exact development of (...) this notion. Another main part of the paper is concerned with a modification of this notion as it occurs in Michael Dummett’s book The Logical Basis of Metaphysics. The two notions are compared and there is a discussion of how they fare as a foundation for a theory of meaning. It is noted that Dummett’s notion has a simpler structure, but it is argued that it is less appropriate for the foundation of a theory of meaning, because the possession of a valid argument for a sentence in Dummett’s sense is not enough to be warranted to assert the sentence. (shrink)

Ludwig Wittgenstein was born in Vienna in 1889 and died in Cambridge in 1951. He studied engineering, first in Berlin and then in Manchester, and he soon began to ask himself philosophical questions about the foundations of mathematics. What are numbers? What sort of truth does a mathematical equation possess? What is the force of proof in pure mathematics? In order to find the answers to such questions, he went to Cambridge in 1911 to work with Russell, who had just (...) produced in collaboration with Whitehead (1861-1947) Principia Mathematica (1910-1913), a monumental treatise which bases mathematics on logic. But on what is logic based? Wittgenstein's attempt to answer this question convinced Russell that he was a genius. During the 1914-8 war he served in the Austrian army and in spare moments continued the work on the foundations of logic which he had begun in 1912. His war-time journal, Notebook s 1914-16 (1961), reveals the development of his ideas more clearly that the final version, Tractatus Logico- Philosophicus, which he published in the early 1920s. (shrink)

The basic ideas of game-theoretical semantics are implicit in logicians' and mathematicians' folklore but used only sporadically (e.g., game quantifiers, back-and-forth methods, partly ordered quantifiers). the general suggestions of this approach for natural languages are emphasized: the univocity of "is," the failure of compositionality, a reconstruction of aristotelian categories, limitations of generative grammars, unity of sentence and discourse semantics, a new treatment of tenses and other temporal notions, etc.

In this volume, Pears examines the internal organization of Wittgenstein's thought and the origins of his philosophy to provide unusually clear insight into the philosopher's ideas. Part I surveys the whole of Wittgenstein's work, while Part II details the central concepts of his early system; both reveal how the details of Wittgenstein's work fit into its general pattern.

The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used in normalization theory. It (...) is argued that these two sorts of concepts must be kept strictly apart. (shrink)

The framework of natural deduction is extended by permitting rules as assumptions which may be discharged in the course of a derivation. this leads to the concept of rules of higher levels and to a general schema for introduction and elimination rules for arbitrary n-ary sentential operators. with respect to this schema, (functional) completeness "or", "if..then" and absurdity is proved.

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)

The notion of normal proof theory, and yet it has been somewhat neglected by the systems of equational logic. The intention here is then to show the normalization procedure for the equational logic of the Labelled Natural Deduction system . With this we believe we are making a step towards filling a gap in the literature on equational logic. Besides presenting a normalization procedure for the LND equational fragment, we employ a new method to prove the normalization theorems for equational (...) logic: proof transformation by rewriting, based on a algebraic calculus on the 'rewrite reasons'. (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)