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.
Uncategorized
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
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 […]
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 […]
Grading for Mastery in Introductory Logic
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
Satisfaction and assignments
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
Letter grades in Brightspace/D2L (or other LMS)
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)
Need a logic course, fast?
I wasn't going to put this online until it was done and cleaned up, but given the situation, maybe this can be of help. I just developed and tried out a course on formal logic for a 13-week semester. It has: a free online textbook: forall x: Calgarybeamer slides for lectures (or screencasts)problem sets, which … Continue reading Need a logic course, fast?
Chalk-and-talk online: whiteboard screencasting (on Linux)
Well, all my logic lectures moved online as of last week. It's been a bit of a scramble, as I'm sure it's been for you as well. I needed to rapidly produce videos of lectures (on logic in my case) I can give with students to watch. I thought I'd quickly share what I'm doing … Continue reading Chalk-and-talk online: whiteboard screencasting (on Linux)
Adding online exercises with automated grading to any logic course with Carnap
A couple of years ago I posted a roundup of interactive logic courseware with an automatic grading component. The favorite commercial solution is Barwise & Etchemendy's Language, Proof, and Logic textbook that comes with software for doing truth tables, natural deduction proofs, and semantics for propositional and first-order logic, which also automatically grades student's solutions. … Continue reading Adding online exercises with automated grading to any logic course with Carnap
BibTeX-friendly PDF management with Zotero
For years I've been jealous of colleagues with Macs who apparently all use BibDesk for managing their article PDF collections and BibTeX citations in one nice program. I think I've finally figured out how to do both things on Linux: Zotero, with the Better BibTeX and ZotFile add-ons. Zotero is first of all a citation … Continue reading BibTeX-friendly PDF management with Zotero
The Emergence of First-Order Logic
The SEP entry on "The Emergence of First-Order Logic" by William Ewald is out today.
Indian Conference on Logic and its Applications 2019
The Association for Logic in India (ALI) announces the eighth edition of its biennial International Conference on Logic and its Applications (ICLA), to be held at the Indian Institute of Technology Delhi from March 3 to 5, 2019. ICLA is a forum for bringing together researchers from a wide variety of fields in which formal logic … Continue reading Indian Conference on Logic and its Applications 2019