We reconstruct Frege’s treatment of certain deducibility problems posed by Boole. It turns out that in his formalization and solution of Boole’s problems Frege anticipates the idea of propositional resolution.

This highly acclaimed book is a major contribution to the philosophy of language as well as a systematic interpretation of Frege, indisputably the father of ...

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.

Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases, going back to Crabbé and Tennant, show that the criterion overgenerates, that is, there are derivations which are intuitively non-paradoxical but which fail to normalize. Tennant’s proposed solution consists in reformulating natural deduction elimination rules in general form. Developing intuitions of Ekman we show that (...) the adoption of general rules has the consequence of hiding redundancies within derivations. Once reductions to get rid of the hidden redundancies are devised, it is clear that the adoption of general elimination rules offers no remedy to the overgeneration of the Prawitz–Tennant analysis. In this way, we indirectly provide further support for a solution to one of the two overgeneration cases developed in previous work. (shrink)

This special issue on general proof theory collects papers resulting from the conference on general proof theory held in November 2015 in Tübingen.

Prawitz observed that Russell’s paradox in naive set theory yields a derivation of absurdity whose reduction sequence loops. Building on this observation, and based on numerous examples, Tennant claimed that this looping feature, or more generally, the fact that derivations of absurdity do not normalize, is characteristic of the paradoxes. Striking results by Ekman show that looping reduction sequences are already obtained in minimal propositional logic, when certain reduction steps, which are prima facie plausible, are considered in addition to the (...) standard ones. This shows that the notion of reduction is in need of clarification. Referring to the notion of identity of proofs in general proof theory, we argue that reduction steps should not merely remove redundancies, but must respect the identity of proofs. Consequentially, we propose to modify Tennant’s paradoxicality test by basing it on this refined notion of reduction. (shrink)

Karl Popper developed a theory of deductive logic in the late 1940s. In his approach, logic is a metalinguistic theory of deducibility relations that are based on certain purely structural rules. Logical constants are then characterized in terms of deducibility relations. Characterizations of this kind are also called inferential definitions by Popper. In this paper, we expound his theory and elaborate some of his ideas and results that in some cases were only sketched by him. Our focus is on Popper's (...) notion of duality, his theory of modalities, and his treatment of different kinds of negation. This allows us to show how his works on logic anticipate some later developments and discussions in philosophical logic, pertaining to trivializing connectives, the duality of logical constants, dual-intuitionistic logic, the conservativeness of language extensions, the existence of a bi-intuitionistic logic, the non-logicality of minimal negation, and to the problem of logicality in general. (shrink)

Intuitionistic sentential logic is shown to be sound and complete with respect to a semantics centered around extensions of atomic bases (i.e. sets of inference rules for atomic sentences). The result is made possible through a non-standard interpretation of disjunction, whereby, roughly speaking, a disjunction is taken to hold just in case every atomic sentence that follows from each of the disjuncts separately holds; it is argued that this interpretation makes good sense provided that rules in atomic bases are conceived (...) of as being accepted hypothetically rather than categorically. (shrink)

in die operative Logik und Mathematik Zweite Auflage Springer-Verlag Berlin Heidelberg New York 1969 Paul Lorenzen o. Prof. der Philosophie an der Universitat Erlangen Geschaftsfilhrende Herausgeber: Prof. Dr. B. Eckmann Eidgenossische Technische Hochschule Zurich Prof. Dr. B. L. van cler Waerclen Mathematisches Institut der Universitat ZUrich ISBN 978-3-642-86519-0 ISBN 978-3-642-86518-3 (eBook) DOl 10.1007/978-3-642-86518-3 Aile Rechte vorbehalten. Kein Teil dieses Buches darf ohne schriftliche Genehmigung des Springer-Verlages ubersetzt oder in irgendeiner Form vervielfaltigt werden © by Springer-Verlag Berlin· Heidelberg 1955 und 1969 (...) Softcover reprint of the hardcover 2nd edition 1969 Library of Congress Catalog Card Number 73-76724 Titel-Nr. 5061 Vorwort zur zweiten Auflage. Fiir die Neuauflage ist der Text nur unwesentlich geandert worden. Es ist - neben der Korrektur einiger Ungenauigkeiten - vor allem die Terminologie und Symbolik an meine spateren Arbeiten angeglichen. Obwohl ich - verstandlicherweise - jetzt die Ansatze der spateren Arbeiten fiir "sachgemaBer" halte, z. B. eine Logik der Dialoge statt einer Logik der Kalkiile, die Verwendung indefiniter Quantoren statt einer expliziten Konstruktion von Sprachschichten, enthalt diese Neu­ auflage den Inhalt der 1. Auflage unverandert. Der Leser kann also einen Vergleich mit meinen spateren Arbeiten (vgl. Literaturverzeichnis) seIber durchfiihren. Mein Dank gilt wiederum dem Verlag fiir seine entgegenkommende Mitarbeit bei der Vorbereitung dieser Neuauflage. Erlangen, den 1. November I968. PAUL LORENZEN. Vorwort zur ersten Auflage. (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)

Theories in the usual sense, as characterized by a language and a set of theorems in that language ("statement view"), are related to theories in the structuralist sense, in turn characterized by a set of potential models and a subset thereof as models ("non-statement view", J. Sneed, W. Stegmüller). It is shown that reductions of theories in the structuralist sense (that is, functions on structures) give rise to so-called "representations" of theories in the statement sense and vice versa, where representations (...) are understood as functions that map sentences of one theory into another theory. It is argued that commensurability between theories should be based on functions on open formulas and open terms so that reducibility does not necessarily imply commensurability. This is in accordance with a central claim by Stegmüller on the compatibility of reducibility and incommensurability that has recently been challenged by D. Pearce. (shrink)

Human agents draw a variety of inferences effortlessly, spontaneously, and with remarkable efficiency – as though these inferences were a reflexive response of their cognitive apparatus. Furthermore, these inferences are drawn with reference to a large body of background knowledge. This remarkable human ability seems paradoxical given the complexity of reasoning reported by researchers in artificial intelligence. It also poses a challenge for cognitive science and computational neuroscience: How can a system of simple and slow neuronlike elements represent a large (...) body of systemic knowledge and perform a range of inferences with such speed? We describe a computational model that takes a step toward addressing the cognitive science challenge and resolving the artificial intelligence paradox. We show how a connectionist network can encode millions of facts and rules involving n-ary predicates and variables and perform a class of inferences in a few hundred milliseconds. Efficient reasoning requires the rapid representation and propagation of dynamic bindings. Our model (which we refer to as SHRUTI) achieves this by representing (1) dynamic bindings as the synchronous firing of appropriate nodes, (2) rules as interconnection patterns that direct the propagation of rhythmic activity, and (3) long-term facts as temporal pattern-matching subnetworks. The model is consistent with recent neurophysiological evidence that synchronous activity occurs in the brain and may play a representational role in neural information processing. The model also makes specific psychologically significant predictions about the nature of reflexive reasoning. It identifies constraints on the form of rules that may participate in such reasoning and relates the capacity of the working memory underlying reflexive reasoning to biological parameters such as the lowest frequency at which nodes can sustain synchronous oscillations and the coarseness of synchronization. (shrink)

Eight distinct rules for implication in the antecedent for the sequent calculus, one of which being Gentzen’s standard rule, can be derived by successively applying a number of cuts to the logical ground sequent A → B, A ⇒ B. A naive translation into natural deduction collapses four of those rules onto the standard implication elimination rule, and the remaining four rules onto the general elimination rule. This collapse is due to the fact that the difference between a formula occurring (...) in the succedent of a premise of a sequent calculus rule and that formula instead occurring in the antecedent of the conclusion cannot be adequately expressed in the framework of natural deduction. In contrast to this, the difference between a formula occurring in the succedent of the conclusion of a sequent calculus rule and that formula instead occurring in the antecedent of a premise corresponds exactly to the distinction between the standard implication elimination rule and its general counterpart. This incongruity can be remedied by introducing a notational facility that requires of the particular premise of a rule to which it is attached to be an assumption, i.e., to prevent it from being the conclusion of another rule application. Applying this facility to implication elimination results in eight distinct rules that correspond exactly to the eight sequent calculus rules. These eight rules are presented and discussed in detail. It turns out that a natural deduction calculus (for positive implication logic) that employs the rule corresponding to the standard left implication rule of the sequent calculus as well as a rule for explicit substitution can be seen as a natural deduction style sequent calculus. (shrink)

In the present paper we discuss a recent suggestion of Schroeder-Heister concerning the possibility of defining an intensional notion of harmony using isomorphism in second-order propositional logic. The latter is not an absolute notion, but its definition is relative to the choice of criteria for identity of proofs. In the paper, it is argued that in order to attain a satisfactory account of harmony, one has to consider a notion of identity stronger than the usual one (based on β- and (...) η-conversions) that the authors have investigated in recent work. (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)