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
(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