Unfortunately, I didn’t think of the title myself. It’s the title of one of the workshops at the Calgary Folk Festival, one where a bunch of artists play together, usually with an emphasis on the words (I haven’t been, so I really don’t know what they’re like, but a few years ago they had Jane Siberry, Buck 65, and Friends of Dean Martinez, and that must have been amazing). Anyway, it would make a great title for a paper on proof speed-up, or for a proof theory or automated deduction conference t-shirt.
And just to put some actual logic into this post, I’ll tell you about a weapon of fast deduction: The schema of equivalence is
(Eq) (A ↔ B) → (C(A) ↔ C(B))
(where A, B, C are propositional formulas and C(A) means C with the variable X replaced everywhere by A). Add this to a complete Hilbert-type system for propositional logic, and you can prove all propositional tautologies with n variables in number of steps linear in n. Without Eq, you can’t do this.
- Matthias Baaz and Richard Zach, Short proofs of tautologies using the schema of equivalence. Computer Science Logic. 7th Workshop, CSL’93. Swansea. Selected Papers (Springer, Berlin, 1994) 33-35
Leave a Reply to Anonymous Cancel reply