Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-18T03:50:01.776Z Has data issue: false hasContentIssue false

ON THE NOTION OF CANONICAL DERIVATIONS FROM OPEN ASSUMPTIONS AND ITS ROLE IN PROOF-THEORETIC SEMANTICS

Published online by Cambridge University Press:  20 March 2015

NISSIM FRANCEZ*
Affiliation:
Computer Science Department, Technion-IIT
*
*COMPUTER SCIENCE DEPARTMENT, TECHNION-IIT, HAIFA, ISRAEL E-mail:francez@cs.technion.ac.il

Abstract

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Davies, R., & Pfenning, F. (2001). A modal analysis of staged computation. Journal of the ACM, 48(3), 555604.Google Scholar
Došen, K., & Schroeder-Heister, P. (1988). Uniqueness, definability and interpolation. Journal of Symbolic Logic, 53, 554570.Google Scholar
Dummett, M. (1993). The Logical Basis of Metaphysics. Cambridge, MA: Harvard University Press. 1993 (Paperback). 1991 (Hard copy).Google Scholar
Francez, N. (2014). Views of proof-theoretic semantics: Reified proof-theoretic meanings. Journal of Computational Logic. Special issue in honour of Roy Dyckhoff. doi:10.1093/logcom/exu035.Google Scholar
Francez, N., & Ben-Avi, G. (2011). Proof-theoretic semantic values for logical operators. Review of symbolic logic, 4(3), 337485.Google Scholar
Francez, N., & Dyckhoff, R. (2012). A note on harmony. Journal of Philosophical Logic, 41(3), 613628.Google Scholar
Hălnass, L., & Schroeder-Heister, P. (1990). A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation, 1, 261283.Google Scholar
Hălnass, L., & Schroeder-Heister, P. (1991). A proof-theoretic approach to logic programming. II. Programs as definitions. Journal of Logic and Computation, 1, 635660.Google Scholar
Kürbis, N. (2012). How fundamental is the fundamental assumption? Teorema, XXXI(2), 519.Google Scholar
Pfenning, F., & Davies, R. (2001). A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11, 511540.CrossRefGoogle Scholar
Prawitz, D. (2006). Meaning approached via proofs. Synthese, 148, 507524.Google Scholar
Prior, A. N. (1960). The runabout inference-ticket. Analysis, 21, 3839.CrossRefGoogle Scholar
Read, S. (2010). General-elimination harmony and the meaning of the logical constants. Journal of philosophic logic, 39, 557576.Google Scholar
Read, S. (2015). General elimination harmony and higher-level rules. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Studia Logica Outstanding Contributions to Logic Series. Springer-Verlag, pp. 293312.Google Scholar
Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of symbolic logic, 49, 12841300.Google Scholar
Schroeder-Heister, P. (2006). Validity concepts in proof-theoretic semantics. In Kahle, R. and Schroeder-Heister, P., editors. Proof-theoretic semantics. Special Issue of Synthese, 148, 525571.Google Scholar
Schroeder-Heister, P. (2008). Proof-theoretic versus model-theoretic consequence. In Perlis, M., editor. The Logica 2007 Yearbook, pp. 187200. Prague: Filosofia.Google Scholar
Schroeder-Heister, P. (2012). The categorical and the hypothetical: A critique of some fundamental assumptions of standard semantics. Synthese, 187(3), 925942.Google Scholar
Schroeder-Heister, P. (2015). Harmony in proof-theoretic semantics: A reductive analysis. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Studia Logica Outstanding Contributions to Logic Series. Springer-Verlag, pp. 329358.CrossRefGoogle Scholar
Tennant, N. (2002). Ultimate normal forms for parallelized natural deduction. Journal of IGPL, 10(3), 299337.Google Scholar
von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541567.Google Scholar
von Plato, J. (2003). Translations from natural deduction to sequent calculus. Mathematical Logic Quarterly, 49, 435443.CrossRefGoogle Scholar