Proving first-order sentences with inference rules is not too different than for propositional ones. We have two slight twists to add: upgrading propositions to relations, and quantifiers. We still keep all our Propositional inference rules, but declare they can now be used on first-order WFFs. For our quantifiers, we introduce new First-order inference rule for adding and eliminating quantifiers from formulas. These four new rules look surprisingly simple, but they do have a couple of subtleties we have to keep track of.
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://email@example.com