# The Flower Calculus

Pablo Donato

► To cite this version:

Pablo Donato. The Flower Calculus. Leibniz International Proceedings in Informatics, 2024, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) (299), pp.5:1-5:24. hal-04472717v3

HAL Id: hal-04472717

https://hal.science/hal-04472717v3

Submitted on 12 Jul 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Flower Calculus

Pablo Donato

<figure><img src="image_2.png" /></figure>

LIX, École polytechnique, France

## Abstract

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.

**2012 ACM Subject Classification** Theory of computation → Proof theory; Theory of computation → Constructive mathematics

**Keywords and phrases** deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination

**Supplementary Material** The source code for a Coq mechanization of additional meta-theoretical results, as well as a web demo of GUI for ITPs based on this work, are available as follows:
*Software (Mechanized Theory): https://github.com/Champitoad/flowers-metatheory [19]*
*Software (Online Demo): https://github.com/Champitoad/flower-prover [20]*

**Acknowledgements** I want to thank Luc Chabassier for writing the Lua script that was used to generate all the flower drawings in this document, and Benjamin Werner for useful feedback on a first draft of this paper. Lastly, I thank Tito for teaching me some invaluable formatting tricks.

# 1 Introduction

**Graphical proof building** Proof assistants — also called *interactive theorem provers* (ITPs) — provide a set of tools to ease the process of formalizing mathematical developments. This includes languages to specify definitions and statements conveniently, but also interfaces to build proofs interactively without having to fill in all the details. The dominant paradigm for these interfaces is that of *tactic languages* [43]: the user is exposed with a set of *goals* that remain to be proved, constituting the *proof state*, and modifies these goals through textual commands, called *tactics*, until there is no goal left. This is currently what is implemented in mainstream proof assistants such as Coq [57] and Lean [44].

In recent years, there have been several efforts to replace or complement textual tactic languages with *graphical user interfaces* (GUIs) [50, 4, 37, 12, 52, 34, 67, 3]. The hope is to make proof assistants more intuitive and accessible to beginners and non-specialists, but also, to some extent, more productive and ergonomic even for experts.

The initial motivation for this work was to design a proof calculus well-suited to *direct manipulation* in such a graphical setting. The idea is that the user should be able to interact directly with the graphical representation of the *proof state*, using a pointing device such as a mouse or fingers on a touch screen. In previous work [21], we proposed a way to synthesize complex logical inferences through *drag-and-drop* actions between two formulas of the current goal/sequent, based on the *subformula linking* (SFL) methodology [12, 13].
**Diagrammatic reasoning** In this work, we show that (single-conclusion) sequents and symbolic formulas built from binary connectives and unary quantifiers are not mandatory for representing the *proof state*. Other authors have defended the idea of using *diagrams* as a more user-friendly frontend for ITPs. In particular, Linker et al. showed how to integrate tactic-based automation in an ITP based on *spider diagrams* [34], which are equivalent in expressive power to classical monadic *first-order logic* (FOL) [28].

We introduce a new data structure for goals inspired by an earlier invention in the history of diagrammatic logic: the *existential graphs* (EGs) of C. S. Peirce [51]. We noticed that our structure could be drawn and manipulated metaphorically in the form of nested *flowers*, and thus chose to name *flower calculus* the proof system for full intuitionistic FOL that we built around it. Our focus in this paper will be to introduce the *flower calculus* to readers unfamiliar with EGs, and to study its fundamental properties through the lens of modern *structural proof theory*.

**Implementation** We have formalized in Coq a bidirectional simulation between the *flower calculus* and cut-free sequent calculus, yielding a soundness theorem and a *weak completeness theorem* for an *analytic fragment* of the *flower calculus* [19]. In this paper, we follow a *semantic* rather than syntactic approach, avoiding translations to and from symbolic formulas to obtain a stronger completeness result.

While currently at an early stage, we are also developing the *Flower Prover*, a prototype of direct-manipulation GUI for ITPs based on the *flower calculus* [20]. The interested reader can try a publicly available version of the prototype online<fnref n="1" />. We leave a detailed account of the Flower Prover and its connection to the *flower calculus* for future work.

**Outline** The article is organized as follows: in Section 2 we give a brief overview of the original diagrammatic syntax of EGs used by Peirce in his system Alpha for classical propositional logic. In Section 3 we retrace the origin of an intuitionistic variant of EGs first introduced by Oostra in [45], that directly inspired our flower metaphor. In Section 4 we illustrate quickly the original mechanism of *lines of identity* used by Peirce to express first-order quantifiers in his Beta system, and show how to recast it in a more traditional binder-based syntax. In Section 5 we introduce our inductive syntax for *flowers*, and in Section 6 we give the full set of inference rules of the *flower calculus* as well as our notion of proof. In Section 7 we give a direct Kripke semantics to *flowers*, and in Section 8 we show that a restricted fragment of *analytic* and *invertible* rules is complete with respect to the semantics. Finally we conclude in Section 9 by a comparison with some related works.

**► Note.** The proof of soundness of the *flower calculus* is given in Appendix B. Contrary to the completeness proof, it is mostly routine work that does not require much insight. Detailed proofs for the deduction and completeness theorems are given respectively in Appendix C.1 and Appendix C.2. Readers already familiar with EGs can find a detailed comparison of the rules of the *flower calculus* with Peirce’s *illative transformations* in Appendix A.

<footnote n="1">¹ https://www.lix.polytechnique.fr/Labo/Pablo.DONATO/flowerprover/</footnote>
## 2 Existential graphs

Peirce designed in total three systems of EGs, which he called respectively Alpha, Beta and Gamma. They were invented chronologically in that order, which also captures their relationship in terms of complexity: Alpha is the foundation on which the other systems are built, and can today be understood as a diagrammatic calculus for classical propositional logic. As we will see in Section 4, Beta corresponds to a variable-free representation of first-order logic without function symbols. The last system Gamma is more experimental, with various unfinished features that have been interpreted as attempts to capture modal [66] and higher-order logics.

**Sheet of Assertion** The most fundamental concept of Alpha is the *sheet of assertion*, denoted by *SA* thereafter. It is the space where statements are scribed by the reasoner, typically a sheet of paper, a blackboard, or a computer display. As its name indicates, scribing a statement on *SA* amounts to *asserting its truth*. Thus naturally, the empty *SA* where nothing is scribed will denote *vacuous truth*, traditionally signified by the symbol $\top$.

**Juxtaposition** As we know from natural deduction, asserting the truth of the *conjunction* $a \wedge b$ of two propositions $a$ and $b$, amounts to asserting *both* the truth of $a$ and the truth of $b$. In Alpha, there is no need to introduce the symbolic connective $\wedge$, since one can just write both $a$ and $b$ at distinct locations on *SA*:

$$a \ b$$

More generally, one might consider any two portions $G$ and $H$ of *SA*, and interpret their juxtaposition $G \ H$ as signifying that we assert the truth of their conjunction.

**Cuts** Asserting the truth of the *negation* $
eg a$ of a proposition $a$, amounts to *denying* the truth of $a$. This is done in Alpha by enclosing $a$ in a closed curve like so:

$$\begin{tikzpicture}
\draw (0,0) circle (1);
\node at (-0.5,0) {a};
\end{tikzpicture}$$

Peirce called such curves *cuts*<fnref n="2" />, because they ought to be seen as literal cuts in the paper sheet that embodies *SA*. Note that they do not need to be circles: all that matters is that $a$ is in a separate area from the rest of *SA*. This is precisely the content of the *Jordan curve theorem* in topology, and thus we can take *cuts* to be arbitrary Jordan curves. This entails in particular that *cuts* cannot intersect each other, but can be freely nested. Then as for juxtaposition, one can replace the proposition $a$ in the interior of the *cut* by any *graph G* — i.e. any portion of *SA* — as long as the *cut* does not intersect other *cuts* in *G*.

**Relationship with formulas** With just these two *icons*, juxtaposition and *cuts*, one can therefore assert the truth of any proposition made up of conjunctions and negations and built from atomic propositions. Importantly, the only symbols needed for doing so are letters $a, b, c, \dots$ denoting atomic propositions, that is “pure” symbols that do not have any logical meaning associated to them.

Now, it is well-known that $\{\wedge, \neg\}$ is *functionally complete*, meaning that any boolean truth function can be expressed as the composition of conjunctions and negations. In particular,

<footnote n="2">² Not to be confused with the name given to instances of the *cut rule* in sequent calculus.</footnote>
<figure><img src="image_3.png" /><figcaption>■ **Figure 1** Proof of the law of excluded middle in Alpha</figcaption></figure>

the symbolic definitions of *falsehood* $\perp \triangleq \neg \top$, classical *disjunction* $A \vee B \triangleq \neg(\neg A \wedge \neg B)$ and classical *implication* $A \supset B \triangleq \neg(A \wedge \neg B)$ can be expressed by the following three graphs:

<figure><img src="image_4.png" /></figure>

Thus one can easily encode any propositional formula into a classically equivalent graph. Conversely, one can translate any graph into a classically equivalent formula, as has been shown for instance in [53]. In fact, there are usually many possible formula readings of a given graph. One reason is that juxtaposition of graphs is a *variadic* operation, as opposed to conjunction of formulas which is *dyadic*: thus formulas that only differ up to *associativity* are associated to the same graph. Also, thanks to the topological nature of SA, juxtaposition is naturally *commutative*: the locations of two juxtaposed graphs do not matter, as long as they live in the same area delimited by a *cut*. The combination of these properties is called the *isotropy* of SA in [39], and is captured in traditional proof theory through the use of (multi)sets for modelling contexts in sequents.

**Illative transformations** In order to have a proof system, one needs a collection of inference rules for deducing true statements from other true statements. In Alpha, inference rules are implemented by what Peirce called *illative transformations* on graphs. In modern terminology, they correspond to *rewriting* rules that can be applied to any *subgraph*. By measuring the depth of a *subgraph* as the number of *cuts* in which it is enclosed, we thus have that the rules of Alpha are applicable on *subgraphs* of arbitrary depth. This makes Alpha deserving of the title of *deep inference* system.

Figure 1 shows a proof of the law of excluded middle $a \vee \neg a$ in Alpha. The first step consists in applying the illative transformation of Iteration to erase the subgraph (a). More generally, Iteration allows to erase any subgraph G as long as G already occurs “higher” in SA, i.e. in an area that encloses the erased occurrence of G. The second step of Insertion allows to erase the other occurrence of (a) because it is scribed in a *negative* area, i.e. an area enclosed in an *odd* number of cuts — 1 in this case<fnref n="3" />. The last step of Double-cut allows to collapse the two remaining cuts, because there is nothing but empty space in between them. This leaves us with the empty SA, having thus reduced the initial goal to trivial truth.

<footnote n="3">³ It might be quite confusing that we call “Insertion” a transformation that *erases* information. This is because we use Peirce’s original terminology, despite the fact that we adopt a *backward* reading of rules where the conclusion that we want to prove is reduced to a sufficient premiss.</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 2 From scrolls to flowers</figcaption></figure>

### 3 Flowers

**The scroll** In [49, pp. 533–535], Peirce explains that he did not immediately come up with the idea of juxtaposition and cuts as diagrammatizations of conjunction and negation. Instead, they arose as the natural development of a more primitive icon that he called the *scroll*. Figure 2a shows Peirce’s drawing of the *scroll* as it appears in [49, Fig. 5]. He defines its intended meaning as that of a “conditional de inesse”, which corresponds to the material implication of classical logic. Then the *graph* of Figure 2a is interpreted as the formula $(A \wedge B) \supset (C \wedge D)$. This agrees with the encoding of implication given in Section 2, if one sees the outer boundary enclosing the antecedent *A B* and the inner boundary enclosing the consequent *C D* as nested *cuts*.

It is no coincidence that Peirce based his most fundamental icon on implication: according to Lewis [33, p. 79], he was the one who introduced the “illative relation” of implication into symbolic logic in the first place, by giving it a distinguished symbol and studying extensively the algebraic laws that govern it (e.g. Peirce’s law $$((A \supset B) \supset A) \supset A)$$.

**The *n*-ary *scroll*** In order to interpret the *scroll* as an *intuitionistic implication*, Oostra proposed in [45] to reify the *scroll* as a primitive icon of EGs, distinguished from the nesting of two *cuts*. In fact he went further, by generalizing both the *cut* and the *scroll* into an *n*-ary construction called the *curl*, where *n* is the number of inner boundaries, called *loops*. Figure 2b shows an example of *curl* with five *loops*, where the unique intersection points between inner and outer boundaries are highlighted in *orange*^4. In [39], the *curl* is simply called *n-ary scroll*, the outer boundary *outloop*, and the inner boundaries *inloops*. Then *cuts* and *rolls* are indeed special cases of *n*-ary *rolls*, respectively with *n* = 0 and *n* = 1.

Like the unary *roll*, the *n*-ary *roll* is to be read as an implication whose antecedent is the content of the *outloop*, and consequent the content of the *inloops*. The generalization consists in taking the *disjunction* of the contents of all *inloops*: this reflects nicely the etymological meaning of the word “disjunction”, since the *inloops* enclose *disjoint* areas of the *outloop* to which they are attached. Then the 5-ary *roll* of Figure 2b can be read as the formula $a \supset (b \vee c \vee d \vee e \vee f)$; and the 0-ary *roll* obtained by removing all *inloops* from the latter as $a \supset \bot$, since a 0-ary *disjunction* is naturally evaluated to its neutral element $\bot$. This coincides with the intuitionistic reading of *negation* $\neg A \triangleq A \supset \bot$.

<footnote>^4 We also shade the negative area delimited by the outer boundary in *gray*.</footnote>
<figure><img src="image_6.png" /><figcaption>■ **Figure 3** Continuity, disjunction and implication in intuitionistic EGs</figcaption></figure>

**Continuity** With this interpretation of the *n*-ary *scroll*, the *Alpha* encodings of disjunction and implication as nested *cuts* given in Section 2 are no longer valid, because they are not intuitionistically equivalent to the associated binary and unary *scrolls*. This is illustrated in Figure 3, where the closeness in meaning is reflected iconically (but not symbolically) in the fact that the *graphs* only differ in the *continuity* (or lack thereof) between inloops and their outloop.

► **Remark 3.1.** This might be related to other manifestations of the notion of continuity in the semantics of intuitionistic logic, such as the well-known Stone-Tarski interpretation of formulas as topological spaces [56], and the interpretation of proofs as continuous maps in the *denotational semantics* of Dana Scott<fnref n="5" /> [1].

**Blooming** In terms of ergonomy, the *n*-ary *scroll* has one notable flaw, also shared with the classical *cut*-based syntax: it quickly induces heavy nestings of curves in the plane, making even relatively simple *graphs* hard to read for an untrained eye. Our solution is to turn *inloops inside-out*, as illustrated in Figure 2c. In this way, we effectively divide the amount of curve-nesting in *rolls* by two. And as an added bonus, the new icon is reminiscent of a *flower*, as if it had bloomed from its curled bud; or as if the pistol cylinder from Figure 2b had transformed into a *pistil*, and its bullet chambers into *petals*.

From that point onwards, we chose to fully embrace the flower metaphor: first in our drawing style as witnessed in Figure 2d, but also in our syntactic terminology, to be introduced in the next pages. Negative (resp. positive) *outloops* are now drawn as *yellow* (resp. *white*) pistils for a slightly more colorful experience, and *inloops* as transparent petals, i.e. of the same color as the area on which they are scribed.

## 4 Gardens

**Lines of identity** To express first-order quantification, Peirce introduced in *Beta* the icon of *lines of identity* (LoIs). In short, the usual binders and variables of predicate calculus are replaced by *lines* that connect the occurrences of bound variables in predicate arguments to their binding point. For instance, the formulas $∃x.P(x) ∧ Q(x)$ and $∀x.R(x) ⊃ S(x)$ can be represented in *Beta* by the *graphs* of Figure 4a.

The kind of quantification is determined by the location of the binding point, which is taken to be the *outermost point* in the line: if it is in a *positive area* as in the upper graph,

<footnote n="5">⁵ Before the advent of Oostra’s intuitionistic EGs, Zalamea gave a detailed analysis of Peirce’s philosophy of the *continuum*, how it relates to modern developments in mathematics, and how it is embodied in EGs [65]. Actually according to Oostra [48, p. 162], “the possibility of developing intuitionistic existential graphs was first suggested by Zalamea in the 1990s [63, 64]”.</footnote>
<figure><img src="image_7.png" /><figcaption>■ **Figure 4** From LoIs to variables</figcaption></figure>

then the quantifier is *existential*; otherwise if it is in a *negative* area as in the lower graph,
the quantifier is *universal*. This is justified by De Morgan's laws: the lower graph can also
be read as the classically equivalent formula $\neg \exists x.R(x) \wedge \neg S(x)$.

**Intuitionistic quantification** In intuitionistic logic however, De Morgan’s laws do not hold anymore. Thus in the flower calculus we need a different way to interpret LoIs as quantifiers. Our key insight is to adopt a polarity-invariant viewpoint: a LoI now has existential (resp. universal) force when its outermost point is located in a petal (resp. pistil). In particular, this implies that LoIs cannot occur at the top-level of SA anymore, but only inside flowers. Thus the two previous Beta graphs are transformed into the single-petal flowers of Figure 4b.

**Variables** Quine experimented with a notation similar to LoIs, but deemed it “too cumbersome for practical use” [51, p. 125]. While his lines connected locations inside symbolic formulas written in linear notation, it is true that having a line for each occurrence of bound variable can quickly lead to unreadable diagrams ridden with overlapping lines. This is not a problem in the context of Peirce’s work, because his aim was “to separate [relational] reasoning into its smallest steps, [...] not to facilitate reasoning, but to facilitate the study of reasoning” [51, p. 111]; and recent formalizations of the algebra of LoIs in category theory support the pertinence of Peirce’s approach [26, 6].

However, keeping in mind our goal of laying the basis for a calculus well-suited to practical reasoning in ITPs, we chose to replace LoIs by a more traditional syntax based on binders and variables. The idea is to substitute every LoI with a variable *binder* scribed in the area of its outermost point, so that the two *flowers* of Figure 4b transform into those of Figure 4c. Areas delimited by pistils and petals now comprise both *flowers* and binders, which can be seen metaphorically as *sprinklers* that irrigate the leaves (atomic predicates) of flowers through invisible LoIs, imagined as underground hoses. Hence we call these areas *gardens*.
<table><thead><tr><th>Kind</th><th>Letters</th></tr></thead><tbody><tr><td>Variables (<i>V</i>)</td><td><i>x</i>, <i>y</i>, <i>z</i></td></tr><tr><td>Flowers (<i>F</i>)</td><td><i>φ</i>, <i>ψ</i>, <i>ξ</i></td></tr><tr><td>Gardens (<i>G</i>)</td><td><i>γ</i>, <i>δ</i></td></tr><tr><td>Sprinklers</td><td><b>x</b>, <b>y</b>, <b>z</b></td></tr><tr><td>Variable vectors</td><td><b>x̄</b>, <b>ȳ</b>, <b>z̄</b></td></tr><tr><td>Substitutions</td><td><i>σ</i>, <i>τ</i></td></tr><tr><td>Bouquets</td><td><i>Φ</i>, <i>Ψ</i>, <i>Ξ</i></td></tr><tr><td>Corollas</td><td><i>Γ</i>, <i>Δ</i></td></tr><tr><td>Contexts</td><td><i>Φ̂</i>, <i>Ψ̂</i>, <i>Ξ̂</i></td></tr><tr><td>Theories</td><td><i>Γ</i>, <i>U</i></td></tr></tbody></table>

(a) Conventions for meta-variables

<figure><img src="image_8.png" /><figcaption>Figure 5 Notations</figcaption></figure>

$$x_1, x_2 \cdot p(x_1, x_2) \sqcup y_1 \cdot q(x_1, y_1), (r(x_2) \sqcup s(y_1)); y_2 \cdot q(x_2, y_2)$$

<figure><img src="image_9.png" /></figure>

$$\forall x_1 \forall x_2 (p(x_1, x_2) \supset (\exists y_1 q(x_1, y_1) \land (r(x_2) \supset s(y_1))) \lor (\exists y_2 q(x_2, y_2)))$$

(b) Interpreting flowers

## 5 Syntax

We are now going to distill the syntactic essence of flowers into an inductive, (multi)set-based data structure. This will allow for a more compact textual notation, that is better suited to proof-theoretical study. We previously illustrated how flowers allow to represent purely relational statements without function symbols. Since functions are just deterministic relations, one can in principle formalize any first-order theory in this syntax<fnref n="6" />.

**Definition 5.1.** A first-order signature is a pair $\Sigma = (\mathcal{P}, \mathcal{ar})$, where $\mathcal{P}$ is the countable set of predicate symbols of $\Sigma$, and $\mathcal{ar} : \mathcal{P} \to \mathbb{N}$ gives an arity to each symbol.

In the following, we fix a countable set of variables $\mathcal{V}$ and a first-order signature $\Sigma$.

**Definition 5.2.** The sets of flowers $\mathcal{F}$ and gardens $\mathcal{G}$ are defined by mutual induction:

**Atom** If $p \in \mathcal{P}$ and $\vec{x} \in \mathcal{V}^{ar}(p)$, then $p(\vec{x}) \in \mathcal{F}$;

**Garden** If $\mathbf{x} \subset \mathcal{V}$ is a finite set and $\Phi \subset \mathcal{F}$ a finite multiset, then $\mathbf{x} \cdot \Phi \in \mathcal{G}$;

**Flower** If $\gamma \in \mathcal{G}$ and $\Delta \subset \mathcal{G}$ is a finite multiset, then $\gamma \sqcup \Delta \in \mathcal{F}$.

Similarly to nested sequents, the syntax of flowers $\phi, \psi$ and gardens $\gamma, \delta$ can be expressed succinctly with the following grammar:

$$\phi, \psi ::= p(x_1, \dots, x_n) \mid \gamma \sqcup \delta_1; \dots; \delta_n$$

$$\gamma, \delta ::= x_1, \dots, x_n \cdot \phi_1, \dots, \phi_n$$

Building on our botanical metaphor, any finite set $\mathbf{x} \subset \mathcal{V}$ of variables is called a *sprinkler*, finite multiset $\Phi \subset \mathcal{F}$ of flowers a *bouquet*, and finite multiset $\Gamma \subset \mathcal{G}$ of gardens a *corolla*. Following the grammar presentation, we will often write gardens as $x_1, \dots, x_n \cdot \phi_1, \dots, \phi_m$, where the $x_i$ are called *binders*; and non-atomic flowers as $\gamma \sqcup \delta_1; \dots; \delta_n$, where $\gamma$ is the *pistil* and the $\delta_i$ are the *petals*. We write $\{E_i\}_i^n$ to denote a finite (multi)set of size $n$ with elements $E_i$ indexed by $1 \le i \le n$. We also omit writing the empty (multi)set, accounting for it with blank space as is done in sequent notation; in particular, $\cdot$ stands for the empty garden $\emptyset \cdot \emptyset$, $\gamma \sqcup \delta$ for the flower with no petals $\gamma \sqcup \delta$, and $\gamma \sqcup \cdot$ for the flower with one empty petal.

<footnote n="6">⁶ Conversely, every relation can be faithfully encoded as its characteristic function, which is the basis for the formalization of mathematics in *type theories*.</footnote>
Note that the order of precedence of operators is, $<, >, ;, <, D$: this is illustrated in Figure 5b, where a flower expression is parsed into the corresponding flower drawing, and then translated as a formula. Also to improve readability, we will most of the time omit the garden dot `.` when the sprinkler is empty, writing $\Phi$ instead of $\cdot \Phi$.

**Remark 5.3.** In some places the choice of letter for meta-variables will be important to disambiguate the kind of syntactic object we denote. Table 5a summarizes our chosen notational conventions in this respect.

We now proceed with routine definitions for handling variables.

**Definition 5.4.** The sets of free variables $fv(-)$ and bound variables $bv(-)$ of a flower/bouquet/garden are defined recursively by:

$$fv(p(\vec{x})) = \vec{x} \qquad fv(\Phi) = \bigcup_{\phi \in \Phi} fv(\phi) \qquad fv(\mathbf{x} \cdot \Phi) = fv(\Phi) \setminus \mathbf{x}$$

$$fv(\mathbf{x} \cdot \Phi \ D \ \Delta) = fv(\mathbf{x} \cdot \Phi) \cup \bigcup_{\mathbf{y} \cdot \Psi \in \Delta} fv(\mathbf{x}, \mathbf{y} \cdot \Psi)$$

$$bv(p(\vec{x})) = \emptyset \qquad bv(\Phi) = \bigcup_{\phi \in \Phi} bv(\phi) \qquad bv(\mathbf{x} \cdot \Phi) = \mathbf{x} \cup bv(\Phi) \qquad bv(\gamma \ D \ \Delta) = bv(\gamma) \cup \bigcup_{\delta \in \Delta} bv(\delta)$$

To avoid reasoning about $\alpha$-equivalence, we adopt in this work the so-called *Barendregt convention* that all variable binders are distinct, both among themselves and from free variables. Formally, we assume that for any *bouquet* $\Phi$ the two following conditions hold:

1. computing $bv(\Phi)$ as a multiset gives the same result as computing it as a set;

2. $bv(\Phi) \cap fv(\Phi) = \emptyset$.

To define substitutions, we introduce a general notion of *function update*, which will be useful for the semantic evaluation of *flowers* in Section 7.

**Definition 5.5.** Let $A, B$ be two sets, $f, g: A \to B$ two functions and $R \subseteq A$ some subset of their domain. The update of $f$ on $R$ with $g$ is the function defined by:

$$(f|_R g)(x) = \begin{cases} g(x) & \text{if } x \in R \\ f(x) & \text{otherwise} \end{cases}$$

— $|_-$ — is left-associative, that is $f|_R g|_S h = (f|_R g)|_S h$. Also if $f$ or $g$ is the identity function 1 we omit writing it, i.e. $f|_R = f|_R 1$ and $|_R g = 1|_R g$.

**Definition 5.6.** A substitution is a function $\sigma: \mathcal{V} \to \mathcal{V}$ with a finite support $\text{supp}(\sigma) = \{x | \sigma(x) \neq x\}$. We write $\sigma: \mathbf{x}$ to denote a substitution $\sigma$ whose support is $\mathbf{x}$. The domain of substitutions is extended to flowers, bouquets and gardens mutually recursively by:

$$\sigma(p(x_1, \dots, x_n)) = p(\sigma(x_1), \dots, \sigma(x_n)) \qquad \sigma(\phi_1, \dots, \phi_n) = \sigma(\phi_1), \dots, \sigma(\phi_n)$$

$$\sigma(\mathbf{x} \cdot \Phi) = \mathbf{x} \cdot \sigma|_{\mathbf{x}}(\Phi) \qquad \sigma(\mathbf{x} \cdot \Phi \ D \ \delta_1; \dots; \delta_n) = \sigma(\mathbf{x} \cdot \Phi) \ D \ \sigma|_{\mathbf{x}}(\delta_1); \dots; \sigma|_{\mathbf{x}}(\delta_n)$$

We say that a *substitution* $\sigma: \mathbf{x}$ is capture-avoiding in a *bouquet* $\Phi$ if $\sigma(\mathbf{x}) \cap bv(\Phi) = \emptyset$.
<figure><img src="image_10.png" /><figcaption>(a) Cross-pollination</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>(b) Self-pollination</figcaption></figure>

<caption>Figure 6 Pollination in flowers</caption>

# 6 Calculus

Equipped with an inductive syntax, we can now express formally the inference rules of the flower calculus. First we need a notion of context to apply rules at arbitrarily deep locations:

**► Definition 6.1 (Context).** Contexts $\hat{\Phi}$ are defined inductively by the following grammar:

$$ \hat{\Phi}, \hat{\Psi}, \hat{\Xi} ::= \Psi, \hat{\phi} \qquad \hat{\phi}, \hat{\psi}, \hat{\xi} ::= \Box | \mathbf{x} \cdot \hat{\Phi} \Box \Delta | \gamma \Box \mathbf{x} \cdot \hat{\Phi}; \Delta $$

Informally, a context can be seen as a *bouquet* with exactly one occurrence of a special flower □ called its hole. The filling of a context $\hat{\Phi}$ with a *bouquet* $\Psi$ (resp. context $\hat{\Psi}$) is the *bouquet* $\hat{\Phi}\{\Psi\}$ (resp. context $\hat{\Phi}\{\hat{\Psi}\}$) equal to $\hat{\Phi}$ where □ has been substituted with $\Psi$ (resp. $\hat{\Psi}$).

**► Definition 6.2 (Polarity).** The number of inversions $\mathrm{inv}(\hat{\Phi})$ of a context $\hat{\Phi}$ is:

$$ \mathrm{inv}(\Box) = 0 \qquad \mathrm{inv}(\Psi, \hat{\phi}) = \mathrm{inv}(\hat{\phi}) \qquad \mathrm{inv}(\mathbf{x} \cdot \hat{\Phi} \Box \Delta) = 1 + \mathrm{inv}(\hat{\Phi}) \qquad \mathrm{inv}(\gamma \Box \mathbf{x} \cdot \hat{\Phi}; \Delta) = \mathrm{inv}(\hat{\Phi}) $$

We say that a context $\hat{\Phi}$ is positive if $\mathrm{inv}(\hat{\Phi})$ is even, and negative otherwise. We denote positive and negative contexts respectively by $\hat{\Phi}^+$ and $\hat{\Phi}^-$.

In order to formulate the equivalent of the Iteration rule of EGs for flowers, we introduce a pollination relation that captures the availability of a flower in a given context:

**► Definition 6.3 (Pollination).** We say that a flower $\phi$ can be pollinated in a context $\hat{\Phi}$, written $\phi \succ \hat{\Phi}$, when there exists a *bouquet* $\Psi$ with $\phi \in \Psi$ and contexts $\hat{\Xi}$ and $\hat{\Xi}_0$ s.t. either:

**Cross-pollination** $\hat{\Phi} = \hat{\Xi}\{\Psi, \hat{\Xi}_0\}$;

**Self-pollination** $\hat{\Phi} = \hat{\Xi}\{\mathbf{x} \cdot \Psi \Box \mathbf{y} \cdot \hat{\Xi}_0; \Delta\}$ for some $\mathbf{x}, \mathbf{y}, \Delta$.

A *bouquet* $\Phi$ can be pollinated in $\hat{\Phi}$, written $\Phi \succ \hat{\Phi}$, if $\phi \succ \hat{\Phi}$ for all $\phi \in \Phi$.

Figure 6 illustrates the meaning of pollination as a relation of justification between locations: the blue dot marks the location of the justifying/pollinating occurrence of $\phi$, and the red dots all the areas that it justifies/pollinates, and thus where $\phi$ is available for use. We distinguish two cases of cross-pollination and self-pollination, as botanists do when describing the reproduction of flowers. This distinction does not exist in classical EGs, because pistils and petals are both identified as instances of cuts<fnref n="7" />.

<footnote n="7">⁷ The same phenomenon is at work in SFL: cross-pollination and self-pollination can be seen as generalizing the *forward* and *backward* interaction connectives $\Box$ and $\triangleright$ of intuitionistic SFL [13, 21], while the</footnote>
<figure><img src="image_12.png" /><figcaption>**Figure 7** Rules of the flower calculus</figcaption></figure>

**Remark 6.4.** Incidentally, the pollination relation also explains the scope of variables. Indeed, one can interpret red dots in Figure 6 as the allowed usage points for the variable bound at the linked blue dot. This hints at a possible type-theoretic variant of the flower calculus where variables are also used for higher-order individuals, including flowers.

**Proofs** The inference rules of the flower calculus are presented in Figure 7. Read from top to bottom, they correspond to traditional inference rules deducing a necessary conclusion from a valid premiss. But we will prefer their backward, bottom-up reading: then they can be seen as rewriting rules that reduce a goal to a sufficient premiss, just like in our illustration of the illative transformations of EGs in Figure 1. Also, all rules manipulate bouquets: this is seen more clearly in the graphical presentation of the rules in appendix (Figures 8 and 9).

We partition the rules into two sets: the *natural* rules denoted by $\mathring{\leq}$ that apply in arbitrary contexts, and the *cultural* rules denoted by $\mathring{\ll}$ that apply exclusively in positive or negative contexts. In particular, every $\mathring{\leq}$-rule is both *analytic* (i.e. every atom in the premiss already appears in the conclusion) and *invertible* (Lemma B.17); on the contrary, all $\mathring{\ll}$-rules are *non-invertible*, and they will be shown to be *admissible* in Section 8.

**Definition 6.5 (Derivation).** Given a set of rules $R$, we write $\Phi \to_R \Psi$ to indicate a rewrite step in $R$, that is an instance of some $r \in R$ with $\Psi$ as premiss and $\Phi$ as conclusion. We

<footnote>original formulation of SFL for classical linear logic had only one interaction connective $\mathring{\leq}$ [12]. Through the Curry-Howard-Lambek correspondence, this is also reminiscent of the adjunction between products (○) and exponentials (▷) in cartesian closed categories, as opposed to the natural isomorphism $(-)^*$ of $*$-autonomous categories.</footnote>
just write $\Phi \to \Psi$ to mean $\Phi \to \mathcal{U} \prec \Psi$. A derivation $\Phi \to_R^n \Psi$ is a sequence of rewrite steps $\Phi_0 \to_R \Phi_1 \dots \to_R \Phi_n$ with $\Phi_0 = \Phi$, $\Phi_n = \Psi$ and $n \ge 0$. Generally the length $n$ of the derivation does not matter, and we just write $\Phi \to_R^* \Psi$. Finally, natural derivations are closed under arbitrary contexts: for every context $\hat{\Xi}$, $\Phi \to_\Xi \Psi$ implies $\hat{\Xi}\{\Phi\} \to_\Xi \hat{\Xi}\{\Psi\}$. We write $\Phi \to_\Xi \Psi$ to denote a shallow natural step, i.e. an instance of a $\mathcal{N}$-rule in the empty context $\square$.

**Definition 6.6 (Proof).** A proof of a bouquet $\Phi$ is a derivation $\Phi \to^* \emptyset$.

In Peircean terms, the empty *bouquet* is the blank SA. Then proving a *bouquet* amounts to erasing it completely from SA, thus reducing it to trivial truth as in Figure 1. Figure 10 in appendix shows an example of $\mathcal{N}$-proof in the flower calculus, both in textual and graphical syntax. Note that we used a non-duplicating version of the rules *ipis* and *ipet*, in order to save some space in the graphical presentation.

If we want to reason about *relative* truth, i.e. $\Phi$ is true under the assumption that $\Psi$ is, we can simply rely on the existence of a *derivation* $\Phi \to^* \Psi$ in the full flower calculus. This will be justified by the soundness of all rules (Theorem B.20) as well as a *strong* completeness result (Corollary 8.8), that relies on the following strong deduction theorem:

**Theorem 6.7 (Strong deduction).** $\Phi \to^* \Psi$ if and only if $\Psi \sqsupset \Phi \to^* \emptyset$.

Contrary to full derivability, *natural derivability* $\Phi \to^*_\Xi \Psi$ is too weak to satisfy a strong deduction theorem. This is a consequence of the fact that $\mathcal{N}$-rules are *invertible*, and thus can only relate *equivalent bouquets*. Indeed, as soon as $\Psi \sqsupset \Phi$ is $\mathcal{N}$-provable but the converse $\Phi \sqsupset \Psi$ is not, it follows from the completeness of $\mathcal{N}$-rules that $\Phi$ and $\Psi$ are not *equivalent*: thus $\Phi \to^*_\Xi \Psi$, contradicting the strong deduction statement.

A trivial way to circumvent this is to define directly the relation of *hypothetical provability* $\Psi \vdash \Phi$ as $\Psi \sqsupset \Phi \to^* \emptyset$. This is closer to what one would find in sequent calculus, where hypothetical proofs are closed derivations of hypothetical sequents, not open derivations. The difference is that sequents capture only the *first-order*<fnref n="8" /> implicative structure of logic, while flowers capture the full structure of intuitionistic FOL. This allows for a nice generalization of the notion of hypothetical provability, which will be useful in our completeness proof:

**Definition 6.8.** We say that $\Phi$ is hypothetically provable from $\Psi$ in a fragment R of rules, written $\Psi \vdash_R \Phi$, if $\hat{\Xi}\{\Phi\} \to_R^* \hat{\Xi}\{\emptyset\}$ for every context $\hat{\Xi}$ such that $\Psi \succ \hat{\Xi}$. We write $\Psi \vdash \Phi$ to denote hypothetical provability in the full flower calculus.

**Theorem 6.9 (Deduction).** $\Psi \vdash_\Xi \Phi$ if and only if $\vdash_\Xi \Psi \sqsupset \Phi$.

# 7 Semantics

We now give a semantics to flowers in Kripke structures. We recall the standard definitions:

**Definition 7.1.** A first-order structure is a pair $(M, [\cdot|])$ where $M$ is a non-empty set called the domain, and $[\cdot|]$ is a map called the interpretation that associates to each predicate symbol $p \in \mathcal{P}$ a relation $[[p]] \subseteq M^{ar(p)}$.

**Definition 7.2.** A Kripke structure is a triplet $\mathcal{K} = (W, \leq, (M_w)_{w \in W})$, where $W$ is the set of worlds, $\leq$ is a pre-order on $W$ called accessibility, and $(M_w)_{w \in W}$ is a family of first-order structures indexed by $W$. Furthermore, we require the following monotonicity conditions to hold whenever $w \leq w'$: 1. $M_w \subseteq M_{w'}$; 2. for every $p \in \mathcal{P}$, $[[p]]_w \subseteq [[p]]_{w'}$.

<footnote n="8">⁸ As opposed to *higher-order*, in the sense of having negatively nested implications.</footnote>
**► Definition 7.3.** Given a Kripke structure $K$ and a world $w$ in $K$, a w-evaluation is a function $e: \mathcal{V} \to M_w$. The interpretation map of $M_w$ is extended to variables and substitutions with respect to any w-evaluation $e$ as follows:

$$ \llbracket x \rrbracket_e = e(x) \qquad \llbracket \sigma \rrbracket_e(x) = \llbracket \sigma(x) \rrbracket_e $$

The crux of Kripke semantics is the forcing relation, that captures the truth-conditions of statements in Kripke structures. While it is usually defined on formulas, here we adapt the definition to flowers, which in our opinion makes it simpler and more uniform since flowers can be seen as built from essentially one big constructor:

**► Definition 7.4.** The depth $|-|$ of a flower/garden is defined by mutual recursion:

$$ |p(\vec{x})| = 0 \qquad |\mathbf{x} \cdot \Phi| = \max_{\phi \in \Phi} |\phi| \qquad |\gamma \sqcup \Delta| = 1 + \max(|\gamma|, \max_{\delta \in \Delta} |\delta|) $$

**► Definition 7.5.** Given some Kripke structure $K$, the forcing relation $w \Vdash \phi [e]$ between a world $w$, a flower $\phi$ and a w-evaluation $e$ is defined by induction on $|\phi|$ as follows:

*Atom* $w \Vdash p(\vec{x})$ [e] iff $\llbracket \vec{x} \rrbracket_e \in \llbracket p \rrbracket_w$;

*Flower* $w \Vdash \mathbf{x} \cdot \Phi \sqcup \{\mathbf{x}_i \cdot \Phi_i\}_{i=1}^n$ [e] iff for every $w' \ge w$ and every $w'$-evaluation $e'$, if $w' \Vdash \Phi$ [$e|_x e'$] then there is some $1 \le i \le n$ and $w'$-evaluation $e''$ such that $w' \Vdash \Phi_i$ [$e|_x e'|_{x_i e''}$].

*Bouquet* $w \Vdash \Phi$ [e] iff $w \Vdash \phi$ [e] for every $\phi \in \Phi$.

Lastly, we define the notion of semantic entailment $\Phi \Vdash \Psi$ on bouquets, mirroring the syntactic entailment $\Phi \vdash \Psi$ of the last section:

**► Definition 7.6.** Let $K$ be a Kripke structure, and $\Phi, \Psi$ some bouquets. We say that $\Phi$ semantically entails $\Psi$ in $K$, written $\Phi \Vdash_K \Psi$, when $w \Vdash \Phi$ [e] implies $w \Vdash \Psi$ [e] for every world $w \in W$ and w-evaluation $e$. This entailment is valid if it holds for any Kripke structure $K$, and in that case we simply write $\Phi \Vdash \Psi$. We say that $\Phi$ is semantically equivalent to $\Psi$, written $\Phi \models \Psi$, when $\Phi \Vdash \Psi$ and $\Psi \Vdash \Phi$.

## 8 Completeness

We now outline a direct completeness proof for the natural fragment $\mathcal{N}$ of the flower calculus: every true flower $\phi$ is naturally provable, i.e. $\Vdash \phi$ implies $\Vdash_{\mathcal{N}} \phi$. Since this fragment is analytic, we cannot reuse most completeness proofs from the literature, because they usually rely on a non-analytic principle like the cut rule of sequent calculus. Our insight was to adapt techniques from the semantic cut-elimination proof given by Hermant in [27], which is nonetheless relatively close to the original completeness proof of Gödel. A novelty of our proof is that it dispenses completely with the need for Henkin witnesses.

First we need to generalize our notions of syntactic and semantic entailment to possibly infinite sets of flowers, so-called theories:

**► Definition 8.1.** Any set $\mathcal{T} \subseteq \mathbb{F}$ of flowers is called a theory. In particular, a bouquet can be regarded as a finite theory, by forgetting the number of repetitions of its elements. We say that a bouquet $\Phi$ is provable from a theory $\mathcal{T}$, written $\mathcal{T} \Vdash \Phi$, if there exists a bouquet $\Psi \subseteq \mathcal{T}$ such that $\Psi \Vdash \Phi$. Given a Kripke structure $K$, a world $w$ in $K$ and a w-evaluation $e$, we say that $\mathcal{T}$ is forced by $w$ under $e$, written $w \Vdash \mathcal{T}$ [e], if $w \Vdash \phi$ [e] for all $\phi \in \mathcal{T}$. Then $\Phi$ is a consequence of $\mathcal{T}$, written $\mathcal{T} \Vdash_K \Phi$, if $w \Vdash \mathcal{T}$ [e] implies $w \Vdash \Phi$ [e] for every world $w$ in $K$ and w-evaluation $e$.
**► Definition 8.2.** A theory $\mathcal{T}$ is said to be $\psi$-consistent when $\mathcal{T} \Vdash_{\mathcal{T}} \psi$, and $\psi$-complete when for all $\phi \in \mathbb{F}$, either $\mathcal{T}, \phi \vdash_{\mathcal{T}} \psi$ or $\phi \in \mathcal{T}$.

Intuitively, a theory $\mathcal{T}$ is $\psi$-consistent when one cannot deduce $\psi$ from it, and $\psi$-complete when it decides any formula $\phi$ relatively to $\psi$. This is better understood by considering the special case where $\psi = (\mathbb{D})$ is the *absurd flower*: then consistency means that one cannot derive any contradiction from $\mathcal{T}$; and completeness that $\mathcal{T}$ either *refutes* $\phi$ syntactically with a proof of $\Phi$, $\phi \mathbb{D} (\mathbb{D})$ for some $\Phi \subseteq \mathcal{T}$, or already *validates* it “semantically”, i.e. without the need for a proof since $\phi \in \mathcal{T}$.

The next two propositions constitute the central argument that allows the completeness proof to go through despite the analyticity of $\mathcal{R}$-rules. They are a direct adaptation of [27, Proposition 7], which Hermant identifies as “an important property of any A-consistent, A-complete theory, [...] that it enjoys some form of the subformula property”.

Roughly, the first proposition captures the intuitionistic truth-conditions that make a flower valid (i.e. true in every model) by modelling them on material implication, just like Peirce would do with his *scroll* (see Section 3): $\phi$ is true if the content $\Phi_i$ of one of its petals (consequents) is, or if the content $\Phi$ of its pistil (antecedent) is not.

**► Proposition 8.3 (Analytic truth).** Let $\psi \in \mathbb{F}$, $\mathcal{T}$ some $\psi$-consistent and $\psi$-complete theory, and $\phi = \mathbf{x} \cdot \Phi \mathbb{D} \Delta$ with $\Delta = \{\delta_i\}_i^n = \{\mathbf{x}_i \cdot \Phi_i\}_i^n$ such that $\phi \in \mathcal{T}$. Then for every substitution $\sigma : \mathbf{x}$, either $\sigma(\Phi_i) \subseteq \mathcal{T}$ for some $1 \le i \le n$, or $\mathcal{T} \Vdash_{\mathcal{T}} \sigma(\Phi)$.

**Proof.** Suppose the contrary, i.e. there is a substitution $\sigma$ such that $\mathcal{T} \vdash_{\mathcal{T}} \sigma(\Phi)$ and for all $1 \le i \le n$, there is some $\phi_i \in \Phi_i$ \textcircled{1} such that $\sigma(\phi_i) \notin \mathcal{T}$. Thus by $\psi$-completeness of $\mathcal{T}$, we get $\mathcal{T}, \sigma(\phi_i) \vdash_{\mathcal{T}} \psi$. So there are $\Psi \subseteq \mathcal{T}$ and $\Psi_i \subseteq \mathcal{T} \cup \sigma(\phi_i)$ such that $\Psi \vdash_{\mathcal{T}} \sigma(\Phi)$ \textcircled{2} and $\Psi_i \vdash_{\mathcal{T}} \psi$ \textcircled{3}. Now it cannot be the case that $\Psi_i \subseteq \mathcal{T}$, otherwise by weakening and $\psi$-consistency of $\mathcal{T}$ we would have $\Psi_i \Vdash_{\mathcal{T}} \psi$. So there must exist $\Psi'_i \subseteq \mathcal{T}$ such that $\Psi_i = \Psi'_i \cup \sigma(\phi_i)$ \textcircled{4}. Again by weakening and $\psi$-consistency of $\mathcal{T}$, we get $\Psi, \cup_{i=1}^n \Psi'_i, \phi \Vdash_{\mathcal{T}} \psi$. Now we derive a contradiction by showing $\Psi, \cup_{i=1}^n \Psi'_i, \phi \Vdash_{\mathcal{T}} \psi$. Let $\hat{\Xi}$ be a context such that $\Psi, \cup_{i=1}^n \Psi'_i, \phi \Vdash_{\mathcal{T}} \hat{\Xi}$ \textcircled{5}. Then $\hat{\Xi}\{\psi\} \to_{\mathcal{T}}^* \hat{\Xi}\{\}\}$ with the following derivation:

$$
\begin{align*}
\hat{\Xi}\{\psi\} & \to_{\text{epis}} \hat{\Xi}\{\cdot \mathbb{D} \cdot \psi\} \\
\to_{\text{poll}\uparrow} & \hat{\Xi}\{\cdot \phi \mathbb{D} \cdot \psi\} \tag{5} \\
\to_{\text{ipis}} & \hat{\Xi}\{\cdot (\cdot \sigma(\Phi) \mathbb{D} \sigma(\Delta)), \phi \mathbb{D} \cdot \psi\} \\
\to_{\text{poll}\downarrow} & \hat{\Xi}\{\cdot (\cdot \mathbb{D} \sigma(\Delta)), \phi \mathbb{D} \cdot \psi\} \tag{2, 5} \\
\to_{\text{srep}} & \hat{\Xi}\{\cdot \phi \mathbb{D} \cdot \{\sigma(\delta_i) \mathbb{D} \cdot \psi\}_i^n\} \\
= & \hat{\Xi}\{\cdot \phi \mathbb{D} \cdot \{\mathbf{x}_i \cdot \sigma(\Phi_i) \mathbb{D} \cdot \psi\}_i^n\} \\
\to_{\text{poll}\downarrow} & \hat{\Xi}\{\cdot \phi \mathbb{D} \cdot \{\mathbf{x}_i \cdot \sigma(\Phi_i) \mathbb{D} \cdot \psi\}_i^n\} \tag{1, 3, 4, 5} \\
\to_{\text{epet}} & \hat{\Xi}\{\cdot \phi \mathbb{D} \cdot \}\} \\
\to_{\text{epet}} & \hat{\Xi}\{\}\}
\end{align*}
$$

<figure><img src="image_13.png" /></figure>

Dually, the second proposition captures the grounds on which a flower can be deemed invalid (i.e. false in at least one model): $\phi$ is not true if assuming that its pistil $\Phi$ is true is not sufficient to conclude that one of its petals $\Phi_i$ is.

**► Proposition 8.4 (Analytic refutation).** Let $\psi \in \mathbb{F}$, $\mathcal{T}$ some $\psi$-consistent and $\psi$-complete theory, and $\phi = \mathbf{x} \cdot \Phi \mathbb{D} \Delta$ with $\Delta = \{\delta_i\}_i^n = \{\mathbf{x}_i \cdot \Phi_i\}_i^n$ such that $\mathcal{T} \Vdash_{\mathcal{T}} \phi$. Then for every $1 \le i \le n$ and substitution $\sigma : \mathbf{x}_i$, there is some $\phi_i \in \Phi_i$ such that $\mathcal{T}, \Phi \Vdash_{\mathcal{T}} \sigma(\phi_i)$.
**Proof.** Suppose the contrary, i.e. there are some $1 \le i \le n$ and $\sigma : \mathbf{x}_i$ such that $\mathcal{T}, \Phi \vdash_{\star} \sigma(\Phi_i)$. Therefore there must exist $\Psi \subseteq \mathcal{T}$ and $\Phi_0 \subseteq \Phi$ ① such that $\Psi, \Phi_0 \vdash_{\star} \sigma(\Phi_i)$ ②. By hypothesis, for every $\Phi' \subseteq \mathcal{T}$ there is a context $\hat{\Xi}$ such that $\Phi' \succ \hat{\Xi}$ and $\hat{\Xi}\{\phi\} \to_{\star} \hat{\Xi}\{\phi\}$. We now derive a contradiction by showing $\hat{\Xi}\{\phi\} \to_{\star} \hat{\Xi}\{\phi\}$ for all $\hat{\Xi}$ such that $\Psi \succ \hat{\Xi}$ ③:

$$ \begin{array}{rcl} \hat{\Xi}\{\phi\} & \to_{\text{ipet}} & \hat{\Xi}\{\mathbf{x} \cdot \Phi \mid \sigma(\Phi_i); \Delta\} \\ & \to_{\text{poll}\downarrow} & \hat{\Xi}\{\mathbf{x} \cdot \Phi \mid \Delta; \Delta\} \quad (1, 2, 3) \\ & \to_{\text{epet}} & \hat{\Xi}\{\} \end{array} $$

<figure><img src="image_14.png" /></figure>

Next, we define the so-called *universal Kripke structure* ⋆($\psi$) relative to a flower $\psi$:

► **Definition 8.5.** Let $\psi \in \mathbb{F}$. The universal Kripke structure ⋆($\psi$) has:

- The set of $\psi$-consistent and $\psi$-complete theories as its worlds;

- Set inclusion $\subseteq$ as its accessibility relation;

- For each world $\mathcal{T}$, a first-order structure whose domain is the set of variables $\mathcal{V}$, and whose interpretation map is given by $[[p]]_{\mathcal{T}} = \{\vec{x} \mid p(\vec{x}) \in \mathcal{T}\}$.

One can easily check that the monotonicity conditions of Kripke structures hold for ⋆($\psi$).

We are now equipped to formulate the main *adequacy lemma*, which relates forcing in ⋆($\psi$) to $\psi$-consistency and $\psi$-completeness:

► **Lemma 8.6 (Adequacy).** Let $\phi, \psi \in \mathbb{F}$, $\mathcal{T}$ a $\psi$-consistent and $\psi$-complete theory, and $\sigma$ a substitution. Then 1. $\sigma(\phi) \in \mathcal{T}$ implies $\mathcal{T} \vdash \phi[\sigma]$, and 2. $\mathcal{T} \nvdash_{\star} \sigma(\phi)$ implies $\mathcal{T} \not\vdash \phi[\sigma]$.

**Proof.** The proof goes by induction on $|\phi|$. We only give an informal sketch, see Appendix C.2 for the detailed proof. There are just two cases to consider:

**Base case** $\phi = p(\vec{x})$. The first statement is trivial. The second statement is immediate from
reflexivity and weakening lemmas on the hypothetical provability relation $\vdash$.

**Recursive case** $\phi = \gamma \mid \Delta$. The first statement follows from Proposition 8.3. The second statement follows from Proposition 8.4, as well as the existence and properties of the completion procedure.

<figure><img src="image_15.png" /></figure>

We get the completeness theorem as a near-direct consequence:

► **Theorem 8.7 (Completeness).** $\Phi \models \Psi$ implies $\Phi \vdash_{\star} \Psi$.

Combined with strong deduction (Theorem 6.7), this also yields a strong completeness theorem for the full flower calculus<fnref n="9" />:

► **Corollary 8.8 (Strong completeness).** $\Phi \models \Psi$ implies $\Psi \to^* \Phi$.

Finally, the composition of the soundness, completeness and deduction theorems (B.20, 8.7 and 6.9) gives the admissibility of $\llcorner$-rules, and thus the analyticity of the flower calculus:

► **Corollary 8.9 (Cult-elimination).** If $\Phi \vdash \Psi$ then $\Phi \vdash_{\star} \Psi$.

<footnote n="9">⁹ Actually it already works for the fragment ⋆ $\cup \{\text{grow}\}$, thanks to the proof of the strong deduction theorem (see Appendix C.1).</footnote>
9 Related works

**Intuitionistic EGs** We have already mentioned the seminal work of Oostra, who introduced in [45] an intuitionistic version of Alpha. In [46] he describes its natural extension with LoIs to get an intuitionistic version of Beta, and in [47] he gives formal soundness and completeness proofs for intuitionistic Alpha, based on a linear notation for graphs. Ma and Pietarinen have developed in [39] their own system of intuitionistic EGs for propositional logic, with a different set of inference rules than Oostra's. They give a more systematic proof theory, including deduction, soundness and completeness theorems with respect to Heyting algebras. Our work brings several new contributions on top of those:

**Variadicity** Our multiset-based definition of flowers captures faithfully the variadic nature of juxtaposition and n-ary scrolls in the diagrammatic syntax. In contrast, previous formalizations rely on a restricted inductive syntax which only captures graphs that are isomorphic to formulas built with binary connectives.

**Intuitionistic binders** While replacing LoIs with binders and variables has already been done by Sowa in the context of classical EGs [55], it seems like we are the first to adapt the idea to the intuitionistic setting.

**Analyticity** To our knowledge, we are the first to give a Kripke semantics to a syntax based on EGs, and to use this to obtain an analyticity result<fnref n="10" />.

**Invertibility** The natural fragment of the flower calculus appears to be the first proof system based on EGs where all rules are invertible.

**Deep inference** While the deep inference literature is most furnished with systems for classical logic, a few works tackle intuitionistic logics: the seminal work of Tiu, who proposed a calculus of structures for intuitionistic FOL [58], was followed by computational interpretations of the implicative fragment in Guenot's thesis [25]. There are also nested sequent systems for (propositional) full intuitionistic linear logic [15], standard and constant-domain intuitionistic FOL [22], and intuitionistic modal logics [14, 31, 36]. The flower calculus is closer to Guenot's nested sequent calculi for implicative logic which also function as rewriting systems, but extends them to full intuitionistic FOL.

**Labelled sequent calculi** For a long time, it was believed that there could not be fully invertible proof systems for intuitionistic logics, even in the propositional case. While this might be true in standard Gentzen formalisms, recent works have shown that it is possible in the context of labelled sequent calculi: first with Lyon's G3IntQ calculus for FOL [35, Section 3.3], and then with the calculus labIS4< of Girlando et al. for the modal logic S4 [24]. In these systems, invertibility is made possible by the addition of semantic information to sequents, in the form of so-called labels and relational atoms that respectively encode the worlds and accessibility relations of Kripke structures. The flower calculus follows instead a purely syntactic approach, by relying on deep inference to retrieve what would normally be semantic information from the context $\hat{\in}$ in the pollination rules poll↑ and poll↓.

<footnote n="10">¹⁰ Ma and Pietarinen claim in [38] that Alpha is analytic because it can simulate the cut rule of sequent calculus. This is a misinterpretation, since this supports precisely the contrary: the ability to simulate the cut rule with a constant number of rules implies the non-analyticity of one the rules involved (namely, Peirce's Deletion rule). Still, the notion of analyticity is not yet fully understood in deep inference systems, as discussed in [10].</footnote>
**Categorical EGs** Since the seminal work of Brady and Trimble in 2000 on the formalization of EGs in category theory [7, 8], there have been various efforts to find rich categorical axiomatizations of Beta. The first approach — initiated in [8] — is based on string diagrams, and has recently enabled strong connections with Frobenius algebras and bicategories or relations [42, 26, 6]. A second approach makes use of the concept of generic figure [11], introduced by Reyes as a basic building block for topos theory [32]. We do not know however of any attempt to uncover the categorical structures underlying intuitionistic EGs. The flower calculus might be an interesting candidate, in that the invertibility of the natural fragment could enable a purely equational approach.

**Coherent logic** We noticed a formal connection between flowers and coherent logic, a subset of the formulas of FOL discovered by Skolem in 1920 [54] that is capable of expressing many mathematical theories, and has close connections to topos theory [30, Section D3.3]. Indeed, the interpretation $[x \cdot \Phi \sqsubseteq \Delta]$ of a generic flower is given by the following formula, which has exactly the shape of a coherent formula as described e.g. in [5]:

$$ \forall x. \left( \bigwedge_{\phi \in \Phi} [\phi] \supset \bigvee_{y \cdot \Psi \in \Delta} \exists y. \bigwedge_{\psi \in \Psi} [\psi] \right) $$

The only difference is that flowers can be nested, while coherent formulas (also called coherent sequents) are first-order, in the sense that $\phi$ and $\psi$ must be atoms. Coherent formulas appear in the theory of focusing in sequent calculi [40], and they lend themselves to simple proof search procedures that allow for explainable proof automation in ITPs [5, 29]. A higher-order variant of coherent formulas that is almost isomorphic to flowers has also been used to construct an intuitionistic version of the arithmetical hierarchy, as well as a fully non-invertible proof system for propositional intuitionistic logic [9].

**Graph calculi** In the last twenty years, Veloso et al. have studied a series of so-called graph calculi, where first-order relations are represented by graphs in the sense of graph theory, and inference rules as graph transformations. The first graph calculus was introduced informally by Curtis and Lowe in 1996 [16], as a graphical notation supposedly capturing both relational calculus, and the sequential calculus of Karger and Hoare [62]. Veloso et al. gave sound and complete syntax and semantics to the calculus in [17], showing that it captures positive first-order logic on binary relations. They then extended their formalism to support relational complementation (negation) [18] as well as various modal [61, 59] and dynamic logics [60].

Graph calculi only handle binary relations and classical logic, while EGs and the flower calculus support relations of arbitrary arity and intuitionistic logic. We conjecture that the relationship between graph calculi and EGs is similar to that between commutative diagrams and string diagrams in category theory: the former represent relations/morphisms as edges between individuals/objects, while the latter represent them dually as points related by lines. EGs could then be understood as a hypergraph generalization of graph calculi, where lines of identity are hyperedges connecting multiple predicate vertices.

**Development calculi** Through their backward reading, the rules of the flower calculus can be understood as primitive tactics for building proofs interactively. In [2, Chapter 3], Ayers calls such systems development calculi. In particular, he presents his own development calculus inspired by McBride's OLEG system [41] and Ganesalingam & Gowers's prover [23] called the Box calculus, where goals are represented by a so-called Box data structure very
similar to flowers. In particular, Boxes have so-called disjunctive pairs to reduce backtracking, that correspond to the petals of flowers. The main difference is that the Box calculus is based on dependent type theory instead of FOL: this allows to store the partial proof terms inside of the Boxes themselves, while this information is lost during the construction of flowers. However, there is no completeness nor analyticity result for the Box calculus. It would be interesting to investigate further connections, in order to develop a dependently-typed version of the flower calculus.

References

1 Samson Abramsky and Achim Jung. *Domain Theory*. Oxford University Press, Inc., USA, 1995.

2 Edward W. Ayers. *A Tool for Producing Verified, Explainable Proofs*. PhD thesis, University of Cambridge, 2021.

3 Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In Liron Cohen and Cezary Kaliszyk, editors, *12th International Conference on Interactive Theorem Proving (ITP 2021)*, volume 193 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 4:1–4:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4, doi:10.4230/LIPIcs.ITP.2021.4.

4 Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Masami Hagiya and John C. Mitchell, editors, *Theoretical Aspects of Computer Software*, volume 789, pages 141–160. Springer Berlin Heidelberg, 1994. Series Title: Lecture Notes in Computer Science. URL: http://link.springer.com/10.1007/3-540-57887-0_94, doi:10.1007/3-540-57887-0_94.

5 Marc Bezem and Thierry Coquand. Automating Coherent Logic. In Geoff Sutcliffe and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning*, Lecture Notes in Computer Science, pages 246–260, Berlin, Heidelberg, 2005. Springer. doi: 10.1007/11591191_18.

6 Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski. Diagrammatic Algebra of First Order Logic, January 2024. arXiv:2401.07055 [cs, math]. URL: http://arxiv.org/abs/2401.07055, doi:10.48550/arXiv.2401.07055.

7 Geraldine Brady and Todd H. Trimble. A categorical interpretation of C.S. Peirce's propositional logic Alpha. *Journal of Pure and Applied Algebra*, 149(3):213-239, June 2000. URL: https://linkinghub.elsevier.com/retrieve/pii/S0022404998001790, doi: 10.1016/S0022-4049(98)00179-0.

8 Geraldine Brady and Todd H. Trimble. A String Diagram Calculus for Predicate Logic and C. S. Peirce's System Beta, June 2000. URL: https://ncatlab.org/nlab/files/BradyTrimbleString.pdf.

9 Taus Brock-Nannestad and Danko Ilik. An Intuitionistic Formula Hierarchy Based on High-School Identities. *Mathematical Logic Quarterly*, 65(1):57-79, May 2019. arXiv: 1601.04876. URL: http://arxiv.org/abs/1601.04876, doi:10.1002/malq.201700047.

10 Paola Bruscoli and Alessio Guglielmi. On Analyticity in Deep Inference. *Mathematical Structures in Computer Science*, 29(Special Issue 8: A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday), 2019. URL: https://people.bath.ac.uk/ag248/p/ADI.pdf, doi:10.1017/S0960129519000136.

11 Gianluca Caterina and Rocco Gangle. A New Syntax for Diagrammatic Logic: A Generic Figures Approach. In Yaroslav D. Sergeyev and Dmitri E. Kvasov, editors, *Numerical Computations: Theory and Algorithms*, Lecture Notes in Computer Science, pages 43–58, Cham, 2020. Springer International Publishing. doi:10.1007/978-3-030-40616-5_4.

12 Kaustuv Chaudhuri. Subformula linking as an interaction method. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, *Interactive Theorem Proving*, volume 7998, pages 386–401. Springer Berlin Heidelberg, 2013. Series Title: Lecture Notes in
Computer Science. URL: http://link.springer.com/10.1007/978-3-642-39634-2_28, doi: 10.1007/978-3-642-39634-2_28.

13 Kaustuv Chaudhuri. Subformula linking for intuitionistic logic with application to type theory. In André Platzer and Geoff Sutcliffe, editors, *Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings*, volume 12699 of *Lecture Notes in Computer Science*, pages 200-216. Springer, 2021. doi:10.1007/978-3-030-79876-5\_12.

14 Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular focused proof systems for intuitionistic modal logics. In *International Conference on Formal Structures for Computation and Deduction*, 2016.

15 Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Simona Ronchi Della Rocca, editor, *Computer Science Logic 2013 (CSL 2013)*, volume 23 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 197-214, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.197, doi:10.4230/LIPIcs.CSL.2013.197.

16 Sharon Curtis and Gavin Lowe. Proofs with graphs. *Science of Computer Programming*, 26(1):197-216, May 1996. URL: https://www.sciencedirect.com/science/article/pii/S0167642395000259, doi:10.1016/0167-6423(95)00025-9.

17 Renata De Freitas, Paulo A. S. Veloso, Sheila R. M. Veloso, and Petrucio Viana. On graph reasoning. *Information and Computation*, 207(10):1000-1014, October 2009. URL: https://www.sciencedirect.com/science/article/pii/S0890540109000984, doi:10.1016/j.ic.2008.11.004.

18 Renata De Freitas, Paulo A. S. Veloso, Sheila R. M. Veloso, and Petrucio Viana. A Calculus for Graphs with Complement. In Ashok K. Goel, Mateja Jamnik, and N. Hari Narayanan, editors, *Diagrammatic Representation and Inference*, volume 6170, pages 84-98. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. Series Title: Lecture Notes in Computer Science. URL: http://link.springer.com/10.1007/978-3-642-14600-8_11, doi:10.1007/978-3-642-14600-8_11.

19 Pablo Donato. flowers-metatheory, November 2022. URL: https://github.com/Champitoad/flowers-metatheory.

20 Pablo Donato. flower-prover, October 2023. URL: https://github.com/Champitoad/flower-prover.

21 Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. A drag-and-drop proof tactic. In *Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs*, CPP 2022, page 197-209, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3497775.3503692.

22 Melvin Fitting. Nested Sequents for Intuitionistic Logics. *Notre Dame Journal of Formal Logic*, 55(1):41-61, 2014. URL: http://projecteuclid.org/euclid.ndjfl/1390246437, doi: 10.1215/00294527-2377869.

23 M. Ganesalingam and W. T. Gowers. A Fully Automatic Theorem Prover with Human-Style Output. *Journal of Automated Reasoning*, 58(2):253-291, February 2017. doi:10.1007/s10817-016-9377-1.

24 Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger. Intuitionistic S4 is decidable. In *2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1-13, June 2023. arXiv:2304.12094 [cs]. URL: http://arxiv.org/abs/2304.12094, doi:10.1109/LICS56636.2023.10175684.

25 Nicolas Guenot. *Nested Deduction in Logical Foundations for Computation*. PhD thesis, Ecole Polytechnique X, April 2013. URL: https://pastel.archives-ouvertes.fr/pastel-00929908.

26 Nathan Haydon and Paweł Sobociński. Compositional Diagrammatic First-Order Logic. In Ahti-Veikko Pietarinen, Peter Chapman, Leonie Bosveld-de Smet, Valeria Giardino, James
Corter, and Sven Linker, editors, *Diagrammatic Representation and Inference*, volume 12169, pages 402–418. Springer International Publishing, Cham, 2020. Series Title: Lecture Notes in Computer Science. URL: http://link.springer.com/10.1007/978-3-030-54249-8_32, doi:10.1007/978-3-030-54249-8_32.

27 Olivier Hermant. Semantic Cut Elimination in the Intuitionistic Sequent Calculus. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Dough Tygar, Moshe Y. Vardi, Gerhard Weikum, and Paweł Urzyczyn, editors, *Typed Lambda Calculi and Applications*, volume 3461, pages 221–233. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. Series Title: Lecture Notes in Computer Science. URL: http://link.springer.com/10.1007/11417170_17, doi:10.1007/11417170_17.

28 John Howse, Gem Stapleton, and John Taylor. Spider Diagrams. *LMS Journal of Computation and Mathematics*, 8:145–194, January 2005. Publisher: Cambridge University Press. URL: https://www.cambridge.org/core/journals/lms-journal-of-computation-and-mathematics/article/spider-diagrams/B312DE2E402F39F9BEF75770F80559D0#, doi:10.1112/S1461157000000942.

29 Predrag Janičić and Julien Narboux. Automated generation of illustrated proofs in geometry and beyond. *Annals of Mathematics and Artificial Intelligence*, July 2023. URL: https://link.springer.com/10.1007/s10472-023-09857-y, doi:10.1007/s10472-023-09857-y.

30 Peter T. Johnstone. *Sketches of an Elephant: A Topos Theory Compendium*, volume 2 of *Oxford Logic Guides*. Clarendon Press, Oxford, England, September 2002.

31 Roman Kuznets and Lutz Straßburger. Maehara-style modal nested calculi. *Archive for Mathematical Logic*, 58(3-4):359–385, May 2019. URL: http://link.springer.com/10.1007/s00153-018-0636-1, doi:10.1007/s00153-018-0636-1.

32 Marie La Palme Reyes, Gonzalo E. Reyes, and Houman Zolfaghari. *Generic figures and their glueings*. Polimetrica, International Scientific Publisher, 2008.

33 C. I. Lewis. A survey of symbolic logic. *Journal of Philosophy, Psychology and Scientific Methods*, 17(3):78–79, 1920. doi:10.2307/2940631.

34 Sven Linker, Jim Burton, and Mateja Jamnik. Tactical Diagrammatic Reasoning. *Electronic Proceedings in Theoretical Computer Science*, 239:29–42, January 2017. URL: http://arxiv.org/abs/1701.07126, doi:10.4204/EPTCS.239.3.

35 Tim Lyon. *Refining Labelled Systems for Modal and Constructive Logics with Applications*. PhD thesis, Vienna University of Technology, July 2021. URL: http://arxiv.org/abs/2107.14487, doi:10.48550/arXiv.2107.14487.

36 Tim S. Lyon. Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. In Anupam Das and Sara Negri, editors, *Automated Reasoning with Analytic Tableaux and Related Methods*, Lecture Notes in Computer Science, pages 409–427, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-86059-2_24.

37 Thomas Långbacka, Rimvydas Rukšėnas, and Joakim von Wright. TkWinHOL: A tool for Window Inference in HOL. In E. Thomas Schubert, Philip J. Windley, and James Alves-Foss, editors, *Higher Order Logic Theorem Proving and Its Applications*, Lecture Notes in Computer Science, pages 245–260, Berlin, Heidelberg, 1995. Springer. doi:10.1007/3-540-60275-5_69.

38 Minghui Ma and Ahti-Veikko Pietarinen. Proof Analysis of Peirce’s Alpha System of Graphs. *Studia Logica*, 105(3):625–647, June 2017. URL: http://link.springer.com/10.1007/s11225-016-9703-y, doi:10.1007/s11225-016-9703-y.

39 Minghui Ma and Ahti-Veikko Pietarinen. A graphical deep inference system for intuitionistic logic. *Logique et Analyse*, 245:73–114, January 2019. URL: http://www.scopus.com/inward/record.url?scp=85066258215&partnerID=8YFLogxK, doi:10.2143/LEA.245.0.3285706.

40 Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. *Annals of Pure and Applied Logic*, 173(5):103091, May 2022. URL: https://linkinghub.elsevier.com/retrieve/pii/S0168007222000057, doi:10.1016/j.apal.2022.103091.
41 Conor McBride. *Dependently Typed Functional Programs and their Proofs*. PhD thesis, University of Edinburgh, July 2000. URL: https://era.ed.ac.uk/handle/1842/374.

42 Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine. arXiv:1601.06098 [cs, math], August 2016. arXiv: 1601.06098. URL: http://arxiv.org/abs/1601.06098.

43 Robin Milner. The use of machines to assist in rigorous proof. *Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences*, 312(1522):411-422, 1984. URL: https://royalsocietypublishing.org/doi/abs/10.1098/rsta.1984.0067, arXiv:https://royalsocietypublishing.org/doi/pdf/10.1098/rsta.1984.0067, doi:10.1098/rsta.1984.0067.

44 Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In André Platzer and Geoff Sutcliffe, editors, *Automated Deduction – CADE 28*, pages 625–635, Cham, 2021. Springer International Publishing.

45 Arnold Oostra. *Los gráficos Alfa de Peirce aplicados a la lógica intuicionista*. Number 2 in Cuadernos de Sistemática Peirceana. Centro de Sistemática Peirceana, 2010.

46 Arnold Oostra. *Gráficos existenciales Beta intuicionistas*. Number 3 in Cuadernos de Sistemática Peirceana. Centro de Sistemática Peirceana, 2011.

47 Arnold Oostra. Equivalence proof for intuitionistic existential alpha graphs. In *Diagrammatic Representation and Inference: 12th International Conference, Diagrams 2021, Virtual, September 28-30, 2021, Proceedings*, page 188–195, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-86062-2_16.

48 Arnold Oostra. *Advances in Peircean Mathematics: The Colombian School*, chapter Intuitionistic and Geometrical Extensions of Peirce’s Existential Graphs, pages 105–180. De Gruyter, 2022.

49 Charles Sanders Peirce. Prolegomena to an Apology for Pragmaticism. *The Monist*, 16(4):492-546, 1906. Publisher: Oxford University Press. URL: https://www.jstor.org/stable/27899680.

50 Brian Ritchie. *The Design and Implementation of an Interactive Proof Editor*. PhD thesis, The University of Edinburgh, 1988. Accepted: 2013-04-02T15:18:04Z Publisher: The University of Edinburgh. URL: https://era.ed.ac.uk/handle/1842/6607.

51 Don D. Roberts. *The Existential Graphs of Charles S. Peirce*. De Gruyter Mouton, Berlin, Boston, 1973. URL: https://doi.org/10.1515/9783110226225 [cited 2023-03-06], doi:doi:10.1515/9783110226225.

52 Benoit Rognier and Guillaume Duhamel. Présentation de la plateforme edukera. In *Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016)*, 2016.

53 Sun-Joo Shin. *The Iconic Logic of Peirce's Graphs*. The MIT Press, 05 2002. doi:10.7551/mitpress/3633.001.0001.

54 Thoralf Skolem. Logisch-kombinatorische untersuchungen Über die erfüllbarkeit oder bewiesbarkeit mathematischer sätze nebst einem theorem Über dichte mengen. In Thoralf Skolem, editor, *Selected Works in Logic*. Universitetsforlaget, 1920.

55 John Sowa. Peirce's Tutorial on Existential Graphs. *Semiotica*, 186:345–394, 2011. doi:10.1515/semi.2011.060.

56 M. H. Stone. Topological representations of distributive lattices and Brouwerian logics. In *Časopis pro pěstování matematiky a fysiky*, volume 067, pages 1–25, 1938. ISSN: 1802-114X Issue: 1 Journal Abbreviation: Časopis Pěst. Mat. Fys. URL: https://dml.cz/handle/10338.dmlcz/124080, doi:10.21136/CPMF.1938.124080.

57 The Coq Development Team. The Coq Proof Assistant, 2022. doi:10.5281/zenodo.7313584.

58 Alwen Tiu. A Local System for Intuitionistic Logic. In Miki Hermann and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning*, Lecture Notes in Computer Science, pages 242–256, Berlin, Heidelberg, 2006. Springer. doi:10.1007/11916277_17.
59 Paulo Veloso, Sheila Veloso, and Mario Benevides. On Graph Calculi for Multi-modal Logics. *Electronic Notes in Theoretical Computer Science*, 312, April 2015. doi:10.1016/j.entcs.2015.04.014.

60 Paulo A. S. Veloso, Sheila R. M. Veloso, and Mario R. F. Benevides. PDL for structured data: a graph-calculus approach. *Logic Journal of the IGPL*, 22(5):737-757, October 2014. doi:10.1093/jigpal/jzu011.

61 Paulo A. S. Veloso, Sheila R. M. Veloso, and Mario R. F. Benevides. On a graph calculus for modalities. *Theoretical Computer Science*, 685:83-103, July 2017. URL: https://www.sciencedirect.com/science/article/pii/S0304397517301238, doi:10.1016/j.tcs.2016.11.037.

62 Burghard Von Karger and C. A. R. Hoare. Sequential calculus. *Information Processing Letters*, 53(3):123-130, February 1995. URL: https://www.sciencedirect.com/science/article/pii/002001909400205D, doi:10.1016/0020-0190(94)00205-D.

63 Fernando Zalamea. Lógica topológica. una introducción a los gráficos existenciales de peirce. Memorias del XIV Coloquio Distrital de Matemáticas y Estadística, 1997.

64 Fernando Zalamea. Pragmaticismo, gráficos y continuidad. hacia el lugar de c. s. peirce en la historia de la lógica. Mathesis 13, pp. 147-156, 1997.

65 Fernando Zalamea. Peirce's logic of continuity: Existential graphs and non-Cantorian continuum. *Review of Modern Logic*, 9(1-2):115-162, January 2003. Publisher: The Review of Modern Logic. URL: https://projecteuclid.org/journals/review-of-modern-logic/volume-9/issue-1-2/Peirces-logic-of-continuity--Existential-graphs-and-non-Cantorian/rml/1081173838.full.

66 J.J. Zeman. *The Graphical Logic of C. S. Peirce*. PhD thesis, University of Chicago, 1964. URL: https://books.google.fr/books?id=EOAqAQAAMAAJ.

67 Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, and Wenhui Sun. Design of point-and-click user interfaces for proof assistants. In *Formal Methods and Software Engineering: 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings*, page 86-103, Berlin, Heidelberg, 2019. Springer-Verlag. doi:10.1007/978-3-030-32409-4_6.
<figure><img src="image_16.png" /><figcaption>Figure 8 Graphical presentation of natural rules ❧</figcaption></figure>
<figure><img src="image_17.png" /><figcaption>Figure 9 Graphical presentation of cultural rules ≁</figcaption></figure>
<figure><img src="image_18.png" /><figcaption>(a) Textual presentation</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>(b) Graphical presentation</figcaption></figure>

<caption>Figure 10 A *natural* proof in the flower calculus</caption>
A Comparison with EGs

In this section, we give a detailed comparison of the rules of the flower calculus with the illative transformations of Peirce's system Beta. To ease the presentation, we introduce an inductive syntax for the graphs of Beta based on our notion of garden.

**► Definition A.1 (β-graph).** The sets of β-nodes $N_β$, β-gardens $Γ_β$ and β-graphs $G_β$ are defined mutually inductively:

**Atom** If $p \in \mathcal{P}$ and $\bar{x} \in \mathcal{V}^{ar}(p)$, then $p(\bar{x}) \in N_β$;

**Graph** If $G \subset N_β$ is a finite multiset, then $G \in G_β$.

**Garden** If $x \subset \mathcal{V}$ is a finite set and $G \subset N_β$ a finite multiset, then $x \cdot G \in Γ_β$;

**Cut** If $\gamma \in Γ_β$, then $[\gamma] \in N_β$.

**► Remark A.2.** Note that a β-graph is defined as a multiset of β-nodes, just like a bouquet is a multiset of flowers. Then like in the flower calculus, and unlike in Peirce's original system, binders (LoIs) cannot appear at the top-level of SA.

**► Example A.3.** The lower graph in Figure 4a can be written in textual notation as the expression $[x \cdot R(x), [ \cdot P(x) ]]$.

We also adapt the notion of context to the Beta setting:

**► Definition A.4 (β-context).** β-contexts $\hat{G}$ are defined inductively by the following grammar:

$$ \hat{G}, \hat{H}, \hat{K} ::= G, \hat{g} $$

$$ \hat{g}, \hat{h}, \hat{k} ::= \square | [\hat{G}] $$

**► Definition A.5 (Polarity).** The number of inversions $inv(\hat{G})$ of a β-context $\hat{G}$ is:

$$ inv(\square) = 0 \quad inv(G, \hat{g}) = inv(\hat{g}) \quad inv([\hat{G}]) = 1 + inv(\hat{G}) $$

The definitions of free variables, bound variables and substitutions can also be adapted straightforwardly.

The set of rules of Beta is given in Figure 11a. Iter, Deit, Ins and Del correspond respectively to the Iteration, Deiteration, Insertion and Deletion principles of Alpha, while Dcut↓ and Dcut↑ capture the Double-cut principle. As for Unif↓ and Unif↑, they correspond roughly to the principles of Insertion and Deletion applied to LoIs. Indeed in their bottom-up reading, Unif↑ and Unif↓ can be understood as capturing respectively the operations of unification and anti-unification on two variables:

**Unification** substituting $z$ for $y$ and removing the binder for $y$ is equivalent in purpose to adding a new LoI between the outermost point of the LoI associated to $y$, and some point of the LoI associated to $z$ in the same area (which is assumed to exist by well-scopedness);

**Anti-unification** substituting $y$ for $z$ and adding a binder for $y$ is equivalent in purpose to severing the LoI associated to $z$ at the location where the binder for $y$ is introduced.

There is no need to formulate an equivalent of the Iteration and Deiteration principles for LoIs. Indeed, their purpose is to manage locally the extension of a line. With binders, the notion of extension is replaced with that of scope, which is handled globally and automatically in the definition of substitutions.

Let us now review the rules of the flower calculus in more detail, starting with the fragment that is a direct adaptation of the rules of Beta:
<figure><img src="image_20.png" /><figcaption>(a) Rules of Beta</figcaption></figure>

<caption>(b) Converse of `epis` rule
$$ \frac{\Phi}{\cdot D \cdot \Phi} \text{ epis} \downarrow $$</caption>

Figure 11 Comparing rules

**Blank Antecedent (epis)** It allows to enclose any *bouquet* in a *petal* attached to an (e)empty (pis)til. This is a weaker, intuitionistic version of Dcut↑, that was already identified by Peirce as the “collapsing of a scroll’s walls’ [49, p. 534], and is called the rule of Blank Antecedent in [39]. The converse rule that would correspond to Dcut↓ — rule `epis`↓ in Figure 11b — is actually shown to be *admissible* by our completeness theorem<fnref n="11" />.

**(De)iteration (poll↓, poll↑)** The (poll)ination rules poll↓ and poll↑ correspond respectively to `Iter` and `Deit`, but reformulated with the pollination relation (Definition 6.3). In fact in their textual presentation (Figure 7), they are more general than (de)iteration rules, because $\Phi \succ \Xi$ allows the pollinating bouquet $\Phi$ to be scattered in the context $\Xi$, i.e. its flowers need not be located in the same area. On the contrary in their graphical presentation (Figure 8), they are less general since only one flower can be pollinated at a time, rather than an entire bouquet of flowers residing in the same area. But it is easy to see that all these variants are equivalent in deductive power, since the pollination of a bouquet (however scattered) can always be simulated by the successive pollinations of each of its flowers.

**Insertion/Deletion (grow, crop, pull, glue)** They correspond to `Ins` and `Del`, but have doubled in number to account for the syntactic distinction between pistils and petals. More precisely, rules `grow` and `crop` allow to insert and delete entire flowers, while rules `pull` and `glue` deal with petals. As for pollination rules, manipulating single flowers/petals (graphical version) or entire bouquets/corollas (textual version) does not change the deductive power of the rules.

**Unification (ipis, ipet, apis, apet)** Rules `ipis` and `ipet` allow to (i) nstantiate a sprinkler located respectively in a (pis)til ($\forall$) and a (pet)al ($\exists$) with an arbitrary substitution, while rules `apis` and `apet` do the opposite operation of (a) bstracting a set of variables by introducing a sprinkler. They correspond respectively to a generalization of `Unif↑` and `Unif↓`, where the

<footnote n="11">¹¹ Interestingly, although an equivalent of `epis`↓ is included in [39], there is no mention of it by Peirce in [49]. It may be a sign that Peirce already intuited its admissibility, or at least considered this direction of the transformation unworthy of attention.</footnote>
variable substitution {$z/y$} becomes an arbitrary substitution $\sigma$. Once again, we have twice the amount of rules to account for the *pistil/petal* distinction, which is not surprising since in the *LoI* syntax of *EGs*, they are special cases of *Insertion/Deletion*. Note that for the instantiation rules *ipis/ipet* to be invertible, we duplicate the whole *flower/petal* where the *sprinkler* occurs, mirroring what is done in multi-conclusion sequent calculi.

The last two rules mainly handle the behavior of disjunctive and absurd statements, i.e. *flowers* with respectively $n \ge 2$ and $n = 0$ *petals*, and are closer to sequent-style introduction/elimination rules:

**Disjunction Introduction (epet)** It allows to erase any flower with an (e)empty (pet)al. According to Oostra [48, p. 109], Peirce already identified epet as a component of his decision procedure for **Alpha** (it is simply called “Operation 1” in [48]). This is no coincidence, since we precisely came up with this rule when trying to design a decision procedure for flowers.

**Disjunction/Falsehood Elimination (srep)** It corresponds to a *n*-ary generalization of the left introduction rule for disjunction in sequent calculus, the 0-ary case capturing falsehood elimination (*ex falso quodlibet* as illustrated in the proof of Figure 10. The binary case is also used in the intuitionistic *EGs* system of [39] together with its converse, which is also shown to be admissible by our completeness theorem. The name srep is short for (s)elf-(*rep*)roduction, which is more clearly visualized in the graphical version of the rule in Figure 8.

## B Soundness

In this section, we show that every rule of the flower calculus is sound with respect to our Kripke semantics for flowers, and thus that $\vdash \phi$ implies $\vdash \phi$ for every $\phi$. We start with a few trivial facts about the update operation of Definition 5.5:

* **Observation B.1 (Associativity).** $f|R g|_S h = f|R \cup S (g|_S h)$.

* **Observation B.2 (Commutativity).** If $R \cap S = \emptyset$ then $f|R g|_S h = f|_S h|R g$.

* **Observation B.3 (Agreement).** If $f(x) = g(x)$ for all $x \in R$ then $f|R = h|R g$.

* **Observation B.4 (Idempotency).** $f|R f = f$.

Semantic entailment is obviously a reflexive and transitive relation:

* **Observation B.5 (Reflexivity).** $\Phi \vdash \Phi$.

* **Observation B.6 (Transitivity).** If $\Phi \vdash \Psi$ and $\Psi \vdash \Xi$, then $\Phi \vdash \Xi$.

The two following lemmas will be useful to reason on the *forcing relation* (Definition 7.5):

* **Lemma B.7 (Monotonicity).** If $w \le w'$ and $w \Vdash \phi [e]$ then $w' \Vdash \phi [e]$.

*Proof.* By a straightforward induction on $|\phi|$. ▶

* **Lemma B.8 (Mirroring).** $w \Vdash \sigma(\phi)[e]$ iff $w \Vdash \phi[e|_x [[\sigma]]_e]$ for $\sigma: x$ *capture-avoiding in* $\phi$ and $x \cap bv(\phi) = \emptyset$.

*Proof.* By induction on $|\phi|$. ▶
**Base case** Suppose $\phi = p(\vec{y})$. We show that $[[\sigma(\vec{y})]]_e \in [[p]]_w$ iff $[[\vec{y}]]_{e|_x[[\sigma]]_e} \in [[p]]_w$ by proving that $[[x]]_{e|_x[[\sigma]]_e} = [[\sigma(x)]]_e$ for any variable $x$. Either:

- $x \in \mathbf{x}$, and $[[x]]_{e|_x[[\sigma]]_e} = [[\sigma]]_e(x) = [[\sigma(x)]]_e$; or

- $x \notin \mathbf{x}$, and $[[x]]_{e|_x[[\sigma]]_e} = e(x) = [[x]]_e = [[\sigma(x)]]_e$.

**Recursive case** Suppose $\phi = \mathbf{y} \cdot \Phi \sqcup \{\mathbf{z}_i \cdot \Psi_i\}_i^n$. We show that $w \Vdash \mathbf{y} \cdot \sigma(\Phi) \sqcup \{\mathbf{z}_i \cdot \sigma(\Psi_i)\}_i^n [e]$ implies $w \Vdash \mathbf{y} \cdot \Phi \sqcup \{\mathbf{z}_i \cdot \Psi_i\}_i^n [e|_x [[\sigma]]_e]$, the argument working in both directions. Let $w' \ge w$ and $e'$ a $w'$-evaluation such that $w' \Vdash \Phi [e|_x [[\sigma]]_{e|_y e'}]$. Since $\sigma$ is capture-avoiding in $\phi$, we know that $fv(\sigma(x)) \cap \mathbf{y} = \emptyset$, and thus $[[\sigma]]_e(x) = [[\sigma(x)]]_e = [[\sigma(x)]_{e|_y e'} = [[\sigma]]_{e|_y e'}(x)$ for any $x \in \mathbf{x}$. Hence by Observation B.3 $w' \Vdash \Phi [e|_x [[\sigma]]_{e|_y e'}|_y e']$, and since by hypothesis $\mathbf{x} \cap \mathbf{y} = \emptyset$ we obtain $w' \Vdash \sigma(\Phi) [e|_y e']$, and thus by hypothesis $w' \Vdash \sigma(\Psi_i) [e|_y e'|_{\mathbf{z}_i} e'']$ for some $1 \le i \le n$ and $w'$-evaluation $e''$. Again by IH we get $w' \Vdash \Psi_i [e|_y e'|_{\mathbf{z}_i} e''|_x [[\sigma]]_{e|_y e'|_{\mathbf{z}_i} e''}]$, and since $\sigma$ is capture-avoiding in $\phi$ we have $fv(\sigma(x)) \cap \mathbf{z}_i = \emptyset$ for any $x \in \mathbf{x}$, and thus $w' \Vdash \Psi_i [e|_y e'|_{\mathbf{z}_i} e''|_x [[\sigma]]_e]$ by Observation B.3. Finally by hypothesis $\mathbf{x} \cap \mathbf{z}_i = \emptyset$, thus we can conclude that $w' \Vdash \Psi_i [e|_x [[\sigma]]_e|_y e'|_{\mathbf{z}_i} e'']$ by Observation B.2.

◀

The following *functoriality* lemma is at the heart of every deep inference formalism. It requires an induction principle for *contexts*:

**Definition B.9 (Depth).** The depth $|\hat{\Phi}|$ of a context $\hat{\Phi}$ is defined recursively by:

$$|\Box| = 0 \qquad |\Psi, \hat{\phi}| = |\hat{\phi}| \qquad |\mathbf{x} \cdot \hat{\Phi} \sqcup \Delta| = |\gamma \sqcup \mathbf{x} \cdot \hat{\Phi}; \Delta| = 1 + |\hat{\Phi}|$$

**Lemma B.10 (Functoriality).** If $\Phi \models \Psi$, then for any $\hat{\Xi}$ either $\hat{\Xi}\{\Phi\} \models \hat{\Xi}\{\Psi\}$ if $\hat{\Xi}$ is positive, or $\hat{\Xi}\{\Psi\} \models \hat{\Xi}\{\Phi\}$ if $\hat{\Xi}$ is negative.

**Proof.** By induction on $|\hat{\Xi}|$. ▶

◀

**Lemma B.11 (Weakening).** $\Phi \models \emptyset$.

**Proof.** Trivial by Definition 7.5. ▶

◀

**Lemma B.12 (Co-weakening).** $\gamma \sqcup \Delta \models \gamma \sqcup \Gamma$; $\Delta$.

**Proof.** Let $\gamma = \mathbf{x} \cdot \Phi$, $w$ a world in some Kripke structure $\mathcal{K}$, $w' \ge w$, $e$ a $w$-evaluation and $e'$ a $w'$-evaluation such that $w \Vdash \gamma \sqcup \Delta [e]$ and $w' \Vdash \Phi [e|_x e']$. Then by hypothesis there must exist some $\mathbf{y} \cdot \Psi \in \Delta$ and $w'$-evaluation $e''$ such that $w' \Vdash \Psi [e|_x e'|_y e'']$, and thus we can conclude. ▶

◀

The less obvious rules in terms of soundness are the pollination rules $\{\text{poll} \downarrow, \text{poll} \uparrow\}$, because of the arbitrary context $\hat{\Xi}$ and reliance on the pollination relation.

**Lemma B.13 (Cross-pollination).** $\Phi, \hat{\Xi}\{\Phi\} \nvDash \Phi, \hat{\Xi}\{\cdot\}$.

**Proof.** Let $w$ a world in some Kripke structure $\mathcal{K}$, and $e$ a $w$-evaluation. We show that $w \Vdash \Phi, \hat{\Xi}\{\Phi\} [e]$ iff $w \Vdash \Phi, \hat{\Xi}\{\cdot\} [e]$ by induction on $|\hat{\Xi}|$. ▶

**Base case** Suppose $\hat{\Xi} = \Xi', \Box$. Then we trivially have $w \Vdash \Phi, \Xi', \Phi [e]$ iff $w \Vdash \Phi, \Xi' [e]$ by Definition 7.5.

**Recursive case** We distinguish two cases:

**Pistil** Suppose $\hat{\Xi} = \Xi', (\mathbf{x} \cdot \hat{\Xi}_0 \sqcup \Delta)$.
1. Suppose $w \Vdash \Phi, \hat{\Xi}\{\Phi\}[e]$. Then $w \Vdash \Phi[e]$, $w \Vdash \Xi'[e]$ and $w \Vdash \mathbf{x} \cdot \hat{\Xi}_0\{\Phi\} \sqcup \Delta[e]$. Thus it remains to show that $w \Vdash \mathbf{x} \cdot \hat{\Xi}_0\{\}\sqcup \Delta[e]$. Let $w' \ge w$ and $e'$ a $w'$-evaluation such that $w' \Vdash \hat{\Xi}_0\{\}[e|_x e']$. By IH we have $\Phi, \hat{\Xi}_0\{\} \Vdash \Phi, \hat{\Xi}_0\{\Phi\}$, and thus by Lemma B.10 $\mathbf{x} \cdot \Phi, \hat{\Xi}_0\{\Phi\} \sqcup \Delta \Vdash \mathbf{x} \cdot \Phi, \hat{\Xi}_0\{\}\sqcup \Delta$. By Lemma B.11 and Lemma B.10 we have $w \Vdash \mathbf{x} \cdot \Phi, \hat{\Xi}_0\{\Phi\} \sqcup \Delta[e]$, and thus $w \Vdash \mathbf{x} \cdot \Phi, \hat{\Xi}_0\{\}\sqcup \Delta[e]$. Then since $w' \Vdash \hat{\Xi}_0\{\}[e|_x e']$, and since by Lemma B.7 (and the fact that $\mathbf{x} \cap \text{fv}(\Phi) = \emptyset$) we have $w' \Vdash \Phi[e|_x e']$, we can conclude that there are some $\mathbf{y} \cdot \Psi \in \Delta$ and $w'$-evaluation $e''$ such that $w' \Vdash \Psi[e|_x e'|_y e'']$.

2. $\Phi, \hat{\Xi}\{\} \Vdash \Phi, \hat{\Xi}\{\Phi\}$ holds by the same argument in the other direction.

Petal Suppose $\hat{\Xi} = \Xi', (\mathbf{x} \cdot \Psi \sqcup \mathbf{y} \cdot \hat{\Xi}_0; \Delta)$.

1. Suppose $x \Vdash \Phi, \hat{\Xi}\{\Phi\}[e]$. Then $w \Vdash \Phi[e]$, $w \Vdash \Xi'[e]$ and $w \Vdash \mathbf{x} \cdot \Psi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\Phi\}; \Delta[e]$. Thus it remains to show that $w \Vdash \mathbf{x} \cdot \Psi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\}; \Delta[e]$. Let $w' \ge w$ and $e'$ a $w'$-evaluation such that $w' \Vdash \Psi[e|_x e']$. Then we can deduce that there exists a $w'$-evaluation $e''$ such that either:

- $w' \Vdash \Psi'[e|_x e'|_y e'']$ for some $\mathbf{y}' \cdot \Psi' \in \Delta$, and we conclude immediately;

- or $w' \Vdash \hat{\Xi}_0\{\Phi\}[e|_x e'|_y e'']$. By Lemma B.7 (and the fact that $\mathbf{x} \cap \text{fv}(\Phi) = \emptyset$ and $\mathbf{y} \cap \text{fv}(\Phi) = \emptyset$) we have $w' \Vdash \Phi[e|_x e'|_y e'']$, and thus $w' \Vdash \Phi, \hat{\Xi}_0\{\Phi\}[e|_x e'|_y e'']$. Then by IH we have $w' \Vdash \Phi, \hat{\Xi}_0\{\}[e|_x e'|_y e''],$ and thus we can conclude in particular that $w' \Vdash \hat{\Xi}_0\{\}[e|_x e'|_y e'']$.

2. $\Phi, \hat{\Xi}\{\} \Vdash \Phi, \hat{\Xi}\{\Phi\}$ holds by the same argument in the other direction.

◀

**Lemma B.14 (Pollination).** If $\Phi \succ \hat{\Xi}$, then $\hat{\Xi}\{\Phi\} \Vdash \hat{\Xi}\{\}$.

**Proof.** We show that $\phi \succ \hat{\Xi}$ implies $\hat{\Xi}\{\phi\} \Vdash \hat{\Xi}\{\}$ for any flower $\phi$ and context $\hat{\Xi}$: then assuming that $\Phi = \phi_1, \dots, \phi_n$, we get

$$ \underbrace{\hat{\Xi}\{\phi_1, \dots, \phi_n\} \Vdash \hat{\Xi}\{\phi_2, \dots, \phi_n\} \Vdash \dots \Vdash \hat{\Xi}\{\}}_{n \text{ times}} $$

and conclude by Observation B.6.

By Definition 6.3, there are a bouquet $\Psi$ and two contexts $\hat{\Xi}', \hat{\Xi}_0$ such that one of the two following cases holds:

**Cross-pollination** $\hat{\Xi} = \hat{\Xi}'\{\Psi, \phi, \hat{\Xi}_0\}$. Then $\phi, \hat{\Xi}_0\{\phi\} \Vdash \phi, \hat{\Xi}_0\{\}$ by Lemma B.13, and we conclude by Lemma B.10.

**Self-pollination** $\hat{\Xi} = \hat{\Xi}'\{\mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0; \Delta\}$ for some $\mathbf{x}, \mathbf{y}, \Delta$. Let $w$ a world in some Kripke structure $\mathcal{K}$ and $e$ a $w$-evaluation. We show that $w \Vdash \mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\phi\}; \Delta[e]$ iff $w \Vdash \mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\}; \Delta[e]$, and conclude by Lemma B.10.

1. Suppose that $w \Vdash \mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\phi\}; \Delta[e]$, and let $w' \ge w$ and $e'$ a $w'$-evaluation such that $w' \Vdash \Psi, \phi[e|_x e']$. Then we can deduce that there exists a $w'$-evaluation $e''$ such that either:

- $w' \Vdash \Psi'[e|_x e'|_y e'']$ for some $\mathbf{y}' \cdot \Psi' \in \Delta$, and we conclude immediately;

- or $w' \Vdash \hat{\Xi}_0\{\phi\}[e|_x e'|_y e'']$. Since $\text{fv}(\phi) \cap \mathbf{y} = \emptyset$ we have $w' \Vdash \phi[e|_x e'|_y e'']$, and thus $w' \Vdash \phi, \hat{\Xi}_0\{\phi\}[e|_x e'|_y e'']$. Then by Lemma B.13 we have $w' \Vdash \phi, \hat{\Xi}_0\{\}[e|_x e'|_y e'']$, and thus we can conclude in particular that $w' \Vdash \hat{\Xi}_0\{\}[e|_x e'|_y e'']$.

2. $\mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\}; \Delta \Vdash \mathbf{x} \cdot \Psi, \phi \sqcup \mathbf{y} \cdot \hat{\Xi}_0\{\phi\}; \Delta$ holds by the same argument in the other direction.
<figure><img src="image_21.png" /></figure>

Proving the soundness of rules involving binders (ipis, ipet, apis, apet) is also quite tedious, which can be understood as stemming from the fact that substitutions simulate the complex dynamics of the LoIs of EGs in a global rather than local way. In particular, one needs to be careful about the scope of bound variables, which in EGs would be handled locally with (de)iteration rules on LoIs.

**Lemma B.15 (Universal instantiation).** If $\sigma : y$ is capture-avoiding in $\Phi \sqcap \Delta$, then $x, y \cdot \Phi \sqcap \Delta \models x \cdot \sigma(\Phi) \sqcap \sigma(\Delta)$.

**Proof.** Let $w$ a world in some Kripke structure $\mathcal{K}$, $w' \ge w$, $e$ a $w$-evaluation and $e'$ a $w$'-evaluation such that $w \Vdash x, y \cdot \Phi \sqcap \Delta [e]$ and $w' \Vdash \sigma(\Phi) [e |_x e']$. Therefore $w' \Vdash \Phi [e |_x e' |_y [[\sigma]]_{e|_x e'}]$ by Lemma B.8, and thus $w' \Vdash \Phi [e |_{x \cup y} (e' |_y [[\sigma]]_{e|_x e'})]$ by Observation B.1. Then by hypothesis, there must be some $z \cdot \Psi \in \Delta$ and $w$'-evaluation $e''$ such that $w' \Vdash \Psi [e |_{x \cup y} (e' |_y [[\sigma]]_{e|_x e'}) |_z e'']$, and thus $w' \Vdash \Psi [e |_x e' |_y [[\sigma]]_{e|_x e'} |_z e'']$. Since $\sigma$ is capture-avoiding in $\Phi \sqcap \Delta$, we know that for any $x \in y$ we have $fv(\sigma(x)) \cap z = \emptyset$, and thus $[[\sigma(x)]]_{e|_x e' |_z e''} = [[\sigma(x)]]_{e|_x e'}$. Hence by Observation B.3 and Observation B.2 we get $w' \Vdash \Psi [e |_x e' |_z e'' |_y [[\sigma]]_{e|_x e' |_z e''}]$, and by Lemma B.8 we conclude that $w' \Vdash \sigma(\Psi) [e |_x e' |_z e'']$. ◀

<figure><img src="image_22.png" /></figure>

**Lemma B.16 (Existential instantiation).** If $\sigma : y$ is capture-avoiding in $\Phi$, then $\gamma \sqcap x \cdot \sigma(\Phi) ; \Delta \models \gamma \sqcap x, y \cdot \Phi ; \Delta$.

**Proof.** Let $\gamma = z \cdot \Xi$, and $w$ a world in some Kripke structure $\mathcal{K}$, $w' \ge w$, $e$ a $w$-evaluation and $e'$ a $w$'-evaluation such that $w \Vdash \gamma \sqcap x \cdot \sigma(\Phi) ; \Delta [e]$ and $w' \Vdash \Xi [e |_z e']$. Then by hypothesis, there must be some $w$'-evaluation $e''$ such that either:

- $w' \Vdash \Xi' [e |_z e' |_z e'']$ for some $z' \cdot \Xi' \in \Delta$, and we conclude immediately;

- or $w' \Vdash \sigma(\Phi) [e |_z e' |_x e'']$. Then by Lemma B.8 we have $w' \Vdash \Phi [e |_z e' |_x e'' |_y [[\sigma]]_{e|_x e' |_x e''}]$, and thus we can conclude with $w' \Vdash \Phi [e |_z e' |_{x \cup y} (e'' |_y [[\sigma]]_{e|_x e' |_x e''})]$ by Observation B.3.

<figure><img src="image_23.png" /></figure>

We are now equipped with enough lemmas to prove the soundness of each rule, starting with the *shallow* version of natural rules. In fact we are able to prove more: that every *Ξ*-rule is *invertible*, i.e. its conclusion entails its premiss.

**Lemma B.17 (Shallow soundness).** If $\Phi \to \Psi$, then $\Phi \nvDash \Psi$.

**Proof.** Let $w$ a world in some Kripke structure $\mathcal{K}$, $w' \ge w$, $e$ a $w$-evaluation and $e'$ a $w$'-evaluation. We proceed by inspection of every *Ξ*-rule.

**poll↓, poll↑** By Lemma B.14.

**epis**

1. Suppose that $w \Vdash \Phi [e]$. Then by Lemma B.7 we have $w' \Vdash \Phi [e]$, and thus we can conclude for instance with $w' \Vdash \Phi [e |_\emptyset e' |_\emptyset e]$.

2. Suppose that $w \Vdash \Delta \sqcap \Phi [e]$. Then since we trivially have $w \ge w$ and $w \Vdash \emptyset [e |_\emptyset e]$, we get that $w \Vdash \Phi [e |_\emptyset e |_\emptyset e'']$ for some $w$-evaluation $e''$, and thus $w \Vdash \Phi [e]$.

**epet** Let $\gamma = x \cdot \Phi$. We trivially have that $w' \Vdash \emptyset [e |_x e' |_\emptyset e]$, and thus can conclude.

**ipis** We trivially have $x, y \cdot \Phi \sqcap \Delta \models x, y \cdot \Phi \sqcap \Delta$ by Observation B.5, and thus we can conclude by Lemma B.15.
ipet The first direction is trivial by Lemma B.12. In the other direction, let $\gamma = z \cdot \Xi$, and suppose that $w \Vdash \gamma \Delta x \cdot \sigma(\Phi)$; $x, y \cdot \Phi$; $\Delta [e]$ and $w' \Vdash \Xi [e |_z e']$. Then there must be some $w'$-evaluation $e''$ such that either:

- $w' \Vdash \Xi' [e |_z e' |_{z'} e'']$ for some $z' \cdot \Xi' \in \Delta$, and we conclude immediately;

- $w' \Vdash \Phi [e |_z e' |_{x \cup y} e'']$, and we also conclude immediately;

- or $w' \Vdash \sigma(\Phi) [e |_z e' |_x e'']$, and we conclude with the same argument as in the proof of Lemma B.16.

srep Let $\gamma_i = y_i \cdot \Psi_i$ for $1 \le i \le n$.

1. Suppose that $w \Vdash x \cdot \Phi$, ($\Delta \{\gamma_i\}_i^n$) $\Delta \Delta [e]$ and $w' \Vdash \Phi [e |_x e']$. We show that $w' \Vdash \gamma_i \Delta \Delta [e |_x e']$ for all $1 \le i \le n$, i.e. for every $w'' \ge w'$ and $w''$-evaluation $e''$, $w'' \Vdash \Psi_i [e |_x e' |_{y_i} e'']$ implies that there is some $z \cdot \Xi \in \Delta$ and $w''$-evaluation $e'''$ such that $w'' \Vdash \Xi [e |_x e' |_{y_i} e'' |_z e''']$. By assumption, Lemma B.7 and the fact that $fv(\Phi) \cap y_i = \emptyset$, we have $w'' \Vdash \Phi [e |_x e' |_{y_i} e'']$. Also since $w'' \Vdash \Psi_i [e |_x e' |_{y_i} e'']$ we immediately get $w'' \Vdash \Delta \{\gamma_i\}_i^n [e |_x e']$, and thus $w'' \Vdash \Delta \{\gamma_i\}_i^n [e |_x e' |_{y_i} e'']$ since $fv(\Delta \{\gamma_i\}_i^n) \cap y_i = \emptyset$. Thus by Observation B.1 we have $w'' \Vdash \Phi$, ($\Delta \{\gamma_i\}_i^n$) $[e |_{x \cup y_i} (e' |_{y_i} e'')]$, and by hypothesis (and the fact that $w'' \ge w$ by transitivity) we obtain that $w'' \Vdash \Xi [e |_{x \cup y_i} (e' |_{y_i} e'') |_z e''']$ for some $z \cdot \Xi \in \Delta$ and $w''$-evaluation $e''''$. Then we conclude again by Observation B.1.

2. Suppose that $w \Vdash x \cdot \Phi \Delta \{\gamma_i \Delta \Delta\}_i^n [e]$ and $w' \Vdash \Phi, (\Delta \{\gamma_i\}_i^n) [e |_x e']$. Then there must be some $1 \le i \le n$ and $w'$-evaluation $e''$ such that $w' \Vdash \Psi_i [e |_x e' |_{y_i} e'']$, and for all $1 \le j \le n$ we know that $w' \Vdash \gamma_j \Delta \Delta [e |_x e']$. Thus since $w' \le w'$ by reflexivity, there must be some $z \cdot \Xi \in \Delta$ and $w'$-evaluation $e'''$ such that $w' \Vdash \Xi [e |_x e' |_{y_i} e'' |_z e''']$, and we can conclude with $w' \Vdash \Xi [e |_x e' |_{y_i \cup z} (e'' |_z e''')]$ by Observation B.1.

<figure><img src="image_24.png" /></figure>

Then the soundness of the contextual closure of natural rules follows immediately from functoriality:

► **Lemma B.18 (Natural soundness).** If $\Phi \to_* \Psi$ then $\Phi \nvDash \Psi$.

**Proof.** By Lemma B.17 and Lemma B.10.

<figure><img src="image_25.png" /></figure>

The soundness of cultural rules is straightforward with the previous lemmas:

► **Lemma B.19 (Cultural soundness).** If $\Phi \to_* \Psi$ then $\Psi \Vdash \Phi$.

**Proof.** By inspection of every $\to_*$-rule.

grow, crop By Lemma B.11 and Lemma B.10.

pull, glue By Lemma B.12 and Lemma B.10.

apis By Lemma B.15 and Lemma B.10.

apet By Lemma B.16 and Lemma B.10.

<figure><img src="image_26.png" /></figure>

Then it follows that every derivation in the flower calculus is sound:

► **Theorem B.20.** If $\Phi \to^* \Psi$ then $\Psi \Vdash \Phi$.

**Proof.** By Lemma B.18, Lemma B.19 and Observation B.5, Observation B.6.

<figure><img src="image_27.png" /></figure>

In particular $\vdash \phi$ implies $\Vdash \phi$, i.e. every provable flower is true.
# C Detailed proofs

## C.1 Deduction theorems

**▶ Lemma C.1 (Positive closure).** If $\Phi \to \Psi$, then $\hat{\Xi}^+\{\Phi\} \to \hat{\Xi}^+\{\Psi\}$.

**Proof.** In the case of a natural step $\Phi \to_* \Psi$, this is immediate by contextual closure (Definition 6.5). Otherwise we have a cultural step $\hat{\Xi}'\{\Phi_0\} \to_* \hat{\Xi}'\{\Psi_0\}$. Then either $\hat{\Xi}'$ is positive, and $\mathrm{inv}(\hat{\Xi}^+\{\hat{\Xi}'\}) = \mathrm{inv}(\hat{\Xi}^+) + \mathrm{inv}(\hat{\Xi}')$ is even since it is the sum of two even numbers; or $\hat{\Xi}'$ is negative, and $\mathrm{inv}(\hat{\Xi}^+\{\hat{\Xi}'\})$ is odd since it is the sum of an even and an odd number. In both cases $\hat{\Xi}^+\{\hat{\Xi}'\}$ has the same polarity as $\hat{\Xi}'$, and thus the same rule can be applied. ◀

### C.1.1 Proof of Theorem 6.7

**Proof.** Suppose that $\Phi \to^* \Psi$. Then we have:

$$ \begin{array}{lcl} \Psi \downarrow \Phi & \to^* & \Psi \downarrow \Psi \quad (\text{Hypothesis + Lemma C.1}) \\ & \to_{\text{poll}\downarrow} & \Psi \downarrow \cdot \\ & \to_{\text{epet}} & \emptyset \end{array} $$

In the other direction, suppose that $\Psi \downarrow \Phi \to^* \emptyset$. Then we have:

$$ \begin{array}{rcl} \Phi & \to_{\text{epis}} & \mathbf{D}\Phi \\ & \to_{\text{grow}} & (\Psi \downarrow \Phi), (\mathbf{D}\Phi) \\ & \to_{\text{poll}\uparrow} & (\Psi \downarrow \Phi), ((\Psi \downarrow \Phi) \downarrow \Phi) \\ & \to^* & (\Psi \downarrow \Phi) \downarrow \Phi \quad (\text{Hypothesis + Lemma C.1}) \\ & \to_{\text{grow}} & \Psi, ((\Psi \downarrow \Phi) \downarrow \Phi) \\ & \to_{\text{poll}\downarrow} & \Psi, ((\mathbf{D}\Phi) \downarrow \Phi) \\ & \to_{\text{srep}} & \Psi, (\mathbf{D}(\Phi \downarrow \Phi)) \\ & \to_{\text{poll}\downarrow} & \Psi, (\mathbf{D}(\Phi \downarrow \cdot)) \\ & \to_{\text{epet}} & \Psi, (\mathbf{D}\cdot) \\ & \to_{\text{epet}} & \Psi \end{array} $$

### C.1.2 Proof of Theorem 6.9

**Proof.** Let $\hat{\Xi}$ be some context. If $\Psi \vdash_* \Phi$, then in particular $\hat{\Xi}'\{\Phi\} \to_* \hat{\Xi}'\{\}\}$ for $\hat{\Xi}' := \hat{\Xi}\{\Psi \downarrow \}$ □. Thus we have:

$$ \hat{\Xi}\{\Psi \downarrow \Phi\} \to_* \hat{\Xi}\{\Psi \downarrow \cdot \} \to_{\text{epet}} \hat{\Xi}\{\} $$

In the other direction, let $\hat{\Xi}$ be some context such that $\Psi \succ \hat{\Xi}$. If $\vdash_* \Psi \downarrow \Phi$, then in particular $\hat{\Xi}\{\Psi \downarrow \Phi\} \to_* \hat{\Xi}\{\}\}$. Thus we have:

$$ \hat{\Xi}\{\Phi\} \to_{\text{epis}} \hat{\Xi}\{\mathbf{D}\Phi\} \to_{\text{poll}\uparrow} \hat{\Xi}\{\Psi \downarrow \Phi\} \to_* \hat{\Xi}\{\} $$

## C.2 Completeness

**▶ Lemma C.2 (Reflexivity).** For any *bouquet* $\Phi$, $\Phi \vdash_* \Phi$.

**Proof.** Trivial by application of the poll↓ rule. ◀
**Lemma C.3 (Weakening).** If $\mathcal{T} \subseteq \mathcal{T}'$ and $\mathcal{T} \vdash \phi$, then $\mathcal{T}' \vdash \phi$.

**Proof.** This follows immediately from Definition 8.1.

<figure><img src="image_28.png" /></figure>

In the following, we suppose some enumeration $(\phi_n)_{n \in \mathbb{N}}$ of $\mathbb{F}$, which should be definable constructively given the inductive nature of flowers. Let $\psi \in \mathbb{F}$, and $\mathcal{T}$ a $\psi$-consistent theory. We now define the completion procedure, which constructs an extension $\mathrm{Com}(\mathcal{T}) \supseteq \mathcal{T}$ with the property that $\mathrm{Com}(\mathcal{T})$ is $\psi$-consistent and $\psi$-complete.

**Definition C.4 (n-completion).** The n-completion $\mathrm{Com}^n(\mathcal{T})$ of $\mathcal{T}$ is defined recursively by:

$$ \mathrm{Com}^0(\mathcal{T}) = \mathcal{T} \qquad \mathrm{Com}^{n+1}(\mathcal{T}) = \begin{cases} \mathrm{Com}^n(\mathcal{T}) \cup \phi_n & \text{if } \mathrm{Com}^n(\mathcal{T}) \cup \phi_n \text{ is } \psi\text{-consistent} \\ \mathrm{Com}^n(\mathcal{T}) & \text{otherwise} \end{cases} $$

**Definition C.5 (Completion).** The completion $\mathrm{Com}(\mathcal{T})$ of $\mathcal{T}$ is the denumerable union of all n-completions:

$$ \mathrm{Com}(\mathcal{T}) = \bigcup_{n \in \mathbb{N}} \mathrm{Com}^n(\mathcal{T}) $$

**Lemma C.6.** For every $\psi \in \mathbb{F}$, $\mathrm{Com}(\mathcal{T})$ is $\psi$-consistent and $\psi$-complete.

**Proof.** For $\psi$-consistency, it is immediate by induction on $n$ that $\mathrm{Com}^n(\mathcal{T})$ is $\psi$-consistent. Then suppose that $\mathrm{Com}(\mathcal{T}) \vdash_{\oplus} \psi$, that is there is some bouquet $\Phi \subseteq \mathrm{Com}(\mathcal{T})$ such that $\Phi \vdash_{\oplus} \psi$. For each $\phi \in \Phi$, there is some rank $n$ such that $\phi \in \mathrm{Com}^n(\mathcal{T})$. Let $m$ be the greatest such rank. Then $\Phi \subseteq \mathrm{Com}^m(\mathcal{T})$, and thus by weakening (Lemma C.3) $\Phi \nvdash_{\oplus} \psi$. Contradiction.

For $\psi$-completeness, suppose that there is some $\phi$ such that $\mathrm{Com}(\mathcal{T})$, $\phi \nvdash_{\oplus} \psi$ and $\phi \notin \mathrm{Com}(\mathcal{T})$, and let $\phi = \phi_n$. Then $\mathrm{Com}(\mathcal{T}) \cup \phi_n$ is $\psi$-consistent, and thus by weakening (Lemma C.3) so is $\mathrm{Com}^n(\mathcal{T}) \cup \phi_n$. This entails that $\phi_n \in \mathrm{Com}^{n+1}(\mathcal{T}) \subseteq \mathrm{Com}(\mathcal{T})$. Contradiction. ◀

<figure><img src="image_29.png" /></figure>

### C.2.1 Proof of Lemma 8.6

**Proof.** By induction on $|\phi|$.

Suppose $\phi = p(\bar{x})$.

1. By definition of forcing (Definition 7.5) and ⋆($\psi$) (Definition 8.5), $\mathcal{T} \Vdash p(\bar{x})[\sigma]$ precisely when $\sigma(p(\bar{x})) \in \mathcal{T}$.

2. Suppose that $\mathcal{T} \Vdash \phi[\sigma]$, that is $\sigma(\phi) \in \mathcal{T}$. Then by weakening (Lemma C.3), we get $\sigma(\phi) \nvdash_{\oplus} \sigma(\phi)$. But this is impossible by reflexivity of $\vdash$ (Lemma C.2).

Suppose $\phi = \mathbf{x} \cdot \Phi \sqcup \{\mathbf{x}_i \cdot \Phi_i\}_i^n$.

1. Let $\mathcal{U} \supseteq \mathcal{T}$ be a $\psi$-consistent and $\psi$-complete theory. Obviously $\sigma(\phi) = \mathbf{x} \cdot \sigma|_{\mathbf{x}}(\Phi) \sqcup \{\mathbf{x}_i \cdot \sigma|_{\mathbf{x} \cup \mathbf{x}_i}(\Phi_i)\}_i^n \in \mathcal{U}$, and thus by Proposition 8.3, for every substitution $\tau$, either $|_{\mathbf{x}}\tau \circ \sigma|_{\mathbf{x} \cup \mathbf{x}_i}(\Phi_i) = \sigma|_{\mathbf{x}}\tau|_{\mathbf{x}_i}(\Phi_i) \subseteq \mathcal{U}$ for some $1 \le i \le n$, or $\mathbf{U} \nvdash_{\oplus} |_{\mathbf{x}}\tau \circ \sigma|_{\mathbf{x}}(\Phi) = \sigma|_{\mathbf{x}}\tau(\Phi)$. In the first case, we get $\mathcal{U} \Vdash \Phi_i[\sigma|_{\mathbf{x}}\tau|_{\mathbf{x}_i}]$ by IH. In the second case, we get $\mathcal{U} \nVdash \Phi[\sigma|_{\mathbf{x}}\tau]$ by IH. In other words, $\mathcal{U} \Vdash \Phi[\sigma|_{\mathbf{x}}\tau]$ implies $\mathcal{U} \Vdash \Phi_i[\sigma|_{\mathbf{x}}\tau|_{\mathbf{x}_i}]$, that is $\mathcal{T} \Vdash \phi[\sigma]$.

2. By Proposition 8.4, for every $1 \le i \le n$ and substitution $\tau$, there is some $\phi_i \in \Phi_i$ such that $\mathbf{T}$, $\sigma|_{\mathbf{x}}(\Phi) \nvdash_{\oplus} |_{\mathbf{x}_i}\tau \circ \sigma|_{\mathbf{x} \cup \mathbf{x}_i}(\phi_i) = \sigma|_{\mathbf{x}}|_{\mathbf{x}_i}\tau(\phi_i)$. By the completion procedure, we get a theory $\mathcal{U} = \mathrm{Com}(\mathcal{T} \cup \sigma|_{\mathbf{x}}(\Phi)) \supseteq \mathcal{T} \cup \sigma|_{\mathbf{x}}(\Phi)$ which is both $\sigma|_{\mathbf{x}}|_{\mathbf{x}_i}\tau(\phi_i)$-consistent and $\sigma|_{\mathbf{x}}|_{\mathbf{x}_i}\tau(\phi_i)$-complete (Lemma C.6). Then by IH, $\mathcal{U} \Vdash \Phi[\sigma|_{\mathbf{x}}]$ since $\sigma|_{\mathbf{x}}(\Phi) \subseteq \mathcal{U}$, and $\mathcal{U} \nVdash \phi_i[\sigma|_{\mathbf{x}}|_{\mathbf{x}_i}\tau]$ since $\mathcal{U}$ is $\sigma|_{\mathbf{x}}|_{\mathbf{x}_i}\tau(\phi_i)$-consistent, that is $\mathcal{T} \nVdash \phi[\sigma]$.

<figure><img src="image_30.png" /></figure>
### C.2.2 Proof of Theorem 8.7

**Proof.** Let $\mathcal{T}$ be a $\psi$-consistent theory. We prove that $\mathcal{T} \not\models \psi$ by showing in particular that $\mathcal{T} \not\models_{\star(\psi)} \psi$, and more specifically that $\text{Com}(\mathcal{T}) \vdash \mathcal{T}[1]$ but $\text{Com}(\mathcal{T}) \not\vdash \psi[1]$. Then it follows by (classical) contraposition that $\mathcal{T} \vdash \psi$ implies $\mathcal{T} \vdash_{\star} \psi$ for any $\psi$ and any $\mathcal{T}$, and thus we can conclude.

- Let $\phi \in \mathcal{T}$. Then $1(\phi) = \phi \in \text{Com}(\mathcal{T})$, thus by $\psi$-consistency and $\psi$-completeness of the completion (Lemma C.6), one can apply adequacy (Lemma 8.6) to get $\text{Com}(\mathcal{T}) \vdash \phi[1]$.

- Similarly, we can apply adequacy (Lemma 8.6) to get $\text{Com}(\mathcal{T}) \not\vdash \psi[1]$.

<figure><img src="image_31.png" /></figure>