L.E.J. Brouwer famously took the subject’s intuition of time to be foundational and from there ventured to build up mathematics. Despite being largely critical of formal methods, Brouwer valued axiomatic systems for their use in both communication and memory. Through the Dutch Mathematical Society, Gerrit Mannoury posed a challenge in 1927 to provide an axiomatization of intuitionistic arithmetic. Arend Heyting’s 1928 axiomatization was chosen as the winner and has since enjoyed the status of being the _de facto_ formalization of intuitionistic (...) arithmetic. We argue that axiomatizations of intuitionistic arithmetic ought to make explicit the role of the subject’s activity in the intuitionistic arithmetical process. While Heyting Arithmetic is useful when we want to contrast constructed objects with platonistic ones, Heyting Arithmetic omits the contribution of the subject and thus falls short as a response to Mannoury’s challenge. We offer our own solution, Doxastic Heyting Arithmetic, or \({\textsf{DHA}}\), which we contend axiomatizes Brouwerian intuitionistic arithmetic. (shrink)

Gödel’s ontological proof is by now well known based on the 1970 version, written in Gödel’s own hand, and Scott’s version of the proof. In this article new manuscript sources found in Gödel’s Nachlass are presented. Three versions of Gödel’s ontological proof have been transcribed, and completed from context as true to Gödel’s notes as possible. The discussion in this article is based on these new sources and reveals Gödel’s early intentions of a liberal comprehension principle for the higher order (...) modal logic, an explicit use of second-order Barcan schemas, as well as seemingly defining a rigidity condition for the system. None of these aspects occurs explicitly in the later 1970 version, and therefore they have long been in focus of the debate on Gödel’s ontological proof. (shrink)

Propositional modal logic is a standard tool in many disciplines, but first-order modal logic is not. There are several reasons for this, including multiplicity of versions and inadequate syntax. In this paper we sketch a syntax and semantics for a natural, well-behaved version of first-order modal logic, and show it copes easily with several familiar difficulties. And we provide tableau proof rules to go with the semantics, rules that are, at least in principle, automatable.

Modal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging (...) over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics. (shrink)

We present in this note a plea for Barcan formula. This view connects Barcan formula with a modal principle that expresses the -Introduction rule of first-order logic.