A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS

In this paper we describe an intuitionistic theory SLP. It is a relatively strong theory containing intuitionistic principles for functionals of many types, in particular, the theory of the “creating subject”, axioms for lawless functionals and some versions of choice axioms. We construct a Beth model for the language of intuitionistic functionals of high types and use it to prove the consistency of SLP.We also prove that the intuitionistic theory SLP is equiconsistent with a classical theory TI. TI is a typed set theory, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types ≤ s is equiconsistent with the corresponding fragment of TI and that it is stronger than the previous fragment of SLP. Thus, both SLP and TI are much stronger than the second order arithmetic. By constructing the intuitionistic theory SLP and interpreting in it the classical set theoryTI, we contribute to the program of justifying classical mathematics from the intuitionistic point of view.

The Friedman-Sheard programme in intuitionistic logic

This paper compares the roles classical and intuitionistic logic play in restricting the free use of truth principles in arithmetic. We consider fifteen of the most commonly used axiomatic principles of truth and classify every subset of them as either consistent or inconsistent over a weak purely intuitionistic theory of truth.

Renewing Moral Intuitionism

According to moral intuitionism, moral properties are objective, but our cognitions of them are not always based on premises. In this paper, I develop a novel version of moral intuitionism and argue that this new intuitionism is worthy of closer attention. The intuitionistic theory I propose, while inspired by the early twentieth-century intuitionism of W.D. Ross, avoids the alleged errors of his view. Furthermore, unlike Robert Audi's contemporary formulation of intuitionism, my theory has the resources to account for the non-inferential character of particular, as opposed to merely general, moral beliefs. I achieve this result by avoiding the appeal to self-evidence to explain the possibility of non-inferential moral knowledge.

On the intuitionistic strength of monotone inductive definitions

We prove here that the intuitionistic theory T0↾ + UMIDN. or even EETJ↾ + UMIDN, of Explicit Mathematics has the strength of –CA0. In Section 1 we give a double-negation translation for the classical second-order μ-calculus, which was shown in [Mö02] to have the strength of –CA0. In Section 2 we interpret the intuitionistic μ-calculus in the theory EETJ↾ + UMIDN. The question about the strength of monotone inductive definitions in T0 was asked by S. Feferman in 1982, and — assuming classical logic — was addressed by M. Rathjen.

Husserl's phenomenological philosophy in Russia

The paper reviews phaenomenological influences on Russian philosophical thought. Before the bolyshevique revolution of 1917, Husserl's ideas had attracted the attention of many Russian theoreticians, and during the last two decades effects of this impact are closely investigated. First of all there were several philosophers under very direct influence of phenomenology: N. O. Lossky, the author of numerous books, in his work on logic; S. L. Frank, who had developed an intuitionistic theory of knowledge Gustav Spet, logician, aesthetician, linguist etc, who accepted Husserl's conceptions in his books on interpretation, philosophy of history and philosophy of language; Alexiy Lossev, who wrote some thirty books, and in his early period (works on ancient dialectics, philosophy of language and logics) was phenomenologically oriented; etc. Husserl's philosophy has traced or affected the ideas of several other Russian thinkers, so in USSR as in exile throughout Europe (for instance, Georges Gurvitch).

Some weak fragments of HA and certain closure properties

We show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.

Models of intuitionistic TT and NF

Let us define the intuitionistic part of a classical theory T as the intuitionistic theory whose proper axioms are identical with the proper axioms of T. For example, Heyting arithmetic HA is the intuitionistic part of classical Peano arithmetic PA.It's a well-known fact, proved by Heyting and Myhill, that ZF is identical with its intuitionistic part.In this paper, we mainly prove that TT, Russell's Simple Theory of Types, and NF, Quine's “New Foundations,” are not equal to their intuitionistic part. So, an intuitionistic version of TT or NF seems more naturally definable than an intuitionistic version of ZF.In the first section, we present a simple technique to build Kripke models of the intuitionistic part of TT (with short examples showing bad properties of finite sets if they are defined in the usual classical way).In the remaining sections, we show how models of intuitionistic NF2 and NF can be obtained from well-chosen classical ones. In these models, the excluded middle will not be satisfied for some non-stratified sentences.