Eliminating definitions and Skolem functions in first-order logic
| Abstract | From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,711 |
| External links |
  Try with proxy. Try with proxy. Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesFernando Ferreira (1994). A Feasible Theory for Analysis. Journal of Symbolic Logic 59 (3):1001-1011.
Klaus Aehlig (2005). Induction and Inductive Definitions in Fragments of Second Order Arithmetic. Journal of Symbolic Logic 70 (4):1087 - 1107.
Dale A. Miller (1987). A Compact Representation of Proofs. Studia Logica 46 (4):347 - 370.
Thomas Strahm (1997). Polynomial Time Operations in Explicit Mathematics. Journal of Symbolic Logic 62 (2):575-594.
Jaakko Hintikka (1998). Truth Definitions, Skolem Functions and Axiomatic Set Theory. Bulletin of Symbolic Logic 4 (3):303-337.
Paulo A. S. Veloso & Sheila R. M. Veloso (2004). On Ultrafilter Logic and Special Functions. Studia Logica 78 (3):459 - 477.
Shmuel Lifsches & Saharon Shelah (1998). Uniformization and Skolem Functions in the Class of Trees. Journal of Symbolic Logic 63 (1):103-127.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads15 ( #78,782 of 551,625 )Recent downloads (6 months)2 ( #37,370 of 551,625 )How can I increase my downloads? |
My notes
Discussion
