Studia Logica 46 (4):347 - 370 (1987)
|Abstract||A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which represents proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
J. B. Kennedy (1995). On the Empirical Foundations of the Quantum No-Signalling Proofs. Philosophy of Science 62 (4):543-560.
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.
John W. Dawson Jr (2006). Why Do Mathematicians Re-Prove Theorems? Philosophia Mathematica 14 (3):269-286.
Uwe Egly (2001). On Different Intuitionistic Calculi and Embeddings From Int to S. Studia Logica 69 (2):249-277.
Frederic D. Portoraro (1998). Strategic Construction of Fitch-Style Proofs. Studia Logica 60 (1):45-66.
Paolo Gentilini (1993). Syntactical Results on the Arithmetical Completeness of Modal Logic. Studia Logica 52 (4):549 - 564.
Jan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. Journal of Symbolic Logic 62 (2):457-486.
George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.
Added to index2009-01-28
Total downloads2 ( #246,081 of 722,873 )
Recent downloads (6 months)1 ( #60,917 of 722,873 )
How can I increase my downloads?