•  131
    This booklet is a Korean adaptation and translation of Part VIII of forall x: Calgary (Fall 2021 edition), which is intended to be introductory material for modal logic. The original text is based on Robert Trueman's A Modal Logic Primer, which is revised and expanded by Richard Zach and Aaron Thomas-Bolduc in forall x: Calgary. (forall x: Calgary is based on forall x: Cambridge by Tim Button, which is in turn based on forall x by P. D. Magnus, and also includes material from forall x: Lorain Co…Read more
  •  411
    The Genealogy of ‘∨’
    Review of Symbolic Logic 16 (3): 862-899. 2023.
    The use of the symbol ∨for disjunction in formal logic is ubiquitous. Where did it come from? The paper details the evolution of the symbol ∨ in its historical and logical context. Some sources say that disjunction in its use as connecting propositions or formulas was introduced by Peano; others suggest that it originated as an abbreviation of the Latin word for “or,” vel. We show that the origin of the symbol ∨ for disjunction can be traced to Whitehead and Russell’s pre-Principia work in forma…Read more
  •  4
    Cet ouvrage offre une introduction accessible à la théorie de la démonstration : il donne les détails des preuves et comporte de nombreux exemples et exercices pour faciliter la compréhension des lecteurs. Il est également conçu pour servir d’aide à la lecture des articles fondateurs de Gerhard Gentzen. L’ouvrage introduit également aux trois principaux formalismes en usage : l’approche axiomatique des preuves, la déduction naturelle et le calcul des séquents. Il donne une démonstration claire e…Read more
  •  15
    Corrections to: Natural Deduction for the Sheffer Stroke and Peirce’s Arrow
    Journal of Philosophical Logic 51 (3): 691-691. 2022.
    A Correction to this paper has been published: https://doi.org/10.1007/s10992-022-09665-5.
  •  413
    Epsilon theorems in intermediate logics
    Journal of Symbolic Logic 87 (2): 682-720. 2022.
    Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper…Read more
  •  65
    An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, includ…Read more
  •  322
    Epimorphism between Fine and Ferguson’s Matrices for Angell’s AC
    Logic and Logical Philosophy 32 (2): 161-179. 2023.
    Angell's logic of analytic containment AC has been shown to be characterized by a 9-valued matrix NC by Ferguson, and by a 16-valued matrix by Fine. We show that the former is the image of a surjective homomorphism from the latter, i.e., an epimorphic image. The epimorphism was found with the help of MUltlog, which also provides a tableau calculus for NC extended by quantifiers that generalize conjunction and disjunction.
  •  63
    forall x: Dortmund is an adaptation and German translation of forall x: Calgary. As such, it is a full-featured textbook on formal logic. It covers key notions of logic such as consequence and validity, the syntax of truth-functional (propositional) logic and truth-table semantics, the syntax of first-order (predicate) logic with identity and first-order interpretations, formalizing German in TFL and FOL, and Fitch-style natural deduction proof systems for both TFL and FOL. It also deals with so…Read more
  •  2093
    Para Todxs: Natal - uma introdução à lógica formal
    with P. D. Magnus, Tim Button, Robert Loftis, Robert Trueman, Aaron Thomas Bolduc, Daniel Durante, Maria da Paz Nunes de Medeiros, Ricardo Gentil de Araújo Pereira, Tiago de Oliveira Magalhães, Hudson Benevides, Jordão Cardoso, Paulo Benício de Andrade Guimarães, and Valdeniz da Silva Cruz Junior
    PPGFIL-UFRN. 2022.
    Livro-texto de introdução à lógica, com (mais do que) pitadas de filosofia da lógica, produzido como uma versão revista e ampliada do livro Forallx: Calgary. Trata-se da versão de 13 de outubro de 2022. Comentários, críticas, correções e sugestões são muito bem-vindos.
  •  59
    We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal sy…Read more
  •  22
    Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot’s free deduction. The elimination rules are “general,” but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules als…Read more
  •  1927
    A textbook for modal and other intensional logics based on the Open Logic Project. It covers normal modal logics, relational semantics, axiomatic and tableaux proof systems, intuitionistic logic, and counterfactual conditionals.
  •  508
    The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.
  •  2118
    forall x: Calgary is a full-featured textbook on formal logic. It covers key notions of logic such as consequence and validity of arguments, the syntax of truth-functional propositional logic TFL and truth-table semantics, the syntax of first-order (predicate) logic FOL with identity (first-order interpretations), symbolizing English in TFL and FOL, and Fitch-style natural deduction proof systems for both TFL and FOL. It also deals with some advanced topics such as modal logic, soundness, and fu…Read more
  •  1457
    Textbook on Gödel’s incompleteness theorems and computability theory, based on the Open Logic Project. Covers recursive function theory, arithmetization of syntax, the first and second incompleteness theorem, models of arithmetic, second-order logic, and the lambda calculus.
  •  1417
    An introductory textbook on metalogic. It covers naive set theory, first-order logic, sequent calculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. The audience is undergraduate students with some background in formal logic.
  •  251
    In Winter 2017, the first author piloted a course in formal logic in which we aimed to (a) improve student engagement and mastery of the content, and (b) reduce maths anxiety and its negative effects on student outcomes, by adopting student oriented teaching including peer instruction and classroom flipping techniques. The course implemented a partially flipped approach, and incorporated group-work and peer learning elements, while retaining some of the traditio…Read more
  •  468
    Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.
  •  445
    Proof Theory of Finite-valued Logics
    Dissertation, Technische Universität Wien. 1993.
    The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim …Read more
  •  921
    Rumfitt on truth-grounds, negation, and vagueness
    Philosophical Studies 175 (8): 2079-2089. 2018.
    In The Boundary Stones of Thought, Rumfitt defends classical logic against challenges from intuitionistic mathematics and vagueness, using a semantics of pre-topologies on possibilities, and a topological semantics on predicates, respectively. These semantics are suggestive but the characterizations of negation face difficulties that may undermine their usefulness in Rumfitt’s project.
  •  402
    Propositional logics in general, considered as a set of sentences, can be undecidable even if they have “nice” representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple—at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what …Read more
  •  296
    The problem of approximating a propositional calculus is to find many-valued logics which are sound for the calculus (i.e., all theorems of the calculus are tautologies) with as few tautologies as possible. This has potential applications for representing (computationally complex) logics used in AI by (computationally easy) many-valued logics. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of many-valued logics. It is shown that the optimal candid…Read more
  •  371
    Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Gödel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Gödel logics by Avron. It is shown that the system is sound an…Read more
  •  940
    Kurt Gödel, paper on the incompleteness theorems (1931)
    In Ivor Grattan-Guinness (ed.), Landmark Writings in Mathematics, North-holland. pp. 917-925. 2004.
    This chapter describes Kurt Gödel's paper on the incompleteness theorems. Gödel's incompleteness results are two of the most fundamental and important contributions to logic and the foundations of mathematics. It had been assumed that first-order number theory is complete in the sense that any sentence in the language of number theory would be either provable from the axioms or refutable. Gödel's first incompleteness theorem showed that this assumption was false: it states that there are sentenc…Read more
  •  812
    Kurt Gödel and Computability Theory
    In Arnold Beckmann, Ulrich Berger, Benedikt Löwe & John V. Tucker (eds.), Logical Approaches to Computational Barriers. Second Conference on Computability in Europe, CiE 2006, Swansea. Proceedings, Springer. pp. 575--583. 2006.
    Although Kurt Gödel does not figure prominently in the history of computabilty theory, he exerted a significant influence on some of the founders of the field, both through his published work and through personal interaction. In particular, Gödel’s 1931 paper on incompleteness and the methods developed therein were important for the early development of recursive function theory and the lambda calculus at the hands of Church, Kleene, and Rosser. Church and his students studied Gödel 1931, and Gö…Read more
  •  343
    All first-order Gödel logics G_V with globalization operator based on truth value sets V C [0,1] where 0 and 1 lie in the perfect kernel of V are axiomatized by Ciabattoni’s hypersequent calculus HGIF.
  •  359
    It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A , where the depth of proofs is linear in the number of variables in A .
  •  350
    Algorithmic Structuring of Cut-free Proofs
    In Börger Egon, Kleine Büning Hans, Jäger Gerhard, Martini Simone & Richter Michael M. (eds.), Computer Science Logic. CSL’92, San Miniato, Italy. Selected Papers, Springer. 1993.
    The problem of algorithmic structuring of proofs in the sequent calculi LK and LKB ( LK where blocks of quantifiers can be introduced in one step) is investigated, where a distinction is made between linear proofs and proofs in tree form. In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k-l-compressibility: "Given a proof of length k , and l ≤ k : Is there is a proof of length ≤ l ?"…Read more
  •  228
    Elimination of Cuts in First-order Finite-valued Logics
    with Matthias Baaz and Christian G. Fermüller
    Journal of Information Processing and Cybernetics EIK 29 (6): 333-355. 1993.
    A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.