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

Alexander V. Gheorghiu; David J. Pym

doi:10.18778/0138-0680.2023.16

Authors

Alexander V. Gheorghiu University College London, Department of Computer Science, Gower St, London WC1E 6BT, London, United Kingdom
David J. Pym 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

DOI:

https://doi.org/10.18778/0138-0680.2023.16

Keywords:

logic programming, proof-theoretic semantics, bilateralism, negationas-failure

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.

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
Google Scholar DOI: https://doi.org/10.1145/322326.322339

R. Brandom, Articulating Reasons: An Introduction to Inferentialism, Harvard University Press (2000), DOI: https://doi.org/10.2307/j.ctvjghvz0
Google Scholar DOI: https://doi.org/10.4159/9780674028739

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
Google Scholar DOI: https://doi.org/10.1007/978-1-4684-3384-5_11

M. Dummett, The Logical Basis of Metaphysics, Harvard University Press (1991).
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1007/s10992-012-9261-3

G. Frege, Die Verneinung. Eine Logische Untersuchung, Beiträge Zur Philosophie des Deutschen Idealismus, (1919), pp. 143–157.
Google Scholar

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.
Google Scholar DOI: https://doi.org/10.1007/978-3-031-24117-8_23

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
Google Scholar DOI: https://doi.org/10.18778/0138-0680.2023.16

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
Google Scholar DOI: https://doi.org/10.1093/logcom/1.2.261

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
Google Scholar DOI: https://doi.org/10.1093/logcom/1.5.635

J. Harland, On Hereditary Harrop Formulae as a Basis for Logic Programming, Ph.D. thesis, The University of Edinburgh (1991).
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1016/0743-1066(93)90007-4

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.
Google Scholar

R. Kowalski, Logic for Problem-Solving, North-Holland Publishing Co. (1986).
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(08)71685-9

N. Kürbis, Proof and Falsity: A Logical Investigation, Cambridge University Press (2019), DOI: https://doi.org/10.1007/s11225-022-10002-9
Google Scholar DOI: https://doi.org/10.1017/9781108686792

J. W. Lloyd, Foundations of Logic Programming, Symbolic Computation, Springer (1984), DOI: https://doi.org/10.1007/978-3-642-96826-6
Google Scholar DOI: https://doi.org/10.1007/978-3-642-96826-6

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
Google Scholar DOI: https://doi.org/10.1093/jigpal/jzt038

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
Google Scholar DOI: https://doi.org/10.1016/0743-1066(89)90031-9

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
Google Scholar DOI: https://doi.org/10.1016/0168-0072(91)90068-W

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.
Google Scholar

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).
Google Scholar DOI: https://doi.org/10.1093/acprof:oso/9780198526339.001.0001

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.
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1016/B978-0-934613-03-3.50014-3

I. Rumfitt, “Yes” and “No”, Mind, vol. 109(436) (2000), pp. 781–823, DOI: https://doi.org/10.1093/mind/109.436.781
Google Scholar DOI: https://doi.org/10.1093/mind/109.436.781

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.
Google Scholar

T. Sandqvist, An Inferentialist Interpretation of Classical Logic, Ph.D. thesis, Uppsala University (2005).
Google Scholar

T. Sandqvist, Classical Logic without Bivalence, Analysis, vol. 69(2) (2009), pp. 211–218, DOI: https://doi.org/10.1093/analys/anp003
Google Scholar DOI: https://doi.org/10.1093/analys/anp003

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
Google Scholar DOI: https://doi.org/10.1093/jigpal/jzv021

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
Google Scholar DOI: https://doi.org/10.1007/978-3-319-26506-3_2

T. Smiley, Rejection, Analysis, vol. 56(1) (1996), pp. 1–9, DOI: https://doi.org/10.1111/j.0003-2638.1996.00001.x
Google Scholar DOI: https://doi.org/10.1093/analys/56.1.1

M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company (1969), DOI: https://doi.org/10.2307/2272429
Google Scholar DOI: https://doi.org/10.2307/2272429

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
Google Scholar DOI: https://doi.org/10.1017/CBO9781139168717

D. van Dalen, Logic and Structure, Universitext, Springer (2012), DOI: https://doi.org/10.1007/978-1-4471-4558-5
Google Scholar DOI: https://doi.org/10.1007/978-1-4471-4558-5

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
Google Scholar DOI: https://doi.org/10.1093/logcom/ext035