Satisfiability or Sat\ is the metatheoretic statementEvery formally intuitionistically consistent set of first-order sentences has a model.The models in question are the Tarskian relational structures familiar from standard first-order model theory, but here treated within intuitionistic metamathematics. We prove that both IZF, intuitionistic Zermelo–Fraenkel set theory, and HAS, second-order Heyting arithmetic, prove Sat\ to be false outright. Following the lead of Carter :75–95, 2008), we then generalize this result to some provably intermediate first-order logics, including the Rose logic. These metatheorems (...) distinguish the intuitionistic foundational significance of Sat\ sharply from that of Sat\, the satisfiability claim for intuitionistic propositional logic. At the same time, they establish intuitionistic connections with and between Test, COMP\, and \. Here, Test is the scheme of Testability, and COMP\ and \ are completeness for intuitionistic propositional logic and predicate logic, respectively. (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)

It is known that the set of intermediate propositional logics that can prove their own completeness theorems is exactly those which prove every instance of the principle of testability, ¬ϕ ∨ ¬¬ϕ. Such logics are called reflexive. This paper classifies reflexive intermediate logics in the first-order case: a first-order logic is reflexive if and only if it proves every instance of the principle of double negation shift and the metatheory created from it proves every instance of the principle of testability.