Eliminating definitions and Skolem functions in first-order logic

Abstract
When working with a first-order theory, it is often convenient to use definitions. That is, if ϕ(x) is a first-order formula with the free variables shown, one can introduce a new relation symbol R to abbreviate ϕ, with defining axiom ∀x (R(x) ↔ ϕ(x)). Of course, this definition can later be eliminated from a proof, simply by replacing every instance of R by ϕ. But suppose the proof involves nested definitions, with a sequence of relation symbols R0, . . . , Rk abbreviating formulae ϕ0, . . . , ϕk, where each ϕi may have multiple occurrences of R0, . . . , Ri−1. In that case, the naive elimination procedure described above can yield an exponential increase in the length of the proof. In Section 2, I show that if the underlying theory proves that there are at least two elements in the universe, a more careful translation allows one to eliminate the new definitions with at most a polynomial increase in length. In fact, I will describe an explicit algorithm that can be implemented in polynomial time. The proof is not difficult, but it relies on the assumption that equality is included in the logic. A similar trick has been used by Solovay in simulating iterated definitions efficiently, as discussed in Section 3.2 of [Pudl´ak 1998]. Consequently, the result proved here may be folklore, but to my knowledge it has not appeared in the literature, and it is needed in Section 3. It is also sometimes convenient, in a first-order setting, to introduce Skolem func-.
Keywords No keywords specified (fix it)
Categories No categories specified
(categorize this paper)
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index Translate to english
 
Download options
PhilPapers Archive


Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 9,360
External links
  •   Try with proxy.
  • Through your library Only published papers are available at libraries
    References found in this work BETA

    No references found.

    Citations of this work BETA

    No citations found.

    Similar books and articles
    Analytics

    Monthly downloads

    Added to index

    2010-12-22

    Total downloads

    6 ( #162,933 of 1,089,055 )

    Recent downloads (6 months)

    5 ( #20,075 of 1,089,055 )

    How can I increase my downloads?

    My notes
    Sign in to use this feature


    Discussion
    Start a new thread
    Order:
    There  are no threads in this forum
    Nothing in this forum yet.