We show that, if a suitable intuitionistic metatheory proves that consistency implies satisfiability for subfinite sets of propositional formulas relative either to standard structures or to Kripke models, then that metatheory also proves every negative instance of every classical propositional tautology. Since reasonable intuitionistic set theories such as HAS or IZF do not demonstrate all such negative instances, these theories cannot prove completeness for intuitionistic propositional logic in the present sense.

In 1957, Gödel proved that completeness for intuitionistic predicate logic HPL implies forms of Markov's Principle, MP. The result first appeared, with Kreisel's refinements and elaborations, in Kreisel. Featuring large in the Gödel-Kreisel proofs are applications of the axiom of dependent choice, DC. Also in play is a form of Herbrand's Theorem, one allowing a reduction of HPL derivations for negated prenex formulae to derivations of negations of conjunctions of suitable instances. First, we here show how to deduce Gödel's results (...) by alternative means, ones arguably more elementary than those of Kreisel. We avoid DC and Herbrand's Theorem by marshalling simple facts about negative translations and Markov's Rule. Second, the theorems of Gödel and Kreisel are commonly interpreted as demonstrating the unprovability of completeness for HPL, if means of proof are confined within strictly intuitionistic metamathematics. In the closing section, we assay some doubts about such interpretations. (shrink)

This chapter presents and illustrates fundamental principles of the intuitionistic mathematics devised by L.E.J. Brouwer and then describes in largely nontechnical terms metamathematical results that shed light on the logical character of that mathematics. The fundamental principles, such as Uniformity and Brouwer’s Theorem, are drawn from the intuitionistic studies of logic and topology. The metamathematical results include Gödel’s negative and modal translations and Kleene’s realizability interpretation. The chapter closes with an assessment of anti-realism as a philosophy of intuitionism.

Let S be a deductive system such that S-derivability (⊦s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and ⊦s, it follows constructively that the K-completeness of ⊦s implies MP(S), a form of Markov's Principle. If ⊦s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if ⊦s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when ⊦s is many-one (...) complete, MP(S) implies the usual Markov's Principle MP. An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implies MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP. These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Godel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article. (shrink)

The historical antecedents of Frege's treatment of binocular vision in "The thought" were the physiological writings of Johannes Mueller, Hermann von Helmholtz, and Emil du Bois-Reymond. In their research on human vision, logic was assigned an unexpected role: it was to be the means by which knowledge of a world extended in three dimensions arises from stimuli that are at best two-dimensional. An examination of this literature yields a richer understanding of Frege's insistence that a proper epistemology requires us to (...) recognize the existence and importance of nonsensible sources of knowledge. (shrink)