eprintid: 10192657
rev_number: 8
eprint_status: archive
userid: 699
dir: disk0/10/19/26/57
datestamp: 2024-05-23 09:03:51
lastmod: 2024-05-23 09:03:51
status_changed: 2024-05-23 09:03:51
type: article
metadata_visibility: show
sword_depositor: 699
creators_name: Pym, D
creators_name: Ritter, E
creators_name: Robinson, E
title: Categorical Proof-theoretic Semantics
ispublished: inpress
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
keywords: Proof-theoretic semantics, Base-extension semantics, Categorical logic, Kripke
Semantics, Presheaves, Sheaves
note: Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
abstract: In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist’s constructions. This naturality includes Sandqvist’s treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist’s semantics can also be viewed as the natural disjunction in a category of sheaves.
date: 2024-01-01
date_type: published
publisher: Springer Science and Business Media LLC
official_url: http://dx.doi.org/10.1007/s11225-024-10101-9
oa_status: green
full_text_type: pub
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 2277860
doi: 10.1007/s11225-024-10101-9
lyricists_name: Pym, David
lyricists_id: DPYMX87
actors_name: Pym, David
actors_id: DPYMX87
actors_role: owner
full_text_status: public
publication: Studia Logica
issn: 0039-3215
citation:        Pym, D;    Ritter, E;    Robinson, E;      (2024)    Categorical Proof-theoretic Semantics.                   Studia Logica        10.1007/s11225-024-10101-9 <https://doi.org/10.1007/s11225-024-10101-9>.    (In press).    Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10192657/1/s11225-024-10101-9.pdf