A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 52 (2):197 - 232 (1993)
There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a framework for presenting proofs in SL based on a partial backward translation of proofs obtained in a familiar TL: Order-Sorted Predicate Logic. The proposed backward translation transfers some formulasF TL belonging to the proof in TL into formulasF SL , such that the formulasF SL either (a) belong to a corresponding deduction in SL (in the best case) or, (b) are semantically related in some precise way, to formulas in the corresponding deduction in SL (in the worst case). The formulasF TL andF SL can obviously be considered aslemmas of their respective proofs. Therefore the transfer of lemmas of TL gives at least a skeleton of the corresponding proof in SL. Since the formulas of a proof keep trace of the strategy used to obtain the proof, clearly the framework can also help in solving another fundamental and difficult problem:the transfer of strategies from classical to non classical logics. We show how to apply the proposed framework, at least to S5, S4(p), K, T, K4. Two conjectures are stated and we propose sufficient (and in general satisfactory) conditions in order to obtain formulas in the proof in SL. Two particular cases of the conjectures are proved to be theorems. Three examples are treated in full detail. The main lines of future research are given.
|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
Melvin Fitting (1985). Proof Methods for Modal and Intuitionistic Logics. Journal of Symbolic Logic 50 (3):855-856.
R. I. Goldblatt (1975). First-Order Definability in Modal Logic. Journal of Symbolic Logic 40 (1):35-40.
Citations of this work BETA
No citations found.
Similar books and articles
Wilfried Sieg & John Byrnes (1998). Normal Natural Deduction Proofs (in Classical Logic). Studia Logica 60 (1):67-106.
Ken-etsu Fujita (1998). On Proof Terms and Embeddings of Classical Substructural Logics. Studia Logica 61 (2):199-221.
Luca Viganò (2000). Labelled Non-Classical Logics. Kluwer Academic Publishers.
Greg Restall (forthcoming). Substructural Logics. Stanford Encyclopedia of Philosophy.
David Basin, Seán Matthews & Luca Viganò (1998). Natural Deduction for Non-Classical Logics. Studia Logica 60 (1):119-160.
Added to index2009-01-28
Total downloads7 ( #441,289 of 1,911,917 )
Recent downloads (6 months)1 ( #459,829 of 1,911,917 )
How can I increase my downloads?