The idea of proof-theoretic validity originated in the work of Gentzen, when he suggested that the meaning of each logical expression was encapsulated in its introduction-rules. The idea was developed by Prawitz and Dummett, but came under attack by Prior under the soubriquet 'analytic validity'. Logical truths and logical consequences are deemed analytically valid by virtue of following, in a way which the present chapter clarifies, from the meaning of the logical constants. But different logics are (...) based on different rules, confer different meanings and so validate different theorems and consequences, some of which are arguably not true or valid at all. It seems to follow that some analytic statements are in fact false. The moral is that we must be careful what rules we adopt and what meanings we use our rules to determine. (shrink)

Proof-theoretic validity has proven a useful tool for proof-theoretic semantics, because it explains the harmony found in the introduction and elimination rules for the intuitionistic calculus. However, the demonstration that a rule of proof is proof-theoretically valid requires checking an infinite number of cases, which raises the question of whether proof-theoretic validity is decidable. It is proven here that it is for the most prominent formulations in the literature for propositional (...) logic. (shrink)

Prawitz conjectured that the proof-theoretically valid logic is intuitionistic logic. Recent work on proof-theoretic validity has disproven this. In fact, it has been shown that proof-theoretic validity is not even closed under substitution. In this paper, we make a minor modification to the definition of proof-theoretic validity found in Prawitz’s 1973paper ‘Towards a foundation of a general proof theory’ and refined by Schroeder-Heister in ‘Validity concepts in proof- (...) class='Hi'>theoretic semantics’ (2006). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic. (shrink)

The interplay of philosophical ambitions and technical reality have given birth to rich and interesting approaches to explain the oft-claimed special character of mathematical and logical knowledge. Two projects stand out both for their audacity and their innovativeness. These are logicism and proof-theoretic semantics. This dissertation contains three chapters exploring the limits of these two projects. In both cases I find the formal results offer a mixed blessing to the philosophical projects. Chapter 1. Is a logicist bound to (...) the claim that as a matter of analytic truth there is an actual infinity of objects? If Hume’s Principle is analytic then in the standard setting the answer appears to be yes. Hodes’s work pointed to a way out by offering a modal picture in which only a potential infinity was posited. However, this project was abandoned due to apparent failures of cross-world predication. I re-explore this idea and discover that in the setting of the potential infinite one can interpret first-order Peano arithmetic, but not second-order Peano arithmetic. I conclude that in order for the logicist to weaken the metaphysically loaded claim of necessary actual infinities, they must also weaken the mathematics they recover. Chapter 2. There have been several recent results bringing into focus the super-intuitionistic nature of most notions of proof-theoretic validity. But there has been very little work evaluating the consequences of these results. In this chapter, I explore the question of whether these results undermine the claim that proof-theoretic validity shows us which inferences follow from the meaning of the connectives when defined by their introduction rules. It is argued that the super-intuitionistic inferences are valid due to the correspondence between the treatment of the atomic formulas and more complex formulas. And so the goals of proof-theoretic validity are not undermined. Chapter 3. Prawitz (1971) conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister (2019). This chapter resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The chapter further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic.Abstract prepared by Will Stafford extracted partially from the dissertation. (shrink)

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)

I explore, from a proof-theoretic perspective, the hierarchy of classical and paraconsistent logics introduced by Barrio, Pailos and Szmuc in (Journal o f Philosophical Logic,49, 93-120, 2021). First, I provide sequent rules and axioms for all the logics in the hierarchy, for all inferential levels, and establish soundness and completeness results. Second, I show how to extend those systems with a corresponding hierarchy of validity predicates, each one of which is meant to capture “validity” at a (...) different inferential level. Then, I point out two potential philosophical implications of these results. (i) Since the logics in the hierarchy differ from one another on the rules, I argue that each such logic maintains its own distinct identity (contrary to arguments like the one given by Dicher and Paoli in 2019). (ii) Each validity predicate need not capture “validity” at more than one metainferential level. Hence, there are reasons to deny the thesis (put forward in Barrio, E., Rosenblatt, L. & Tajer, D. (Synthese, 2016)) that the validity predicate introduced in by Beall and Murzi in (Journal o f Philosophy,110(3), 143–165, 2013) has to express facts not only about what follows from what, but also about the metarules, etc. (shrink)

In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of intuitionistic propositional (...) logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist’s constructions. This naturality includes Sandqvist’s treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist’s semantics can also be viewed as the natural disjunction in a category of sheaves. (shrink)

Prawitz conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister. This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity (...) by restricting proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic. (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)

In Prawitz’s semantics, the validity of an argument may be defined, either relatively to an atomic base which determines the meaning of the non-logical terminology, or relatively to the whole class of atomic bases, namely as logical validity. In the first case, which may be qualified as local, one has to choose whether validity of arguments is or not monotonic over expansions of bases, while in the second case, which may be qualified as global, one has to (...) choose whether the reduction functions which justify non-primitive inferences are or not base-depending. I claim that these oppositions enjoy some conceptual symmetries, and that these symmetries may be understood as putting restrictions on one’s choice both at the local and at the global level. This produces two different proof-theoretic semantics in line with Prawitz’s tenets. However, I also argue that the symmetries stem from a deeper interaction within Prawitz’s semantics, i.e. non-logical meanings vs interpretation of rules. This interaction is in turn based on some primitive ingredients which, when suitably combined, produce other two Prawitz-compatible readings. The four readings form a diagram where some order relations hold. I finally claim that this diagram is complete, namely that, if we combine the ingredients in ways other than those giving rise to the four readings above, we obtain nothing new, or nothing compatible with general semantic requirements. Thus, symmetries between the local and the global level, and interaction between non-logical meaning and interpretation of rules, produce a complete classification of potential Prawitzian semantics. (shrink)

Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central (...) result shows that Harrop’s rule is valid under substitution, which refutes the completeness conjecture for intuitionistic logic. (shrink)

기존의 증명론적 의미론은 대부분 논리상항의 의미에 대한 증명론적 규명에 그 초점이 맞추어져왔다. 그러나 원자문장의 의미에 대한 증명론적 규명이 이루어지지 않는 한 증명론적 의미론은 불완전한 이론에 머무르게 된다. 이 글에서는 증명론적 의미론의 원자적 기반에 관한 문제가 검토되고 그 해결책이 모색될 것이다. 증명론적 의미론의 대표적인 형태인 프라위츠와 덤밋의 증명론적 타당성개념의 핵심 사항들에 대해 논의하고, 이 이론에 대한 원자적 기반의 문제를 제기한 후, 최소한 귀납적으로 정의된 술어에 관해서는 만족스런 원자적 기반이 마련될 수 있음을 보일 것이며, 이를 넘어서 보다 포괄적인 원자적 기반을 제시하는 문제가 (...) 검토되고 그 해결책이 모색될 것이다. (shrink)

Proof-theoretic semantics is an inferentialist theory of meaning, usually developed in a multiple-assumption and single-conclusion framework. In that framework, this theory seems unable to justify classical logic, so some authors have proposed a multiple-conclusion reformulation to accomplish this goal. In the first part of this paper, the debate originated by this proposal is briefly exposed and used to defend the diverging opinion that proof-theoretic semantics should always endorse a single-assumption and single-conclusion framework. In order to adopt (...) this approach some of its _criteria_ of validity, especially separability, need to be weakened. This choice is evaluated and defended. The main argument in this direction is based on the circular dependences of meaning between multiple assumptions and conjunctions, and between multiple conclusions and disjunctions. In the second part of this paper, some systems that suit the new requirements are proposed for both intuitionistic and classical logic. A proof that they are valid, according to the weakened _criteria_, is sketched. (shrink)

This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusion of a deduction.

Validity, the central concept of the so-called ‘proof-theoretic semantics’ is described as correctly applying to the arguments that denote proofs. In terms of validity, I propose an anti-realist characterization of the notions of truth and correct assertion, at the core of which is the idea that valid arguments may fail to be recognized as such. The proposed account is compared with Dummett’s and Prawitz’s views on the matter.

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed (...) discuss the subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

Dummett’s justification procedures are revisited. They are used as background for the discussion of some conceptual and technical issues in proof-theoretic semantics, especially the role played by assumptions in proof-theoretic definitions of validity.

By maintaining that a conditional sentence can be taken to express the validity of a rule of inference, we offer a solution to the Miners Paradox that leaves both modus ponens and disjunction elimination intact. The solution draws on Sundholm's recently proposed account of Fitch's Paradox.

According to Schroeder-Heister 2018, proof-theoretic semantics is ‘an alternative to truth-condition semantics. It is based on the fundamental assumption that the central notion in terms of which meanings are assigned to certain expressions of our language, in particular to logical constants, is that of proof rather than truth. In this sense proof-theoretic semantics is semantics in terms of proof. Proof-theoretic semantics also means the semantics of proofs, i.e. the semantics of entities which (...) describe how we arrive at certain assertions given certain assumptions.' This text advocates that proof-theoretic semantics, as described above, was an approach to semantical issues in logic that appeared in mainstream philosophical literature at least a couple of centuries before the tradition of general proof theory (cf. Prawitz 1971) came into being. This is done by means of an interpretive analysis of Kant’s 1762 essay Die falsche Spitzfindigkeit der vier syllogistischen Figuren, in which two theses are argued: first, that the issue of justifying the logical validity of inferences is approached by Kant in this text, in a strong sense, in terms of proofs; and second, that the purpose of his effort is to establish a point concerning the semantical equivalence between certain distinct valid inferences. (shrink)

Prawitz proposed certain notions of proof-theoretic validity and conjectured that intuitionistic logic is complete for them [11, 12]. Considering propositional logic, we present a general framework of five abstract conditions which any proof-theoretic semantics should obey. Then we formulate several more specific conditions under which the intuitionistic propositional calculus turns out to be semantically incomplete. Here a crucial role is played by the generalized disjunction principle. Turning to concrete semantics, we show that prominent proposals, including (...) Prawitz’s, satisfy at least one of these conditions, thus rendering IPC semantically incomplete for them. Only for Goldfarb’s [1] proof-theoretic semantics, which deviates from standard approaches, IPC turns out to be complete. Overall, these results show that basic ideas of proof-theoretic semantics for propositional logic are not captured by IPC. (shrink)

Three distinctly different interpretations of Aristotle’s notion of a sullogismos in Prior Analytics can be traced: (1) a valid or invalid premise-conclusion argument (2) a single, logically true conditional proposition and (3) a cogent argumentation or deduction. Remarkably the three interpretations hold similar notions about the logical relationships among the sullogismoi. This is most apparent in their conflating three processes that Aristotle especially distinguishes: completion (A4-6)reduction(A7) and analysis (A45). Interpretive problems result from not sufficiently recognizing Aristotle’s remarkable degree of metalogical (...) sophistication to distinguish logical syntax from semantics and, thus, also from not grasping him to refine the deduction system of his underlying logic. While it is obvious that Aristotle most often uses ‘sullogimos’ to denote a valid argument of a certain kind, we show that at Prior Analytics A4-6, 7, 45 Aristotle specifically treats a sullogismos as an elemental argument pattern having only valid instances and that such a pattern then serves as a rule of deduction in his syllogistic logic. By extracting Aristotle’s understanding of three proof-theoretic processes, this paper provides new insight into what Aristotle thinks reasoning syllogistically is and, moreover, it resolves three problems in the most recent interpretation that takes a sullogismos to be a deduction. (shrink)

This paper presents a novel proof-theoretic account of dialogue coherence. It focuses on an abstract class of cooperative information-oriented dialogues and describes how their structure can be accounted for in terms of a multi-agent hybrid inference system that combines natural deduction with information transfer and observation. We show how certain dialogue structures arise out of the interplay between the inferential roles of logical connectives (i.e., sentence semantics), a rule for transferring information between agents, and a rule for information (...) flow between agents and their environment. The order of explanation is opposite in direction to that adopted in game-theoretic semantics, where sentence semantics (or a notion of valid inference) is derived from winning dialogue strategies. That approach and the current one may, however, be reconcilable, since we focus on cooperative dialogue, whereas the game-theoretic tradition concentrates on adversarial dialogue. (shrink)

This paper presents a novel proof-theoretic account of dialogue coherence. It focuses on an abstract class of cooperative information-oriented dialogues and describes how their structure can be accounted for in terms of a multi-agent hybrid inference system that combines natural deduction with information transfer and observation. We show how certain dialogue structures arise out of the interplay between the inferential roles of logical connectives (i.e., sentence semantics), a rule for transferring information between agents, and a rule for information (...) flow between agents and their environment. The order of explanation is opposite in direction to that adopted in game-theoretic semantics, where sentence semantics (or a notion of valid inference) is derived from winning dialogue strategies. That approach and the current one may, however, be reconcilable, since we focus on cooperative dialogue, whereas the game-theoretic tradition concentrates on adversarial dialogue. (shrink)

The problem analysed in this paper is whether we can gain knowledge by using valid inferences, and how we can explain this process from a model-theoretic perspective. According to the paradox of inference (Cohen & Nagel 1936/1998, 173), it is logically impossible for an inference to be both valid and its conclusion to possess novelty with respect to the premises. I argue in this paper that valid inference has an epistemic significance, i.e., it can be used by an agent (...) to enlarge his knowledge, and this significance can be accounted in model-theoretic terms. I will argue first that the paradox is based on an equivocation, namely, it arises because logical containment, i.e., logical implication, is identified with epistemological containment, i.e., the knowledge of the premises entails the knowledge of the conclusion. Second, I will argue that a truth-conditional theory of meaning has the necessary resources to explain the epistemic significance of valid inferences. I will explain this epistemic significance starting from Carnap’s semantic theory of meaning and Tarski’s notion of satisfaction. In this way I will counter (Prawitz 2012b)’s claim that a truth-conditional theory of meaning is not able to account the legitimacy of valid inferences, i.e., their epistemic significance. (shrink)

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...) previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in Frege (...) and open formulas in Tarksi, we concentrate on the semantic status of predicates. We register a dual attitude of Dummett towards Frege’s ascription of reference to predicates. On the one it is needed to endow quantifiers with their appropriate meaning. On the other hand, the introduction of concepts, as semantic correlate of predicates, smuggles a realist flavor in the overall semantic picture. In concluding the excursus (and with it the chapter), we stress Dummett’s will of developing a semantic picture free from this realist trait. In the second chapter, we present the idea of a proof-theoretic semantics. As for Frege true sentences denotes the truth-value True, so here closed' (i.e. categorical) valid argumentations denotes proofs. If a language contains implication-like operators, in order to characterize the condition of validity of a closed argumentation one has to introduce a notion of validity applying to ‘open’ (i.e. hypothetical) argumentations. We argue that this problem is analogous to the one posed by quantifiers in Frege-Tarksi’s style semantics. That is, implication forces one to introduce notion of validity for argumentations, which is more substantial than the correctness of the assertion of their conclusions. As we saw, the corresponding claim in the truth-based approach—that quantifiers require one to introduce a notion of truth, which is more substantial than the one of an assertion being correct—was the source of realism. Hence, Dummett proposes to reduce the semantic contribution of open argumentations to the one of their ‘closed instances’. In the truth-based perspective, this would correspond to the denial of the need of introducing concepts as the semantic correlates of predicates. We argue that Dummett’s fear, that an irreducible notion of function (represented by the need of ascribing validity to open argumentations) would lead to realism, turns out to be ill-founded. In the third chapter, we discuss the role played by the notion of truth in the anti-realist account. The notion of truth is what the anti-realist needs to cope with the so-called paradox of deduction. The analysis of the paradox yields to distinguishing between the truth of a sentence and the truth of a sentence being recognized. In terms of these conceptual couple, we reconsider the relationship between truth and assertion in an anti-realist perspective. Grounds are provided for a thesis (which was already advanced in chapter two), according to which the notion of the assertion of a sentence being correct is primarily connected only with the canonical means of establishing a sentence. The possibility of establishing a sentence by indirect means is conceptually dependent on the practice of establishing logical relationship of dependence among sentences. That is, the notion of a closed valid non-canonical argumentation is of any theoretical relevance only in presence of a notion of validity applying to open argumentations. In the fourth chapter, we discuss the possibility of characterizing in the proof-theoretic-semantics a notion of refutation. We develop an original characterization of refutations starting from an informal inductive specification of the condition of refutations of logically complex sentences. A sub-structural logic, called dual-intuitionistic logic, stands to this notion in the same relationship in which intuitionistic logic stands to the notion of proof so far consdered. All notions developed in chapter 2 have their corresponding (dual) ones in the framework developed. In particular, the distinctions canonical/non-canonical and closed/open argumentations. In the refutation based perspective, elimination rules have priority over introductions and the (only) assumption over the (many) conclusions. In the conclusions, we indicate the ingredients that an anti-realist approach to meaning should incorporate, in order to avoid the difficulties we registered. The core of an alternative view is a different conception of the relationship between categorical and hypothetical notions, in which the validity of open argumentations is not reduced to that of their instances, but rather it is directly defined. As a limit case, one would get a notion of validity applying to closed argumentations. (shrink)

Prawitz has recently developed a theory of epistemic grounding that differs in many respects from his earlier semantics of arguments and proofs. An innovative approach to inferences yields a new conception of the intertwinement of the notions of valid inference and proof. We aim at singling out three reasons that may have led Prawitz to the ground-theoretic turn, i.e.: a better order in the explanation of the relation between valid inferences and proofs; a notion of valid inference based (...) on which valid inferences and proofs are recognisable as such; a reconstruction of the deductive activity that makes inferences capable of yielding justification per se. These topics are discussed by Prawitz with reference to a very general and ancient question: why and how correct deduction has the epistemic power to compel us to accept its conclusions, provided its premises are justified? We conclude by remarking that, in spite of some improvements, the ground-theoretic approach shares with the previous one a problem of vacuous validity which, as Prawitz himself points out, blocks in both cases a satisfactory explanation of epistemic compulsion. (shrink)

We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in (...) the weight of ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size, and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP. (shrink)

Dag Prawitz’s theory of grounds proposes a fresh approach to valid inferences. Its main aim is to clarify nature and reasons of their epistemic power. The notion of ground is taken to denote what one is in possession of when in a state of evidence, and valid inferences are described in terms of operations that make us pass from grounds we already have to new grounds. Thanks to a rigorously developed proof-as-chains conception, the ground-theoretic framework permits Prawitz to (...) overcome some conceptual difficulties of his earlier proof-theoretic explanation. Though from different points of view, anyway, the two accounts share an issue of recognizability of relevant operational properties. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book (...) opens with an introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of p roofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book (...) opens with an introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

We investigate the philosophical significance of the existence of different semantic systems with respect to which a given deductive system is sound and complete. Our case study will be Corcoran's deductive system D for Aristotelian syllogistic and some of the different semantic systems for syllogistic that have been proposed in the literature. We shall prove that they are not equivalent, in spite of D being sound and complete with respect to each of them. Beyond the specific case of syllogistic, the (...) goal is to offer a general discussion of the relations between informal notions—in this case, an informal notion of deductive validity—and logical apparatuses such as deductive systems and (model-theoretic or other) semantic systems that aim at offering technical, formal accounts of informal notions. Specifically, we will be interested in Kreisel's famous 'squeezing argument'; we shall ask ourselves what a plurality of semantic systems (understood as classes of mathematical structures) may entail for the cogency of specific applications of the squeezing argument. More generally, the analysis brings to the fore the need for criteria of adequacy for semantic systems based on mathematical structures. Without such criteria, the idea that the gap between informal and technical accounts of validity can be bridged is put under pressure. (shrink)

It has been common in contemporary logic and philosophy of logic to identify the validity of an inference with its conclusion being a (logical) consequence of its premisses.

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system (...) N2Int of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped. (shrink)

The Born’s rule to interpret the square of wave function as the probability to get a specific value in measurement has been accepted as a postulate in foundations of quantum mechanics. Although there have been so many attempts at deriving this rule theoretically using different approaches such as frequency operator approach, many-world theory, Bayesian probability and envariance, literature shows that arguments in each of these methods are circular. In view of absence of a convincing theoretical proof, recently some researchers (...) have carried out experiments to validate the rule up-to maximum possible accuracy using multi-order interference (Sinha et al, Science, 329, 418 [2010]). But, a convincing analytical proof of Born’s rule will make us understand the basic process responsible for exact square dependency of probability on wave function. In this paper, by generalizing the method of calculating probability in common experience into quantum mechanics, we prove the Born’s rule for statistical interpretation of wave function. (shrink)

This note is about the “calculational style” of presenting proofs introduced by Dijkstra and Scholten and adopted in some books on theoretical computer science. We define the concept of a calculation, which is a formal counterpart of the idea of a calculational proof. The definition is in terms of a new formalization DS of predicate logic. Any proof tree in the system DS can be represented as a sequence of calculations. This fact shows that any logically valid predicate (...) formula has a calculational proof. (shrink)

This paper analyses the notion of ‘interpretation’, which is often tied to the semantic approach to logic, where it is used when referring to truth-value assignments, for instance. There are, however, other uses of the notion that raise interesting problems. These are the cases in which interpreting a logic is closely related to its justification for a given application. The paper aims to present an understanding of interpretations that supports the model-theoretic characterization of validity to the detriment of (...) the proof-theoretic one. This is done by making use of the hierarchy of ST-related logics. Finally, a localist conception of logic is defended as the natural view stemming from the model-theoretic approach. (shrink)

Take a formula of first-order logic which is a logical consequence of some other formulae according to model theory, and in all those formulae replace schematic letters with English expressions. Is the argument resulting from the replacement valid in the sense that the premisses could not have been true without the conclusion also being true? Can we reason from the model-theoretic concept of logical consequence to the modal concept of validity? Yes, if the model theory is the standard (...) one for sentential logic; no, if it is the standard one for the predicate calculus; and yes, if it is a certain model theory for free logic. These conclusions rely inter alia on some assumptions about possible worlds, which are mapped into the models of model theory. Plural quantification is used in the last section, while part of the reasoning is relegated to an appendix that includes a proof of completeness for a version of free logic. (shrink)

In proof-theoretic semantics, meaning is based on inference. It may be seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formulas is given by an inductive definition generated by provability in a ‘base’ of atomic rules. Base-extension semantics for classical and intuitionistic propositional logic have been explored by several authors. In this paper, we develop base-extension semantics for the classical propositional modal systems (...) K, KT , K4, and S4, with □ as the primary modal operator. We establish appropriate soundness and completeness theorems and establish the duality between □ and a natural presentation of ♢. We also show that our semantics is in its current form not complete with respect to euclidean modal logics. Our formulation makes essential use of relational structures on bases. (shrink)

The paper gives a tentative reconstruction of the classical theory of so called fallacious arguments. Its title refers to the following observations.One of the fallacies listed in traditional logic ispetitio principii. It seem natural to add to the list another, similar fallacy. An argumentationArg + considered as a part of a theoretical contextC commits this fallacy relatively toC, if it contains an inference such that the principle of this inference has not been proved inC. By principle of a given inference (...) the conditional is meant whose antecedent and consequent are the conjuction of all the premisses and the conclusion of the inference respectively.If the principle of a given inference has been proved in a given contextC, the inference is valid relatively toC and the premisses are implying the conclusion relatively toC. Both these concepts, of valid inference and of implication do involve the concept of an effectively performed proof; hence they are pragmatic concepts. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s (...) manifestation argument does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett’s and Dag Prawitz’ philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural deduction. I point out a problem for defining the meaning of negation in this framework and prospects for an account of the (...) meanings of modal operators in terms of rules of inference. (shrink)

In this dissertation, we shall investigate whether Tennant's criterion for paradoxicality(TCP) can be a correct criterion for genuine paradoxes and whether the requirement of a normal derivation(RND) can be a proof-theoretic solution to the paradoxes. Tennant’s criterion has two types of counterexamples. The one is a case which raises the problem of overgeneration that TCP makes a paradoxical derivation non-paradoxical. The other is one which generates the problem of undergeneration that TCP renders a non-paradoxical derivation paradoxical. Chapter 2 (...) deals with the problem of undergeneration and Chapter 3 concerns the problem of overgeneration. Chapter 2 discusses that Tenant’s diagnosis of the counterexample which applies CR−rule and causes the undergeneration problem is not correct and presents a solution to the problem of undergeneration. Chapter 3 argues that Tennant’s diagnosis of the counterexample raising the overgeneration problem is wrong and provides a solution to the problem. Finally, Chapter 4 addresses what should be explicated in order for RND to be a proof-theoretic solution to the paradoxes. (shrink)

From the point of view of proof-theoretic semantics, it is argued that the sequent calculus with introduction rules on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can cope with non-well-founded phenomena such as contradictory reasoning. The fact that, in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as (...) a crucial advantage over natural deduction, where substitution is built into the general framework. (shrink)

Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity Π1 0 and, similarly, for any class Π n 0 . We provide (...) a more general version of the fine structure relationships for iterated reflection principles (due to U. Schmerl [25]). This allows us, in a uniform manner, to analyze main fragments of arithmetic axiomatized by restricted forms of induction, including IΣ n , IΣ n − , IΠ n − and their combinations. We also obtain new conservation results relating the hierarchies of uniform and local reflection principles. In particular, we show that (for a sufficiently broad class of theories T) the uniform Σ1-reflection principle for T is Σ2-conservative over the corresponding local reflection principle. This bears some corollaries on the hierarchies of restricted induction schemata in arithmetic and provides a key tool for our generalization of Schmerl's theorem. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from (...) a technical point of view. (shrink)

In this paper I offer a proof-theoretic defence of meaning-invariant logical pluralism. I argue that there is a relation of co-determination between the operational and structural aspects of a logic. As a result, some features of the consequence relation are induced by the connectives. I propose that a connective is defined by those rules which are conservative and unique, while at the same time expressing only connective-induced structural information. This is the key to stabilizing the meaning of the (...) connectives across multiple determinations of the consequence relation. (shrink)

We further develop a recent new proof (by Greenberger, Horne, and Zeilinger—GHZ) that local deterministic hidden-variable theories are inconsistent with certain strict correlations predicted by quantum mechanics. First, we generalize GHZ's proof so that it applies to factorable stochastic theories, theories in which apparatus hidden variables are causally relevant to measurement results, and theories in which the hidden variables evolve indeterministically prior to the particle-apparatus interactions. Then we adopt a more general measure-theoretic approach which requires that GHZ's (...) argument be modified in order to produce a valid proof. Finally, we motivate our more general proof's assumptions in a somewhat different way from previous authors in order to strengthen the implications of our proof as much as possible. After developing GHZ's proof along these lines, we then consider the analogue, for our proof, of Bohr's reply to the EPR argument, and conclude (pace GHZ) that in at least one respect (viz. that of most concern to Bohr) the proof is no more powerful than Bell's. Nevertheless, we point out some new advantages of our proof over Bell's, and over other algebraic proofs of nonlocality. And we conclude by giving a modified version of our proof that, like Bell's, does not rely on experimentally unrealizable strict correlations, but still leads to a testable “quasi-algebraic” locality inequality.“... to admit things not visible to the gross creatures that we are is, in my opinion, to show a decent humility, and not just a lamentable addiction to metaphysics.”J. S. Bell. (shrink)

By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$ , is $\Pi_{n+2}$ conservative over $I\Sigma_n$ . We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left (...) open by Sieg [23] and Hájek [9]. We also give a new proof of independence of $B\Sigma_{n+1}$ over $I\Sigma_n$ by a direct recursion-theoretic argument and answer an open problem formulated by Gaifman and Dimitracopoulos [8]. (shrink)