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)

In this paper we show how Dummett-Prawitz-style proof-theoretic semantics has to be modified in order to cope with paradoxical phenomena. It will turn out that one of its basic tenets has to be given up, namely the definition of the correctness of an inference as validity preservation. As a result, the notions of an argument being valid and of an argument being constituted by correct inference rules will no more coincide. The gap between the two notions is accounted for by (...) introducing the distinction between sense and denotation in the proof-theoretic-semantic setting. (shrink)

The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.

The hypothetical notion of consequence is normally understood as the transmission of a categorical notion from premisses to conclusion. In model-theoretic semantics this categorical notion is 'truth', in standard proof-theoretic semantics it is 'canonical provability'. Three underlying dogmas, (I) the priority of the categorical over the hypothetical, (II) the transmission view of consequence, and (III) the identification of consequence and correctness of inference are criticized from an alternative view of proof-theoretic semantics. It is argued that consequence is a basic semantical (...) concept which is directly governed by elementary reasoning principles such as definitional closure and definitional reflection, and not reduced to a categorical concept. This understanding of consequence allows in particular to deal with non-wellfounded phenomena as they arise from circular definitions. (shrink)

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

Such a conception, says Dummett, will form "a base camp for an assault on the metaphysical peaks: I have no greater ambition in this book than to set up a base ...

In this paper it is shown that addition of certain reductions to the standard cut removing reductions of deductions in prepositional logic makes prepositional logic non-normalizable. From this follows that some provable propositions in prepositional logic has no direct proof.