Geodesic
Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 239-266.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: logic programming, proof-theoretic semantics, bilateralism, negationas-failure 
@article{BSL_2023_52_2_a3,
     author = {Gheorghiu, Alexander V. and Pym, David J.},
     title = {Definite {Formulae,} {Negation-as-Failure,} and the {Base-Extension} {Semantics} of {Intuitionistic} {Propositional} {Logic}},
     journal = {Bulletin of the Section of Logic},
     pages = {239--266},
     publisher = {mathdoc},
     volume = {52},
     number = {2},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a3/}
}
TY  - JOUR
AU  - Gheorghiu, Alexander V.
AU  - Pym, David J.
TI  - Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 239
EP  - 266
VL  - 52
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a3/
LA  - en
ID  - BSL_2023_52_2_a3
ER  - 
%0 Journal Article
%A Gheorghiu, Alexander V.
%A Pym, David J.
%T Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
%J Bulletin of the Section of Logic
%D 2023
%P 239-266
%V 52
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a3/
%G en
%F BSL_2023_52_2_a3
Gheorghiu, Alexander V.; Pym, David J. Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic. Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 239-266. http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a3/

[1] 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

[2] R. Brandom, Articulating Reasons: An Introduction to Inferentialism, Harvard University Press (2000) | DOI

[3] K. L. Clark, Negation as Failure, [in:] Logic and Data Bases, Springer (1978), pp. 293–322 | DOI

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

[5] N. Francez, Bilateralism in Proof-theoretic Semantics, Journal of Philosophical Logic, vol. 43 (2014), pp. 239–259 | DOI

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

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

[8] 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

[9] 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

[10] 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

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

[12] J. Harland, Success and Failure for hereditary Harrop Formulae, The Journal of Logic Programming, vol. 17(1) (1993), pp. 1–29 | DOI

[13] 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.

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

[15] 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

[16] N. Kürbis, Proof and Falsity: A Logical Investigation, Cambridge University Press (2019) | DOI

[17] J. W. Lloyd, Foundations of Logic Programming, Symbolic Computation, Springer (1984) | DOI

[18] D. Makinson, On an Inferential Semantics for Classical Logic, Logic Journal of IGPL, vol. 22(1) (2014), pp. 147–154 | DOI

[19] D. Miller, A Logical Analysis of Modules in Logic Programming, Journal of Logic Programming, vol. 6(1-2) (1989), pp. 79–108 | DOI

[20] 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

[21] 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.

[22] 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).

[23] 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.

[24] R. Reiter, On closed world data bases, [in:] Readings in artificial intelligence, Elsevier (1981), pp. 119–140 | DOI

[25] I. Rumfitt, “Yes” and “No”, Mind, vol. 109(436) (2000), pp. 781–823 | DOI

[26] 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.

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

[28] T. Sandqvist, Classical Logic without Bivalence, Analysis, vol. 69(2) (2009), pp. 211–218 | DOI

[29] T. Sandqvist, Base-extension Semantics for Intuitionistic Sentential Logic, Logic Journal of the IGPL, vol. 23(5) (2015), pp. 719–731 | DOI

[30] 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

[31] T. Smiley, Rejection, Analysis, vol. 56(1) (1996), pp. 1–9 | DOI

[32] M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company (1969) | DOI

[33] A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2000) | DOI

[34] D. van Dalen, Logic and Structure, Universitext, Springer (2012) | DOI

[35] H. Wansing, Falsification, Natural Deduction and Bi-intuitionistic Logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450 | DOI