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的语义学亦可视为层范畴中的自然析取。