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

Gheorghiu, Alexander V.; Pym, David J.

dc.contributor.author	Gheorghiu, Alexander V.
dc.contributor.author	Pym, David J.
dc.date.accessioned	2023-10-12T10:06:04Z
dc.date.available	2023-10-12T10:06:04Z
dc.date.issued	2023-07-18
dc.identifier.issn	0138-0680
dc.identifier.uri	http://hdl.handle.net/11089/48072
dc.description.abstract	Proof-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.iso	en
dc.publisher	Wydawnictwo Uniwersytetu Łódzkiego	pl
dc.relation.ispartofseries	Bulletin of the Section of Logic;2	en
dc.rights.uri	https://creativecommons.org/licenses/by-nc-nd/4.0
dc.subject	logic programming	en
dc.subject	proof-theoretic semantics	en
dc.subject	bilateralism	en
dc.subject	negationas-failure	en
dc.title	Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic	en
dc.type	Other
dc.page.number	239-266
dc.contributor.authorAffiliation	Gheorghiu, Alexander V. - University College London, Department of Computer Science, Gower St, London WC1E 6BT, London, United Kingdom	en
dc.contributor.authorAffiliation	Pym, 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 Kingdom	en
dc.identifier.eissn	2449-836X
dc.references	K. 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.322339	en
dc.references	R. Brandom, Articulating Reasons: An Introduction to Inferentialism, Harvard University Press (2000), DOI: https://doi.org/10.2307/j.ctvjghvz0	en
dc.references	K. 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_11	en
dc.references	M. Dummett, The Logical Basis of Metaphysics, Harvard University Press (1991).	en
dc.references	N. 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-3	en
dc.references	G. Frege, Die Verneinung. Eine Logische Untersuchung, Beiträge Zur Philosophie des Deutschen Idealismus, (1919), pp. 143–157.	en
dc.references	A. 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.references	A. 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 submitted	en
dc.references	L. 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.261	en
dc.references	L. 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.635	en
dc.references	J. Harland, On Hereditary Harrop Formulae as a Basis for Logic Programming, Ph.D. thesis, The University of Edinburgh (1991).	en
dc.references	J. 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-4	en
dc.references	R. 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.references	R. Kowalski, Logic for Problem-Solving, North-Holland Publishing Co. (1986).	en
dc.references	S. 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-9	en
dc.references	N. Kürbis, Proof and Falsity: A Logical Investigation, Cambridge University Press (2019), DOI: https://doi.org/10.1007/s11225-022-10002-9	en
dc.references	J. W. Lloyd, Foundations of Logic Programming, Symbolic Computation, Springer (1984), DOI: https://doi.org/10.1007/978-3-642-96826-6	en
dc.references	D. 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/jzt038	en
dc.references	D. 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-9	en
dc.references	D. 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-W	en
dc.references	T. 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.references	D. 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.references	D. 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.references	R. 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_3	en
dc.references	I. Rumfitt, “Yes” and “No”, Mind, vol. 109(436) (2000), pp. 781–823, DOI: https://doi.org/10.1093/mind/109.436.781	en
dc.references	T. 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.references	T. Sandqvist, An Inferentialist Interpretation of Classical Logic, Ph.D. thesis, Uppsala University (2005).	en
dc.references	T. Sandqvist, Classical Logic without Bivalence, Analysis, vol. 69(2) (2009), pp. 211–218, DOI: https://doi.org/10.1093/analys/anp003	en
dc.references	T. 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/jzv021	en
dc.references	P. 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_2	en
dc.references	T. Smiley, Rejection, Analysis, vol. 56(1) (1996), pp. 1–9, DOI: https://doi.org/10.1111/j.0003-2638.1996.00001.x	en
dc.references	M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company (1969), DOI: https://doi.org/10.2307/2272429	en
dc.references	A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2000), DOI: https://doi.org/10.1017/CBO9781139168717	en
dc.references	D. van Dalen, Logic and Structure, Universitext, Springer (2012), DOI: https://doi.org/10.1007/978-1-4471-4558-5	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.contributor.authorEmail	Gheorghiu, Alexander V. - alexander.gheorghiu.19@ucl.ac.uk
dc.contributor.authorEmail	Pym, David J. - d.pym@ucl.ac.uk
dc.identifier.doi	10.18778/0138-0680.2023.16
dc.relation.volume	52

Files in this item

Name:: 239-266_Gheorghiu,_Pym.pdf
Size:: 1.759Mb
Format:: PDF

View/Open

This item appears in the following Collection(s)

Bulletin of the Section of Logic 52/2 (2023) [5]

Show simple item record

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