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

翻译：在证明论语义学中，模型论有效性被证明论有效性所取代。公式的有效性通过归纳定义，从原子公式的有效性基础出发，利用从证明论规则推导出的归纳子句进行定义。其关键目标是在无需形式模型的情况下证明证明规则的完备性。为命题直觉主义逻辑建立这一理论引发了一些技术性和概念性问题。我们将Sandqvist的（完备的）直觉主义命题逻辑基础扩展语义学与预层范畴中的范畴论证明论联系起来，从范畴论角度重构其可靠性和完备性论证，从而揭示Sandqvist构造的自然性。这种自然性包括Sandqvist基于二阶或消去规则表述对析取的处理。这些构造不仅体现了有效性，更体现了特定形式的正当性对象。通过进一步分析表明，从有效性视角看，Sandqvist语义学也可视为层范畴中的自然析取。