Jean van Heijenoort was best known for his editorial work in the history of mathematical logic. I survey his contributions to model-theoretic proof theory, and in particular to the falsifiability tree method. This work of van Heijenoort’s is not widely known, and much of it remains unpublished. A complete list of van Heijenoort’s unpublished writings on tableaux methods and related work in proof theory is appended.

Which intermediate propositional logics can prove their own completeness? I call a logic reflexive if a second-order metatheory of arithmetic created from the logic is sufficient to prove the completeness of the original logic. Given the collection of intermediate propositional logics, I prove that the reflexive logics are exactly those that are at least as strong as testability logic, that is, intuitionistic logic plus the scheme $\neg φ ∨ \neg\neg φ. I show that this result holds regardless of whether Tarskian (...) or Kripke semantics is used in the definition of completeness. I also show that the operation of creating a second-order metatheory is injective, thereby insuring that I am actually considering each logic independently. (shrink)

There are two different ways to introduce the notion of truthin constructive mathematics. The first one is to use a Tarskian definition of truth in aconstructive (meta)language. According to some authors, (Kreisel, van Dalen, Troelstra ... ),this definition is entirely similar to the Tarskian definition of classical truth (thesis A).The second one, due essentially to Heyting and Kolmogorov, and known as theBrouwer–Heyting–Kolmogorov interpretation, is to explain informally what it means fora mathematical proposition to be constructively proved. According to other authors (...) (Martin-Löfand Shapiro), this interpretation and the Tarskian definition of truth amount to thesame (thesis B). My aim in this paper is to show that thesis A is only reasonable, that thesis Bis false and to answer the following question: what is defined by the Tarskian definition ofconstructive truth? (shrink)

We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a _meta_-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the (...) object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth’s clause for disjunction instead of Kripke’s). It is this complexity that motivates us to use BI as a case-study for this approach to semantics. (shrink)

In order to prove the validity of logical rules, one has to assume these rules in the metalogic. However, rule-circular ‘justifications’ are demonstrably without epistemic value. Is a non-circular justification of a logical system possible? This question attains particular importance in view of lasting controversies about classical versus non-classical logics. In this paper the question is answered positively, based on meaning-preserving translations between logical systems. It is demonstrated that major systems of non-classical logic, including multi-valued, paraconsistent, intuitionistic and quantum logics, (...) can be translated into classical logic by introducing additional intensional operators into the language. Based on this result it is argued that classical logic is representationally optimal. In sec. 6 it is investigated whether non-classical logics can be likewise representationally optimal. The answer is predominantly negative but partially positive. Nevertheless the situation is not symmetric, because classical logic has important ceteris paribus advantages as a unifying metalogic. (shrink)

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)

In Sect. 1 it is argued that systems of logic are exceptional, but not a priori necessary. Logics are exceptional because they can neither be demonstrated as valid nor be confirmed by observation without entering a circle, and their motivation based on intuition is unreliable. On the other hand, logics do not express a priori necessities of thinking because alternative non-classical logics have been developed. Section 2 reflects the controversies about four major kinds of non-classical logics—multi-valued, intuitionistic, paraconsistent and quantum (...) logics. Its purpose is to show that there is no particular domain or reason that demands the use of a non-classical logic; the particular reasons given for the non-classical logic can also be handled within classical logic. The result of Sect. 2 is substantiated in Sect. 3, where it is shown (referring to other work) that all four kinds of non-classical logics can be translated into classical logic in a meaning-preserving way. Based on this fact a justification of classical logic is developed in Sect. 4 that is based on its representational optimality. It is pointed out that not many but a few non-classical logics can be likewise representationally optimal. However, the situation is not symmetric: classical logic has ceteris paribus advantages as a unifying metalogic, while non-classical logics can have local simplicity advantages. (shrink)