<> <http://www.w3.org/2000/01/rdf-schema#comment> "The repository administrator has not yet configured an RDF license."^^<http://www.w3.org/2001/XMLSchema#string> . <> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/10192657> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/AcademicArticle> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Article> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/title> "Categorical Proof-theoretic Semantics"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/ontology/bibo/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."^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/date> "2024-01-01" . <https://discovery.ucl.ac.uk/id/document/1746404> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Document> . <https://discovery.ucl.ac.uk/id/org/ext-dcea299cf48188065b5f59a4cae50003> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Organization> . <https://discovery.ucl.ac.uk/id/org/ext-dcea299cf48188065b5f59a4cae50003> <http://xmlns.com/foaf/0.1/name> "Springer Science and Business Media LLC"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/publisher> <https://discovery.ucl.ac.uk/id/org/ext-dcea299cf48188065b5f59a4cae50003> . <https://discovery.ucl.ac.uk/id/publication/ext-00393215> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://purl.org/ontology/bibo/Collection> . <https://discovery.ucl.ac.uk/id/publication/ext-00393215> <http://xmlns.com/foaf/0.1/name> "Studia Logica"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/publication/ext-00393215> . <https://discovery.ucl.ac.uk/id/publication/ext-00393215> <http://www.w3.org/2002/07/owl#sameAs> <urn:issn:00393215> . <https://discovery.ucl.ac.uk/id/publication/ext-00393215> <http://purl.org/ontology/bibo/issn> "00393215" . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/ontology/bibo/status> <http://purl.org/ontology/bibo/status/forthcoming> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> . <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_1> <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> . <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_2> <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/creator> <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/ontology/bibo/authorList> <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> . <https://discovery.ucl.ac.uk/id/eprint/10192657#authors> <http://www.w3.org/1999/02/22-rdf-syntax-ns#_3> <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> . <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> . <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> <http://xmlns.com/foaf/0.1/givenName> "D"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> <http://xmlns.com/foaf/0.1/familyName> "Pym"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-5b29cdee98c9e156dd7501015c8c235a> <http://xmlns.com/foaf/0.1/name> "D Pym"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> . <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> <http://xmlns.com/foaf/0.1/givenName> "E"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> <http://xmlns.com/foaf/0.1/familyName> "Robinson"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-7ed1eb3fab5082e2c31126ac228e66b0> <http://xmlns.com/foaf/0.1/name> "E Robinson"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://xmlns.com/foaf/0.1/Person> . <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> <http://xmlns.com/foaf/0.1/givenName> "E"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> <http://xmlns.com/foaf/0.1/familyName> "Ritter"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/person/ext-393ec211f146c4e6404ae1444fedde9c> <http://xmlns.com/foaf/0.1/name> "E Ritter"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/EPrint> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/ArticleEPrint> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/terms/isPartOf> <https://discovery.ucl.ac.uk/id/repository> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746404> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746404> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Text)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://purl.org/dc/elements/1.1/hasVersion> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasPublished> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746404> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/1/s11225-024-10101-9.pdf> . <https://discovery.ucl.ac.uk/id/document/1746404> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/1/s11225-024-10101-9.pdf> . <https://discovery.ucl.ac.uk/id/eprint/10192657/1/s11225-024-10101-9.pdf> <http://www.w3.org/2000/01/rdf-schema#label> "s11225-024-10101-9.pdf"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746405> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Other)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://eprints.org/relation/isIndexCodesVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/2/indexcodes.txt> . <https://discovery.ucl.ac.uk/id/document/1746405> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/2/indexcodes.txt> . <https://discovery.ucl.ac.uk/id/eprint/10192657/2/indexcodes.txt> <http://www.w3.org/2000/01/rdf-schema#label> "indexcodes.txt"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746406> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Other)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://eprints.org/relation/islightboxThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/3/lightbox.jpg> . <https://discovery.ucl.ac.uk/id/document/1746406> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/3/lightbox.jpg> . <https://discovery.ucl.ac.uk/id/eprint/10192657/3/lightbox.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "lightbox.jpg"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746407> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Other)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://eprints.org/relation/ispreviewThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/4/preview.jpg> . <https://discovery.ucl.ac.uk/id/document/1746407> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/4/preview.jpg> . <https://discovery.ucl.ac.uk/id/eprint/10192657/4/preview.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "preview.jpg"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746408> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Other)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://eprints.org/relation/ismediumThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/5/medium.jpg> . <https://discovery.ucl.ac.uk/id/document/1746408> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/5/medium.jpg> . <https://discovery.ucl.ac.uk/id/eprint/10192657/5/medium.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "medium.jpg"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://eprints.org/ontology/hasDocument> <https://discovery.ucl.ac.uk/id/document/1746409> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://eprints.org/ontology/Document> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://www.w3.org/2000/01/rdf-schema#label> "Categorical Proof-theoretic Semantics (Other)"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://eprints.org/relation/isVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://eprints.org/relation/isVolatileVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://eprints.org/relation/issmallThumbnailVersionOf> <https://discovery.ucl.ac.uk/id/document/1746404> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://eprints.org/ontology/hasFile> <https://discovery.ucl.ac.uk/id/eprint/10192657/6/small.jpg> . <https://discovery.ucl.ac.uk/id/document/1746409> <http://purl.org/dc/terms/hasPart> <https://discovery.ucl.ac.uk/id/eprint/10192657/6/small.jpg> . <https://discovery.ucl.ac.uk/id/eprint/10192657/6/small.jpg> <http://www.w3.org/2000/01/rdf-schema#label> "small.jpg"^^<http://www.w3.org/2001/XMLSchema#string> . <https://discovery.ucl.ac.uk/id/eprint/10192657> <http://www.w3.org/2000/01/rdf-schema#seeAlso> <https://discovery.ucl.ac.uk/id/eprint/10192657/> . <https://discovery.ucl.ac.uk/id/eprint/10192657/> <http://purl.org/dc/elements/1.1/title> "HTML Summary of #10192657 \n\nCategorical Proof-theoretic Semantics\n\n" . <https://discovery.ucl.ac.uk/id/eprint/10192657/> <http://purl.org/dc/elements/1.1/format> "text/html" . <https://discovery.ucl.ac.uk/id/eprint/10192657/> <http://xmlns.com/foaf/0.1/primaryTopic> <https://discovery.ucl.ac.uk/id/eprint/10192657> .