Ansten Klev

In this chapter we will provide the logical framework of dialogues for immanent reasoning, the dialogical framework incorporating features of Constructive Type Theory and making explicit the players’ reasons for asserting a proposition. We will therefore be using the material provided in Chaps. 2, 3, 4, and 5 on CTT and on the standard dialogical framework and assume the reader is familiar enough with it. The framework of dialogues for immanent reasoning takes a further step in the task of making explicit the dynamic foundations of reasoning, based on equality in action: reasons adducing statements are introduced in the object-language, and the Proponent’s task in formal dialogues is to force the Opponent to provide herself the reasons the Proponent needs in order to justify his thesis; once the Opponent has produced her reasons, the Proponent uses equality rules (the Socratic rule for instance) to copy these reasons and use them to his own ends. In this respect, CTT proof-objects are adapted to the dialogical framework, yielding two new elements in our framework: local reasons, the backbone of dialogues for immanent reasoning at the play level which will be introduced in this chapter and the next (Chaps. 6 and 7 ); and strategic reasons, justifications at the strategy level corresponding to proof-objects which will be the object of Chap. 9. Having local reasons in the dialogical framework provides a structure in which the reasons given and asked for actually appear in the object-language, and the Proponent can then (locally) justify his statements by explicitly copying the Opponent’s reasons for his own statements.

The present volume develops a new way of linking Constructive Type Theory (CTT) with dialogical logic by following these three complementary paths, as mentioned in the preface: A. The path observing that Sundholm’s (1997) notion of epistemic assumption is closely linked to the Copy-cat and Socratic rules and that it provides the dialogical conception of definitional equality; B. the path joining (in principle) Martin-Löf in his (2017a, 2017b) suggestions, according to which the new insights provided by the dialogical framework mainly amount to the following three interconnected points: B.1. the introduction of rules of interaction rather than of rules of inference; B.2. the challenge to the semantization of pragmatics and the claim of the deontic nature of logic; B.3. the central role of the notion of execution in the rules of interaction: executions are responses to questions of knowing how. C. The path stressing the importance of the play level and the associated notion of dialogue-definiteness.

This chapter will provide a more technical approach to the standard (non-CTT) dialogical framework at the play level. The next chapter ( 5 ) will do the same at the strategy level. It will then be possible to introduce local reasons in the dialogues and thus start making it explicit that dialogues are games of giving and asking for reasons; in this sense, the elements contributing to the meaning as use will appear in the object language. The link to equality in action will then be spelled out in the following two chapters ( 6 and 7 ), based on what will be presented in the next two chapters ( 4 and 5 ).

The Curry–Howard correspondence, according to which propositions are types, suggests that every paradox formulable in natural deduction has a type-theoretical counterpart. I will give a purely type-theoretical formulation of Curry’s paradox. On the basis of the definition of a type, Γ(A), Curry’s reasoning can be adapted to show the existence of an object of the arbitrary type A. This is paradoxical for several reasons, among others that A might be an empty type. The solution to the paradox consists in seeing that Γ(A) is not a well-defined type.

This book honors the original and influential work by Göran Sundholm in the fields of the philosophy and history of logic and mathematics. Borne from two conferences held in Paris and Leiden on the occasion of Göran Sundholm’s retirement in 2019, the contributions collected in this volume represent work from leading logicians and philosophers. Reflecting Sundholm’s contributions to the history and philosophy of logic, this book is divided into two parts: the architecture and archaeology of logic. The essays collected in the ‘architecture’ section cover primarily the systematic approach to basic logical concepts taken by Sundholm, including type theory, epistemic assumptions, and notions of consequence. The ‘archaeology’ section includes contributions focused on Sundholm’s contributions to the history of philosophy and logic. Enclosing these two sections are, on the one end, autobiographical remarks of Sundholm's and, on the other, a paper on cooking and philosophy, reflecting another of Sundholm's passions in life. This book is of interest to logicians, philosophers, mathematicians, and computer scientists.

According to the iterative conception of set, sets are formed in stages. According to the purely iterative conception of set, sets are formed by iterated application of a set-of operation. The cumulative hierarchy is a mathematical realization of the iterative conception of set. A mathematical realization of the purely iterative conception can be found in Peter Aczel’s type-theoretic model of constructive set theory. I will explain Aczel’s model construction in a way that presupposes no previous familiarity with the theories on which it is based.

The aim here is to investigate assertion and inference as notions of logic. Assertion will be explained in terms of its purpose, which is to give interlocutors the right to request the assertor to do a certain task. The assertion is correct if, and only if, the assertor knows how to do this task. Inference will be explained as an assertion equipped with what I shall call a justification profile, a strategy for making good on the assertion. The inference is valid if, and only if, correctness is preserved from the premiss assertions to the conclusion assertion. Most of this is a spelling out of views on assertion and inference presented by Per Martin-Löf in lectures since 2015.

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.

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.

A detailed argument is provided for the thesis that Dedekind was a logicist about arithmetic. The rules of inference employed in Dedekind's construction of arithmetic are, by his lights, all purely logical in character, and the definitions are all explicit; even the definition of the natural numbers as the abstract type of simply infinite systems can be seen to be explicit. The primitive concepts of the construction are logical in their being intrinsically tied to the functioning of the understanding.

The spiritus asper as used by Frege in a letter to Russell from 1904 bears resemblance to Church’s lambda. It is natural to ask how they relate to each other. An alternative approach to functional abstraction developed by Per Martin-Löf some thirty years ago allows us to describe the relationship precisely. Frege’s spiritus asper provides a way of restructuring a unary function name in Frege’s sense such that the argument place indicator occurs all the way to the right. Martin-Löf’s alternative approach shows that this is only half of what lambda does. The other half is the deletion of the argument place indicator, resulting in what Frege would have called an isolated function name.

There seems to be a view that intuitionists not only take the Axiom of Choice (AC) to be true, but also believe it a consequence of their fundamental posits. Widespread or not, this view is largely mistaken. This article offers a brief, yet comprehensive, overview of the status of AC in various intuitionistic and constructivist systems. The survey makes it clear that the Axiom of Choice fails to be a theorem in most contexts and is even outright false in some important contexts. Of the systems surveyed, only intensional type theory renders AC a theorem, but the extent of AC in that theory does not include, for instance, real analysis. Only a small amount of extensionality is required in order for the obvious proof an intuitionist might offer for AC to break down.

The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin‐Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. Along the way, connections to philosophical debates concerning identity are noted. Some use of logical symbolism is inevitable in any serious discussion of type theory, but the emphasis here is on basic ideas rather than technicalities.

This paper discusses some of the ways in which Martin-Löf type theory differs from set theory. The discussion concentrates on conceptual, rather than technical, differences. It revolves around four topics: sets versus types; syntax; functions; and identity. The difference between sets and types is spelt out as the difference between unified pluralities and kinds, or sorts. A detailed comparison is then offered of the syntax of the two languages. Emphasis is placed on the distinction between proposition and judgement, drawn by type theory, but not by set theory. Unlike set theory, type theory treats the notion of function as primitive. It is shown that certain inconveniences pertaining to function application that afflicts the set- theoretical account of functions are thus avoided. Finally, the distinction, drawn in type theory, between judgemental and propositional identity is discussed. It is argued that the criterion of identity for a domain cannot be formulated in terms of propositional identity. It follows that the axiom of extensionality cannot be taken as a statement of the criterion of identity for sets.

Cet article donne un aperçu des diverses traces de la doctrine des catégories dans les écrits de Carnap. Les notions de catégories jouent un rôle particulièrement important dans le livre Der logische Aufbau der Welt, mais on les retrouve également dans de nombreuses autres œuvres de Carnap. Sa thèse fait allusion à des catégories en plusieurs endroits. Son approche de la logique a été, pendant longtemps, fondée sur la théorie des types, incarnation de la doctrine des catégories dans la logique moderne. Et son point de vue sur la science unifiée est mieux compris à l’aide de la notion de catégorie.

Les contributions de Carnap au Congrès de 1935 marquent un triple changement dans sa philosophie: son tournant sémantique; ce qui sera appelé plus tard « la libéralisation de l’empirisme»; et son adoption du « langage des choses» comme base du langage de la science. C’est ce troisième changement qui est examiné ici. On s’interroge en particulier sur les motifs qui ont poussé Carnap à adopter le langage des choses comme langage protocolaire de la science unifiée et sur les vertus de ce langage, comparé aux autres types de langage protocolaire.

An act’s form of apprehension determines whether it is a perception, an imagination, or a signitive act. It must be distinguished from the act’s quality, which determines whether the act is, for instance, assertoric, merely entertaining, wishing, or doubting. The notion of form of apprehension is explained by recourse to the so-called content-apprehension model ; it is characteristic of the Logical Investigations that in it all objectifying acts are analyzed in terms of that model. The distinction between intuitive and signitive acts is made, and the notion of saturation is described, by recourse to the notion of form of apprehension.

The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, whereas the higher-order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.