Start / Iowa Type Theory Commute / Different proof systems distinguishing logical rules from domain axioms

Different proof systems, distinguishing logical rules from domain axioms

12 min • 2 september 2021

I highlight two basic points in this continuing warm-up to proof theory: there are different proof systems for the same logics, and it is customary to separate purely logical rules (dealing with propositional connectives and quantifiers, for example) from rules or axioms for some particular domain (like axioms about arithmetic, or whatever domain is of interest).