The framework of natural deduction is extended by permitting rules as assumptions which may be discharged in the course of a derivation. this leads to the concept of rules of higher levels and to a general schema for introduction and elimination rules for arbitrary n-ary sentential operators. with respect to this schema, (functional) completeness "or", "if..then" and absurdity is proved.

The present article focuses on the antinomy of pure practical reason and the deduction of the Highest Good in the Dialectic of Pure Practical Reason (in the second Critique). Although Kant claims that the Dialectic contains both the antinomy and the deduction, the boundaries dividing one from the other are at best vague. It is difficult to make out where the antinomy of practical reason ends and where the deduction begins. To locate both and to distinguish one from the other (...) (with special attention paid to the modality of the Highest Good) are the chief aims of this article. Additionally but no less importantly, I show, against the line of criticism originally traceable to Schopenhauer, that the antinomy of practical reason amounts to more than a reflection of Kant’s “architectonic obsession.” Not only does the antinomy of practical reason correspond to a genuine dialectical problem in the Critique of Practical Reason, but it also shares a fundamental (even if not immediately apparent) similarity with the antinomy of pure speculative reason. Finally, I consider Kant’s transcendental deduction of the Highest Good against the backdrop of his other deductions, especially the deduction of the categories in the Critique of Pure Reason, and defend it against the charge of potential circularity. (shrink)

It seems beyond doubt that a thinker can come to know a conclusion by deducing it from premisses that he knows already, but philosophers have found it puzzling how a thinker could acquire knowledge in this way. Assuming a broadly externalist conception of knowledge, I explain why judgements competently deduced from known premisses are themselves knowledgeable. Assuming an exclusionary conception of judgeable content, I further explain how such judgements can be informative. (According to the exclusionary conception, which I develop from (...) some remarks in Ramsey, a judgement's content is given by the hitherto live possibilities that it excludes or rules out.) I propose that the value of logic lies in its allowing us to combine different sources of knowledge, so that we can learn things that we could not learn from those sources individually. I conclude by arguing that while single-conclusion logics possess that value, multiple-conclusion logics do not. (shrink)

Having been neglected or maligned for most of this century, Newton's method of 'deduction from the phenomena' has recently attracted renewed attention and support. John Norton, for example, has argued that this method has been applied with notable success in a variety of cases in the history of physics and that this explains why the massive underdetermination of theory by evidence, seemingly entailed by hypothetico-deductive methods, is invisible to working physicists. This paper, through a detailed analysis of Newton's deduction of (...) one particular 'proposition' in optics 'from the phenomena', gives a clearer account than hitherto of the method - highlighting the fact that it is really one of deduction from the phenomena plus 'background knowledge'. It argues, that, although the method has certain heuristic virtues, examination of its putative accreditational strengths reveals a range of important problems that its defenders have yet adequately to address. (shrink)

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

Like Kant's Critique of Pure Reason, we now have both an A- and a substantially revised B-edition of Henry Allison's commentary to and defence of that work: Kant's Transcendental Idealism: An Interpretation and Defense . Unlike Kant's Critique, however, Allison's first edition is unlikely to persist as an occasional rival to the second, since reviewers rightly consider the second to have superseded the landmark scholarship of the first. Nevertheless, before Allison's first edition is entirely supplanted, I would like to save (...) a neglected insight from its treatment of the B-deduction that is not retained in the second edition. (shrink)

The way from linearly written derivations in natural deduction, introduced by Jaskowski and often used in textbooks, is a straightforward root-first translation. The other direction, instead, is tricky, because of the partially ordered assumption formulas in a tree that can get closed by the end of a derivation. An algorithm is defined that operates alternatively from the leaves and root of a derivation and solves the problem.

According to non-conceptualist interpretations, Kant held that the application of concepts is not necessary for perceptual experience. Some have motivated non-conceptualism by noting the affinities between Kant's account of perception and contemporary relational theories of perception. In this paper I argue (i) that non-conceptualism cannot provide an account of the Transcendental Deduction and thus ought to be rejected; and (ii) that this has no bearing on the issue of whether Kant endorsed a relational account of perceptual experience.

This essay partly builds on and partly criticizes a striking idea of Dieter Henrich. Henrich argues that Kant's distinction in the first Critique between the question of fact (quid facti) and the question of law (quid juris) provides clues to the argumentative structure of a philosophical "Deduction". Henrich suggests that the unity of apperception plays a role analogous to a legal factum. By contrast, I argue, first, that the question of fact in the first Critique is settled by the Metaphysical (...) Deduction, which establishes the purity of origin of the Categories, and, second, that in the second Critique, the relevant factum is the Fact of Reason, which amounts to the fact that the Moral Law is pure in origin. (shrink)

Drawing upon Martin-Löf’s semantic framework for his constructive type theory, semantic values are assigned also to natural-deduction derivations, while observing the crucial distinction between consequence among propositions and inference among judgements. Derivations in Gentzen’s format with derivable formulae dependent upon open assumptions, stand, it is suggested, for proof-objects, whereas derivations in Gentzen’s sequential format are proof-acts.

This paper examines critically the reconstruction of the ‘Sherlock Holmes sense of deduction’ proposed jointly by M.B. Hintikka and J. Hintikka in the 1980s, and its successor, the interrogative model of inquiry developed by J. Hintikka and his collaborators in the 1990s. The Hintikkas’ model explicitly used game theory in order to formalize a naturalistic approach to inquiry, but the imi abandoned both the game-theoretic formalism, and the naturalistic approach. It is argued that the latter better supports the claim that (...) the imi provides a ‘logic of discovery’, and safeguards its empirical adequacy. Technical changes necessary to this interpretation are presented, and examples are discussed, both formal and informal, that are better analyzed when these changes are in place. The informal examples are borrowed from Conan Doyle’s The Case of Silver Blaze, a favorite of M.B. and J. Hintikka. (shrink)

The two major options on which the current debate on the interpretation of quantum mechanics relies, namely realism and empiricism, are far from being exhaustive. There is at least one more position available, which is metaphysically as agnostic as empiricism, but which shares with realism a committment to considering the structure of theories as highly significant. The latter position has been named transcendentalism after Kant. In this paper, a generalized version of Kant's method is used. This yields a reasoning that (...) one is entitled to call a transcendental deduction of some major formal features of quantum mechanics. (shrink)

Natural deduction is the type of logic most familiar to current philosophers, and indeed is all that many modern philosophers know about logic. Yet natural deduction is a fairly recent innovation in logic, dating from Gentzen and Jaśkowski in 1934. This article traces the development of natural deduction from the view that these founders embraced to the widespread acceptance of the method in the 1960s. I focus especially on the different choices made by writers of elementary textbooks—the standard conduits of (...) the method to a generation of philosophers—with an eye to determining what the ‘essential characteristics’ of natural deduction are. (shrink)

We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.

Chapter 4 of Dennis Schulting’s book Kant’s Radical Subjectivism targets those commentators who take there to be a gap in the transcendental deduction of the categories, arguing instead that there is no gap between the necessary application of the categories and their exemplification in the object of experience. In these comments on the chapter, I suggest a minimal sense in which the fact that there is a gap is non-negotiable. The interesting question is not whether there is a gap which (...) needs to be bridged, but how and why Kant makes the step from subjectivity to objectivity. (shrink)

We present a reference model for finding evidence of discrimination in datasets of historical decision records in socially sensitive tasks, including access to credit, mortgage, insurance, labor market and other benefits. We formalize the process of direct and indirect discrimination discovery in a rule-based framework, by modelling protected-by-law groups, such as minorities or disadvantaged segments, and contexts where discrimination occurs. Classification rules, extracted from the historical records, allow for unveiling contexts of unlawful discrimination, where the degree of burden over protected-by-law (...) groups is evaluated by formalizing existing norms and regulations in terms of quantitative measures. The measures are defined as functions of the contingency table of a classification rule, and their statistical significance is assessed, relying on a large body of statistical inference methods for proportions. Key legal concepts and reasonings are then used to drive the analysis on the set of classification rules, with the aim of discovering patterns of discrimination, either direct or indirect. Analyses of affirmative action, favoritism and argumentation against discrimination allegations are also modelled in the proposed framework. Finally, we present an implementation, called LP2DD, of the overall reference model that integrates induction, through data mining classification rule extraction, and deduction, through a computational logic implementation of the analytical tools. The LP2DD system is put at work on the analysis of a dataset of credit decision records. (shrink)

We show, first, that the normalization procedure for S4 modal logic presented by Dag Prawitz in [5] does not work. We then develop a new natural deduction system for S4 classical modal logic that is logically equivalent to that of Prawitz, and we show that every derivation in this new system can be transformed into a normal derivation.

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 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)

In this article some problems associated with Kant's transcendental deduction of the categories will be examined. Kant wrote that the deduction was one of the most difficult and arduous investigations ever undertaken in metaphysics. It is the deduction that must establish the lawfulness of claims to knowledge on the part of pure reason and determine the very possibility of metaphysics.

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid to which properties of theories result in the presence of which rules of inference, and to restrictions on the sets of formulas to which the rules may be employed, restrictions (...) determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck. (shrink)

The problem of Kant’s Neglected Alternative is that while his Aesthetic provides an argument that space and time are empirically real – in applying to all appearances – its argument seems to fall short of the conclusion that space and time are transcendentally ideal, in not applying to any things in themselves. By considering an overlooked passage in which Kant explains why his Transcendental Deduction is ‘unavoidably necessary’, I argue that it is not solely in his Aesthetic but more so (...) in his Deduction where he intends to provide his argument for the transcendental ideality of space and time. His Deduction shows that space and time do not have a valid application to any things in themselves by arguing that the categories do have a valid application to everything in space and time, but that the categories do not have a valid application to any things in themselves. (shrink)

ABSTRACT We show that there is a polynomial over the rational number field corresponding to each propositional formula in a given many-valued logic. To decide whether a propositional formula can be deduced from a finite set of such formulas (deduction problem), we only need to decide whether a polynomial vanishes on an algebraic variety. By using Wu's method, an algorithm for this problem is presented.

The paper studies the extension of harmony and stability, major themes in proof-theoretic semantics, from single-conclusion natural-deduction systems to multiple -conclusions natural-deduction, independently of classical logic. An extension of the method of obtaining harmoniously-induced general elimination rules from given introduction rules is suggested, taking into account sub-structurality. Finally, the reductions and expansions of the multiple -conclusions natural-deduction representation of classical logic are formulated.

This paper presents two systems of natural deduction for the rejection of non-tautologies of classical propositional logic. The first system is sound and complete with respect to the body of all non-tautologies, the second system is sound and complete with respect to the body of all contradictions. The second system is a subsystem of the first. Starting with Jan Łukasiewicz's work, we describe the historical development of theories of rejection for classical propositional logic. Subsequently, we present the two systems of (...) natural deduction and prove them to be sound and complete. We conclude with a ‘Theorem of Inversion’. (shrink)

This paper is concerned with a natural deduction system for First Degree Entailment (FDE). First, we exhibit a brief history of FDE and of combined systems whose underlying idea is used in developing the natural deduction system. Then, after presenting the language and a semantics of FDE, we develop a natural deduction system for FDE. We then prove soundness and completeness of the system with respect to the semantics. The system neatly represents the four-valued semantics for FDE.

This article examines Quine's original proposal for a natural deduction calculus including an existential specification rule, it argues that it introduces a new paradigm of natural deduction alternative to Gentzen's but has some substantial defects. As an alternative the article puts forward a system of sequent natural deduction.

A truth-preservation fallacy is using the concept of truth-preservation where some other concept is needed. For example, in certain contexts saying that consequences can be deduced from premises using truth-preserving deduction rules is a fallacy if it suggests that all truth-preserving rules are consequence-preserving. The arithmetic additive-associativity rule that yields 6 = (3 + (2 + 1)) from 6 = ((3 + 2) + 1) is truth-preserving but not consequence-preserving. As noted in James Gasser’s dissertation, Leibniz has been criticized for (...) using that rule in attempting to show that arithmetic equations are consequences of definitions. -/- A system of deductions is truth-preserving if each of its deductions having true premises has a true conclusion—and consequence-preserving if, for any given set of sentences, each deduction having premises that are consequences of that set has a conclusion that is a consequence of that set. Consequence-preserving amounts to: in each of its deductions the conclusion is a consequence of the premises. The same definitions apply to deduction rules considered as systems of deductions. Every consequence-preserving system is truth-preserving. It is not as well-known that the converse fails: not every truth-preserving system is consequence-preserving. Likewise for rules: not every truth-preserving rule is consequence-preserving. There are many famous examples. In ordinary first-order Peano-Arithmetic, the induction rule yields the conclusion ‘every number x is such that: x is zero or x is a successor’—which is not a consequence of the null set—from two tautological premises, which are consequences of the null set, of course. The arithmetic induction rule is truth-preserving but not consequence-preserving. Truth-preserving rules that are not consequence-preserving are non-logical or extra-logical rules. Such rules are unacceptable to persons espousing traditional truth-and-consequence conceptions of demonstration: a demonstration shows its conclusion is true by showing that its conclusion is a consequence of premises already known to be true. The 1965 Preface in Benson Mates (1972, vii) contains the first occurrence of truth-preservation fallacies in the book. (shrink)

This short blog article presents a solution to the “Scandal of Deduction,” the counter-intuitive finding that no new information is generated by either deduction or deterministic computation. I argue that, since physical computation necessarily involves communications, we cannot expect computation to reduce our uncertainty until it has been completed and its output received as a “message.” This has a number of implications for how we understand semantic theories of information.

Ph.D. thesis submitted for Philosophy (KCL) on 24 July 2007. Supervisors: Keith Hossack, Mark Sainsbury and Wilfried Meyer-Viol.

PARC is an "appended numeral" system of natural deduction that I learned as an undergraduate and have taught for many years. Despite its considerable pedagogical strengths, PARC appears to have never been published. The system features explicit "tracking" of premises and assumptions throughout a derivation, the collapsing of indirect proofs into conditional proofs, and a very simple set of quantificational rules without the long list of exceptions that bedevil students learning existential instantiation and universal generalization. The system can be used (...) with any Copi-style set of inference rules, so it is quite adaptable to many mainstream symbolic logic textbooks. Consequently, PARC may be especially attractive to logic teachers who find Jaskowski/Gentzen-style introduction/elimination rules to be far less "natural" than Copi-style rules. The PARC system is also keyboard-friendly in comparison to the widely adopted Jaskowski-style graphical subproof system of natural deduction, viz., Fitch diagrams and Copi "bent arrow" diagrams. (shrink)

This paper is about the nature of the relationship between (1) the doctrine of Non-Conceptualism about mental content, (2) Kant's Transcendental Idealism, and (3) the Transcendental Deduction of the Pure Concepts of the Understanding, or Categories, in the B (1787) edition of the Critique of Pure Reason, i.e., the B Deduction. Correspondingly, the main thesis of the paper is this: (1) and (2) yield serious problems for (3), yet, in exploring these two serious problems for the B Deduction, we also (...) discover some deeply important and perhaps surprising philosophical facts about Kant's theory of cognition and his metaphysics. (shrink)

The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination.

This paper presents detailed formalizations of ontological arguments in a simple modal natural deduction calculus. The first formal proof closely follows the hints in Scott’s manuscript about Gödel’s argument and fills in the gaps, thus verifying its correctness. The second formal proof improves the first one, by relying on the weaker modal logic KB instead of S5 and by avoiding the equality relation. The second proof is also technically shorter than the first one, because it eliminates unnecessary detours and uses (...) Axiom 1 for the positivity of properties only once. The third and fourth proofs formalize, respectively, Anderson’s and Bjørdal’s variants of the ontological argument, which are known to be immune to modal collapse. (shrink)