The challenge The authoring platform of choice in many math-heavy disciplines is LaTeX. It produces typeset documents of excellent quality and handles formulas and mathematical diagrams extremely well. Practically every researcher or instructor in mathematics, physics, and computer science is adept at using it, and it has a wide user base outside these core disciplines … Continue reading…
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.
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
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: I just ran LaTeXML on the forall … Continue reading Converting LaTeX to HTML: technical notes
I’m happy to report that forall x: Calgary is now available in an HTML version for reading online. It turned […]
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
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…
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…
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 ……
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 ‘∨’