Show simple item record

Comparing Sense and Denotation in Bilateralist Proof Systems for Proofs and Refutations

dc.contributor.authorAyhan, Sara
dc.date.accessioned2025-11-19T14:27:55Z
dc.date.available2025-11-19T14:27:55Z
dc.date.issued2025-05-30
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/56722
dc.description.abstractIn this paper a framework to distinguish in a Fregean manner between sense and denotation of \(\lambda\)-term-annotated derivations will be applied to a bilateralist sequent calculus displaying two derivability relations, one for proving and one for refuting. Therefore, a two-sorted typed \(\lambda\)-calculus will be used to annotate this calculus and a Dualization Theorem will be given, stating that for any derivable sequent expressing a proof, there is also a derivable sequent expressing a refutation and vice versa. By having joint \(\lambda\)-term annotations for proof systems in natural deduction and sequent calculus style, a comparison with respect to sense and denotation between derivations in those systems will be feasible, since the annotations elucidate the structural correspondences of the respective derivations. Thus, we will have a basis for determining in which cases, firstly, derivations expressing a proof vs. derivations expressing a refutation and, secondly, derivations in natural deduction vs. in sequent calculus can be identified and on which level.en
dc.language.isoen
dc.publisherWydawnictwo Uniwersytetu Łódzkiegopl
dc.relation.ispartofseriesBulletin of the Section of Logic;1en
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0
dc.subjectproof-theoretic semanticsen
dc.subjectbilateralismen
dc.subjectbi-intuitionistic logicen
dc.subjectmeaning of proofsen
dc.subjectproof identityen
dc.subjectrefutationsen
dc.titleComparing Sense and Denotation in Bilateralist Proof Systems for Proofs and Refutationsen
dc.typeArticle
dc.page.number23-58
dc.contributor.authorAffiliationRuhr University Bochum, Institute of Philosophy Ien
dc.identifier.eissn2449-836X
dc.referencesS. Ayhan, Uniqueness of Logical Connectives in a Bilateralist Setting, [in:] M. Blicha, I. Sedlár (eds.), The Logica Yearbook 2020, College Publications, London (2021), pp. 1–16.en
dc.referencesS. Ayhan, What is the meaning of proofs? A Fregean distinction in proof-theoretic semantics, Journal of Philosophical Logic, vol. 50 (2021), pp. 571–591, DOI: https://doi.org/10.1007/s10992-020-09577-2en
dc.referencesS. Ayhan, Introduction: Bilateralism and Proof-Theoretic Semantics: Part I, Bulletin of the Section of Logic, vol. 52(2) (2023), pp. 101–108, DOI: https://doi.org/10.18778/0138-0680.2023.12en
dc.referencesS. Ayhan, Introduction: Bilateralism and Proof-Theoretic Semantics: Part II, Bulletin of the Section of Logic, vol. 52(3) (2023), pp. 267–274, DOI: https://doi.org/10.18778/0138-0680.2023.24en
dc.referencesS. Ayhan, Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations, Journal of Logic and Computation, vol. 35(2) (2025), DOI: https://doi.org/10.1093/logcom/exae014en
dc.referencesS. Ayhan, H. Wansing, On synonymy in proof-theoretic semantics. The case of 2Int, Bulletin of the Section of Logic, vol. 52(2) (2023), pp. 187–237, DOI: https://doi.org/10.18778/0138-0680.2023.18en
dc.referencesH. Barendregt, Lambda Calculi with Types, [in:] S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (eds.), Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford (1992), pp. 117–309, DOI: https://doi.org/10.1093/oso/9780198537618.003.0002en
dc.referencesK. Došen, Identity of Proofs Based on Normalization and Generality,Bulletin of Symbolic Logic, vol. 9(4) (2003), pp. 477–503, DOI: https://doi.org/10.2178/bsl/1067620091en
dc.referencesM. Dummett, Frege: Philosophy of Language, Harper & Row, New York (1973).en
dc.referencesJ.-Y. Girard, Proofs and Types, Cambridge University Press, Cambridge (1989).en
dc.referencesR. Goré, Dual Intuitionistic Logic Revisited, [in:] R. Dyckhoff (ed.),Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000, vol. 1847 of Lecture Notes in Computer Science, Springer-Verlag, Berlin (2000), pp. 252–267, DOI: https://doi.org/10.1007/10722086_21en
dc.referencesR. Goré, I. Shillito, Bi-Intuitionistic Logics: a New Instance of an Old Problem, [in:] N. Olivetti, R. Verbrugge, S. Negri, G. Sandu (eds.), Advances in Modal Logic 13, College Publications (2020), pp. 269–288.en
dc.referencesJ. Horty, Frege on Definitions: A Case Study of Semantic Content, Oxford University Press, Oxford (2007), DOI: https://doi.org/10.1093/acprof:oso/9780199732715.001.0001en
dc.referencesT. Kowalski, H. Ono, Analytic cut and interpolation for bi-intuitionistic logic, The Review of Symbolic Logic, vol. 10(2) (2017), pp. 259–283, DOI: https://doi.org/10.1017/S175502031600040Xen
dc.referencesG. Kreisel, A survey of proof theory II, [in:] J. E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, North Holland, Amsterdam (1971), pp. 109–170, DOI: https://doi.org/10.1016/S0049-237X(08)70845-0en
dc.referencesE. G. K. López-Escobar, Refutability and elementary number theory,Indigationes Mathematicae, vol. 75(4) (1972), pp. 362–374, DOI: https://doi.org/10.1016/1385-7258(72)90053-4en
dc.referencesP. Martin-Löf, About models for intuitionistic type theories and the notion of definitional equality, [in:] S. Kanger (ed.), Proceedings of the Third Scandinavian Logic Symposium, North Holland, Amsterdam (1975), pp. 81–109, DOI: https://doi.org/10.1016/S0049-237X(08)70727-4en
dc.referencesD. Nelson, Constructible Falsity, The Journal of Symbolic Logic, vol. 14(1) (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973en
dc.referencesL. Pinto, T. Uustalu, A proof-theoretic study of bi-intuitionistic propositional sequent calculus, Journal of Logic and Computation, vol. 28(1) (2018), pp. 165–202, DOI: https://doi.org/10.1093/logcom/exx044en
dc.referencesL. Postniece, Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic, Ph.D. thesis, The Australian National University, Canberra (2010).en
dc.referencesD. Prawitz, Ideas and results in proof theory, [in:] J. E. Fenstad (ed.),Proceedings of the Second Scandinavian Logic Symposium, North Holland, Amsterdam (1971), pp. 235–307, DOI: https://doi.org/10.1016/S0049-237X(08)70849-8en
dc.referencesD. Prawitz, Towards A Foundation of A General Proof Theory, [in:] P. Suppes, L. Henkin, A. Joja, G. C. Moisil (eds.), Logic, Methodology, and Philosophy of Science IV, North Holland, Amsterdam (1973), pp. 225–250, DOI: https://doi.org/10.1016/S0049-237X(09)70361-1en
dc.referencesC. Rauszer, A formalization of the propositional calculus of H-B logic,Studia Logica, vol. 33(1) (1974), pp. 23–34, DOI: https://doi.org/10.1007/BF02120864en
dc.referencesP. Schroeder-Heister, Proof-Theoretic Semantics, [in:] E. N. Zalta, U. Nodelman (eds.), The Stanford Encyclopedia of Philosophy, Summer 2024 ed., Metaphysics Research Lab, Stanford University (2024), URL: https://plato.stanford.edu/archives/sum2024/entries/proof-theoretic-semantics/en
dc.referencesM. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Elsevier Science, Amsterdam (2006), DOI: https://doi.org/10.1016/s0049-237x(06)x8001-1en
dc.referencesL. Tranchini, Proof-theoretic semantics, paradoxes and the distinction between sense and denotation, Journal of Logic and Computation, vol. 26(2) (2016), pp. 495–512, DOI: https://doi.org/10.1093/logcom/exu028en
dc.referencesH. Wansing, Falsification, natural deduction and bi-intuitionistic logic,Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450, DOI: https://doi.org/10.1093/logcom/ext035en
dc.referencesH. Wansing, On Split Negation, Strong Negation, Information, Falsification, and Verification, [in:] K. Bimbó (ed.), J. Michael Dunn on Information Based Logics. Outstanding Contributions to Logic, vol. 8, Springer (2016), pp. 161–189, DOI: https://doi.org/10.1007/978-3-319-29300-4_10en
dc.referencesH. Wansing, A more general general proof theory, Journal of Applied Logic, vol. 25 (2017), pp. 23–46, DOI: https://doi.org/10.1016/j.jal.2017.01.002en
dc.contributor.authorEmailsara.ayhan@rub.de
dc.identifier.doi10.18778/0138-0680.2025.03
dc.relation.volume54


Files in this item

Thumbnail
Name:
23-58_Ayhan.pdf
Size:
1.321Mb
Format:
PDF
View/Open

This item appears in the following Collection(s)

Show simple item record

https://creativecommons.org/licenses/by-nc-nd/4.0
Except where otherwise noted, this item's license is described as https://creativecommons.org/licenses/by-nc-nd/4.0