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
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
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
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
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 ‘∨’
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.
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
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
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
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 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
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
I've been thinking for a long time about how to do assignments, exams, and grading differently in my intro logic course. Provincial budget cuts mean my enrolment will double to 200 students in the Fall term, and the fact that it will have to be fully online raises additional challenges. So maybe now is a … Continue reading Grading for Mastery in Introductory Logic
When you define satisfaction for quantified formulas, e.g., \(\forall x\, A\), you have to have a way to make \(x\) range over all elements of the domain. Here are the common options: A. Tarski-style: use variable assignments \(s\colon V \to D\) (where \(V\) is the set of variables and \(D\) the domain), then define \[\mathfrak{M}, … Continue reading Satisfaction and assignments
So, we're all moving to online courses, and for some of us that means we have to figure out how to switch from scribbling feedback and letter grades on papers, handing them back to students, and turning those letter grades into a course grade at the end. Most of us are using learning management systems … Continue reading Letter grades in Brightspace/D2L (or other LMS)
