Deductive Logic is designed as an intermediate-level text directed at upper-division students from philosophy and the humanities. Its focus is exclusively on deductive logic, avoiding altogether topics such as informal reasoning and scientific method normally included in introductory logic courses. Its exposition of logical topics is informal, with emphasis on explaining the basic concepts and procedures of modern symbolic logic in the simplest and most intuitive manner possible rather than on developing a rigorous (...) class='Hi'>formal system and providing proofs of its properties. The fact that the text presupposes a course offered to philosophy students and serves to introduce them to logic as the "language of philosophy" has strongly influenced the selection of topics. The topics here are controversial, and the problems not easily resolved, but this text strives to relate the formal logical structures introduced to issues of philosophic interest. (shrink)

A philosophical argument in ordinary language is made the basis for a series of deductive logic exercises. Problems of translating the reasoning and alternative symbolizations are discussed to help guide students toward accurate charitable formalizations. Finally, the inference is critically evaluated in light of its deductive validity.

This introduction to formal logic is one of the few paperbacks available that provides a broad survey of the field. In addition to a clear presentation of sentential and first order quantificational logic, there is a discussion of the philosophical significance of recent work by Church, Gödel, and Tarski. The proof technique employed throughout is the indirect argument. Since proofs of this sort can be converted into mechanical tests of validity, it is easier than most for a (...) beginning student to grasp. Furthermore, this style of argument has long been recognized as the most obvious method of showing arguments in ordinary language to be invalid. Interesting treatments of the construction of decision machines, the nature of formal systems, and the application of logic to mathematics are included in the last section. Numerous exercises are included for which some answers are provided.--R. P. M. (shrink)

Warren Goldfarb, Deductive Logic, Hackett Publishing Company, 2003.    : 0872206602. Deductive Logic is an introductory textbook in formal logic. The book is divided into four parts covering truth-functional logic, monadic quantifi- cation, polyadic quantification and names and identity, and there are exercises for all these topics at the end of the book. In the truth-functional logic part, the reader learns to produce paraphrases of English statements and arguments in logical (...) notation, then about the semantic properties of such paraphrased statements and arguments, such as satisfiability, implication and equivalence and finally there is an axiomatic proof method and some important extras such as disjunctive normal form and expressive adequacy. Parts two and three mirror this analysis/assessment/reflection structure for monadic and polyadic quantification, though this time the proof system is a natural deduction one, and part three contains a completeness proof for that system. The fourth part of the book introduces names, the identity predicate and descriptions and examines the additional expressive power which these provide. I do not think there should be any doubt that this is an excellent book; it presents the essential topics of a first logic course with accuracy, clarity and attention to detail, and it makes material that can be confusing the first time round—say, the translation of conditionals—transparent and easy to understand. But there are a lot of good introductory logic textbooks out there, so I will say something about how it resembles and differs from some other books, and then discuss one minor irritation with this one. (shrink)

Clear focus on its application of formal logic to ordinary English is the most distinctive feature of this textbook for the introductory course in deductive logic. Great care is taken with the appropriate translation into logical languages of ordinary English sentences. Evaluation of these translations promotes a more effective use of ordinary language. The Principles of Deductive Logic presents symbolic logic in a fuller and more leisurely fashion than other introductory textbooks. Early chapters (...) cover informal material, including definition and informal fallacies. The remainder of the text is devoted to the treatment of four distinct artificial languages. The Categorical language is the language of syllogistic logic. The Extended Categorical language enriches this first language with the symbolic connectives for conjunction and negation. The Propositional Connective language and the First-Order language are the two basic languages of modern logic. Each language is accompanied by a deductive system, and is used as an instrument for exploring ordinary language, including ordinary arguments The book contains a large number of exercises whose answers are supplied in the back of the book, and many more that can be assigned as homework. A solution’s manual is available to instructors upon their request. The request must be written on college or university letterhead. (shrink)

Deductive Logic is an introductory textbook in formal logic. The book is divided into four parts covering (i) truth-functional logic, (ii) monadic quantifi- cation, (iii) polyadic quantification and (iv) names and identity, and there are exercises for all these topics at the end of the book. In the truth-functional logic part, the reader learns to produce paraphrases of English statements and arguments in logical notation (this subsection is called “analysis”), then about the semantic properties (...) of such paraphrased statements and arguments, such as satisfiability, implication and equivalence (“logical assessment”) and finally (“reflection”) there is an axiomatic proof method and some important extras such as disjunctive normal form and expressive adequacy. Parts two and three mirror this analysis/assessment/reflection structure for monadic and polyadic quantification, though this time the proof system is a natural deduction one, and part three contains a completeness proof for that system. The fourth part of the book introduces names, the identity predicate and descriptions and examines the additional expressive power which these provide. (shrink)

. Artificial Intelligence (AI) has long dealt with the issue of finding a suitable formalization for commonsense reasoning. Defeasible argumentation has proven to be a successful approach in many respects, proving to be a confluence point for many alternative logical frameworks. Different formalisms have been developed, most of them sharing the common notions of argument and warrant. In defeasible argumentation, an argument is a tentative (defeasible) proof for reaching a conclusion. An argument is warranted when it ultimately prevails over other (...) conflicting arguments. In this context, defeasible consequence relationships for modelling argument and warrant as well as their logical properties have gained particular attention. This article analyzes two non-monotonic inference operators Carg and Cwar intended for modelling argument construction and dialectical analysis (warrant), respectively. As a basis for such analysis we will use the LDSar framework, a unifying approach to computational models of argument using Labelled Deductive Systems (LDS). In the context of this logical framework, we show how labels can be used to represent arguments as well as argument trees, facilitating the definition and study of non-monotonic inference operators, whose associated logical properties are studied and contrasted. We contend that this analysis provides useful comparison criteria that can be extended and applied to other argumentation frameworks. (shrink)

This is a textbook covering the basics of formal logic and elementary metatheory. Its distinguishing feature is that it has more emphasis on metatheory than comparable introductory textbooks. It was originally written to accompany lectures in an introductory to intermediate logic course at the University of Oxford, but it is designed to be used independently.

The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.

We can formalize judgments as logical formulas. Judgment aggregation deals with judgments of several agents, which need to be aggregated to a collective judgment. There are several logical formalizations of judgment aggregation. This paper focuses on a modal formalization which nicely expresses classical properties of judgment aggregation rules and famous results of social choice theory, like Arrow’s impossibility theorem. A natural deduction system for modal logic of judgment aggregation is presented in this paper. The system is sound and complete. (...) As an example of derivation, a formal proof of Arrow’s impossibility theorem is given. (shrink)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra's words, (...) "letting the symbols do the work") have led to the "calculational style," an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz's principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED. (shrink)

The paper deals with the problem of the nature of logic and its normativity in the context of the normativity of scientific knowledge in general. We proceed from a division between fundamental aspects of scientific knowledge which are related to the nature and subject matter of particular sciences, and its applied aspects which are related to the possible applications of sciences. This division fully applies to logic. The authors note that if we view logic as a completely (...) objective discipline, devoid of any "anthropological basis", then the only rational alternative to anti-realist approaches is an ontological (realistic) strategy to justify the logical ones that seek to justify a certain kind of being. To do this, it is necessary to abandon the normative interpretation of logical evaluations and logical systems. Logic can gain a true ontological foundation, based on the devoid of the normative color of understanding logical evaluations as a particular kind of object. Logic has both a deductive core, and various applied disciplines, modern informal logic among them. While formal deductive logic is concentrated on the systems of abstract logical entities (objects) such as truth values and logical functions, the main task of informal logic consist in studying a real argument, which people apply in communicative processes, by elaborating certain standards, criteria and procedures for their interpretation and evaluation. No science can be normative in its basic (fundamental) aspects, and so is logic. Nevertheless, any science is in some degree normative with respect to its applied aspects, and informal logic perfectly illustrates this in view of a normative evolving of applied systems of the modern theories of argumentation. In addition to denying the normativity of formal deductive logic as a fundamental theoretical discipline, the authors of this article demonstrate the fundamental possibility of normative measurement of logical knowledge, in particular in the applied aspect of the development of modern informal logic. (shrink)

In this paper we make some observations about Natural Deduction derivations [Prawitz, 1965, van Dalen, 1986, Bell and Machover, 1977]. We assume the reader is familiar with it and with proof-theory in general. Our development will be simple, even simple-minded, and concrete. However, it will also be evident that general ideas motivate our examples, and we think both our specific examples and the ideas behind them are interesting and may be useful to some readers. In a sentence, the bare technical (...) content of this paper is: Extending natural deduction with global well-formedness conditions can neatly and cheaply capture classical and intermediate logics. The interest here is in the ‘neatly’ and ‘cheaply’. By ‘neatly’ we mean ‘preserving proof-normalisation’,1 and ‘maintaining the subformula property’, and by ‘cheaply’ we mean ‘preserving the formal structure of deductions’ (so that a deduction in the original system is still, formally, a deduction in the extended system, and in particular it requires no extra effort to write just because it is in the extended system). To illustrate what we have in mind consider intuitionistic first-order logic (FOL) [van Dalen, 1986] as a paradigmatic example of a formal notion of deduction. A natural deduction derivation (or deduction) is an inductively defined tree structure where each node contains an instance of a formula. A deduction is valid when each successive node follows from its predecessors in accordance with some predetermined inference rules. A particular attraction of Natural Deduction is its clean and economical presentation. Here for example are deduction (fragments) proving A ∧ B from A and B, and ∀x. (P (x) ∧ Q(x)) from ∀x. P (x) and ∀x. Q(x): ∀x. P (x) (∀E). (shrink)

This book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are here divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics.The original results of this book are split into two parts. This division reflects the division (...) of the book itself. The first type of results concern model-theoretic and complexity properties of hybrid logics. Since hybrid logics which we call standard are quite well investigated, the efforts focused on hybrid logics referred to as non-standard in this book. Non-standard hybrid logics are understood as modal logics with global counting operators ) whose expressive power matches the expressive power of binder-free standard hybrid logics. The relevant results comprise: 1. Establishing a sound and complete axiomatization for the modal logic K with global counting operators ), which can be easily extended onto other frame classes, 2. Establishing tight complexity bounds, namely NExpTime-completeness for the modal logic with global counting operators defined over the classes of arbitrary, reflexive, symmetric, serial and transitive frames ), MT), MD), MB), MK4) with numerical subscripts coded in binary. Establishing the exponential-size model property for this logic defined over the classes of Euclidean and equivalential frames ), MS5).Results of the second type consist of designing concrete deductive systems for standard and non-standard hybrid logics. More precisely, they include: 1. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for a rich class of binder-free standard hybrid logics. An interesting feature of indicated calculi is the nonbranching character of the rule, 2. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for non-standard hybrid logics. The internalization technique applied to a tableau calculus for the modal logic with global counting operators is novel in the literature, 3. Devising the first hybrid algorithm involving an inequality solver for modal logics with global counting operators. Transferring the arithmetical part of reasoning to an inequality solver turned out to be sufficient in ensuring termination.The book is directed to philosophers and logicians working with modal and hybrid logics, as well as to computer scientists interested in deductive systems and decision procedures for logics. Extensive fragments of the first part of the book can also serve as an introduction to hybrid logics for wider audience interested in logic.The content of the book is situated in the areas of formal logic and theoretical computer science with some elements of the theory of computational complexity. (shrink)

The Logic of Causation: Definition, Induction and Deduction of Deterministic Causality is a treatise of formal logic and of aetiology. It is an original and wide-ranging investigation of the definition of causation (deterministic causality) in all its forms, and of the deduction and induction of such forms. The work was carried out in three phases over a dozen years (1998-2010), each phase introducing more sophisticated methods than the previous to solve outstanding problems. This study was intended as (...) part of a larger work on causal logic, which additionally treats volition and allied cause-effect relations (2004). The Logic of Causation deals with the main technicalities relating to reasoning about causation. Once all the deductive characteristics of causation in all its forms have been treated, and we have gained an understanding as to how it is induced, we are able to discuss more intelligently its epistemological and ontological status. In this context, past theories of causation are reviewed and evaluated (although some of the issues involved here can only be fully dealt with in a larger perspective, taking volition and other aspects of causality into consideration, as done in Volition and Allied Causal Concepts). Phase I: Macroanalysis. Starting with the paradigm of causation, its most obvious and strongest form, we can by abstraction of its defining components distinguish four genera of causation, or generic determinations, namely: complete, partial, necessary and contingent causation. When these genera and their negations are combined together in every which way, and tested for consistency, it is found that only four species of causation, or specific determinations, remain conceivable. The concept of causation thus gives rise to a number of positive and negative propositional forms, which can be studied in detail with relative ease because they are compounds of conjunctive and conditional propositions whose properties are already well known to logicians. The logical relations (oppositions) between the various determinations (and their negations) are investigated, as well as their respective implications (eductions). Thereafter, their interactions (in syllogistic reasoning) are treated in the most rigorous manner. The main question we try to answer here is: is (or when is) the cause of a cause of something itself a cause of that thing, and if so to what degree? The figures and moods of positive causative syllogism are listed exhaustively; and the resulting arguments validated or invalidated, as the case may be. In this context, a general and sure method of evaluation called ‘matricial analysis’ (macroanalysis) is introduced. Because this (initial) method is cumbersome, it is used as little as possible – the remaining cases being evaluated by means of reduction. Phase II: Microanalysis. Seeing various difficulties encountered in the first phase, and the fact that some issues were left unresolved in it, a more precise method is developed in the second phase, capable of systematically answering most outstanding questions. This improved matricial analysis (microanalysis) is based on tabular prediction of all logically conceivable combinations and permutations of conjunctions between two or more items and their negations (grand matrices). Each such possible combination is called a ‘modus’ and is assigned a permanent number within the framework concerned (for 2, 3, or more items). This allows us to identify each distinct (causative or other, positive or negative) propositional form with a number of alternative moduses. This technique greatly facilitates all work with causative and related forms, allowing us to systematically consider their eductions, oppositions, and syllogistic combinations. In fact, it constitutes a most radical approach not only to causative propositions and their derivatives, but perhaps more importantly to their constituent conditional propositions. Moreover, it is not limited to logical conditioning and causation, but is equally applicable to other modes of modality, including extensional, natural, temporal and spatial conditioning and causation. From the results obtained, we are able to settle with formal certainty most of the historically controversial issues relating to causation. Phase III: Software Assisted Analysis. The approach in the second phase was very ‘manual’ and time consuming; the third phase is intended to ‘mechanize’ much of the work involved by means of spreadsheets (to begin with). This increases reliability of calculations (though no errors were found, in fact) – but also allows for a wider scope. Indeed, we are now able to produce a larger, 4-item grand matrix, and on its basis find the moduses of causative and other forms needed to investigate 4-item syllogism. As well, now each modus can be interpreted with greater precision and causation can be more precisely defined and treated. In this latest phase, the research is brought to a successful finish! Its main ambition, to obtain a complete and reliable listing of all 3-item and 4-item causative syllogisms, being truly fulfilled. This was made technically feasible, in spite of limitations in computer software and hardware, by cutting up problems into smaller pieces. For every mood of the syllogism, it was thus possible to scan for conclusions ‘mechanically’ (using spreadsheets), testing all forms of causative and preventive conclusions. Until now, this job could only be done ‘manually’, and therefore not exhaustively and with certainty. It took over 72’000 pages of spreadsheets to generate the sought for conclusions. This is a historic breakthrough for causal logic and logic in general. Of course, not all conceivable issues are resolved. There is still some work that needs doing, notably with regard to 5-item causative syllogism. But what has been achieved solves the core problem. The method for the resolution of all outstanding issues has definitely now been found and proven. The only obstacle to solving most of them is the amount of labor needed to produce the remaining (less important) tables. As for 5-item syllogism, bigger computer resources are also needed. (shrink)

What seem to be Kurt Gödel’s first notes on logic, an exercise notebook of 84 pages, contains formal proofs in higher-order arithmetic and set theory. The choice of these topics is clearly suggested by their inclusion in Hilbert and Ackermann’s logic book of 1928, the Grundzüge der theoretischen Logik. Such proofs are notoriously hard to construct within axiomatic logic. Gödel takes without further ado into use a linear system of natural deduction for the full language of (...) higher-order logic, with formal derivations closer to one hundred steps in length and up to four nested temporary assumptions with their scope indicated by vertical intermittent lines. (shrink)

We present an algebraic proof of the theorem stating that there are continuum many axiomatic extensions of global consequence associated with modal system E that do not admit the local deduction detachment theorem. We also prove that all these logics lack the finite frame property and have exactly three proper axiomatic extensions, each of which admits the local deduction detachment theorem.

Excerpt from Logic, Vol. 1: Deduction The present work aims at embracing a full course of Logic, both Formal and Inductive. In an introductory chapter, are set forth such doctrines of psychology as have a bearing on Logic, the nature of knowledge in general, and the classification of the sciences the intention being to avoid doctrinal digressions in the course of the work. Although preparatory to the under standing of what follows, this chapter may be passed (...) over lightly on a first perusal of the work. The part on Deduction contains the usual doctrines of the Syllogism, with the additions of Hamilton, and a full abstract of the novel and elaborate schemes of De Morgan and Boole. The Inductive portion comprises the methods of induc tive research, and all those collateral topics brought for ward by Mr. Mill, as part of the problem of Induction; various modifications being made in the manner of state ment, the order of topics, and the proportion of the hand ling. The greatest innovation is the rendering of Cause by the new doctrine called the Conservation, Persistence, or Correlation of Force. Mr. Mill's view of the relation of Deduction and Induc tion is fully adopted, as being the solution of the otherwise inextricable puzzle of the syllogism, and the means of giving unity and comprehensiveness to Logic. About the Publisher Forgotten Books publishes hundreds of thousands of rare and classic books. Find more at www.forgottenbooks.com This book is a reproduction of an important historical work. Forgotten Books uses state-of-the-art technology to digitally reconstruct the work, preserving the original format whilst repairing imperfections present in the aged copy. In rare cases, an imperfection in the original, such as a blemish or missing page, may be replicated in our edition. We do, however, repair the vast majority of imperfections successfully; any imperfections that remain are intentionally left to preserve the state of such historical works. (shrink)

In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that (i) represents classical proofs in a more natural way than standard Gentzen-style natural deduction, (ii) admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, (iii) provides the means to prove a Non-contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, especially in (...) class='Hi'>formal argumentation, (iv) naturally leads to defining a notion of depth of a proof, to the effect that, for every fixed natural k, normal k-depth deducibility is a tractable problem and converges to classical deducibility as k tends to infinity. (shrink)

By indirect-deduction theorems introduced in the present paper we mean the theorems that allow to formalize indirect reasonings occurring in deductive practice in general and in mathematics in particular. We discuss the relationship between the introduced theorems and some logical calculi being virtually confined to propositional calculi with implication and negation. It is worth to notice that the above theorems are very handy and effective in proving logical theses.

This is the 3rd edition. Although a number of new technological applications require classical deductive computation with non-classical logics, many key technologies still do well—or exclusively, for that matter—with classical logic. In this first volume, we elaborate on classical deductive computing with classical logic. The objective of the main text is to provide the reader with a thorough elaboration on both classical computing – a.k.a. formal languages and automata theory – and classical deduction with the (...) classical first-order predicate calculus with a view to computational implementations, namely in automated theorem proving and logic programming. The present third edition improves on the previous ones by providing an altogether more algorithmic approach: There is now a wholly new section on algorithms and there are in total fourteen clearly isolated algorithms designed in pseudo-code. Other improvements are, for instance, an emphasis on functions in Chapter 1 and more exercises with Turing machines. (shrink)

In his Logic, Pierre Gassendi proposes that our inductive inferences lack the information we would need to be certain of the claims that they suggest. Not even deductivist inference can insure certainty about empirical claims because the experientially attained premises with which we adduce support for such claims are no greater than probable. While something is surely amiss in calling deductivist inference "probabilistic," it seems Gassendi has hit upon a now-familiar, sensible point—namely, the use of deductive reasoning in (...) empirical contexts, while providing certain formal guarantees, does not insulate empirical arguments from judgment by the measure of belief which we invest in their premises. The more general point, which distinguishes Gassendi among his contemporaries, is that the strength shared by all empirical claims consists in the warrant from experience for those claims we introduce in their support. (shrink)

In lively and readable prose, Arthur presents a new approach to the study of logic, one that seeks to integrate methods of argument analysis developed in modern “informal logic” with natural deduction techniques. The dry bones of logic are given flesh by unusual attention to the history of the subject, from Pythagoras, the Stoics, and Indian Buddhist logic, through Lewis Carroll, Venn, and Boole, to Russell, Frege, and Monty Python. A previous edition of this book appeared (...) under the title _Natural Deduction_. This new edition adds clarifications of the notions of explanation, validity and formal validity, a more detailed discussion of derivation strategies, and another rule of inference, Reiteration. (shrink)

This article identifies and formalizes the logical features of analogous terms that justify their use in deduction. After a survey of doctrines in Aristotle, Aquinas, and Cajetan, the criteria of “analogy of proper proportionality” are symbolized in first-order predicate logic. A common genus justifies use of a common term, but does not provide the inferential link required for deduction. Rather, the respective differentiae foster this link through their identical proportion. A natural-language argument by analogy is formalized so as to (...) exhibit these criteria, thereby showing the validity of analogical deduction. (shrink)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED . This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations have led to the "calculational style," (...) an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system , we prove Leibniz's principle for intuitionistic logic and also prove that any valid formula of predicate logic can be proved in I-CED. (shrink)

I provide a general introduction to the notion at issue in this volume, i.e. deduction, and to some akin notions like inference and reasoning. I also argue that logic is, or should be concerned with three attitudes: an archaeological attitude, a nomological attitude, and an aetiological attitude. Then, I sum up the content of the contributions in this volume.

The three essays presented here concern natural connections between grammatical derivations and structures provided by certain standard grammar formalisms, on the one hand, and deductions in logical systems, on the other hand. In the first essay we analyse the adequacy of Polish notation for higher-order languages. The Ajdukiewicz algorithm (Ajdukiewicz 1935) is discussed in terms of generalized MP-deductions. We exhibit a failure in Ajdukiewicz’s original version of the algorithm and give a correct one; we prove that generalized MP-deductions have the (...) frontier property, which is essential for the plausibility of Polish notation. The second essay deals with logical systems corresponding to different grammar formalisms, as e.g. Finite State Acceptors, Context-Free Grammars, Categorial Grammars, and others. We show how can logical methods be used to establish certain linguistically significant properties of formal grammars. The third essay discusses the interplay between Natural Deduction proofs in grammar oriented logics and semantic structures expressible by typed lambda terms and combinators. (shrink)

This paper presents an outline of a new theory of relevant deduction which arose from the purpose of solving paradoxes in various fields of analytic philosophy. In distinction to relevance logics, this approach does not replace classical logic by a new one, but distinguishes between relevance and validity. It is argued that irrelevant arguments are, although formally valid, nonsensical and even harmful in practical applications. The basic idea is this: a valid deduction is relevant iff no subformula of the (...) conclusion is replaceable on some of its occurrences by any other formula salva validitate of the deduction. The paper first motivates the approach by showing that four paradoxes seemingly very distant from each other have a common source. Then the exact definition of relevant deduction is given and its logical properties are investigated. An extension to relevance of premises is discussed. Finally the paper presents an overview of its applications in philosophy of science, ethics, cognitive psychology and artificial intelligence. (shrink)

In this paper I focus on two contrasting concepts of deduction and induction that have appeared in introductory (formal) logic texts over the past 75 years or so. According to the one, deductive and inductive arguments are defined solely by reference to what arguers claim about the relation between the premises and the conclusions. According to the other, they are defined solely by reference to that relation itself. Arguing that these definitions have defects that are due to (...) their simplicity, I develop definitions that remove these defects by assigning a combination of roles to both arguers’ claims concerning the premises/conclusion relation and the relation itself. Along the way I also present and briefly defend definitions of both deductive and inductive validity that are significantly different from the norm. (shrink)

Let ⊢ be the ordinary deduction relation of classical first-order logic. We provide an "analytic" subrelation ⊢a of ⊢ which for propositional logic is defined by the usual "containment" criterion Γ ⊢a φ iff Γ⊢φ and Atom ⊆ Atom, whereas for predicate logic, ⊢a is defined by the extended criterion Γ⊢aφ iff Γ⊢aφ and Atom ⊆' Atom, where Atom ⊆' Atom means that every atomic formula occurring in φ "essentially occurs" also in Γ. If Γ, φ are (...) quantifier-free, then the notions "occurs" and "essentially occurs" for atoms between Γ and φ coincide. If ⊢ is formalized by Gentzen's calculus of sequents, then we show that ⊢a is axiomatizable by a proper fragment of analytic inference rules. This is mainly due to cut elimination. By "analytic inference rule " we understand here a rule r such that, if the sequent over the line is analytic, then so is the sequent under the line. We also discuss the notion of semantic relevance as contrasted to the previous syntactic one. We show that when introducing semantic sequents as axioms, i.e. when extending the pure logical axioms and rules by mathematical ones, the property of syntactic relevance is lost, since cut elimination no longer holds. We conclude that no purely syntactic notion of analytic deduction can ever replace successfully the complex semantico-syntactic deduction we already possess. (shrink)

How do people make deductions? The orthodox view in psychology is that they use formal rules of inference like those of a “natural deduction” system.Deductionargues that their logical competence depends, not on formal rules, but on mental models. They construct models of the situation described by the premises, using their linguistic knowledge and their general knowledge. They try to formulate a conclusion based on these models that maintains semantic information, that expresses it parsimoniously, and that makes explicit something (...) not directly stated by any premise. They then test the validity of the conclusion by searching for alternative models that might refute the conclusion. The theory also resolves long-standing puzzles about reasoning, including how nonmonotonic reasoning occurs in daily life. The book reports experiments on all the main domains of deduction, including inferences based on prepositional connectives such as “if” and “or,” inferences based on relations such as “in the same place as,” inferences based on quantifiers such as “none,” “any,” and “only,” and metalogical inferences based on assertions about the true and the false. Where the two theories make opposite predictions, the results confirm the model theory and run counter to the formal rule theories. Without exception, all of the experiments corroborate the two main predictions of the model theory: inferences requiring only one model are easier than those requiring multiple models, and erroneous conclusions are usually the result of constructing only one of the possible models of the premises. (shrink)

In this paper two deductive systems associated with relevance logic are studied from an algebraic point of view. One is defined by the familiar, Hilbert-style, formalization of R; the other one is a weak version of it, called WR, which appears as the semantic entailment of the Meyer-Routley-Fine semantics, and which has already been suggested by Wójcicki for other reasons. This weaker consequence is first defined indirectly, using R, but we prove that the first one turns out to (...) be an axiomatic extension of WR. Moreover we provide WR with a natural Gentzen calculus. It is proved that both deductive systems have the same associated class of algebras but different classes of models on these algebras. The notion of model used here is an abstract logic, that is, a closure operator on an abstract algebra; the abstract logics obtained in the case of WR are also the models, in a natural sense, of the given Gentzen calculus. (shrink)

In the common man reasoning the presence of vague predicates is pervasive and under the name “fuzzy logic in narrow sense” or “formal fuzzy logic” there are a series of attempts to formalize such a kind of phenomenon. This paper is devoted to discussing the limits of these attempts both from a technical point of view and with respect the original and principal task: to define a mathematical model of the vagueness. For example, one argues that, since (...) vagueness is necessarily connected with the intuition of the continuum, we have to look at the order-based topology of the interval [0,1] and not at the discrete topology of the set {0,1}. In accordance, in switching from classical logic to a logic for the vague predicates, we cannot avoid the use of the basic notions of real analysis as, for example, the ones of “approximation“, “convergence“, “continuity“. In accordance, instead of defining the compactness of the logical consequence operator and of the deduction operator in terms of finiteness, we have to define it in terms of continuity. Also, the effectiveness of the deduction apparatus has to be defined by using the tools of constructive real analysis and not the one of recursive arithmetic. This means that decidability and semi-decidability have to be defined by involving effective limit processes and not by finite steps stopping processes. (shrink)

The main subject of this very original and engaging book is the history of the idea of formal proof. Von Plato shows how that idea emerged, from the Greeks to the crucial last few decades of the ni...

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening (...) or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

We present systems of Natural Deduction based on Strict Implication for the main normal modal logics between K and S5. In this work we consider Strict Implication as the main modal operator, and establish a natural correspondence between Strict Implication and strict subproofs.

This paper critically examines a formal argument against deducing ‘ought’-judgments from ‘is’-judgments, an argument suggested by a literal reading of a famous passage in Hume'sTreatise of Human Nature. According to this argument, judgments of the two kinds have different logical structures (i.e., their subjects are differently related to their predicates) and this difference disallows cross-categorical deductive inferences. I draw on Fregean accounts of the ‘is’- copula and on syntactical interpretations of ‘ought’-judgments that have become standard in deontic (...) class='Hi'>logic to argue that twentieth century work in philosophical grammar and logic casts doubt on all three of the argument's premises. (shrink)

Recently discovered documents have shown how Gentzen had arrived at the final form of natural deduction, namely by trying out a great number of alternative formulations. What led him to natural deduction in the first place, other than the general idea of studying “mathematical inference as it appears in practice,” is not indicated anywhere in his publications or preserved manuscripts. It is suggested that formal work in axiomatic logic lies behind the birth of Gentzen’s natural deduction, rather than (...) any single decisive influence in the work of others. Various axiomatizations are explored in turn, from the classical axioms of Hilbert and Ackermann to the intuitionistic axiomatization of Heyting. (shrink)

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. (shrink)

The comprehension principle of set theory asserts that a set can be formed from the objects satisfying any given property. The principle leads to immediate contradictions if it is formalized as an axiom scheme within classical first order logic. A resolution of the set paradoxes results if the principle is formalized instead as two rules of deduction in a natural deduction presentation of logic. This presentation of the comprehension principle for sets as semantic rules, instead of as a (...) comprehension axiom scheme, can be viewed as an extension of classical logic, in contrast to the assertion of extra-logical axioms expressing truths about a pre-existing or constructed universe of sets. The paradoxes are disarmed in the extended classical semantics because truth values are only assigned to those sentences that can be grounded in atomic sentences. (shrink)

The issue of the emergence of formal axiomatic logical systems due to the emergence of logical antinomies in formal axiomatic systems, specifically the issue of developing formal logical axiomatics in the calculus of considerations was investigated in the considered research. At the same time, in order to determine the characteristics of the implementation of the logical-methodological principles and provisions of the deductive reasoning obviously, conceptual-logical foundations of the calculus of considerations was studied and the main propositions (...) of the calculus of considerations and the analysis of the initial logical operations on them were given in the study. The basic laws of logic and the expression of one logical act with another one were also explained in the research work by giving the concepst of proportional form and tautology in the calculus of considerations. At the same time, main properties and the procedure of setting of the formal deductive theory in the calculus of considerations were studied in the article. In order to provide an adequate characterization of the conceptual and methodological bases of the calculus of considerations in the research work, the basic logical laws of the calculus of considerations developed by the German mathematician and thinker P. Hilbert were also given. In addition, the main principles and methodological provisions of the deductive method were investigated, and the rules of deriving new conclusions from the axioms were interpreted. At the end of the reviewed article, the main principles and methods of the formal axiomatic mathematical systems built on a deductive basis, specifically the calculus of considerations, were studied and a logical-methodological analysis of the calculus of considerations was carried out on this basis. In this framework, the syntactic and semantic analysis of formalized language in formal axiomatic logical systems was carried out separately, the constituent parts of those systems, including the construction scheme, were given. (shrink)

We propose a natural deduction calculus for the modal logic S4.2. The system is designed to match as much as possible the structure and the properties of the standard system of natural deduction for first-order classical logic, exploiting the formal analogy between modalities and quantifiers. The system is proved sound and complete with respect to (w.r.t.) the standard Hilbert-style formulation of S4.2. Normalization and its consequences are obtained in a natural way, with proofs that closely follow the (...) analogous ones for first-order logic. (shrink)

The paper is devoted to the concise description of some Natural Deduction System (ND for short) for Linear Temporal Logic. The system's distinctive feature is that it is labelled and analytical. Labels convey necessary semantic information connected with the rules for temporal functors while the analytical character of the rules lets the system work as a decision procedure. It makes it more similar to Labelled Tableau Systems than to standard Natural Deduction. In fact, our solution of linearity representation is (...) rather independent of the underlying proof method, provided that some form of (analytic) cut is admissible. We will also discuss some generalisations of the system and compare it with other formalizations of linearity. (shrink)