First Order Theories

Abstract

The logic we have been considering in this book is commonly known as first-order predicate logic, or just simply first-order logic. We have developed a system of natural deduction in order that we may draw valid conclusions from a set of premisses in first order logic. One notion we have not looked at so far, however, is that of identity, also known as equality. In this section we shall introduce this notion and define it by extending our rules of deduction to include introduction and elimination rules for identity. The resulting logic is thus known as first order logic with identity or as first order logic with equality.