You are here

Inference with quantifiers

18 March, 2015 - 11:51
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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.