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.

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

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)

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)

The traditional picture of logic takes it for granted that "valid arguments have a fundamental epistemic significance", but neither model theory nor traditional proof theory dealing with formal system has been able to give an account of this significance. Since valid arguments as usually understood do not in general have any epistemic significance, the problem is to explain how and why we can nevertheless use them sometimes to acquire knowledge. It is suggested that we should distinguish between arguments and acts (...) of inferences and that we have to reconsider the latter notion to arrive at the desired explanation. More precisely, the notions should be developed so that the following relationship holds: one gets in possession of a ground for a conclusion by inferring it from premisses for which one already has grounds, provided that the inference in question is valid. The paper proposes explications of the concepts of ground and deductively valid inference so that this relationship holds as a conceptual truth. Logical validity of inference is seen as a special case of deductive validity, but does not add anything as far as epistemic significance is concerned—it resides already in the deductively valid inferences. (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)

This monograph proposes a new way of implementing interaction in logic. It also provides an elementary introduction to Constructive Type Theory. The authors equally emphasize basic ideas and finer technical details. In addition, many worked out exercises and examples will help readers to better understand the concepts under discussion. One of the chief ideas animating this study is that the dialogical understanding of definitional equality and its execution provide both a simple and a direct way of implementing the CTT approach (...) within a game-theoretical conception of meaning. In addition, the importance of the play level over the strategy level is stressed, binding together the matter of execution with that of equality and the finitary perspective on games constituting meaning. According to this perspective the emergence of concepts are not only games of giving and asking for reasons, they are also games that include moves establishing how it is that the reasons brought forward accomplish their explicative task. Thus, immanent reasoning games are dialogical games of Why and How. (shrink)

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)

In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in making type theories (...) more expressive for formal semantics. It not only gives a satisfactory solution to the basic problem of ‘multiple categorisation’ caused by interpreting common nouns as types, but provides a powerful formal framework to model interesting linguistic phenomena such as copredication, whose formal treatment has been found difficult in a Montagovian setting. In particular, we show how to formally introduce dot-types in a type theory with coercive subtyping and study some type-theoretic constructs that provide useful representational tools for reference transfers and multiple word meanings in formal lexical semantics. (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)

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)

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)

On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. As (...) recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (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)

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)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (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 now move to the demonstration of the left-to-right direction of the equivalence result. Let us assume that there is a winning $$\mathbf {P}$$ P -strategy in the dialogical game for $$\varphi $$ φ.

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)

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)

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)

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)

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)

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.

What is the appropriate notion of truth for sentences whose meanings are understood in epistemic terms such as proof or ground for an assertion? It seems that the truth of such sentences has to be identified with the existence of proofs or grounds, and the main issue is whether this existence is to be understood in a temporal sense as meaning that we have actually found a proof or a ground, or if it could be taken in an abstract, tenseless (...) sense. Would the latter alternative amount to realism with respect to proofs or grounds in a way that would be contrary to the supposedly anti-realistic standpoint underlying the epistemic understanding of linguistic expressions? Before discussing this question, I shall consider reasons for construing linguistic meaning epistemically and relations between such reasons and reasons for taking an anti-realist point of view towards the discourse in question. (shrink)

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)

In Transparent Intensional Logic we can recognize two distinct notions of computation that loosely correspond to term rewriting and term interpretation as known from lambda calculus. Our goal will be to further explore these two notions and examine some of their properties.

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (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)

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)

We outline a class of term-languages for epistemic grounding inspired by Prawitz’s theory of grounds. We show how denotation functions can be defined over these languages, relating terms to proof-objects built up of constructive functions. We discuss certain properties that the languages may enjoy both individually and with respect to their expansions. Finally, we provide a ground-theoretic version of Prawitz’s completeness conjecture, and adapt to our framework a refutation of this conjecture due to Piecha and Schroeder-Heister.

In the present day and age, it seems that every constructivist philosopher of mathematics and her brother wants to be known as an intuitionist. In this paper, It will be shown that such a self-identification is in most cases mistaken. For one thing, not any old (or new) constructivism is intuitionism because not any old relevant construction is carried out mentally in intuition, as Brouwer envisaged. (edited).

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.

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)

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)

In this paper we propose a way to deal with natural language inference by implementing Modern Type Theoretical Semantics in the proof assistant Coq. The paper is a first attempt to deal with NLI and natural language reasoning in general by using the proof assistant technology. Valid NLIs are treated as theorems and as such the adequacy of our account is tested by trying to prove them. We use Luo’s Modern Type Theory with coercive subtyping as the formal language into (...) which we translate natural language semantics, and we further implement these semantics in the Coq proof assistant. It is shown that the use of a MTT with an adequate subtyping mechanism can give us a number of promising results as regards NLI. Specifically, it is shown that a number of inference cases, i.e. quantifiers, adjectives, conjoined noun phrases and temporal reference among other things can be successfully dealt with. It is then shown, that even though Coq is an interactive and not an automated theorem prover, automation of all of the test examples is possible by introducing user-defined automated tactics. Lastly, the paper offers a number of innovative approaches to NL phenomena like adjectives, collective predication, comparatives and factive verbs among other things, contributing in this respect to the theoretical study of formal semantics using MTTs. (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)

A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined.

In this paper we present a study of adjectival/adverbial modification using modern type theories, i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented given their proof-theoretic nature. In MTT-semantics, common (...) nouns are interpreted as types rather than predicates. Therefore, in order to capture the semantics of adjectives adequately, one needs to meet the challenge of modeling CNs modified by adjectives as types. To explicate that this can be done successfully, we first look at the mainstream classification of adjectives, i.e. intersective, subsective and non-subsective adjectives. There, we show that the rich type structure available in MTTs, along with a suitable subtyping framework, offers an adequate mechanism to model these cases. In particular, this modelling naturally takes care of the characterising inferences associated with each class of adjectives. Then, more advanced issues on adjectival modification are discussed: degree adjectives, comparatives and multidimensional adjectives. There, it is shown that the use of indexed types can be usefully applied in order to deal with these cases. In the same vein, the issue of adverbial modification is discussed. We study two general typings for sentence and VP adverbs respectively. It is shown that the rich type structure in MTTs further provides useful organisational mechanisms in giving formal semantics for adverbs. In particular, we discuss the use of \-types to capture the veridicality/non-veridicality distinction and further discuss cases of intensional adverbs using the type theoretic notion of context. We also look at manner, subject and speech act adverbials and propose solutions using MTTs. Finally, we show that the current proof technology can help mechanically check the associated inferences. A number of our proposals concerning adjectival and adverbial modification have been formalised in the proof assistant Coq and many of the associated inference patterns are checked to be correctly captured. (shrink)

We introduce _Interleave-Disjunction-Lock parallel multiple context-free grammars_ (IDL-PMCFG), a novel grammar formalism designed to describe the syntax of free word order languages that allow for extensive interleaving of grammatical constituents. Though interleaved constituents, and especially the so-called hyperbaton, are common in several ancient (Classical Latin and Greek, Sanskrit...) and modern (Hungarian, Finnish...) languages, these syntactic structures are often difficult to express in existing formalisms. The IDL-PMCFG formalism combines Seki et al.’s parallel multiple context-free grammars (PMCFG) with Nederhof and Satta’s IDL (...) expressions. We define the semantics of IDL-PMCFGs and study their expressivity, proving that IDL-PMCFG extends both PMCFG and IDL-CFG (context-free grammars equipped with IDL expressions) and that IDL-PMCFG parsing is \(\mathrm {NP}\) -hard. We then introduce COMPĀ, a programming language extending Ranta’s Grammatical Framework (GF) and built as a high-level front-end formalism to IDL-PMCFG for practical grammar development. We present a parsing algorithm for IDL-PMCFG inspired by earlier Earley-style PMCFG parsing algorithms and Nederhof and Satta’s IDL graphs and give a worst-case estimate of its complexity as a function of several metrics on IDL expressions, the size of the input and a new notion of the _G_-density of a language. (shrink)

In this paper, we study dialogue as a game, but not only in the sense in which there would exist winning strategies and a priori rules. Dialogue is not governed by game rules like for chess or other games, since even if we start from a priori rules, it is always possible to play with them, provided that some invariant properties are preserved. An important discovery of Ludics is that such properties may be expressed in geometrical terms. The main feature (...) of a dialogue is “convergence”. Intuitively, a dialogue “diverges” when it stops prematurely by some disruption, or a violation of the tacit agreed upon conditions of the discourse. It converges when the two speakers go together towards a situation where they agree at least on some points. As we shall see, convergence may be thought of through the geometrical concept of orthogonality . Utterances in a dialogue have as their content, not only the processes (similar to proofs) which lead to them from a monologic view, but also their interactions with other utterances. Finally, any utterance must be seen as co-constructed in an interaction between two processes. That is to say that it not only contains one speaker’s intentions but also his or her expectations from the other interlocutor. From our viewpoint, discursive strategies like narration , elaboration , topicalization may derive from such interactions, as well as speech acts like assertion, question and denegation. (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)

This paper outlines a framework for the abstract investigation of the concept of canonicity of names and of naming systems. Degrees of canonicity of names and of naming systems are distinguished. The structure of the degrees is investigated, and a notion of relative canonicity is defined. The notions of canonicity are formally expressed within a Carnapian system of second-order modal logic.

If proofs are nothing more than truth makers, then there is no force in the standard argument against classical logic (there is no guarantee that there is either a proof forA or a proof fornot A). The standard intuitionistic conception of a mathematical proof is stronger: there are epistemic constraints on proofs. But the idea that proofs must be recognizable as such by us, with our actual capacities, is incompatible with the standard intuitionistic explanations of the meanings of the logical (...) constants. Proofs are to be recognizable in principle, not necessarily in practice, as shown in section 1. Section 2 considers unknowable propositions of the kind involved in Fitch''s paradox:p and it will never be known thatp. It is argued that the intuitionist faces a dilemma: give up strongly entrenched common sense intuitions about such unknowable propositions, or give up verificationism. The third section considers one attempt to save intuitionism while partly giving up verificationism: keep the idea that a proposition is true iff there is a proof (verification) of it, and reject the idea that proofs must be recognizable in principle. It is argued that this move will have the effect that some standard reasons against classical semantics will be effective also against intuitionism. This is the case with Dummett''s meaning theoretical argument. At the same time the basic reason for regarding proofs as more than mere truth makers is lost. (shrink)