We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce's existential graphs. It works as a rewriting system over inductive objects called ''flowers'', that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.

翻译：我们引入花演算，一种受皮尔士存在图启发的直觉主义一阶逻辑深层推理证明系统。它作为一种作用于称为“花”的归纳对象上的重写系统运行，这些对象既可作为拓扑图获得图形化解释，又可作为类似于相干公式的嵌套式矢列获得文本化呈现。重要的是，该演算完全摒弃了传统符号连接词的概念，仅对包含原子谓词的嵌套花进行操作。我们证明了完整演算的可靠性以及一个分析片段相对于克里普克语义的完备性。据我们所知，这为基于存在图的证明系统提供了首个分析性结果，将语义切消技术适配于深层推理框架。此外，完备性所针对的核心规则集具有完全可逆性，这一性质对于自动和交互式证明搜索均具有重要价值。