I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental issues indicate that (...) the interpretation is unsustainable regardless: (1) it is hard to determine, without appealing to propositional intentions on pain of circularity, what intention a proof-object should be understood as a fulfillment of; (2) due to a difficult fulfillment dilemma, it is unclear, at best, what the object of an intention corresponding to a proposition is. (shrink)

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

How is Frege able to claim that the notion of judgement is essential to his logic without introducing a form of psychologism? I argue first that Frege’s logical notion of judgement is to be distinguished from an empirical notion of judgement, that it cannot be understood as an abstract, idealized notion, and that there are doubts concerning a transcendental reading of Frege’s writings. Then, I explain that the logical notion of judgement has to be understood from a first-person perspective, to (...) be contrasted with a third-person perspective, in which judgement is understood as an empirical, psychological phenomenon. Frege’s logic is essentially a first-person engagement, as each of us can make use of the ideography as a science of logic only if we ourselves have made the relevant judgements. Finally, I claim that the judging agent as conceived by Frege can, after all, be understood as a transcendental ego. (shrink)

Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of demonstration. One thereby has (...) grounded the assertion by an act of demonstration, and a grounding account of assertion therefore suits constructive type theory. Because the act of demonstration in which such a proof object is constructed results in knowledge that A is true, the constructivist account of assertion has to ward off some of the criticism directed against knowledge accounts of assertion. It is especially the internal relation between a judgement being grounded and its being known that makes it possible to do so. The grounding account of assertion can be considered as a justification account of assertion, but it also differs from justification accounts recently proposed, namely in the treatment of selfless assertions, that is, assertions which are grounded, but are not accompanied by belief. (shrink)

A central problem for any truthmaker theory is the problem of negative truths. In this paper, I develop a novel, piecemeal strategy for solving this problem. The strategy puts central focus on a truth-relevant notion of aboutness within a metaphysically modest version of truthmaker theory and uses key conceptual tools gained by taking a deeper look at the best attempts to solve the problem of intentionality. I begin this task by critically discussing past proposed solutions to P-NEG in light of (...) Russell’s debate with Demos. This reveals a central difficulty with addressing the problem, specifically that one cannot be committed to incompatibility facts in one’s account of negation and of the truth of negative truths. I then present an aboutness-based version of truthmaker theory. Utilising what I call the strict and full account of aboutness, I extract aboutness-based theories of truth and falsity. I use this machinery to present a promising new strategy for solving P-NEG which does not have the problems of alternative approaches. Finally, I present and respond to some potential objections. (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)

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.