We develop a diagrammatic proof system for a fragment of structural semantics inspired by the Greimas semiotic square, using spider diagrams as the underlying formalism. The basic terms are represented as diagrammatic configurations, and the relations of contradiction and implication are interpreted as transformations governed by a set of inference rules. These transformations are realised as derivations, with proof trees serving as witnesses. Our main result shows that the construction of the four meta-terms can be captured uniformly: each is derivable from a conjunctive pair of basic configurations via a fixed derivation schema composed of contour introduction and habitat transformation rules. This yields a proof-theoretic account of the combinatorial operation underlying meta-term formation, and provides a semantic interpretation of the Greimasian operation `+' as a derivational construction rather than a logical combination. We further show that diagrammatic negation in this setting is not a Boolean complement, but a restricted, zone-determined semantic counter-position, reflecting the relational character of opposition in structural semiotics. The resulting framework provides a compositional, rule-based semantics in which complex configurations are generated constructively from simpler ones. In addition to extending the expressive scope of spider diagram calculi, the system illustrates how diagrammatic reasoning can be used to formalise non-classical semantic operations within a unified inferential setting.

翻译：我们开发了一个基于格雷马斯符号方阵的结构语义学分段的图式证明系统，以蜘蛛图作为基础形式化工具。基本术语通过图式配置表示，矛盾与蕴含关系被解释为受推理规则集控制的变换。这些变换通过推导实现，其中证明树作为验证依据。我们的主要结果表明，四个元术语的构造可统一刻画：每个元术语均可通过一个由轮廓引入和生境变换规则组成的固定推导模式，从基本配置的合取对推导得出。这为元术语形成背后的组合操作提供了证明论解释，并将格雷马斯式操作“+”解释为推导性构造而非逻辑组合。我们进一步表明，该框架中的图式否定并非布尔补运算，而是一种受限的、由区域决定的语义对立，反映了结构符号学中对立的关系性特征。所构建的框架提供了一种组合性的、基于规则的语义学，其中复杂配置通过构造性方式从简单配置生成。除扩展蜘蛛图演算的表达范围外，该体系还展示了图式推理如何在统一推理框架内形式化非经典语义操作。