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.

I offer an analysis of the sentence "the concept horse is a concept". It will be argued that the grammatical subject of this sentence, "the concept horse", indeed refers to a concept, and not to an object, as Frege once held. The argument is based on a criterion of proper-namehood according to which an expression is a proper name if it is so rendered in Frege's ideography. The predicate "is a concept", on the other hand, should not be thought of (...) as referring to a function. It will be argued that the analysis of sentences of the form "C is a concept" requires the introduction of a new form of statement. Such statements are not to be thought of as having function--argument form, but rather the structure subject--copula--predicate. (shrink)

Richard Dedekind’s theorem 66 states that there exists an infinite set. Its proof invokes such apparently nonmathematical notions as the thought-world and the self. This article discusses the content and context of Dedekind’s proof. It is suggested that Dedekind took the notion of the thought-world from Hermann Lotze. The influence of Kant and Bernard Bolzano on the proof is also discussed, and the reception of the proof in the mathematical and philosophical literature is covered in detail.

The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in (...) a proof-theoretical manner. (shrink)

Husserl, in his doctrine of categories, distinguishes what he calls regions from what he calls formal categories. The former are most general domains, while the latter are topic-neutral concepts that apply across all domains. Husserl’s understanding of these notions of category is here discussed in detail. It is, moreover, argued that similar notions of category may be recognized in Carnap’s Der logische Aufbau der Welt.

We offer an interpretation of the words and works of Richard Dedekind and the David Hilbert of around 1900 on which they are held to entertain diverging views on the structure of a deductive science. Firstly, it is argued that Dedekind sees the beginnings of a science in concepts, whereas Hilbert sees such beginnings in axioms. Secondly, it is argued that for Dedekind, the primitive terms of a science are substantive terms whose sense is to be conveyed by elucidation, whereas (...) Hilbert dismisses elucidation and consequently treats the primitives as schematic. (shrink)

Lecture notes from Husserl's logic lectures published during the last 20 years offer a much better insight into his doctrine of the forms of meaning than does the fourth Logical Investigation or any other work published during Husserl's lifetime. This paper provides a detailed reconstruction, based on all the sources now available, of Husserl's system of logical grammar. After having explained the notion of meaning that Husserl assumes in his later logic lectures as well as the notion of form of (...) meaning as it features in ‘doctrine of the forms of meaning’, I present a system of rules that describes all the various forms of meaning that Husserl singles out in his lectures. (shrink)

An act’s form of apprehension (Auffassungsform) 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 (Inhalt-Auffassung Schema); 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 (Fu ̈lle) is described, by recourse to the notion of form of apprehension. (shrink)

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. (shrink)

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.

Using infinite time Turing machines we define two successive extensions of Kleene’s ${\mathcal{O}}$ and characterize both their height and their complexity. Specifically, we first prove that the one extension—which we will call ${\mathcal{O}^{+}}$ —has height equal to the supremum of the writable ordinals, and that the other extension—which we will call ${\mathcal{O}}^{++}$ —has height equal to the supremum of the eventually writable ordinals. Next we prove that ${\mathcal{O}^+}$ is Turing computably isomorphic to the halting problem of infinite time Turing computability, (...) and that ${\mathcal{O}^{++}}$ is Turing computably isomorphic to the halting problem of eventual computability. (shrink)

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. (shrink)

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 put 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. (shrink)

By maintaining that a conditional sentence can be taken to express the validity of a rule of inference, we offer a solution to the Miners Paradox that leaves both modus ponens and disjunction elimination intact. The solution draws on Sundholm's recently proposed account of Fitch's Paradox.

Unified science is a recurring theme in Carnap's work from the time of the Aufbau until the end of the 1930's. The theme is not constant, but knows several variations. I shall extract three quite precise formulations of the thesis of unified science from Carnap's work during this period: from the Aufbau, from Carnap's so-called syntactic period, and from "Testability and Meaning" and related papers. My main objective is to explain these formulations and to discuss their relation, both to each (...) other and to other aspects of Carnap's work. (shrink)

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. (shrink)

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. (shrink)

According to the sortal conception of the universe of individuals every individual falls under a highest sortal, or category. It is argued here that on this conception the identity relation is defined between individuals a and b if and only if a and b fall under a common category. Identity must therefore be regarded as a relation of the form \, with three arguments x, y, and Z, where Z ranges over categories, and where the range of x and y (...) depends on the value of Z. An identity relation of this kind can be made good sense of in Martin-Löf’s type theory. But identity so construed requires a reformulation of Hume’s Principle that makes this principle unfit for explaining the sortal concept of cardinal number. The Neo-Logicist can therefore not appeal to the sortal conception in tackling the Julius Caesar problem, as proposed by Hale and Wright. (shrink)