We present a decision procedure for the ∀∃ theory of the lattice of Σ1 sentences of Peano Arithmetic.

It has been argued, by Penrose and others, that Gödel's proof of his first incompleteness theorem shows that human mathematics cannot be captured by a formal system F: the Gödel sentence G(F) of F can be proved by a (human) mathematician but is not provable in F. To this argment it has been objected that the mathematician can prove G(F) only if (s)he can prove that F is consistent, which is unlikely if F is complicated. Penrose has invented a new (...) argument intended to avoid this objection. In the paper I try to show that Penrose's new argument is inconclusive. (shrink)

We present a decision procedure for the ∀∃ theory of the lattice of Σ1 sentences of Peano Arithmetic.

It is commonly agreed that the well-known Lucas-Penrose arguments and even Penrose's 'new argument' in [Penrose, R. (1994): Shadows of the Mind, Oxford University Press] are inconclusive. It is, perhaps, less clear exactly why at least the latter is inconclusive. This note continues the discussion in [Lindström, P. (2001): Penrose's new argument, J. Philos. Logic 30, 241-250; Shapiro, S.(2003): Mechanism, truth, and Penrose's new argument, J. Philos. Logic 32, 19-42] and elsewhere of this question.

It is one of the tasks of the philosophy of mathematics to explain in a Kantian way, how and to what extent, mathematics as we know it, is possible. It should be clear, however, that, as things stand at present, a philosophical theory of mathematics can in this respect, it seems, be little more than a declaration of faith or the lack of it.

We present a quite simple proof of the fixed point theorem for GL. We also use this proof to show that Sambin's algorithm yields a fixed point.

Improving on a result of Arana, we construct an effective family (φ r | r ∈ ℚ ⋂ [0, 1]) of Σ n -conservative Π n sentences, increasing in strength as r decreases, with the property that ¬φ p is Π n -conservative over PA + φ q whenever p < q. We also construct a family of Σ n sentences with properties as above except that the roles of Σ n and Π n are reversed. The latter result allows (...) to re-obtain an unpublished result of Solovay, the presence of a subset order-isomorphic to the reals in every non-trivial end-segment of every branch of the E-tree, and to generalize it to analogues of the E-tree at higher levels of the arithmetical hierarchy. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice (ZFC). This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively (...) pursued today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)