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

Ayhan, Sara

dc.contributor.author	Ayhan, Sara
dc.date.accessioned	2025-11-19T14:27:55Z
dc.date.available	2025-11-19T14:27:55Z
dc.date.issued	2025-05-30
dc.identifier.issn	0138-0680
dc.identifier.uri	http://hdl.handle.net/11089/56722
dc.description.abstract	In 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.iso	en
dc.publisher	Wydawnictwo Uniwersytetu Łódzkiego	pl
dc.relation.ispartofseries	Bulletin of the Section of Logic;1	en
dc.rights.uri	https://creativecommons.org/licenses/by-nc-nd/4.0
dc.subject	proof-theoretic semantics	en
dc.subject	bilateralism	en
dc.subject	bi-intuitionistic logic	en
dc.subject	meaning of proofs	en
dc.subject	proof identity	en
dc.subject	refutations	en
dc.title	Comparing Sense and Denotation in Bilateralist Proof Systems for Proofs and Refutations	en
dc.type	Article
dc.page.number	23-58
dc.contributor.authorAffiliation	Ruhr University Bochum, Institute of Philosophy I	en
dc.identifier.eissn	2449-836X
dc.references	S. 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.references	S. 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-2	en
dc.references	S. 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.12	en
dc.references	S. 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.24	en
dc.references	S. 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/exae014	en
dc.references	S. 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.18	en
dc.references	H. 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.0002	en
dc.references	K. 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/1067620091	en
dc.references	M. Dummett, Frege: Philosophy of Language, Harper & Row, New York (1973).	en
dc.references	J.-Y. Girard, Proofs and Types, Cambridge University Press, Cambridge (1989).	en
dc.references	R. 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_21	en
dc.references	R. 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.references	J. 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.0001	en
dc.references	T. 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/S175502031600040X	en
dc.references	G. 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-0	en
dc.references	E. 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-4	en
dc.references	P. 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-4	en
dc.references	D. Nelson, Constructible Falsity, The Journal of Symbolic Logic, vol. 14(1) (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973	en
dc.references	L. 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/exx044	en
dc.references	L. Postniece, Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic, Ph.D. thesis, The Australian National University, Canberra (2010).	en
dc.references	D. 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-8	en
dc.references	D. 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-1	en
dc.references	C. 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/BF02120864	en
dc.references	P. 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.references	M. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Elsevier Science, Amsterdam (2006), DOI: https://doi.org/10.1016/s0049-237x(06)x8001-1	en
dc.references	L. 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/exu028	en
dc.references	H. 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/ext035	en
dc.references	H. 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_10	en
dc.references	H. 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.002	en
dc.contributor.authorEmail	sara.ayhan@rub.de
dc.identifier.doi	10.18778/0138-0680.2025.03
dc.relation.volume	54