Antonio Piccolomini D'Aragona

We discuss the relationship between different variants of proof-theoretic semantics, particularly those stemming from Dag Prawitz’s initial ideas and some subsequent developments due to Peter Schroeder-Heister. We clarify that the known proofs of incompleteness of intuitionistic logic with respect to (monotonic or non-monotonic) proof-theoretic semantics of the latter kind do not apply to Prawitz’s original semantics. Nevertheless, we settle negatively the question of the completeness of intuitionistic logic with respect to Prawitz’s approach, thus refuting a conjecture he has made. Finally, we point to some features of the discussed variants of proof-theoretic semantics that we consider to be philosophically unsatisfactory.

In a paper from 1998, Göran Sundholm has tried to convince Dag Prawitz that a semantic theory of deduction had better employ three notions of proof: proof-object, proof-act and proof-trace. In Prawitz’s semantics of valid arguments, however, the three notions can be said to collapse into each other. In this paper I shall first of all argue that this collapse results in a number of circularity and decidability problems. I shall also argue that it is maybe for getting rid of these problems that Prawitz’s later theory of grounds seems to allow for an objects-acts-traces distinction partly reminiscent of Sundholm’s. But Prawitz’s ground-theoretic picture retains many significant peculiarities. These mainly concern the way objects, acts and traces relate to each other and the epistemic status assigned to proof-objects. The main aim of this paper is to provide an overview and comparison of Prawitz’s and Sundholm’s semantics, and to argue that the divergences between the two stem from a difference in how Prawitz and Sundholm respectively conceive of the notion of assertion. To conclude, I discuss a problem of vacuous validity recently raised by Prawitz and investigate to some extent the possibility of reading it via Sundholm’s (and Martin-Löf’s) approach(es).

Undoubtedly, the theory of grounds share many points with the whole corpus of Prawitz’s semantic investigations. The questions that Prawitz aims to answer are, after all, the same that had already inspired the semantics of valid arguments and proofs: what are correct inferences and reasoning, and why are they able to convey knowledge, justification, and epistemic constraint? However, radically different—indeed, we could say almost diametrically opposite—is the perspective from which these questions are understood and addressed.

Our mental activity is characterized by a series of processes and acts through which, by elaborating information, knowledge, thoughts and beliefs, we pass to other information, other knowledge, other thoughts and other beliefs. These operations, as well as their purposes, can concern several levels of awareness and voluntariness, varying degrees of complexity, a different use of time and different memory resources, thus implying a greater or lesser force in the results obtained. Frequently, an absolute unconsciousness is accompanied by unintentionality and automatism, and immediacy, rapidity and relative simplicity produce or generate uncertain or fallible acquisitions. At the opposite extreme, the completion of operations can be totally conscious and voluntary, often complex, long and tiring, and lead to a state whose epistemic content seems conclusive and not refutable. Obviously, between these two poles there are many intermediate stages, in which various elements are combined in a partial and heterogeneous way.

In this chapter, we take into account Prawitz’s semantics of valid arguments and proofs. Together with the more recent theory of grounds, these semantics belong to the field of proof-theoretic semantics, and have two main sources of inspiration: on the one hand, some pioneering research by Gentzen; on the other, the fundamental results that Prawitz himself has obtained with reference to some of Gentzen’s theories. Along with other ideas stemming from the related intuitionistic tradition, these two suggestions merge in almost all Prawitz’s semantic investigations. Thus, the next section is dedicated to the introduction of some technical—and arguably indispensable—concepts and results.

Prawitz’s theory of grounds aims to explain how and why some inferences have the epistemic power to confer evidence to the conclusion starting from justified premises. For this question to be answered, in the previous chapters we have suggested the necessity of an approach that formalized the notion of evidence independently from more basic concepts such as truth, valid argument or proof. In this chapter, we will start our discussion of the theory of grounds. Before that, however, it seems to us necessary to indicate the articles to which Prawitz has entrusted the development of his new approach, and that will therefore constitute our sources.

I discuss two possible ways for dealing with a constructive, proof-based notion of logical consequence. The first, qualified as _extensional_, amounts to the idea that a given proof-structure is _justifiable_ under every interpretation of the non-logical terminology it involves. The second, qualified as _intensional_, requires on the contrary that the given proof-structure be _justified_ independently of its non-logical meaning. Contrarily to the extensional approach, the intensional account calls for a prior treatment of the notion of identity of proofs. Identity can be in turn addressed in an _extensional_ or _intensional_ way. Although these issues are obviously of a more general interest, I investigate them in a framework which seems to me to be particularly well-suited for the purpose, i.e., Prawitz’s (non-monotonic) Theory of Grounds.

This book provides philosophers and logicians with a broad spectrum of views on contemporary research on the problem of deduction, its justification and explanation. The variety of distinct approaches exemplified by the single chapters allows for a dialogue between perspectives that, usually, barely communicate with each other. The contributions concern (in a possibly intertwined way) three major perspectives in logic: philosophical, historical, formal. The philosophical perspective has to do with the relationship between deductive validity and truth, and questions the alleged conclusiveness of deduction and its epistemic contribution. It also discusses the role of linguistic acts in deductive practice, and provides a cognitive-didactic contribution on how we may learn through deduction. In the historical perspective, the contributions discuss the ideas of some major historical figures, such as Bolzano, Girard, Gödel, and Peano. Finally, in the formal perspective, the mathematics of deduction is dealt with mainly from an intuitionistic-constructivist or proof-theoretic point of view, with focus on “ecumenic” or internalistic approaches to logical validity, on the nature and identity of proofs, and on dialogical setups. Chapter [14] is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.

This book presents an in-depth and critical reconstruction of Prawitz’s epistemic grounding, and discusses it within the broader field of proof-theoretic semantics. The theory of grounds is also provided with a formal framework, through which several relevant results are proved. Investigating Prawitz’s theory of grounds, this work answers one of the most fundamental questions in logic: why and how do some inferences have the epistemic power to compel us to accept their conclusion, if we have accepted their premises? Prawitz proposes an innovative description of inferential acts, as applications of constructive operations on grounds for the premises, yielding a ground for the conclusion. The book is divided into three parts. In the first, the author discusses the reasons that have led Prawitz to abandon his previous semantics of valid arguments and proofs. The second part presents Prawitz’s grounding as found in his ground-theoretic papers. Finally, in the third part, a formal apparatus is developed, consisting of a class of languages whose terms are equipped with denotation functions associating them to operations and grounds, as well as of a class of systems where important properties of the terms can be proved.

One of Etchemendy's arguments against the Tarskian and model‐theoretic notion of logical truth is based on a reduction principle according to which a universally quantified sentence is true if, and only if, all of its instances are logically true. The reduction of logical truth to mere truth reveals that the concept of validity at play in Tarski and in model‐theory relies upon extra‐logical assumptions. A similar reduction had already been put forward by Prawitz, although not with focus on extra‐logical assumptions. Prawitz's reduction concerns rather the possibility of understanding the Tarskian and model‐theoretic approach as implying any epistemic modality. We take into account a possible strategy that an advocate of Tarski and model‐theory may use against Etchemendy's objection, and argue that this strategy fails with respect to Prawitz's criticism. This permits us to shed light upon a difference between Prawitz's and Etchemendy's standpoints: while Etchemendy's reduction shows that the Tarskian and model‐theoretic notion of logical truth cannot be understood as an adequate formal counterpart of truth‐preservation solely by virtue of logical form, Prawitz's reduction insists on the fact that truth‐preservation solely by virtue of logical form is insufficient for epistemic modality to obtain.