An inference is valid if it guarantees the transferability of knowledge from the premisses to the conclusion. If knowledge is here understood as demonstrative knowledge, and demonstration is explained as a chain of valid inferences, we are caught in an explanatory circle. In recent lectures, Per Martin-Löf has sought to avoid the circle by specifying the notion of knowledge appealed to in the explanation of the validity of inference as knowledge of a kind weaker than demonstrative knowledge. The resulting explanation (...) is the main topic of this article. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

In a recent paper by Tranchini (Topoi, 2019), an introduction rule for the paradoxical proposition ρ∗ that can be simultaneously proven and disproven is discussed. This rule is formalized in Martin-Löf’s constructive type theory (CTT) and supplemented with an inferential explanation in the style of Brouwer-Heyting-Kolmogorov semantics. I will, however, argue that the provided formalization is problematic because what is paradoxical about ρ∗ from the viewpoint of CTT is not its provability, but whether it is a proposition at all.

Abstract The purpose of this paper is twofold: (i) we will argue that formal semantics might have faltered due to its failure in distinguishing between two fundamentally very different types of concepts, namely ontological concepts, that should be types in a strongly-typed ontology, and logical concepts, that are predicates corresponding to properties of, and relations between, objects of various ontological types; and (ii) we show that accounting for these differences amounts to a new formal semantics; one that integrates lexical and (...) compositional semantics in one coherent framework and one where formal semantics is embedded with a strongly typed ontology; an ontology that reflects our commonsense knowledge of the world and the way we talk about it in ordinary language. We will show how in such a framework a number of challenges in the semantics of natural language are adequately and systematically treated. (shrink)

Presenting the first comprehensive, in-depth study of hyperintensionality, this book equips readers with the basic tools needed to appreciate some of current and future debates in the philosophy of language, semantics, and metaphysics. After introducing and explaining the major approaches to hyperintensionality found in the literature, the book tackles its systematic connections to normativity and offers some contributions to the current debates. The book offers undergraduate and graduate students an essential introduction to the topic, while also helping professionals in related (...) fields get up to speed on open research-level problems. (shrink)

Penelope Maddy has recently addressed the set-theoretic multiverse, and expressed reservations on its status and merits ([Maddy, 2017]). The purpose of the paper is to examine her concerns, by using the interpretative framework of set-theoretic naturalism. I first distinguish three main forms of 'multiversism', and then I proceed to analyse Maddy's concerns. Among other things, I take into account salient aspects of multiverse-related mathematics , in particular, research programmes in set theory for which the use of the multiverse seems to (...) be crucial, and show how one may provide responses to Maddy's concerns based on a careful analysis of 'multiverse practice'. (shrink)

ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In (...) the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory. (shrink)

In this paper, we provide a detailed critical review of current approaches to ecthesis in Aristotle’s Prior Analytics, with a view to motivate a new approach, which builds upon previous work by Marion & Rückert (2016) on the dictum de omni. This approach sets Aristotle’s work within the context of dialectic and uses Lorenzen’s dialogical logic, hereby reframed with use of Martin-Löf's constructive type theory as ‘immanent reasoning’. We then provide rules of syllogistic for the latter, and provide proofs of (...) e-conversion, Darapti and Bocardo and e-subalternation, while showing how close to Aristotle’s text these proofs remain. (shrink)

Predicativity is a notable example of fruitful interaction between philosophy and mathematical logic. It originated at the beginning of the 20th century from methodological and philosophical reflections on a changing concept of set. A clarification of this notion has prompted the development of fundamental new technical instruments, from Russell's type theory to an important chapter in proof theory, which saw the decisive involvement of Kreisel, Feferman and Schütte. The technical outcomes of predica-tivity have since taken a life of their own, (...) but have also produced a deeper understanding of the notion of predicativity, therefore witnessing the " light logic throws on problems in the foundations of mathematics. " (Feferman 1998, p. vii) Predicativity has been at the center of a considerable part of Feferman's work: over the years he has explored alternative ways of explicating and analyzing this notion and has shown that predicative mathematics extends much further than expected within ordinary mathematics. The aim of this note is to outline the principal features of predicativity, from its original motivations at the start of the past century to its logical analysis in the 1950-60's. The hope is to convey why predicativity is a fascinating subject, which has attracted Feferman's attention over the years. (shrink)

This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. -/- Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned.

The aim of the present book is to give a comprehensive account of the ‘state of the art’ of substructural logics, focusing both on their proof theory and on their semantics (both algebraic and relational. It is for graduate students in either philosophy, mathematics, theoretical computer science or theoretical linguistics as well as specialists and researchers.

Prawitz has recently developed a theory of epistemic grounding that differs in many respects from his earlier semantics of arguments and proofs. An innovative approach to inferences yields a new conception of the intertwinement of the notions of valid inference and proof. We aim at singling out three reasons that may have led Prawitz to the ground-theoretic turn, i.e.: a better order in the explanation of the relation between valid inferences and proofs; a notion of valid inference based on which (...) valid inferences and proofs are recognisable as such; a reconstruction of the deductive activity that makes inferences capable of yielding justification per se. These topics are discussed by Prawitz with reference to a very general and ancient question: why and how correct deduction has the epistemic power to compel us to accept its conclusions, provided its premises are justified? We conclude by remarking that, in spite of some improvements, the ground-theoretic approach shares with the previous one a problem of vacuous validity which, as Prawitz himself points out, blocks in both cases a satisfactory explanation of epistemic compulsion. (shrink)

I explore the possibility of a structuralist interpretation of homotopy type theory (HoTT) as a foundation for mathematics. There are two main aspects to HoTT's structuralist credentials. First, it builds on categorical set theory (CST), of which the best-known variant is Lawvere's ETCS. I argue that CST has merit as a structuralist foundation, in that it ascribes only structural properties to typical mathematical objects. However, I also argue that this success depends on the adoption of a strict typing system which (...) undermines the metaphysical seriousness of this structuralism. Homotopy type theory adds to CST a distinctive theory of identity between sets, which arguably allows its objects to be seen as ante rem structures. I examine the prospects for such a view, and address many other interpretive problems as they arise. (shrink)

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient (...) to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted. (shrink)

The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...) senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics. (shrink)

In the Univalent Foundations of mathematics spatial notions like “point” and “path” are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory can be justified intuitively as a theory of shapes in the same way that ZFC can be justified intuitively as a theory of collections. I first clarify (...) what such an “intuitive justification” should be by distinguishing between formal and pre-formal “meaning explanations” in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like “shape”, “path” etc. (shrink)

We offer an analysis of the disciplinary transformations underwent by mathematical or symbolic logic since its emergence in the late 19 th century. Examined are its origins as a hybrid of philosophy and mathematics, the maturity and institutionalisation attained under the label “logic and foundations,” a second wave of institutionalisation in the Postwar period, and the institutional developments since 1975 in connection with computer science and with the study of language and informatics. Although some “internal history” is discussed, the main (...) focus is on the emergence, consolidation and convolutions of logic as a discipline, through various professional associations and journals, in centers such as Torino, Göttingen, Warsaw, Berkeley, Princeton, Carnegie Mellon, Stanford, and Amsterdam. (shrink)

We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...) consider an idea within intuitionism about what it is to justify the assertion of a proposition. It depends on Heyting’s view of the meaning of a proposition, but does not presuppose the concept of inference or of proof as chains of inferences. I discuss this idea and what is required in order to use it for an adequate notion of valid inference. (shrink)

We construct an extension P of the standard language of classical propositional logic by adjoining to the alphabet of a new category of logical-pragmatic signs. The well formed formulas of are calledradical formulas (rfs) of P;rfs preceded by theassertion sign constituteelementary assertive formulas of P, which can be connected together by means of thepragmatic connectives N, K, A, C, E, so as to obtain the set of all theassertive formulas (afs). Everyrf of P is endowed with atruth value defined classically, (...) and everyaf is endowed with ajustification value, defined in terms of the intuitive notion of proof and depending on the truth values of its radical subformulas. In this framework, we define the notion ofpragmatic validity in P and yield a list of criteria of pragmatic validity which hold under the assumption that only classical metalinguistic procedures of proof be accepted. We translate the classical propositional calculus (CPC) and the intuitionistic propositional calculus (IPC) into the assertive part of P and show that this translation allows us to interpret Intuitionistic Logic as an axiomatic theory of the constructive proof concept rather than an alternative to Classical Logic. Finally, we show that our framework provides a suitable background for discussing classical problems in the philosophy of logic. (shrink)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, but the term (...) itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

We argue that logical semantics might have faltered due to its failure in distinguishing between two fundamentally very different types of concepts: ontological concepts, that should be types in a strongly-typed ontology, and logical concepts, that are predicates corresponding to properties of and relations between objects of various ontological types. We will then show that accounting for these differences amounts to the integration of lexical and compositional semantics in one coherent framework, and to an embedding in our logical semantics of (...) a strongly-typed ontology that reflects our commonsense view of the world and the way we talk about it in ordinary language. We will show that in such a framework a number of challenges in natural language semantics can be adequately and systematically treated. (shrink)

Inference versus consequence , an invited lecture at the LOGICA 1997 conference at Castle Liblice, was part of a series of articles for which I did research during a Stockholm sabbatical in the autumn of 1995. The article seems to have been fairly effective in getting its point across and addresses a topic highly germane to the Uppsala workshop. Owing to its appearance in the LOGICA Yearbook 1997 , Filosofia Publishers, Prague, 1998, it has been rather inaccessible. Accordingly it is (...) republished here with only bibliographical changes and an afterword. (shrink)

The goals of reduction andreductionism in the natural sciences are mainly explanatoryin character, while those inmathematics are primarily foundational.In contrast to global reductionistprograms which aim to reduce all ofmathematics to one supposedly ``universal'' system or foundational scheme, reductive proof theory pursues local reductions of one formal system to another which is more justified in some sense. In this direction, two specific rationales have been proposed as aims for reductive proof theory, the constructive consistency-proof rationale and the foundational reduction rationale. However, (...) recent advances in proof theory force one to consider the viability of these rationales. Despite the genuine problems of foundational significance raised by that work, the paper concludes with a defense of reductive proof theory at a minimum as one of the principal means to lay out what rests on what in mathematics. In an extensive appendix to the paper,various reduction relations betweensystems are explained and compared, and arguments against proof-theoretic reduction as a ``good'' reducibilityrelation are taken up and rebutted. (shrink)

The book is about logical analysis of natural language. Since we humans communicate by means of natural language, we need a tool that helps us to understand in a precise manner how the logical and formal mechanisms of natural language work. Moreover, in the age of computers, we need to communicate both with and through computers as well. Transparent Intensional Logic is a tool that is helpful in making our communication and reasoning smooth and precise. It deals with all kinds (...) of linguistic context in a fully compositional and anti-contextual way. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

Proof-Theoretic Semantics, by FrancezNissim. London: College Publications, 2015. Pp. xx + 415.

The Univalent Foundations of Mathematics provide not only an entirely non-Cantorian conception of the basic objects of mathematics but also a novel account of how foundations ought to relate to mathematical practice. In this paper, I intend to answer the question: In what way is UF a new foundation of mathematics? I will begin by connecting UF to a pragmatist reading of the structuralist thesis in the philosophy of mathematics, which I will use to define a criterion that a formal (...) system must satisfy if it is to be regarded as a “structuralist foundation.” I will then explain why both set-theoretic foundations like ZFC and category-theoretic foundations like ETCS satisfy this criterion only to a very limited extent. Then I will argue that UF is better-able to live up to the proposed criterion for a structuralist foundation than any currently available foundational proposal. First, by showing that most criteria of identity in the practice of mathematics can be formalized in terms of the preferred criterion of identity between the basic objects of UF. Second, by countering several objections that have been raised against UF’s capacity to serve as a foundation for the whole of mathematics. (shrink)

This paper offers a new interpretation for Wittgenstein`s treatment of mathematical identities. As it is widely known, Wittgenstein`s mature philosophy of mathematics includes a general rejection of abstract objects. On the other hand, the traditional interpretation of mathematical identities involves precisely the idea of a single abstract object – usually a number –named by both sides of an equation.

The aim of this paper is to reconsider several proposals that have been put forward in order to develop a Proof-Theoretical Semantics, from the by now classical neo-verificationist approach provided by D. Prawitz and M. Dummett in the Seventies, to an alternative, more recent approach mainly due to the work of P. Schroeder-Heister and L. Hallnäs, based on clausal definitions. Some other intermediate proposals are very briefly sketched. Particular attention will be given to the role played by the so-called Fundamental (...) Assumption. We claim that whereas, in the neo-verificationist proposal, the condition expressed by that Assumption is necessary to ensure the completeness of the justification procedure ( from the outside , so to speak), within the definitional framework it is a built-in feature of the proposal. The latter approach, therefore, appears as an alternative solution to the problem which prompted the neo-verificationists to introduce the Fundamental Assumption. (shrink)

This paper addresses the problem of upgrading functional information to knowledge. Functional information is defined as syntactically well-formed, meaningful and collectively opaque data. Its use in the formal epistemology of information theories is crucial to solve the debate on the veridical nature of information, and it represents the companion notion to standard strongly semantic information, defined as well-formed, meaningful and true data. The formal framework, on which the definitions are based, uses a contextual version of the verificationist principle of truth (...) in order to connect functional to semantic information, avoiding Gettierization and decoupling from true informational contents. The upgrade operation from functional information uses the machinery of epistemic modalities in order to add data localization and accessibility as its main properties. We show in this way the conceptual worthiness of this notion for issues in contemporary epistemology debates, such as the explanation of knowledge process acquisition from information retrieval systems, and open data repositories. (shrink)

This paper aims to develop the implications of logical expressivism for a theory of dialogue coherence. I proceed in three steps. Firstly, certain structural properties of cooperative dialogue are identified. Secondly, I describe a variant of the multi-agent natural deduction calculus that I introduced in Piwek (J Logic Lang Inf 16(4):403–421, 2007 ) and demonstrate how it accounts for the aforementioned structures. Thirdly, I examine how the aforementioned system can be used to formalise an expressivist account of logical vocabulary that (...) is inspired by Brandom (Making it explicit: reasoning, representing, and discursive commitment, 1994 ; Articulating reasons: an introduction to inferentialism, 2000 ). This account conceives of the logical vocabulary as a tool which allows speakers to describe the inferential practices which underlie their language use, i.e., it allows them to make those practices explicit. The rewards of this exercise are twofold: (1) We obtain a more precise account of logical expressivism which can be defended more effectively against the critique that such accounts lead to cultural relativism. (2) The formalised distinction between engaging in a practice and expressing it, opens the way for a revision of the theory of dialogue coherence. This revision eliminates the need for logically complex formulae to account for certain structural properties of cooperative dialogue. (shrink)

Graham Solomon, to whom this collection is dedicated, went into hospital for antibiotic treatment of pneumonia in Oc- ber, 2001. Three days later, on Nov. 1, he died of a massive stroke, at the age of 44. Solomon was well liked by those who got the chance to know him—it was a revelation to?nd out, when helping to sort out his a?airs after his death, how many “friends” he had whom he had actually never met, as his email included correspondence (...) with philosophers around the world running sometimes to hundreds of messages. He was well respected in the philosophical community more broadly. He was for several years a member of the editorial board for the Western Ontario Series in Philosophy of Science. While he was employed at Wilfrid Laurier University in Waterloo, Ontario, several of us at the University of Wat- loo always regarded our own department as a sort of second academic home for him. We therefore decided that it would be appropriate to hold a memorial conference in his honour. Thanks to the generous?nancial support of the Humphrey Conference Fund, we were able to do so in May 2003. Many of the papers in this volume were presented at that conf- ence. (shrink)

The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed (...) in the original derivation of the Paradox. Instead we propose that the central tenet of verificationism is most accurately formulated as follows: if φ is true, then there exists a proof of φ Building on the work of Artemov (Bull Symb Log 7(1): 1-36, 2001), a system of explicit modal logic with proof quantifiers is introduced to reason about such statements. When the original reasoning of the Paradox is developed in this setting, we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs. This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence. (shrink)

I argue that the implementation of theDummettian program of an ``anti-realist'' semanticsrequires quite different conceptions of the technicalmeaning-theoretic terms used than those presupposed byDummett. Starting from obvious incoherences in anattempt to conceive truth conditions as assertibilityconditions, I argue that for anti-realist purposesnon-epistemic semantic notions are more usefully kept apart from epistemic ones rather than beingreduced to them. Embedding an anti-realist theory ofmeaning in Martin-Löf's Intuitionistic Type Theory(ITT) takes care, however, of many notorious problemsthat have arisen in trying to specify suitableintuitionistic (...) notions of semantic value,truth-conditions, and validity, taking into accountthe so-called ``defeasibility of evidence'' forassertions in empirical discourses. (shrink)

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.

The aims of this paper are twofold: firstly, to say something about that philosophy of mathematics known as 'intuitionism' and, secondly, to fit these remarks into a more general message for the philosophy of mathematics as a whole. What I have to say on the first score can, without too much inaccuracy, be compressed into two theses. The first is that the intuitionistic critique of classical mathematics can be seen as based primarily on epistemological rather than on meaning-theoretic considerations. The (...) second is that the intuitionist's chief objection to the classical mathematician's use of logic does not center on the use of particular logical principles (in particular, the law of excluded middle and its ilk). Rather on the role the classical mathematician assigns (or at least extends) generally (i.e. regardless of the particular principles used) to the use of logic in the production mathematical proofs. Thus, the intuitionist critique of logic that we shall be presenting is far more radical than that which has commonly been presented. -/- Concerning the second, more general, theme, my claim is this: some restriction of the role of logical inference in mathematical proof such as that mentioned above is necessary if one is to account for the seeming difference in the epistemic conditions of provers whose reasoning is based on genuine insight into the subject-matter being investigated, and would-be provers whose reasoning is based not on such insight, but rather on principles of inference which hold of every subject-matter indifferently. (shrink)

This monograph proposes a new way of studying the different forms of correlational inference, known in the Islamic jurisprudence as qiyās. According to the authors’ view, qiyās represents an innovative and sophisticated form of dialectical reasoning that not only provides new epistemological insights into legal argumentation in general but also furnishes a fine-grained pattern for parallel reasoning which can be deployed in a wide range of problem-solving contexts and does not seem to reduce to the standard forms of analogical reasoning (...) studied in contemporary philosophy of science and argumentation theory. After an overview of the emergence of qiyās and of the work of al-Shīrāzī penned by Soufi Youcef, the authors discuss al-Shīrāzī’s classification of correlational inferences of the occasioning factor. The second part of the volume deliberates on the system of correlational inferences by indication and resemblance. The third part develops the main theoretical background of the authors’ work, namely, the dialogical approach to Martin-Löf's Constructive Type Theory. The authors present this in a general form and independently of adaptations deployed in parts I and II. Part III also includes an appendix on the relevant notions of Constructive Type Theory, which has been extracted from an overview written by Ansten Klev. The book concludes with some brief remarks on contemporary approaches to analogy in Common and Civil Law and also to parallel reasoning in general. (shrink)

This paper provides a detailed comparison between discourse representation theory and dependent type semantics, two frameworks for discourse semantics. Although it is often stated that DRT and those frameworks based on dependent types are mutually exchangeable, we argue that they differ with respect to variable handling, more specifically, how substitution and other operations on variables are defined. This manifests itself in two recalcitrant problems posed for DRT; namely, the overwrite problem and the duplication problem. We will see that these problems (...) still pose a challenge for various extended compositional systems based on DRT, while they do not arise in a framework of DTS where substitution and other operations are defined in the standard type-theoretic manner without stipulating any additional constraints. We also compare the notions of contexts underlying these two kinds of frameworks, namely, contexts represented as assignment functions and contexts represented as proof terms, and see what different predictions they make for some linguistic examples. (shrink)

Dag Prawitz’s theory of grounds proposes a fresh approach to valid inferences. Its main aim is to clarify nature and reasons of their epistemic power. The notion of ground is taken to denote what one is in possession of when in a state of evidence, and valid inferences are described in terms of operations that make us pass from grounds we already have to new grounds. Thanks to a rigorously developed proof-as-chains conception, the ground-theoretic framework permits Prawitz to overcome some (...) conceptual difficulties of his earlier proof-theoretic explanation. Though from different points of view, anyway, the two accounts share an issue of recognizability of relevant operational properties. (shrink)

An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation (‘It is unwarranted that. . . ’) and intuitionistic negation (‘It is refutable that. . . ’). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete.

The meaning of a declarative sentence and that of an interrogative sentence differ in their aspect of mood. A semantics of mood has to account for the differences in meaning between these sentences, and it also has to explain that sentences in different moods may have a common core. The meaning of the declarative mood is to be explained not in terms of actual force (contra Dummett), but in terms of potential force. The meaning of the declarative sentence (including its (...) mood) is called the assertion-candidate, which is explained by what one must know in order to be entitled to utter the declarative with assertive force. Both a cognitive notion (knowledge) and a pragmatic notion (assertive force) are thus part of the explanation of the assertion-candidate. Davidson’s criticism that such a theory is in need of an account of the distinction between standard and non-standard uses of the declarative is answered: without counter-indications an utterance of a declarative sentence is understood as having assertive force. The meaning of an interrogative sentence, the question-candidate, and that of the other sentence types can ultimately be explained in terms of their specific relations to the assertion-candidate. Martin-Löf’s constructive type theory is used to show the philosophical relevance of a semantics of mood. The constructivist notion of proposition needs to be embedded in a theory of the assertion-candidate, which fulfils the offices of being the meaning of the declarative sentence, the content of judgement and assertion and the bearer of epistemic truth. (shrink)

This paper attempts to show that mathematical knowledge does not grow by a simple process of accumulation and that it is possible to provide a quasi-empirical (in Lakatos's sense) account of mathematical theories. Arguments supporting the first thesis are based on the study of the changes occurred within Eudidean geometry from the time of Euclid to that of Hilbert; whereas those in favour of the second arise from reflections on the criteria for refutation of mathematical theories.

ZFC has sentences that quantify over all sets or all ordinals, without restriction. Some have argued that sentences of this kind lack a determinate meaning. We propose a set theory called TOPS, using Natural Deduction, that avoids this problem by speaking only about particular sets.

This paper proposes a unified dependent type analysis of three puzzling phenomena: inversely linked interpretations, weak definite readings in possessives and Haddock-type readings. We argue that the three problematic readings have the same underlying surface structure, and that the surface structure postulated can be interpreted properly and compositionally using dependent types. The dependent type account proposed is the first, to the best of our knowledge, to formally connect the three phenomena. A further advantage of our proposal over previous analyses is (...) that it offers a principled solution to the puzzle of why both inversely linked interpretations and weak definite readings are blocked with certain prepositions. (shrink)

The two different layers of logical theory—epistemological and ontological—are considered and explained. Special attention is given to epistemic assumptions of the kind that a judgement is granted as known, and their role in validating rules of inference, namely to aid the inferential preservation of epistemic matters from premise judgements to conclusion judgement, while ordinary Natural Deduction assumptions serve to establish the holding of consequence from antecedent propositions to succedent proposition.