# MUltseq 2.0

MUltseq is a sequent theorem prover for arbitrary finite-valued logics. It was developed over 20 years ago by Àngel Gil and Gernot Salzer. Version 2.0 was presented today at TACL 2024 in Barcelona. I also updated MUltlog to v1.7, which includes a script to generate sequent calculus rules for use with MUltseq.

# W. W. Tait, 1929–2024

The eminent proof theorist and philosopher of mathematics William Walker ("Bill") Tait died March 15, 2024 in Chicago. He was 95. Bill was born on January 22, 1929, in Freeport, NY, and received a BA from Lehigh University in 1952 where he was taught by Adolph Grünbaum. He undertook graduate studies in philosophy (1952–54) and … Continue reading W. W. Tait, 1929–2024

# Converting LaTeX to HTML: technical notes

I just posted on the OLP that forall x: Calgary now has an HTML version for reading online. Here are some technical notes in case that's helpful for anyone. First, LaTeX to HTML conversion has long been tricky. No solution is perfect. There are basically three workable approaches: Assume that your LaTeX code is basically … Continue reading Converting LaTeX to HTML: technical notes

# Sheffer stroke before Sheffer: Edward Stamm

It came up in discussion at the Formal Turn conference the other day, so I thought I'd preserve an old Twitter thread here: The first person to publish results on NAND and NOR (Sheffer stroke and Peirce arrow) was the Polish mathematician and Philosopher Edward Stamm (1886–1940). The publication was "Beitrag zur Algebra der Logik … Continue reading Sheffer stroke before Sheffer: Edward Stamm

# Introduction à la théorie de la démonstration: Élimination des coupures, normalisation et preuves de cohérence

Mancosu, Paolo, Sergio Galvan, and Richard Zach. 2022. Introduction à la théorie de la démonstration: Élimination des coupures, normalisation et preuves de cohérence. Paris: Vrin. Traduction française de An Introduction to Proof Theory. Cet ouvrage offre une introduction accessible à la théorie de la démonstration : il donne les détails des preuves et comporte de nombreux … Continue reading Introduction à la théorie de la démonstration: Élimination des coupures, normalisation et preuves de cohérence

# An epimorphism between Fine and Ferguson’s matrices for Angell’s AC

Zach, Richard. 2022. “An Epimorphism Between Fine and Ferguson’s Matrices for Angell’s AC.” Logic and Logical Philosophy, Forthcoming, 1–19. https://doi.org/10.12775/LLP.2022.025. 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. It is shown that the former is the image … Continue reading An epimorphism between Fine and Ferguson’s matrices for Angell’s AC

# Epsilon theorems in intermediate logics

Baaz, Matthias, and Richard Zach. 2022. Epsilon theorems in intermediate logics. The Journal of Symbolic Logic 87(2), pp. 682–720. DOI: 10.1017/jsl.2021.103. Open access. Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this … Continue reading Epsilon theorems in intermediate logics

# The genealogy of ‘∨’

Elkind, Landon D. C., and Richard Zach. 2022. The Genealogy of ‘∨.’ The Review of Symbolic Logic, 1–38. DOI: 10.1017/S1755020321000587. forthcoming 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 … Continue reading The genealogy of ‘∨’

# Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D

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 systems only differ in the presence or absence of external structural rules. With the exception of S5, the systems are modular in the sense that different structural rules capture different properties of the accessibility relation. We provide the first direct semantical cut-free completeness proofs for K, T, and D, and show how this method fails in the case of B and S4.

# Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi

Zach, Richard. 2021. “Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi.” The Review of Symbolic Logic 14 (3): 645–86. doi:10.1017/S1755020320000015. 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 … Continue reading Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi

# An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs

Paolo Mancosu, Sergio Galvan, and Richard Zach. An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs. Oxford: Oxford University Press, 2021. DOI: 10.1093/oso/9780192895936.001.0001 Published in the UK on August 17, 2021. Available in hardcover and paperback. An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details worked out … Continue reading An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs

# New details on why Tarski was reluctant to leave Poland before WWII

Paolo Mancosu has a new paper out in the Journal of Humanistic Mathematics: This article makes available some early letters chronicling the relationship between the biologist Joseph H. Woodger and the logician Alfred Tarski. Using twenty-five unpublished letters from Tarski to Woodger preserved in the Woodger Papers at University College, London, I reconstruct their relationship … Continue reading New details on why Tarski was reluctant to leave Poland before WWII

# Updates to OLP for Fall 2021 edition of Sets, Logic, Computation

In preparation for the Fall 2021 edition of Sets, Logic, Computation, the material in the Open Logic Project has seen […]

# Famous logicians and their inconsistent theories

A couple of days ago, Daniel Litt linked to Patrick Brosnan's computer-verified "proof" of the inconsistency of Peano arithmetic. The proof is correct; I just put it in quotes because it relies on a quirk of the proof verification system used (Metamath), which requires you to explicitly prohibit certain variable substitutions. The axiom of PA … Continue reading Famous logicians and their inconsistent theories

# forall x: Calgary goes international (and other updates)

ICYMI, forall x: Calgary has been translated into German and Portuguese! forall x: Dortmund by Simon Wimmer is the German […]

# Learning Outcomes and Grade Specifications in a Formal Logic Course

Zach, Richard. 2021. “Learning Outcomes and Grade Specifications in a Formal Logic Course.” Poster presentation presented at the Mastery Grading University Conference 2021, Online, June 11. https://drive.google.com/file/d/1q6rAyXfrz2k79NtaHoMREQ9IDagnbvLN/view. Formal logic is a staple of undergraduate philosophy departments. Courses are typically run as straight lectures, with problem sets and exams. I will describe a design for such … Continue reading Learning Outcomes and Grade Specifications in a Formal Logic Course

# MUltlog 1.13 released

MUltlog is a Prolog program that converts a specification of a finite-valued logic (propositional or first-order) into optimal inference rules for a number of related analytic proof systems: many-sided sequent calculus, signed tableaux, many-sided natural deduction, and clause translation calculi for signed resolution. The specification of the logic can be produced by a simple TCL/TK … Continue reading MUltlog 1.13 released

# Teaching Logic Online: Report

Well, my intro to formal logic (Logic I) course is in the can. I think it was a success! I could not have done it without Graham Leach-Krouse's Carnap system, and my excellent team (Husna Farooqui, Sarah Hatcher, Hannah O'Riain, and Dvij Raval). A while back I wrote about the plan to implement specification based … Continue reading Teaching Logic Online: Report

# Many-valued logic in the OLP

We have four new chapters in the OLP. They contain draft material on many-valued logics. The Introduction explains their syntax […]

# Fall 2020 edition of forall x: Calgary

The Fall 2020 edition of forall x: Calgary is now available. The changes are: some behind-the-scenes reorganization of the files […]