Pokaż uproszczony rekord

Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic

dc.contributor.authorGheorghiu, Alexander V.
dc.contributor.authorPym, David J.
dc.date.accessioned2023-10-12T10:06:04Z
dc.date.available2023-10-12T10:06:04Z
dc.date.issued2023-07-18
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/48072
dc.description.abstractProof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of them as provided by uniform proof-search—the proof-theoretic foundation of logic programming (LP)—to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS.en
dc.language.isoen
dc.publisherWydawnictwo Uniwersytetu Łódzkiegopl
dc.relation.ispartofseriesBulletin of the Section of Logic;2en
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0
dc.subjectlogic programmingen
dc.subjectproof-theoretic semanticsen
dc.subjectbilateralismen
dc.subjectnegationas-failureen
dc.titleDefinite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logicen
dc.typeOther
dc.page.number239-266
dc.contributor.authorAffiliationGheorghiu, Alexander V. - University College London, Department of Computer Science, Gower St, London WC1E 6BT, London, United Kingdomen
dc.contributor.authorAffiliationPym, David J. - University College London, Department of Computer Science, Gower St, London WC1E 6BT, London, United Kingdom; University College London, Department of Philosophy, Gower St, London WC1E 6BT, London, United Kingdom; University of London, Institute of Philosophy, Senate House, Malet St, London WC1E 7HU, London, United Kingdomen
dc.identifier.eissn2449-836X
dc.referencesK. R. Apt, M. H. Van Emden, Contributions to the theory of logic programming, Journal of the ACM, vol. 29(3) (1982), pp. 841–862, DOI: https://doi.org/10.1145/322326.322339en
dc.referencesR. Brandom, Articulating Reasons: An Introduction to Inferentialism, Harvard University Press (2000), DOI: https://doi.org/10.2307/j.ctvjghvz0en
dc.referencesK. L. Clark, Negation as Failure, [in:] Logic and Data Bases, Springer (1978), pp. 293–322, DOI: https://doi.org/10.1007/978-1-4684-3384-5_11en
dc.referencesM. Dummett, The Logical Basis of Metaphysics, Harvard University Press (1991).en
dc.referencesN. Francez, Bilateralism in Proof-theoretic Semantics, Journal of Philosophical Logic, vol. 43 (2014), pp. 239–259, DOI: https://doi.org/10.1007/s10992-012-9261-3en
dc.referencesG. Frege, Die Verneinung. Eine Logische Untersuchung, Beiträge Zur Philosophie des Deutschen Idealismus, (1919), pp. 143–157.en
dc.referencesA. V. Gheorghiu, S. Docherty, D. J. Pym, Reductive Logic, Coalgebra, and Proof-search: A Perspective from Resource Semantics, [in:] A. Palmigiano, M. Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond, Springer Outstanding Contributions to Logic Series, Springer (2023), to appear.en
dc.referencesA. V. Gheorghiu, D. J. Pym, From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic (Accessed 08 February 2023), URL: https://arxiv.org/abs/2210.05344 submitteden
dc.referencesL. Hallnäs, P. Schroeder-Heister, A Proof-theoretic Approach to Logic Programming: I. Clauses as Rules, Journal of Logic and Computation, vol. 1(2) (1990), pp. 261–283, DOI: https://doi.org/10.1093/logcom/1.2.261en
dc.referencesL. Hallnäs, P. Schroeder-Heister, A Proof-theoretic Approach to Logic Programming: II. Programs as Definitions, Journal of Logic and Computation, vol. 1(5) (1991), pp. 635–660, DOI: https://doi.org/10.1093/logcom/1.5.635en
dc.referencesJ. Harland, On Hereditary Harrop Formulae as a Basis for Logic Programming, Ph.D. thesis, The University of Edinburgh (1991).en
dc.referencesJ. Harland, Success and Failure for hereditary Harrop Formulae, The Journal of Logic Programming, vol. 17(1) (1993), pp. 1–29, DOI: https://doi.org/10.1016/0743-1066(93)90007-4en
dc.referencesR. Kowalski, Logic for Problem Solving, https://www.doc.ic.ac.uk/~rak/papers/LFPScommentary.pdf (Accessed 15 August 2022), commentary on the book ‘Logic for Problem Solving’ by R. Kowalski.en
dc.referencesR. Kowalski, Logic for Problem-Solving, North-Holland Publishing Co. (1986).en
dc.referencesS. A. Kripke, Semantical Analysis of Intuitionistic Logic I, [in:] Studies in Logic and the Foundations of Mathematics, vol. 40, Elsevier (1965), pp. 92–130, DOI: https://doi.org/10.1016/S0049-237X(08)71685-9en
dc.referencesN. Kürbis, Proof and Falsity: A Logical Investigation, Cambridge University Press (2019), DOI: https://doi.org/10.1007/s11225-022-10002-9en
dc.referencesJ. W. Lloyd, Foundations of Logic Programming, Symbolic Computation, Springer (1984), DOI: https://doi.org/10.1007/978-3-642-96826-6en
dc.referencesD. Makinson, On an Inferential Semantics for Classical Logic, Logic Journal of IGPL, vol. 22(1) (2014), pp. 147–154, DOI: https://doi.org/10.1093/jigpal/jzt038en
dc.referencesD. Miller, A Logical Analysis of Modules in Logic Programming, Journal of Logic Programming, vol. 6(1-2) (1989), pp. 79–108, DOI: https://doi.org/10.1016/0743-1066(89)90031-9en
dc.referencesD. Miller, G. Nadathur, F. Pfenning, A. Scedrov, Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic, vol. 51(1) (1991), pp. 125–157, DOI: https://doi.org/10.1016/0168-0072(91)90068-Wen
dc.referencesT. Piecha, P. Schroeder-Heister, The Definitional View of Atomic Systems in Proof-theoretic Semantics, [in:] The Logica Yearbook 2016, College Publications London (2017), pp. 185–200.en
dc.referencesD. J. Pym, E. Ritter, Reductive logic and Proof-search: Proof Theory, Semantics, and Control, vol. 45 of Oxford Logic Guides, Oxford University Press (2004).en
dc.referencesD. J. Pym, E. Ritter, E. Robinson, Proof-theoretic Semantics in Sheaves (Extended Abstract), [in:] Proceedings of the Eleventh Scandinavian Logic Symposium — SLSS 11 (2022), pp. 36–38.en
dc.referencesR. Reiter, On closed world data bases, [in:] Readings in artificial intelligence, Elsevier (1981), pp. 119–140, DOI: https://doi.org/10.1007/978-1-4684-3384-5_3en
dc.referencesI. Rumfitt, “Yes” and “No”, Mind, vol. 109(436) (2000), pp. 781–823, DOI: https://doi.org/10.1093/mind/109.436.781en
dc.referencesT. Sandqvist, Atomic Bases and the Validity of Peirce’s Law, https://drive.google.com/file/d/1fX8PWh8w2cpOkYS39zR2OGfNEhQESKkl/view (Accessed 15 August 2022), presentation at the World Logic Day event at UCL: The Meaning of Proofs.en
dc.referencesT. Sandqvist, An Inferentialist Interpretation of Classical Logic, Ph.D. thesis, Uppsala University (2005).en
dc.referencesT. Sandqvist, Classical Logic without Bivalence, Analysis, vol. 69(2) (2009), pp. 211–218, DOI: https://doi.org/10.1093/analys/anp003en
dc.referencesT. Sandqvist, Base-extension Semantics for Intuitionistic Sentential Logic, Logic Journal of the IGPL, vol. 23(5) (2015), pp. 719–731, DOI: https://doi.org/10.1093/jigpal/jzv021en
dc.referencesP. Schroeder-Heister, T. Piecha, Atomic Systems in Proof-Theoretic Semantics: Two Approaches, [in:] Ángel Nepomuceno Fernández, O. P. Martins, J. Redmond (eds.), Epistemology, Knowledge and the Impact of Interaction, Springer Verlag (2016), pp. 47–62, DOI: https://doi.org/10.1007/978-3-319-26506-3_2en
dc.referencesT. Smiley, Rejection, Analysis, vol. 56(1) (1996), pp. 1–9, DOI: https://doi.org/10.1111/j.0003-2638.1996.00001.xen
dc.referencesM. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company (1969), DOI: https://doi.org/10.2307/2272429en
dc.referencesA. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2000), DOI: https://doi.org/10.1017/CBO9781139168717en
dc.referencesD. van Dalen, Logic and Structure, Universitext, Springer (2012), DOI: https://doi.org/10.1007/978-1-4471-4558-5en
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.contributor.authorEmailGheorghiu, Alexander V. - alexander.gheorghiu.19@ucl.ac.uk
dc.contributor.authorEmailPym, David J. - d.pym@ucl.ac.uk
dc.identifier.doi10.18778/0138-0680.2023.16
dc.relation.volume52


Pliki tej pozycji

Thumbnail
Nazwa:
239-266_Gheorghiu,_Pym.pdf
Rozmiar:
1.759MB
Format:
PDF
Oglądaj/Otwórz

Pozycja umieszczona jest w następujących kolekcjach

Pokaż uproszczony rekord

https://creativecommons.org/licenses/by-nc-nd/4.0
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako https://creativecommons.org/licenses/by-nc-nd/4.0