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
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
forall x now in HTML for extra accessibility
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
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
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