Weapons of Fast Deduction

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) (AB) → (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.

2 thoughts on “Weapons of Fast Deduction

  1. If instead of a schema you have a formula with propositional quantifiers which universally bind all propositional variables and the s/s-type variable you have a version of Lesniewski’s axiom of extensionality in protothetic (dating back to something like 1921 or 1923), which not only shortens proofs but also allows one to prove new stuff.

Leave a Reply

Your email address will not be published. Required fields are marked *