David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
When working with a ﬁrst-order theory, it is often convenient to use deﬁnitions. That is, if ϕ(x) is a ﬁrst-order formula with the free variables shown, one can introduce a new relation symbol R to abbreviate ϕ, with deﬁning axiom ∀x (R(x) ↔ ϕ(x)). Of course, this deﬁnition can later be eliminated from a proof, simply by replacing every instance of R by ϕ. But suppose the proof involves nested deﬁnitions, 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 deﬁnitions 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 diﬃcult, but it relies on the assumption that equality is included in the logic. A similar trick has been used by Solovay in simulating iterated deﬁnitions eﬃciently, 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 ﬁrst-order setting, to introduce Skolem func-.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Melvin Fitting (2002). Interpolation for First Order S5. Journal of Symbolic Logic 67 (2):621-634.
Robin Hirsch, Ian Hodkinson & Roger D. Maddux (2002). Provability with Finitely Many Variables. Bulletin of Symbolic Logic 8 (3):348-379.
Melvin Fitting (2012). Barcan Both Ways. Journal of Applied Non-Classical Logics 9 (2-3):329-344.
G. Aldo Antonelli (1992). Revision Rules: An Investigation Into Non-Monotonic Inductive Deﬁnitions. Dissertation, University of Pittsburgh
W. W. Tait (2003). The Completeness of Heyting First-Order Logic. Journal of Symbolic Logic 68 (3):751-763.
Jan Von Plato (2007). In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs. Bulletin of Symbolic Logic 13 (2):189-225.
Added to index2010-12-22
Total downloads11 ( #290,080 of 1,789,728 )
Recent downloads (6 months)3 ( #261,181 of 1,789,728 )
How can I increase my downloads?