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 Author
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 Author

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

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

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

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. 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 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 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 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).

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

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

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

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). 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.

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

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

T. Sandqvist, Classical Logic without Bivalence, Analysis, vol. 69(2) (2009), pp. 211–218, DOI: https://doi.org/10.1093/analys/anp003 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 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 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 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 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 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 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 DOI: https://doi.org/10.1093/logcom/ext035