Quine's argument for a naturalized epistemology is routinely perceived as an argument from despair: traditional epistemology must be abandoned because all attempts to deduce our scientific theories from sense experience have failed. In this paper, I will show that this picture is historically inaccurate and that Quine's argument against first philosophy is considerably stronger and subtler than the standard conception suggests. For Quine, the first philosopher's quest for foundations is inherently incoherent; the very idea of a self-sufficient sense datum language (...) is a mistake, there is no science-independent perspective from which to validate science. I will argue that a great deal of the confusion surrounding Quine's argument is prompted by certain phrases in his seminal ‘Epistemology Naturalized’. Scrutinizing Quine's work both before and after the latter paper provides a better key to understanding his remarkable views about the epistemological relation between theory and evidence. (shrink)

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

In the domain of ontology design as well as in Knowledge Representation, modeling universals is a challenging problem.Most approaches that have addressed this problem rely on Description Logics (DLs) but many difficulties remain, due to under-constrained representation which reduces the inferences that can be drawn and further causes problems in expressiveness. In mathematical logic and program checking, type theories have proved to be appealing but, so far they have not been applied in the formalization of ontologies. To bridge this gap, (...) we present in this paper a theory for representing ontologies in a dependently typed framework which relies on strong formal foundations including both a constructive logic and a functional type system. The language of this theory defines in a precise way what ontological primitives such as classes, relations, properties, etc., and thereof roles, are. The first part of the paper details how these primitives are defined and used within the theory. In a second part, we focus on the formalization of the role primitive. A review of significant role properties leads to the specification of a role profile and most of the remaining work details through numerous examples, how the proposed theory is able to fully satisfy this profile. It is demonstrated that dependent types can model several non-trivial aspects of roles including a formal solution for generalization hierarchies, identity criteria for roles and other contributions. A discussion is given on how the theory is able to cope with many of the constraints inherent in a good role representation. (shrink)

Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us to (...) formalize and analyze free ride in terms of proof theory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs. (shrink)

The fundamental assumption of Dummett’s and Prawitz’ proof-theoretic justification of deduction is that ‘if we have a valid argument for a complex statement, we can construct a valid argument for it which finishes with an application of one of the introduction rules governing its principal operator’. I argue that the assumption is flawed in this general version, but should be restricted, not to apply to arguments in general, but only to proofs. I also argue that Dummett’s and Prawitz’ project of (...) providing a logical basis for metaphysics only relies on the restricted assumption. (shrink)

Inferentialism is the conviction that to be meaningful in the distinctively human way, or to have a 'conceptual content', is to be governed by a certain kind of inferential rules. The term was coined by Robert Brandom as a label for his theory of language; however, it is also naturally applicable (and is growing increasingly common) within the philosophy of logic.

The notion of harmony has played a pivotal role in a number of debates in the philosophy of logic. Yet there is little agreement as to how the requirement of harmony should be spelled out in detail or even what purpose it is to serve. Most, if not all, conceptions of harmony can already be found in Michael Dummett's seminal discussion of the matter in The Logical Basis of Metaphysics. Hence, if we wish to gain a better understanding of the (...) notion of harmony, we do well to start here. Unfortunately, however, Dummett's discussion is not always easy to follow. The following is an attempt to disentangle the main strands of Dummett's treatment of harmony. The different variants of harmony as well as their interrelations are clarified and their individual shortcomings qua interpretations of harmony are demonstrated. Though no attempt is made to give a detailed alternative account of harmony here, it is hoped that our discussion will lay the ground for an adequate rigorous treatment of this central notion. (shrink)

In part one, I give an (unsystematic) overview of the development of logical tools which have been employed in the course of the analysis of referring expressions, i.e. definite and (specific) indefinite singular terms, of natural language. I present Russell's celebrated theory of definite descriptions which I see as an attempt to explain definite reference in terms of unique existence (and reference in general in terms of existence simpliciter); and I present Hilbert's E-calculus as an attempt to explain existence in (...) terms of choice. Then I turn to contemporary, dynamic approaches to the analysis of singular terms and point out that only within a dynamic framework can the Russellian and Hilbertian ideas yield a truly satisfactory analysis of singular terms, and consequently of reference and coreference. I call attention to the fact that current results of formal semantics demonstrate the advantages of viewing singular terms as denoting updates, i.e. as a means of changing the context (information state), and especially that part of the context which I call the individually. (shrink)

There are two ways of understanding the notion of a contradiction: as a conjunction of a statement and its negation, or as a pair of statements one of which is the negation of the other. Correspondingly, there are two ways of understanding the Law of Non-Contradiction (LNC), i.e., the law that says that no contradictions can be true. In this paper I offer some arguments to the effect that on the first (collective) reading LNC is non-negotiable, but on the second (...) (distributive) reading it is perfectly plausible to suppose that LNC may, in some rather special and perhaps undesirable circumstances, fail to hold. (shrink)

According to the species of neo-logicism advanced by Hale and Wright, mathematical knowledge is essentially logical knowledge. Their view is found to be best understood as a set of related though independent theses: (1) neo-fregeanism-a general conception of the relation between language and reality; (2) the method of abstraction-a particular method for introducing concepts into language; (3) the scope of logic-second-order logic is logic. The criticisms of Boolos, Dummett, Field and Quine (amongst others) of these theses are explicated and assessed. (...) The issues discussed include reductionism, rejectionism, the Julius Caesar problem, the Bad Company objections, and the charge that second-order logic is set theory in disguise. (shrink)

While according to the inferentialists, meaning is always a kind of inferential role, proponents of other approaches to semantics often doubt that actual meanings, as they see them, can be generally reduced to inferential roles. In this paper we propose a formal framework for considering the hypothesis of the.

A solid foundation of modal logic requires a clear conception of the notion of modality. Modern modal logic treats modality as a propositional operator. I shall present an alternative according to which modality applies primarily to illocutionary force, that is, to the force, or mood, of a speech act. By a first step of internalization, modality applied at this level is pushed to the level of speech-act content. By a second step of internalization, we reach a propositional operator validating the (...) modal logic S4. After a brief discussion of problematic modality and possibility, the article concludes with an extension of the account that identifies modality with illocutionary force. Throughout, close attention is paid to the intended interpretation of the formalism. All of the rules stipulated will be justified on the basis of this interpretation. (shrink)

Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. A further aim is to argue that (...) a comparison between a plurality of theories is beneficial to the philosophical analysis. We may, for example, discover helpful features of one theory that we may want to import into another context, thus enriching our repertoire of formal tools. Or, through comparison with a less well-known theory, we may gain a better understanding of the characteristics of the theories we are familiar with. As argued in this chapter, CTT has much to offer in all of these respects. (shrink)

This paper formulates a bilateral account of harmony that is an alternative to one proposed by Francez. It builds on an account of harmony for unilateral logic proposed by Kürbis and the observation that reading the rules for the connectives of bilateral logic bottom up gives the grounds and consequences of formulas with the opposite speech act. I formulate a process I call 'inversion' which allows the determination of assertive elimination rules from assertive introduction rules, and rejective elimination rules from (...) rejective introduction rules, and conversely. It corresponds to Francez's notion of vertical harmony. I also formulate a process I call 'conversion', which allows the determination of rejective introduction rules from assertive elimination rules and conversely, and the determination of assertive introduction rules from rejective elimination rules and conversely. It corresponds to Francez's notion of horizontal harmony. The account has a number of features that distinguish it from Francez's. (shrink)

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions (...) in normal form have the subformula property. (shrink)

This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski’s Rule is treated as a general introduction rule for implication. (...) The general introduction rule for negation has a similar form. Maximal formulas with implication or negation as main operator require reduction procedures of a more intricate kind not present in normalisation for intuitionist logic. (shrink)

Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is (...) to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. (shrink)

This paper presents rules of inference for a binary quantifier I for the formalisation of sentences containing definite descriptions within intuitionist positive free logic. I binds one variable and forms a formula from two formulas. Ix[F, G] means ‘The F is G’. The system is shown to have desirable proof-theoretic properties: it is proved that deductions in it can be brought into normal form. The discussion is rounded up by comparisons between the approach to the formalisation of definite descriptions recommended (...) here and the more usual approach that uses a term-forming operator ι, where ιxF means ‘the F’. (shrink)

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

This paper presents a way of formalising definite descriptions with a binary quantifier ι, where ιx[F, G] is read as ‘The F is G’. Introduction and elimination rules for ι in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ιx[F, G] are given, and it is shown that deductions in the system can be brought into normal form.

We present an inferentialist account of the epistemic modal operator might. Our starting point is the bilateralist programme. A bilateralist explains the operator not in terms of the speech act of rejection ; we explain the operator might in terms of weak assertion, a speech act whose existence we argue for on the basis of linguistic evidence. We show that our account of might provides a solution to certain well-known puzzles about the semantics of modal vocabulary whilst retaining classical logic. (...) This demonstrates that an inferentialist approach to meaning can be successfully extended beyond the core logical constants. (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.

This short paper has two loosely connected parts. In the first part, I discuss the difference between classical and intuitionist logic in relation to different the role of hypotheses play in each logic. Harmony is normally understood as a relation between two ways of manipulating formulas in systems of natural deduction: their introduction and elimination. I argue, however, that there is at least a third way of manipulating formulas, namely the discharge of assumption, and that the difference between classical and (...) intuitionist logic can be characterised as a difference of the conditions under which discharge is allowed. Harmony, as ordinarily understood, has nothing to say about discharge. This raises the question whether the notion of harmony can be suitably extended. This requires there to be a suitable fourth way of manipulating formulas that discharge can stand in harmony to. The question is whether there is such a notion: what might it be that stands to discharge of formulas as introduction stands to elimination? One that immediately comes to mind is the making of assumptions. I leave it as an open question for further research whether the notion of harmony can be fruitfully extended in the way suggested here. In the second part, I discuss bilateralism, which proposes a wholesale revision of what it is that is assumed and manipulated by rules of inference in deductions: rules apply to speech acts – assertions and denials – rather than propositions. I point out two problems for bilateralism. First, bilaterlists cannot, contrary to what they claim to be able to do, draw a distinction between the truth and assertibility of a proposition. Secondly, it is not clear what it means to assume an expression such as '+ A' that is supposed to stand for an assertion. Worse than that, it is plausible that making an assumption is a particular speech act, as argued by Dummett (Frege: Philosophy of Language, p.309ff). Bilaterlists accept that speech acts cannot be embedded in other speech acts. But then it is meaningless to assume + A or − A. (shrink)

Philosophers are divided on whether the proof- or truth-theoretic approach to logic is more fruitful. The paper demonstrates the considerable explanatory power of a truth-based approach to logic by showing that and how it can provide (i) an explanatory characterization —both semantic and proof-theoretical—of logical inference, (ii) an explanatory criterion for logical constants and operators, (iii) an explanatory account of logic’s role (function) in knowledge, as well as explanations of (iv) the characteristic features of logic —formality, strong modal force, generality, (...) topic neutrality, basicness, and (quasi-)apriority, (v) the veridicality of logic and its applicability to science, (v) the normativity of logic, (vi) error, revision, and expansion in/of logic, and (vii) the relation between logic and mathematics. The high explanatory power of the truth-theoretic approach does not rule out an equal or even higher explanatory power of the proof-theoretic approach. But to the extent that the truth-theoretic approach is shown to be highly explanatory, it sets a standard for other approaches to logic, including the proof-theoretic approach. (shrink)

We outline an intuitionistic view of knowledge which maintains the original Brouwer–Heyting–Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view coreflectionA→KAis valid and the factivity of knowledge holds in the formKA→ ¬¬A‘known propositions cannot be false’.We show that the traditional form of factivityKA→Ais a distinctly classical principle which, liketertium non datur A∨ ¬A, does not hold intuitionistically, but, along with the whole of (...) classical epistemic logic, is intuitionistically valid in its double negation form ¬¬(KA¬A).Within the intuitionistic epistemic framework the knowability paradox is resolved in a constructive manner. We argue that this paradox is the result of an unwarranted classical reading of constructive principles and as such does not have the consequences for constructive foundations traditionally attributed it. (shrink)

It is often claimed that nominalistic programmes to reconstruct mathematics fail, since they will at some point involve the notion of logical consequence which is unavailable to the nominalist. In this paper we use an idea of Goodman and Quine to develop a nominalistically acceptable explication of logical consequence.

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

This paper responds to recent work in the philosophy of Homotopy Type Theory by James Ladyman and Stuart Presnell. They consider one of the rules for identity, path induction, and justify it along ‘pre-mathematical’ lines. I give an alternate justification based on the philosophical framework of inferentialism. Accordingly, I construct a notion of harmony that allows the inferentialist to say when a connective or concept is meaning-bearing and this conception unifies most of the prominent conceptions of harmony through category theory. (...) This categorical harmony is stated in terms of adjoints and says that any concept definable by iterated adjoints from general categorical operations is harmonious. Moreover, it has been shown that identity in a categorical setting is determined by an adjoint in the relevant way. Furthermore, path induction as a rule comes from this definition. Thus we arrive at an account of how path induction, as a rule of inference governing identity, can be justified on mathematically motivated grounds. (shrink)

We argue that the need for commentary in commonly used linear calculi of natural deduction is connected to the “deletion” of illocutionary expressions that express the role of propositions as reasons, assumptions, or inferred propositions. We first analyze the formalization of an informal proof in some common calculi which do not formalize natural language illocutionary expressions, and show that in these calculi the formalizations of the example proof rely on commentary devices that have no counterpart in the original proof. We (...) then present a linear natural deduction calculus that makes use of formal illocutionary expressions in such a way that unique readability for derivations is guaranteed – thus showing that formalizing illocutionary expressions can eliminate the need for commentary. (shrink)

The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used in normalization theory. It (...) is argued that these two sorts of concepts must be kept strictly apart. (shrink)

Logical inferentialism claims that the meaning of the logical constants should be given, not model-theoretically, but by the rules of inference of a suitable calculus. It has been claimed that certain proof-theoretical systems, most particularly, labelled deductive systems for modal logic, are unsuitable, on the grounds that they are semantically polluted and suffer from an untoward intrusion of semantics into syntax. The charge is shown to be mistaken. It is argued on inferentialist grounds that labelled deductive systems are as syntactically (...) pure as any formal system in which the rules define the meanings of the logical constants. (shrink)

The focus of this paper are Dummett's meaning-theoretical arguments against classical logic based on consideration about the meaning of negation. Using Dummettian principles, I shall outline three such arguments, of increasing strength, and show that they are unsuccessful by giving responses to each argument on behalf of the classical logician. What is crucial is that in responding to these arguments a classicist need not challenge any of the basic assumptions of Dummett's outlook on the theory of meaning. In particular, I (...) shall grant Dummett his general bias towards verificationism, encapsulated in the slogan 'meaning is use'. The second general assumption I see no need to question is Dummett's particular breed of molecularism. Some of Dummett's assumptions will have to be given up, if classical logic is to be vindicated in his meaning-theoretical framework. A major result of this paper will be that the meaning of negation cannot be defined by rules of inference in the Dummettian framework. (shrink)

After some motivating remarks in Section 1, in Section 2 we show how to replace an axiomatic basis for any one of a broad range of sentential logics having finitely many axiom schemes and Modus Ponens as the sole proper rule, by a basis with the same axiom schemes and finitely many one-premiss rules. Section 3 mentions some questions arising from this replacement procedure , explores another such procedure, and discusses some aspects of the consequence relations associated with the different (...) axiomatizations in play. Several open problems are mentioned. An appendix briefly treats the issue of a similar ‘at most one-premiss rules’ reformulation of proof systems with sequent-to-sequent rules. (shrink)

We develop a bottom-up approach to truth-value semantics for classical logic of partial terms based on equality and apply it to prove the conservativity of the addition of partial description and selection functions, independently of any strictness assumption.

We show how mereotopological notions can be expressed by extending intuitionistic propositional logic with propositional quantification and a strong modal operator. We first prove completeness for the logics wrt Kripke models; then we trace the correspondence between Kripke models and topological spaces that have been enhanced with an explicit notion of expressible region. We show how some qualitative spatial notions can be expressed in topological terms. We use the semantical and topological results in order to show how in some extensions (...) of the logics it is possible to express connectedness, non-emptiness and a set of jointly exhaustive, pairwise disjoint, binary relations that play a significant role in qualitative spatial reasoning. (shrink)

David Nelson’s constructive logics with strong negation may beviewed as alternative paraconsistent logic. These logics have been developedbefore da Costa’s works. We address some philosophical aspects of Nelson’slogics and give technical results concerning Kripke models and tableau calculi. We also suggest possible applications of paraconsistent constructivelogics.

This is primarily a conceptual paper. The goal of the paper is to put into perspective the proof-theory of hybrid logic and in particular, try to give an answer to the following question: Why does the proof-theory of hybrid logic work so well compared to the proof-theory of ordinary modal logic?Roughly, there are two different kinds of proof systems for modal logic: Systems where the formulas involved in the rules are formulas of the object language, that is, ordinary modal-logical formulas, (...) and systems where the formulas involved in the rules are metalingustic formulas obtained by attaching labels representing possible worlds to ordinary modal-logical formulas. Systems of the second kind often also involve an explicit representation of the accessibility relation. From a proof-theoretic point of view, modal-logical systems of the first kind are less well-behaved than systems of the second kind.It turns out that this can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of well-behaved proof systems without involving metalinguistic machinery. What has happened is that the metalinguistic machinery has been internalized in the object language. This gives an answer to the initial question, which is that the proof-theory of hybrid logic works so well because the metalinguistic semantic machinery has been internalized in the object language. (shrink)

A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an (...) identity of derivations. This will be used to give a new proof of the normalization theorem for natural deduction, as a consequence of the cut-elimination theorem for the system of sequents. (shrink)

We introduce a simple inference system based on two primitive relations between terms, namely, inclusion and exclusion relations. We present a normalization theorem, and then provide a characterization of the structure of normal proofs. Based on this, inferences in a syllogistic fragment of natural language are reconstructed within our system. We also show that our system can be embedded into a fragment of propositional minimal logic.

Kalrnaric. We set out a system T, consisting of normal proofs constructed by means of elegantly symmetrical introduction and elimination rules. In the system T there are two requirements, called ( ) and ()), on applications of discharge rules. T is sound and complete for Kalmaric arguments. ( ) requires nonvacuous discharge of assumptions; ()) requires that the assumption discharged be the sole one available of highest degree. We then consider a 'Duhemian' extension T*, obtained simply by dropping the requirement (...) ()). T* is a proper subsystem of intuitionistic relevant logic. Our main result is that T* is a double negation consistency companion to classical logic. Thus all one needs to add to T* to obtain classical logic is the (intuitionistic) absurdity rule, and the (classical) rule of double nega-. (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)

Is it possible to give a justification of our own practice of deductive inference? The purpose of this paper is to explain what such a justification might consist in and what its purpose could be. On the conception that we are going to pursue, to give a justification for a deductive practice means to explain in terms of an intuitively satisfactory notion of validity why the inferences that conform to the practice coincide with the valid ones. That is, a justification (...) should provide an analysis of the notion of validity and show that the inferences that conform to the practice are just the ones that are valid. Moreover, a complete justification should also explain the purpose, or point, of our inferential practice. We are first going to discuss the objection that any justification of our deductive practice must use deduction and therefore be circular. Then we will consider a particular model of justificatory explanation, building on Georg Kreisel’s concept of informal rigour. Finally, in the main part of the paper, we will discuss three ideas for defining the notion of validity: (i) the classical conception according to which the notion of (bivalent) truth is taken as basic and validity is defined in terms of the preservation of truth; (ii) the constructivist idea of starting instead with the notion of (a canonical) proof (or verification) and define validity in terms of this notion; (iii) the idea of taking the notions of rational acceptance and rejection as given and define an argument to be valid just in case it is irrational to simultaneously accept its premises and reject its conclusion (or conclusions, if we allow for multiple conclusions). Building on work by Dana Scott, we show that the last conception may be viewed as being, in a certain sense, equivalent to the first one. Finally, we discuss the so-called paradox of inference and the informativeness of deductive arguments. (shrink)

Semantic justifications of the classical rules of logical inference typically make use of a notion of bivalent truth, understood as a property guaranteed to attach to a sentence or its negation regardless of the prospects for speakers to determine it as so doing. For want of a convincing alternative account of classical logic, some philosophers suspicious of such recognition-transcending bivalence have seen no choice but to declare classical deduction unwarranted and settle for a weaker system; intuitionistic logic in particular, buttressed (...) by assertion-conditional semantics, is often considered to enjoy a degree of meaning-theoretical respectability unattainable by classical logic.The decision to forgo the classical inference rules is not always made lightly. Thus, Dummett: " In the resolution of the conflict between [the view that generally accepted classical modes of inference ought to be theoretically accommodated, and the demand that any such accommodation be achieved without recourse to bivalence] lies, as I see it, one of the most fundamental and intractable problems in the theory of meaning; indeed, in all philosophy. "The present article ventures to suggest that the conflict need not be irresoluble. Helping ourselves only to such conceptual resources as are standardly invoked by proponents of intuitionistic logic, we shall formulate a rudimentary meaning theory for a selection of logical constants, define a relation of valid inferability, and prove that the latter includes all of classical first-order logic. The result is essentially that reported in Sandqvist as Theorem 2.20.2. TheoryWe will be considering a standard-syntax first-order language with ⊃, ⊥ and ∀ as its only primitive logical constants. We assume countable supplies of individual constants, individual functors , and predicates , as well as a denumerably infinite set of individual variables. By a basic 1 formula we will mean one that …[Full Text of this Article]. (shrink)