Ignacio Jane has argued that second-order logic presupposes some amount of set theory and hence cannot legitimately be used in axiomatizing set theory. I focus here on his claim that the second-order formulation of the Axiom of Separation presupposes the character of the power set operation, thereby preventing a thorough study of the power set of infinite sets, a central part of set theory. In reply I argue that substantive issues often cannot be separated from a logic, but rather must (...) be presupposed. I call this the logic-metalogic link. There are two facets to the logic-metalogic link. First, when a logic is entangled with a substantive issue, the same position on that issue should be taken at the meta- level as at the object level; and second, if an expression has a clear meaning in natural language, then the corresponding concept can equally well be deployed in a formal language. The determinate nature of the power set operation is one such substantive issue in set theory. Whether there is a determinate power set of an infinite set can only be presupposed in set theory, not proved, so the use of second-order logic cannot be ruled out by virtue of presupposing one answer to this question. Moreover, the legitimacy of presupposing in the background logic that the power set of an infinite set is determinate is guaranteed by the clarity and definiteness of the notions of all and of subset. This is also exactly what is required for the same presupposition to be legitimately made in an axiomatic set theory, so the use of second-order logic in set theory rather than first-order logic does not require any new metatheoretic commitments. (shrink)

In this paper I dispute the current view that intuitionistic logic is the common basis for the three main trends of constructivism in the philosophy of mathematics: intuitionism, Russian constructivism and Bishop’s constructivism. The point is that the so-called ‘Markov’s principle’, which is accepted by Russian constructivists and rejected by the other two, is expressible in intuitionistic first-order logic, and so it appears to have the status of a logical principle. The result of appending this principle to a complete intuitionistic (...) axiom system for first-order predicate logic constitutes a new logic, which could well be called ‘Markov’s logic’, and which should be regarded as the true logical system underlying Russian constructivism. (shrink)

We introduce a general notion of semantic structure for first-order theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo–Fraenkel set theory, the completeness of such semantics is equivalent to the Boolean prime ideal theorem. Using a result of McCarty, we conclude that the completeness of Kripke semantics is equivalent, over intuitionistic Zermelo–Fraenkel set theory, to the Law of Excluded Middle plus BPI. Along the way, we also prove the equivalence, over ZF, between (...) BPI and the completeness theorem for Kripke semantics for both first-order and propositional theories. (shrink)

We introduce a notion of the Kripke model for classical logic for which we constructively prove the soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.