David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 46 (4):347 - 370 (1987)
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)|
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
Raymond M. Smullyan (1968). First-Order Logic. New York [Etc.]Springer-Verlag.
Gerhard Gentzen (1969). The Collected Papers of Gerhard Gentzen. Amsterdam, North-Holland Pub. Co..
Alonzo Church (1940). A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5 (2):56-68.
Dag Prawitz (1968). Hauptsatz for Higher Order Logic. Journal of Symbolic Logic 33 (3):452-457.
William Craig (1957). Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. Journal of Symbolic Logic 22 (3):250-268.
Citations of this work BETA
Willem Heijltjes (2010). Classical Proof Forestry. Annals of Pure and Applied Logic 161 (11):1346-1366.
Matthias Baaz, Stefan Hetzl & Daniel Weller (2012). On the Complexity of Proof Deskolemization. Journal of Symbolic Logic 77 (2):669-686.
Stefan Hetzl (2010). On the Form of Witness Terms. Archive for Mathematical Logic 49 (5):529-554.
Stefan Hetzl, Alexander Leitsch & Daniel Weller (2011). CERES in Higher-Order Logic. Annals of Pure and Applied Logic 162 (12):1001-1034.
Richard McKinley (2013). Canonical Proof Nets for Classical Logic. Annals of Pure and Applied Logic 164 (6):702-732.
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 downloads18 ( #226,745 of 1,937,419 )
Recent downloads (6 months)1 ( #456,797 of 1,937,419 )
How can I increase my downloads?