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.

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