Elementary-base cirquent calculus II: Choice quantifiers

TL;DR

This paper introduces CL17, a first-order extension of cirquent calculus with choice quantifiers, which is sound, complete, and decidable, advancing the logical framework for elementary games and computability logic.

Contribution

It constructs the first-order version CL17 of the propositional calculus CL16, incorporating choice quantifiers and establishing its soundness, completeness, and decidability.

Findings

CL17 is sound and complete for elementary games.

CL17 is decidable, unlike classical predicate calculus.

It extends the previous propositional calculus with first-order features.

Abstract

Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article "Elementary-base cirquent calculus I: Parallel and choice connectives" built the sound and complete axiomatization CL16 of a propositional fragment of computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). The atoms of the language of CL16 represent elementary, i.e., moveless, games, and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version CL17 of CL16, also enjoying soundness and completeness. The language of CL17 augments that of CL18 by including choice quantifiers. Unlike classical predicate calculus, CL17 turns out to be decidable.

Equations

$$X\bigl{[}\bigl{(}(A\wedge C\sqcap^{\mathfrak{b}}D)\sqcap^{\mathfrak{a}}(B\wedge C\sqcap^{\mathfrak{b}}D)\bigr{)}\sqcap^{\mathfrak{c}}\bigl{(}(A\sqcap^{\mathfrak{a}}B\wedge C)\sqcap^{\mathfrak{b}}(A\sqcap^{\mathfrak{a}}B\wedge D)\bigr{)}\bigr{]}\leadsto X[A\sqcap^{\mathfrak{a}}B\wedge C\sqcap^{\mathfrak{b}}D],$$

$$X[\mbox{\large$\sqcap$}^{\mathfrak{a}}x(A\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}yB)\sqcap^{\mathfrak{c}}\mbox{\large$\sqcap$}^{\mathfrak{b}}y(\mbox{\large$\sqcap$}^{\mathfrak{a}}xA\wedge B)]\leadsto X[\mbox{\large$\sqcap$}^{\mathfrak{a}}xA\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}yB],$$

$$X\bigl{[}\bigl{(}(A\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}xC)\sqcap^{\mathfrak{a}}(B\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}xC)\bigr{)}\sqcap^{\mathfrak{c}}\mbox{\large$\sqcap$}^{\mathfrak{b}}x(A\sqcap^{\mathfrak{a}}B\wedge C)\bigr{]}\leadsto X[A\sqcap^{\mathfrak{a}}B\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}xC],$$

$$X[\mbox{\large$\sqcap$}^{\mathfrak{a}}x(A\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}yB)\sqcap^{\mathfrak{c}}\mbox{\large$\sqcap$}^{\mathfrak{b}}y(\mbox{\large$\sqcap$}^{\mathfrak{a}}xA\wedge B)]\leadsto X[\mbox{\large$\sqcap$}^{\mathfrak{a}}xA\wedge\mbox{\large$\sqcap$}^{\mathfrak{b}}yB]$$

Full text

MSC: primary: 03B47; secondary: 03B70; 03F03; 03F20; 68T15.

Keywords: Proof theory; Cirquent calculus; Resource semantics; Deep inference; Computability logic

1 Preface

Cirquent calculus is a family of deep inference (cf. [1]) proof systems permitting various sorts of component-sharing between different parts of logical expressions. The earlier article [8] constructed a cirquent calculus system CL16 for the elementary-base, recurrence-free propositional fragment of computability logic (the game-semantically conceived logic of computational problems introduced in [2]) and proved its soundness and completeness. The present article takes that result to the first-order level, with the so called choice quantifiers. The resulting system CL17, in contrast to its classical counterpart, is a decidable predicate logic. While a variety of propositional systems have been built by now in cirquent calculus [3, 4, 6, 7, 8, 9, 10, 11], CL17 is the first cirquent calculus system with quantifiers. The formal semantics for its language (and beyond) was set up in [5], but no axiomatizations had been attempted so far.

Being a continuation of [8] in the proper sense, the present article should only be read in combination with its predecessor, as it relies on but does not reintroduce the main concepts from [8]. Nor does it discuss related literature or the relevant motivations and philosophy underlying cirquent calculus and computability logic, as this, again, is done in [8].

The language of CL17 extends that of CL16 by augmenting its logical vocabulary with the choice universal quantifier $\sqcap$ (“chall”) and choice existential quantifier $\sqcup$ (“chexists”), and allowing atoms of any arities. Throughout this article, for simplicity, we assume that the universe of discourse is always the set $\mathbb{N}$ of natural numbers, by innocent abuse of concepts identified with the corresponding decimal numerals. If so, \mbox{\large\sqcap}xG(x) is the game where, at the beginning of a play, the environment chooses one of $n\in\mathbb{N}$, after which the game continues as $G(n)$; if such a choice is never made, then the environment loses. \mbox{\large\sqcup}xG(x) is similar, only here it is the machine who can and must make an initial choice. Thus, \mbox{\large\sqcap}xG(x) is in fact nothing but the infinite choice conjunction $G(0)\sqcap G(1)\sqcap G(2)\sqcap\cdots$, and \mbox{\large\sqcup}xG(x) is the infinite choice disjunction $G(0)\sqcup G(1)\sqcup G(2)\sqcup\cdots$.

2 Syntax

The language of CL17 is the same as that of first-order classical logic, only with the quantifiers $\forall,\exists$ replaced by their choice (“constructive”) counterparts \mbox{\large\sqcap},\mbox{\large\sqcup}, and additionally including the choice connectives $\sqcap,\sqcup$ as well as the decimal numerals $0,1,2,\cdots$ referred to as constants. We will be typically using $x,y,z,\cdots$ as metavariables for the variables of the language, $p,q,r,\cdots$ for its predicate letters, and $a,b,c\cdots$ for its constants.

We fix four pairwise disjoint infinite sets $\mathbb{C}(\sqcup)$, $\mathbb{C}(\sqcap)$, \mathbb{C}(\mbox{\large\sqcup}) and \mathbb{C}(\mbox{\large\sqcap}), whose elements will be referred to as $\sqcup$-clusters, $\sqcap$-clusters, $\sqcup$****-clusters and $\sqcap$****-clusters, respectively. The Gothic letters $\mathfrak{a},\mathfrak{b},\mathfrak{c},\cdots$ will be used as metavariables for clusters.

A term is either a variable or a constant. A nonlogical atom is $p(t_{1},\cdots,t_{n})$, where $p$ is an $n$-ary predicate letter and $t_{1},\cdots,t_{n}$ are terms. A nonlogical literal is either $A$ or $\neg A$, where $A$ is a nonlogical atom. The expressions $\top$ and $\bot$ are said to be logical literals. A (choice) universal quantor (resp. existential quantor) is the expression \mbox{\large\sqcap}^{\mathfrak{c}} (resp. \mbox{\large\sqcup}^{\mathfrak{c}}), where $\mathfrak{c}$ is a $\sqcap$- (resp. $\sqcup$-) cluster.

Definition 2.1

A cirquent is defined inductively as follows:

• •

Each (logical or nonlogical) literal is a cirquent.

• •

If $A$ and $B$ are cirquents, then $(A)\wedge(B)$ is a cirquent.

• •

If $A$ and $B$ are cirquents, then $(A)\vee(B)$ is a cirquent.

• •

If $A$ and $B$ are cirquents and $\mathfrak{c}$ is a $\sqcap$-cluster, then $(A)\sqcap^{\mathfrak{c}}(B)$ is a cirquent.

• •

If $A$ and $B$ are cirquents and $\mathfrak{c}$ is a $\sqcup$-cluster, then $(A)\sqcup^{\mathfrak{c}}(B)$ is a cirquent.

• •

If $A$ is a cirquent, $x$ is a variable and $\mathfrak{c}$ is a $\sqcap$-cluster, then \mbox{\large\sqcap}^{\mathfrak{c}}x(A) is a cirquent.

• •

If $A$ is a cirquent, $x$ is a variable and $\mathfrak{c}$ is a $\sqcup$-cluster, then \mbox{\large\sqcup}^{\mathfrak{c}}x(A) is a cirquent.

A cirquent of the form $(A)\wedge(B)$ is said to be $\wedge$-rooted, a cirquent of the form $A\sqcap^{\mathfrak{c}}B$ is said to be $\sqcap^{\mathfrak{c}}$-rooted, and similarly for \vee,\sqcup^{\mathfrak{c}},\mbox{\large\sqcap}^{\mathfrak{c}},\mbox{\large\sqcup}^{\mathfrak{c}}. If we simply say “$\sqcap$-rooted”, it should be understood as “$\sqcap^{\mathfrak{c}}$-rooted for whatever $\mathfrak{c}$”. Similarly for \sqcup,\mbox{\large\sqcap},\mbox{\large\sqcup}.

As in [8], negation is only allowed to be applied to atoms. \neg\mbox{\large\sqcap}^{\mathfrak{c}}xF should be understood as an abbreviation of \mbox{\large\sqcup}^{\mathfrak{c}}x\neg F, and \neg\mbox{\large\sqcup}^{\mathfrak{c}}xF as an abbreviation of \mbox{\large\sqcap}^{\mathfrak{c}}x\neg F. All other conventions of [8] regarding the usage of $\neg$ and $\rightarrow$ remain in force.

When omitting parentheses in cirquents, our convention is that $\neg$, \mbox{\large\sqcap}^{\mathfrak{c}}x and \mbox{\large\sqcup}^{\mathfrak{c}}x have the highest precedence, then comes $\rightarrow$, then $\sqcap^{\mathfrak{c}}$ and $\sqcup^{\mathfrak{c}}$, and then $\wedge$ and $\vee$.

All (other) standard terminological and notational conventions of traditional logic also remain in force. This includes the concepts of free and bound occurrences of variables, or the practice of representing a cirquent as $A(x)$ when first mentioning it, and then writing $A(t)$ to mean the result of replacing in $A(x)$ all free occurrences of the variable $x$ by the term $t$. A cirquent is said to be closed iff it has no free occurrences of variables.

3 Semantics

We (re)define LegalRuns as the set of all runs $\Gamma$ satisfying the following conditions:

Every move of $\Gamma$ is the string $\mathfrak{c}.a$, where either (1) $\mathfrak{c}$ is a $\sqcap$- or $\sqcup$-cluster and $a\in\{0,1\}$, or (2) $\mathfrak{c}$ is a $\sqcap$- or $\sqcup$-cluster and $a\in\mathbb{N}$. 2. 2.

Whenever $\Gamma$ contains a move $\mathfrak{c}.a$ where $\mathfrak{c}$ is a $\sqcap$- or $\sqcap$-cluster, the move is $\bot$-labeled. 3. 3.

Whenever $\Gamma$ contains a move $\mathfrak{c}.a$ where $\mathfrak{c}$ is a $\sqcup$- or $\sqcup$-cluster, the move is $\top$-labeled. 4. 4.

For any cluster $\mathfrak{c}$, $\Gamma$ contains at most one move of the form $\mathfrak{c}.a$.

The intuitive meaning of condition 1 is that every move signifies either a choice between “left” ([math]) and “right” ($1$) in a $\sqcap$- or $\sqcup$-cluster, or a choice among the constants $0,1,2,\cdots$ in some $\sqcap$- or $\sqcup$-cluster. Conditions 2 and 3 say that the environment moves (chooses) only in $\sqcap$- or $\sqcap$-clusters, and the machine only in $\sqcup$- or $\sqcup$-clusters. Finally, condition 4 says that, in any given cluster, a choice can be made only once.

As in [8], given a run $\Gamma\in LegalRuns$, we say that a cirquent of the form $A\sqcup^{\mathfrak{c}}B$ or $A\sqcap^{\mathfrak{c}}B$ is $\Gamma$-resolved iff $\Gamma$ contains one of the moves $\mathfrak{c}.0$ or $\mathfrak{c}.1$; then by the $\Gamma$-resolvent of the cirquent we mean $A$ if such a move is $\mathfrak{c}.0$, and $B$ if it is $\mathfrak{c}.1$. Extending this terminology to quantifiers, we say that a cirquent of the form \mbox{\large\sqcup}^{\mathfrak{c}}xA(x) or \mbox{\large\sqcap}^{\mathfrak{c}}xA(x) is $\Gamma$-resolved iff $\Gamma$ contains the move $\mathfrak{c}.a$ for some constant $a$; then by the $\Gamma$-resolvent of such a cirquent we mean $A(a)$. Sometimes, instead of saying that the cirquent $A\sqcup^{\mathfrak{c}}B$ (or $A\sqcap^{\mathfrak{c}}B$, or \mbox{\large\sqcap}^{\mathfrak{c}}xA(x), or \mbox{\large\sqcup}^{\mathfrak{c}}xA(x)) is resolved, we may simply say that the cluster $\mathfrak{c}$ is resolved. In all cases, as expected, “unresolved” means “not resolved”.

An interpretation is a function ∗ that assigns to every $n$-ary predicate letter $p$ a relation $p^{*}\subseteq\mathbb{N}^{n}$. When $(c_{1},\cdots,c_{n})\in p^{*}$, we say that ∗ makes the atom $p(c_{1},\cdots,c_{n})$ true, or simply that $p^{*}(c_{1},\cdots,c_{n})$ is true. As usual, “false” means “not true”. The concepts of truth and falsity extend to $\top$, $\bot$ and all $\neg,\wedge,\vee$-combinations of closed atoms in the standard way: $\top^{*}$ is always true; $\bot^{*}$ is always false; $(\neg A)^{*}$ is true iff $A^{*}$ is false; $(A\wedge B)^{*}$ is true iff both $A^{*}$ and $B^{*}$ are true; $(A\vee B)^{*}$ is true iff at least one of $A^{*},B^{*}$ is true. When a cirquent is represented as $A(t)$, we usually write $A^{*}(t)$ instead of \bigl{(}A(t)\bigr{)}^{*}.

Remember from [8] that, when we say “won” without specifying a player (as in the following definition), it always means “won by the machine”. Similarly for “lost”.

Definition 3.1

Every closed cirquent $C$ and interpretation ∗ induces a unique game $C^{*}$, which we refer to as “$C$ under ∗”, defined as follows. The set $\mbox{\bf Lr}^{C^{*}}$ of legal runs of such a game is nothing but LegalRuns. Since $\mbox{\bf Lr}^{C^{*}}$ does not depend on $C$ or ∗, subsequently we shall simply say “legal run” rather than “legal run of $C^{*}$”. The $\mbox{\bf Wn}^{C^{*}}$ component of the game $C^{*}$ is defined by stipulating that a legal run $\Gamma$ is a won run of $C^{*}$ iff one of the following conditions is satisfied:

1. $C$ is a literal and $C^{*}$ is true.

2. $C$ has the form $A_{0}\wedge A_{1}$ (resp. $A_{0}\vee A_{1}$) and, for both (resp. at least one) $i\in\{0,1\}$, $\Gamma$ is a won run of $A_{i}^{*}$.

3. $C$ is a $\Gamma$-resolved $\sqcap$-, $\sqcup$-, $\sqcap$- or $\sqcup$-rooted cirquent and, where $B$ is the resolvent, $\Gamma$ is a won run of $B^{*}$.

4. $C$ is a $\Gamma$-unresolved $\sqcap$- or $\sqcap$-rooted cirquent.

When an interpretation ∗ is fixed in the context or is irrelevant, by abuse of notation we may omit explicit references to it, and identify a cirquent $C$ with the game $C^{*}$. For instance, we may say that the machine wins $C$ instead of saying that the machine wins $C$ under ∗.

Definition 3.2

Consider a closed cirquent $C$.

1. For an interpretation ∗, a solution of $C$ under ∗, or simply a solution of $C^{*}$, is an HPM $\cal H$ such that ${\cal H}\models C^{*}$. We say that $C$ is computable under ∗, or simply that $C^{*}$ is computable, iff $C^{*}$ has a solution.

2. A logical solution of $C$ is an HPM $\cal H$ such that, for any interpretation ∗, $\cal H$ is a solution of $C^{*}$. We say that $C$ is (logically) valid if it has a logical solution; otherwise $C$ is invalid.

4 Axiomatics

Just like CL16, our present system CL17 has $\top$ as its only axiom. The inference rules of CL17 are listed below, where all notational conventions from [8] remain in force. Note that all rules of CL16 are also rules of CL17, even if “somewhat” renamed.

Por-commutativity:

$X[B\vee A]\leadsto X[A\vee B]$.

Pand-commutativity:

$X[B\wedge A]\leadsto X[A\wedge B]$.

Por-associativity:

$X[A\vee(B\vee C)]\leadsto X[(A\vee B)\vee C]$.

Pand-associativity:

$X[A\wedge(B\wedge C)]\leadsto X[(A\wedge B)\wedge C]$.

Por-identity:

$X[A]\leadsto X[A\vee\bot]$.

Pand-Identity:

$X[A]\leadsto X[A\wedge\top]$.

Por-domination:

$X[\top]\leadsto X[A\vee\top]$.

Pand-domination:

$X[\bot]\leadsto X[A\wedge\bot]$.

Left chor-choosing:

$X[A_{1},\cdots,A_{n}]\leadsto X[A_{1}\sqcup^{\mathfrak{c}}B_{1},\cdots,A_{n}\sqcup^{\mathfrak{c}}B_{n}]$,  where $A_{1}\sqcup^{\mathfrak{c}}B_{1}$, $\cdots$, $A_{n}\sqcup^{\mathfrak{c}}B_{n}$ are all $\sqcup^{\mathfrak{c}}$-rooted subcirquents of the conclusion.

Right chor-choosing:

$X[B_{1},\cdots,B_{n}]\leadsto X[A_{1}\sqcup^{\mathfrak{c}}B_{1},\cdots,A_{n}\sqcup^{\mathfrak{c}}B_{n}]$,  where $A_{1}\sqcup^{\mathfrak{c}}B_{1}$, $\cdots$, $A_{n}\sqcup^{\mathfrak{c}}B_{n}$ are all $\sqcup^{\mathfrak{c}}$-rooted subcirquents of the conclusion.

Chexists-choosing:

X[A_{1}(a),\cdots,A_{n}(a)]\leadsto X[\mbox{\large\sqcup}^{\mathfrak{c}}x_{1}A_{1}(x_{1}),\cdots,\mbox{\large\sqcup}^{\mathfrak{c}}x_{n}A_{n}(x_{n})], where $a$ is any constant and \mbox{\large\sqcup}^{\mathfrak{c}}x_{1}A_{1}(x_{1}),\cdots,\mbox{\large\sqcup}^{\mathfrak{c}}x_{n}A_{n}(x_{n}) are all \mbox{\large\sqcup}^{\mathfrak{c}}-rooted subcirquents of the conclusion.

Left chand-cleansing:

X\bigl{[}Y[A]\sqcap^{\mathfrak{c}}C\bigr{]}\leadsto X\bigl{[}Y[A\sqcap^{\mathfrak{c}}B]\sqcap^{\mathfrak{c}}C\bigr{]}.

Right chand-cleansing:

X\bigl{[}C\sqcap^{\mathfrak{c}}Y[B]\bigr{]}\leadsto X\bigl{[}C\sqcap^{\mathfrak{c}}Y[A\sqcap^{\mathfrak{c}}B]\bigr{]}.

Chall-cleansing:

X\bigl{[}\mbox{\large\sqcap}^{\mathfrak{c}}xY[A(x)]\bigr{]}\leadsto X\bigl{[}\mbox{\large\sqcap}^{\mathfrak{c}}xY[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)]\bigr{]}.

Pand-distribution:

$X[(A\vee C)\wedge(B\vee C)]\leadsto X[(A\wedge B)\vee C]$.

Chand-distribution:

$X[(A\vee C)\sqcap^{\mathfrak{c}}(B\vee C)]\leadsto X[(A\sqcap^{\mathfrak{c}}B)\vee C]$.

Chall-distribution:

X[\mbox{\large\sqcap}^{\mathfrak{c}}x(A\vee B)]\leadsto X[\mbox{\large\sqcap}^{\mathfrak{c}}xA\vee B], where $x$ has no free occurrences in $B$.

Trivialization:

$X[\top]\leadsto X[\neg A\vee A]$, where $A$ is a nonlogical atom.

Chandchotomy:

[TABLE]

where $\mathfrak{c}$ does not occur in the conclusion.

Challchotomy:

[TABLE]

where $\mathfrak{c}$ does not occur in the conclusion, $x$ has no free occurrences in \mbox{\large\sqcap}^{\mathfrak{b}}yB and $y$ has no free occurrences in \mbox{\large\sqcap}^{\mathfrak{a}}xA.

Chandallchotomy:

[TABLE]

where $\mathfrak{c}$ does not occur in the conclusion and $x$ has no free occurrences in $A\sqcap^{\mathfrak{a}}B$.

Chand-splitting:

$A,B\leadsto A\sqcap^{\mathfrak{c}}B$, where neither $A$ nor $B$ has occurrences of $\mathfrak{c}$.

Chall-splitting:

A(a)\leadsto\mbox{\large\sqcap}^{\mathfrak{c}}xA(x), where neither $\mathfrak{c}$ nor $a$ has occurrences in $A(x)$.

We will be using the word “Commutativity” as a common name of Por-commutativity and Pand-commutativity. Similarly for all other rules. Throughout the rest of this article, “$A$ is provable” always means “$A$ is provable in CL17”, written $\mbox{{\bf CL17}}\vdash A$.

Example 4.1

The cirquent \mbox{\large\sqcup}^{\mathfrak{a}}xp(x)\vee\mbox{\large\sqcup}^{\mathfrak{b}}xp(x)\rightarrow\mbox{\large\sqcup}^{\mathfrak{c}}xp(x) can be shown to be unprovable. However, it becomes provable if the two clusters $\mathfrak{a}$ and $\mathfrak{b}$ are the same. Below is a proof of \mbox{\large\sqcup}^{\mathfrak{a}}xp(x)\vee\mbox{\large\sqcup}^{\mathfrak{a}}xp(x)\rightarrow\mbox{\large\sqcup}^{\mathfrak{c}}xp(x), i.e., of \bigl{(}\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\wedge\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x).

1. $\top$    Axiom

2. $\top\wedge\top$    Pand-identity: 1

3. \bigl{(}\neg p(a)\vee p(a)\bigr{)}\wedge\bigl{(}\neg p(a)\vee p(a)\bigr{)}    Trivialization: 2 (twice)

4. \bigl{(}\neg p(a)\wedge\neg p(a)\bigr{)}\vee p(a)   Pand-distribution: 3

5. \bigl{(}\neg p(a)\wedge\neg p(a)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)    Chexists-choosing: 4

6. \mbox{\large\sqcap}^{\mathfrak{a}}x\Bigl{(}\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)\Bigr{)}    Chall-splitting: 5

7. \mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)    Chall-distribution: 6

8. \Bigl{(}\mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)\Bigr{)}\sqcap^{\mathfrak{b}}\Bigl{(}\mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)\Bigr{)}    Chand-splitting: 7,7

9. \mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\sqcap^{\mathfrak{b}}\mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)   Chand-distribution: 8

10. \mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\neg p(x)\wedge\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\bigr{)}\sqcap^{\mathfrak{b}}\mbox{\large\sqcap}^{\mathfrak{a}}x\bigl{(}\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\wedge\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)    Chall-cleansing: 9 (twice)

11. \bigl{(}\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\wedge\mbox{\large\sqcap}^{\mathfrak{a}}x\neg p(x)\bigr{)}\vee\mbox{\large\sqcup}^{\mathfrak{c}}xp(x)    Challchotomy: 10

5 The preservation lemma

A surface occurrence of a subcirquent or an operator in a given cirquent is an occurrence which is not in the scope of a choice operator (i.e., of $\sqcap^{\mathfrak{c}}$, $\sqcup^{\mathfrak{c}}$, \mbox{\large\sqcap}^{\mathfrak{c}} or \mbox{\large\sqcup}^{\mathfrak{c}} for whatever $\mathfrak{c}$).

Definition 5.1

Given a closed cirquent $C$ and a legal run $\Gamma$, the $\Gamma$-residue of $C$ is the \sqcap,\sqcup,\mbox{\large\sqcap},\mbox{\large\sqcup}-free cirquent obtained from $C$ as a result of repeatedly replacing until no longer possible:

1. every surface occurrence of every $\Gamma$-resolved $\sqcap$-, $\sqcup$-, $\sqcap$- or $\sqcup$-rooted subcirquent by its resolvent;

2. every surface occurrence of every $\Gamma$-unresolved $\sqcap$- or $\sqcap$-rooted subcirquent by $\top$;

3. every surface occurrence of every $\Gamma$-unresolved $\sqcup$- or $\sqcup$-rooted subcirquent by $\bot$.

Lemma 5.2

Consider any closed cirquent $C$, interpretation ∗ and legal run $\Gamma$. Let $R_{C}$ be the $\Gamma$-residue of $C$. Then $\Gamma$ is a won (by the machine) run of $C^{*}$ iff $R_{C}^{*}$ is true.

Proof. Let $C$, ∗, $\Gamma$, $R_{C}$ be as above. We proceed by induction on the complexity of $C$.

If $C$ is a literal, then $R_{C}=C$. Hence, from clause 1 of Definition 3.1 (and the fact that all other clauses of that definition are about non-literal cases), $\Gamma$ is a won run of $C^{*}$ iff $R_{C}^{*}$ is true.

If $C$ is of the form $A\wedge B$, then obviously $R_{C}=R_{A}\wedge R_{B}$, where $R_{A}$ is the residue of $A$ and $R_{B}$ is the residue of $B$. By Definition 3.1, $\Gamma$ is a won run of $(A\wedge B)^{*}$ iff it is a won run of both ${A}^{*}$ and ${B}^{*}$. But, by the induction hypothesis, $\Gamma$ is a won run of both $A^{*}$ and $B^{*}$ iff both $R_{A}^{*}$ and $R_{B}^{*}$ are true. “Both $R_{A}^{*}$ and $R_{B}^{*}$ are true”, in turn, means nothing but that $R_{A}^{*}\wedge R_{B}^{*}$, i.e., $R_{C}^{*}$, is true.

The case of $C$ having the form $A\vee B$ will be handled similarly.

Suppose $C$ is of the form $A\sqcap^{\mathfrak{c}}B$. If $C$ is unresolved, then, by clause 4 of Definition 3.1, $\Gamma$ is a won run of $C^{*}$. But then, as desired, $R_{C}^{*}$ is true because $R_{C}=\top$. Now suppose $C$ is resolved. Without loss of generality we may assume that the resolvent is $A$. Notice that then $R_{C}$ is the residue of not only $C$ but also of $A$. We have: $\Gamma$ is a won run of $C^{*}$ iff (by clause 3 of Definition 3.1) it is a won run of $A^{*}$ iff (by the induction hypothesis) $R_{C}^{*}$ is true, as desired.

The remaining cases of $C$ having the form $A\sqcup^{\mathfrak{c}}B$, \mbox{\large\sqcap}^{\mathfrak{c}}xA(x) or \mbox{\large\sqcup}^{\mathfrak{c}}xA(x) will be handled similarly.   $\Box$

Lemma 5.3

1. Each application of any of the rules of CL17 preserves logical validity in the premises-to-conclusion direction, i.e., if all premises are valid, then so is the conclusion.

2. Each application of any of the rules of CL17 other than (the three versions of) Choosing also preserves logical validity in the conclusion-to-premises direction, i.e., if the conclusion is valid, then so are all premises.

Proof. As in [8], we will implicitly rely on the clean environment assumption, allowing us to rule out the possibility that the environment ever makes any illegal moves. We shall also implicitly rely on the straightforward fact that if, for every interpretation ∗, computability of a cirquent $A$ under ∗ implies computability of a cirquent $B$ under the same ∗, then logical validity of $A$ implies logical validity of $B$.

If $E\leadsto F$ is an application of any of the rules other than Splitting, Chotomy or Choosing, it is not hard to see that, for any interpretation ∗, $E^{*}$ and $F^{*}$ are identical as games. So, a logical solution of $E$ is automatically a logical solution of $F$, and vice versa. Let us just look at Chall-cleansing as an example. Consider an application $E\leadsto F$ of this rule, where E=X\bigl{[}\mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[A(x)]\bigr{]} and F=X\bigl{[}\mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)]\bigr{]}. Fix some arbitrary interpretation for the present context, and let $\Gamma$ be an arbitrary legal run. We want to show that $\Gamma$ is a won run of $E$ iff it is a won run of $F$. If $\mathfrak{c}$ is $\Gamma$-unresolved, then $\Gamma$ is a won run of the \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)] component of the conclusion just as it is a won run of the \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[A(x)] component of the premise. Then, since $E$ and $F$ only differ in that one has \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)] where the other has \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[A(x)], we find that $\Gamma$ is a won run of both games $E,F$ or neither. Now assume $\mathfrak{c}$ is resolved, i.e., $\Gamma$ contains the move $\mathfrak{c}.a$ for some constant $a$. Then $\Gamma$ is a won run of \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)] iff it is a won run of $Y(a)[A(a)]$ iff it is a won run of \mbox{\large\sqcap}^{\mathfrak{c}}xY(x)[A(x)]. This, again, implies that $\Gamma$ is a won run of both games $E,F$ or neither.

Chor-choosing is taken care of in the proof of Lemma 6.1 of [8], which shows that this rule preserves computability under any given interpretation. The same can be said about either direction of Chand-splitting.

Consider an application X[A_{1}(a),\cdots,A_{n}(a)]\leadsto X[\mbox{\large\sqcup}^{\mathfrak{c}}x_{1}A_{1}(x_{1}),\cdots,\mbox{\large\sqcup}^{\mathfrak{c}}x_{n}A_{n}(x_{n})] of Chexists-choosing, and assume $\cal M$ is a logical solution of the premise. Let ${\cal N}$ be an HPM that, at the beginning of the play, makes the move $\mathfrak{c}.a$, after which it plays exactly as $\cal M$ would. Obviously $\cal N$ is a logical solution of the conclusion.

Of the three Chotomy rules, let us just consider Challchotomy, with the remaining two rules being similar. Consider an application

[TABLE]

of Challchotomy. It is not hard to see that, under any interpretation, any won run of the conclusion is also (“even more so”) a won run of the premise, meaning that a solution of the conclusion would automatically also be a solution of the premise. This takes care of the conclusion-to-premise direction. For the premise-to-conclusion direction, fix an arbitrary interpretation and assume that $\cal M$ is a solution of the premise. Let $\cal N$ be an HPM that, until it sees that its environment has resolved either $\mathfrak{a}$ or $\mathfrak{b}$, plays just as $\cal M$ would play in the scenario where $\mathfrak{c}$ is not (yet) resolved but otherwise $\cal M$’s imaginary environment is making the same moves as $\cal N$’s real environment is making. If and when it sees that a move $\mathfrak{a}.i$ (resp. $\mathfrak{b}.i$) has been made by its environment, $\cal N$ imagines that $\cal M$’s environment has correspondingly made not only the same move $\mathfrak{a}.i$ (resp. $\mathfrak{b}.i$) but also $\mathfrak{c}.0$ (resp. $\mathfrak{c}.1$), and continues playing exactly as $\cal M$ would continue playing in that case. With a little thought, $\cal N$ can be seen to be a solution of the conclusion.

Finally, consider an application A(a)\leadsto\mbox{\large\sqcap}^{\mathfrak{c}}xA(x) of Chall-splitting.

For the conclusion-to-premise direction, assume $\cal M$ is a logical solution of \mbox{\large\sqcap}^{\mathfrak{c}}xA(x). Let $\cal N$ be the HPM that plays exactly as $\cal M$ would play in the scenario where, at the very beginning of the play, the environment makes the move $\mathfrak{c}.a$. It is not hard to see that $\cal N$ is a logical solution of $A(a)$.

For the premise-to-conclusion direction, assume $\cal M$ is a logical solution of $A(a)$. Let $\cal N$ be an HPM that plays \mbox{\large\sqcap}^{\mathfrak{c}}xA(x) as follows. While continuously polling its run tape, $\cal N$ maintains a list $L$ of moves, initially empty. This is just to keep track of which moves made by the environment have already been “processed” by $\cal N$. Call the moves that are not in $L$ unprocessed. $\cal N$ further maintains a partial function $f:\mathbb{N}\rightarrow\mathbb{N}$. Call the value of $f(c)$ the image of $c$, and call the constants at which $f$ is not (yet) defined imageless. Initially, the image of each constant occurring in $A(x)$ is that constant itself, and all other constants are imageless.

At the beginning of the play, $\cal N$ waits till the environment makes the move $\mathfrak{c}.b$ for some constant $b$. If and when this happens (and if not, $\cal N$ wins \mbox{\large\sqcap}^{\mathfrak{c}}xA(x) by doing nothing), $\cal N$ adds $\mathfrak{c}.b$ to $L$, declares $b$ to be the image of (the so far imageless) $a$, and starts simulating an imaginary play of $A(a)$ by $\cal M$. In this simulation:

• •

Whenever $\cal N$ sees an unprocessed move $\mathfrak{a}.i$ on its run tape where $\mathfrak{a}$ is a $\sqcap$-cluster, it adds this move to $L$ and appends $\bot\mathfrak{a}.i$ to the content of the imaginary run tape of $\cal M$.

• •

Whenever $\cal N$ sees an unprocessed move $\mathfrak{a}.c$ on its run tape where $\mathfrak{a}$ is a $\sqcap$-cluster, it adds this move to $L$ and appends $\bot\mathfrak{a}.d$ to the content of the imaginary run tape of $\cal M$, where $d$ is an (say, the smallest) imageless constant; after that $\cal M$ declares $c$ to be the image of $d$.

• •

Whenever $\cal N$ sees that the simulated $\cal M$ made a move $\mathfrak{a}.i$ where $\mathfrak{a}$ is a $\sqcup$-cluster, it makes the same move $\mathfrak{a}.i$ in its real play.

• •

Whenever $\cal N$ sees that the simulated $\cal M$ made a move $\mathfrak{a}.c$ where $\mathfrak{a}$ is a $\sqcup$-cluster and $c$ is imageless, $\cal N$ makes the same move $\mathfrak{a}.c$ in its real play, and declares $c$ to be its own image.

• •

Whenever $\cal N$ sees that the simulated $\cal M$ made a move $\mathfrak{a}.c$ where $\mathfrak{a}$ is a $\sqcup$-cluster and $c$ is not imageless, $\cal N$ makes the move $\mathfrak{a}.d$ in its real play, where $d$ is the image of $c$.

We claim that $\cal N$ is a logical solution of \mbox{\large\sqcap}^{\mathfrak{c}}xA(x). To see this, consider an arbitrary interpretation ∗ and an arbitrary “real” play by $\cal N$. Let $\Gamma_{\cal N}$ be the run that has taken place in that play, and $\Gamma_{\cal M}$ be the run that has correspondingly taken place in $\cal M$’s play as imagined by $\cal N$. Our goal is to show that $\Gamma_{\cal N}$ is a won run of \bigl{(}\mbox{\large\sqcap}^{\mathfrak{c}}xA(x)\bigr{)}^{*}. Let $R_{\cal M}$ be the $\Gamma_{\cal M}$-residue of $A(a)$, and let $c_{1},\cdots,c_{n}$ be all constants occurring in $R_{\cal M}$. Notice that each such constant has acquired an image at some time during the work of $\cal N$ (and never lost or changed it afterwards). Let $R_{\cal N}$ be the result of replacing in $R_{\cal M}$ each occurrence of each $c_{i}\in\{c_{1},\cdots,c_{n}\}$ by the image of $c_{i}$. Let ∘ be an interpretation such that, for any atom $X$ of $R_{\cal M}$, $X^{\circ}$ is true iff so is $Y^{*}$, where $Y$ is the result of replacing all constants in $X$ by their images.

An analysis of the work of $\cal N$, details of which are left to the reader, reveals that $R_{\cal N}$ is the $\Gamma_{\cal N}$-residue of \mbox{\large\sqcap}^{\mathfrak{c}}xA(x), and that $R_{\cal N}^{*}$ is true iff so is $R_{\cal M}^{\circ}$. Since $\cal M$ is a logical solution of $A(a)$, $\Gamma_{\cal M}$ is a won run of $A^{\circ}(a)$. By Lemma 5.2, this implies that $R_{\cal M}^{\circ}$ is true. Hence so is $R_{\cal N}^{*}$, which, again by Lemma 5.2, implies that $\Gamma$ is a won run of \bigl{(}\mbox{\large\sqcap}^{\mathfrak{c}}xA(x)\bigr{)}^{*}, as desired.   $\Box$

6 Rank and purification

Our proofs in this section closely follow those given in Section 7 of [8]. As in [8], ${}^{n}a$ means “tower of $a$’s of height $n$” (tetration), defined inductively by ${}^{1}a=a$ and ${}^{n+1}a=a^{(^{n}a)}$.

Definition 6.1

The rank $\mbox{Rank}(C)$ of a cirquent $C$ is the number defined as follows:

1. If $C$ is a literal, then its rank is $1$.

2. If $C$ is $A\sqcup^{\mathfrak{c}}B$ or $A\sqcap^{\mathfrak{c}}B$, then its rank is $\mbox{Rank}(A)+\mbox{Rank}(B)$.

3. If $C$ is \mbox{\large\sqcup}^{\mathfrak{c}}xA or \mbox{\large\sqcap}^{\mathfrak{c}}xA, then its rank is $\mbox{Rank}(A)+1$.

4. If $C$ is $A\wedge B$, then its rank is $5^{k}$, where $k=\mbox{Rank}(A)+\mbox{Rank}(B)$.111In fact, a smaller number can be taken here and below instead of $5$, but why bother.

5. If $C$ is $A\vee B$, then its rank is  ${}^{k}5$, where $k=\mbox{Rank}(A)+\mbox{Rank}(B)$.

Due to due to the monotonicity of the functions $x+y$, $x+1$, $5^{x}$ and ${}^{x}5$, we have:

Lemma 6.2

The rank function is monotone in the following sense. Consider a cirquent $A$ with a subcirquent $B$. Assume $B^{\prime}$ is a cirquent with $\mbox{Rank}(B^{\prime})<\mbox{Rank}(B)$, and $A^{\prime}$ is the result of replacing an occurrence of $B$ by $B^{\prime}$ in $A$. Then $\mbox{Rank}(A^{\prime})<\mbox{Rank}(A)$.

Definition 6.3

We say that a cirquent $E$ is pure iff the following conditions are satisfied:

1. $E$ has no surface occurrence of $\bot$ unless $E$ itself is $\bot$.

2. $E$ has no surface occurrence of $\wedge$ which is in the scope of $\vee$.

3. $E$ has no surface occurrence of $\sqcap^{\mathfrak{c}}$ or \mbox{\large\sqcap}^{\mathfrak{c}} (whatever cluster $\mathfrak{c}$) which is in the scope of $\vee$.

4. $E$ has no surface occurrence of the form $A_{1}\vee\cdots\vee A_{n}$ such that, for some atom $A$, both $A$ and $\neg A$ are among $A_{1},\cdots,A_{n}$.

5. $E$ has no surface occurrences of $\top$ unless $E$ itself is $\top$.

6. If $E$ is of the form $A_{1}\wedge\cdots\wedge A_{n}$ ($n\geq 2$), then at least one $A_{i}$ ($1\leq i\leq n$) is neither $\sqcap$- nor $\sqcap$-rooted.

7. If $E$ is of the form $A\sqcap^{\mathfrak{c}}B$, then neither $A$ nor $B$ contains the cluster $\mathfrak{c}$.

8. If $E$ is of the form \mbox{\large\sqcap}^{\mathfrak{c}}xA, then $A$ does not contain the cluster $\mathfrak{c}$.

Below we describe a procedure which takes a cirquent $E$ and applies to it a series of modifications. Each modification changes the value of $E$ so that the old value of $E$ follows from the new value by one of the rules of CL17 other than Choosing and Splitting. The procedure is divided into eight stages, and the purpose of each stage $i\in\{1,\cdots,8\}$ is to make $E$ satisfy the corresponding condition $\#i$ of Definition 6.3.

Procedure Purification applied to a cirquent $E$: Starting from Stage 1, each of the following eight stages is a loop that should be iterated until it no longer modifies (the current value of) $E$; then the procedure goes to the next stage, unless the current stage was Stage 8, in which case the procedure terminates and returns (the then-current value of) $E$.

Stage 1: If $E$ has a surface occurrence of the form $\bot\vee A$ or $A\vee\bot$, change the latter to $A$ using Por-identity perhaps in combination with Por-commutativity. Next, if $E$ has a surface occurrence of the form $\bot\wedge A$ or $A\wedge\bot$, change it to $\bot$ using Pand-domination perhaps in combination with Pand-commutativity.

Stage 2: If $E$ has a surface occurrence of the form $(A\wedge B)\vee C$ or $C\vee(A\wedge B)$, change it to $(A\vee C)\wedge(B\vee C)$ using Pand-distribution perhaps in combination with Por-commutativity.

Stage 3: (a) If $E$ has a surface occurrence of the form $A\sqcap^{\mathfrak{c}}B\vee C$ or $C\vee A\sqcap^{\mathfrak{c}}B$, change it to $(A\vee C)\sqcap^{\mathfrak{c}}(B\vee C)$ using Chand-distribution perhaps in combination with Por-commutativity. (b) Next, if $E$ has a surface occurrence of the form \mbox{\large\sqcap}^{\mathfrak{c}}xA\vee B or B\vee\mbox{\large\sqcap}^{\mathfrak{c}}xA, change it to \mbox{\large\sqcap}^{\mathfrak{c}}x(A\vee B) using Chall-distribution perhaps in combination with Por-commutativity.

Stage 4: If $E$ has a surface occurrence of the form $A_{1}\vee\cdots\vee A_{n}$ and, for some atom $A$, both $A$ and $\neg A$ are among $A_{1},\cdots,A_{n}$, change $A_{1}\vee\cdots\vee A_{n}$ to $\top$ using Trivialization, perhaps in combination with Por-domination, Por-commutativity and Por-associativity.

Stage 5: If $E$ has a surface occurrence of the form $\top\vee A$ or $A\vee\top$, change it to $\top$ using Por-domination perhaps in combination with Por-commutativity. Next, if $E$ has a surface occurrence of the form $\top\wedge A$ or $A\wedge\top$, change it to $A$ using Pand-identity perhaps in combination with Pand-commutativity.

Stage 6: In all three cases below, $\mathfrak{c}$ is a $\sqcap$-cluster not occurring in $E$. (a) If $E$ has a surface occurrence of the form $A\sqcap^{\mathfrak{a}}B\wedge C\sqcap^{\mathfrak{b}}D$, change it to \bigl{(}(A\wedge C\sqcap^{\mathfrak{b}}D)\sqcap^{\mathfrak{a}}(B\wedge C\sqcap^{\mathfrak{b}}D)\bigr{)}\sqcap^{\mathfrak{c}}\bigl{(}(A\sqcap^{\mathfrak{a}}B\wedge C)\sqcap^{\mathfrak{b}}(A\sqcap^{\mathfrak{a}}B\wedge D)\bigr{)} using Chandchotomy. (b) Next, if $E$ has a surface occurrence of the form \mbox{\large\sqcap}^{\mathfrak{a}}xA\wedge\mbox{\large\sqcap}^{\mathfrak{b}}yB, change it to \mbox{\large\sqcap}^{\mathfrak{a}}x(A\wedge\mbox{\large\sqcap}^{\mathfrak{b}}yB)\sqcap^{\mathfrak{c}}\mbox{\large\sqcap}^{\mathfrak{b}}y(\mbox{\large\sqcap}^{\mathfrak{a}}xA\wedge B) using Challchotomy. (c) Next, if $E$ has a surface occurrence of the form A\sqcap^{\mathfrak{a}}B\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC or \mbox{\large\sqcap}^{\mathfrak{b}}xC\wedge A\sqcap^{\mathfrak{a}}B, change it to \bigl{(}(A\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC)\sqcap^{\mathfrak{a}}(B\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC)\bigr{)}\sqcap^{\mathfrak{c}}\mbox{\large\sqcap}^{\mathfrak{b}}x(A\sqcap^{\mathfrak{a}}B\wedge C) using Chandallchotomy perhaps in combination with Pand-commutativity.

Stage 7: If $E$ is of the form $X[A\sqcap^{\mathfrak{c}}B]\sqcap^{\mathfrak{c}}C$ (resp. $C\sqcap^{\mathfrak{c}}X[A\sqcap^{\mathfrak{c}}B]$), change it to $X[A]\sqcap^{\mathfrak{c}}C$ (resp. $C\sqcap^{\mathfrak{c}}X[B]$) using Left (resp. Right) chand-cleansing.

Stage 8: If $E$ is of the form \mbox{\large\sqcap}^{\mathfrak{c}}xX[\mbox{\large\sqcap}^{\mathfrak{c}}yA(y)], change it to \mbox{\large\sqcap}^{\mathfrak{c}}xX[A(x)] using Chall-cleansing.

Lemma 6.4

Each stage of the Purification procedure strictly reduces the rank of $E$.

Proof. Each stage replaces an occurrence of a subcirquent $A$ of $E$ by some cirquent $B$. In view of Lemma 6.2, in order to show that such a replacement reduces the rank of $E$, it is sufficient to show that $\mbox{Rank}(B)<\mbox{Rank}(A)$. Here we shall only consider Stages 3(b), 6(b,c) and 8, as all other stages or cases are covered in the proof of Lemma 7.4 of [8].

Stage 3(b): With $k$ abbreviating $\mbox{Rank}(A)+\mbox{Rank}(B)$, the rank of \mbox{\large\sqcap}^{\mathfrak{c}}xA\vee B or B\vee\mbox{\large\sqcap}^{\mathfrak{c}}xA is ${}^{k+1}5$, and the rank of \mbox{\large\sqcap}^{\mathfrak{c}}x(A\vee B) is ${}^{k}5+1$. The latter is clearly smaller than the former.

Stage 6(b): With $k$ abbreviating $\mbox{Rank}(A)+\mbox{Rank}(B)$, the rank of \mbox{\large\sqcap}^{\mathfrak{a}}xA\wedge\mbox{\large\sqcap}^{\mathfrak{b}}yB is $5^{k+2}$, and the rank of \mbox{\large\sqcap}^{\mathfrak{a}}x(A\wedge\mbox{\large\sqcap}^{\mathfrak{b}}yB)\sqcap^{\mathfrak{c}}\mbox{\large\sqcap}^{\mathfrak{b}}y(\mbox{\large\sqcap}^{\mathfrak{a}}xA\wedge B) is $5^{k+1}+5^{k+1}$. Of course the latter is smaller than the former.

Stage 6(c): With $a$, $b$ and $c$ standing for the ranks of $A$, $B$ and $C$, respectively, the rank of A\sqcap^{\mathfrak{a}}B\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC or \mbox{\large\sqcap}^{\mathfrak{b}}xC\wedge A\sqcap^{\mathfrak{a}}B is $5^{a+b+c+1}$, and the rank of \bigl{(}(A\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC)\sqcap^{\mathfrak{a}}(B\wedge\mbox{\large\sqcap}^{\mathfrak{b}}xC)\bigr{)}\sqcap^{\mathfrak{c}}\mbox{\large\sqcap}^{\mathfrak{b}}x(A\sqcap^{\mathfrak{a}}B\wedge C) is $5^{a+c+1}+5^{b+c+1}+5^{a+b+c}+1$. Obviously the latter is smaller than the former.

Stage 8: Each iteration of this stage replaces a subcirquent \mbox{\large\sqcap}^{\mathfrak{c}}yA(y) by $A(x)$. Since the rank of $A(x)$ is obviously the same as the rank of $A(y)$, the rank \mbox{Rank}\bigl{(}A(x)\bigr{)}+1 of \mbox{\large\sqcap}^{\mathfrak{c}}xA(x) is greater than the rank \mbox{Rank}\bigl{(}A(y)\bigr{)} of $A(y)$.   $\Box$

Where $A$ is the initial value of $E$ in the Purification procedure and $B$ is its final value (which exists by Lemma 6.4), we call $B$ the purification of $A$.

Lemma 6.5

For any closed cirquent $E$ and its purification $F$, we have:

1. If $F$ is provable in CL17, then so is $E$.

2. $E$ is valid iff so is $F$.

3. $F$ is pure.

4. The rank of $F$ does not exceed the rank of $E$.

Proof. Clause 1: When obtaining $F$ from $E$, each transformation performed during the Purification procedure applies, in the conclusion-to-premise direction, one of the inference rules of CL17. Reversing the order of those transformations, we get a derivation of $E$ from $F$ in CL17. Appending that derivation to a proof of $F$ (if one exists) yields a proof of $E$.

Clause 2: Immediate from the two clauses of Lemma 5.3 and the fact that, when obtaining $F$ from $E$ using the Purification procedure, Choosing is never used.

Clause 3: One by one, Stage 1 eliminates all surface occurrences of $\bot$ in $E$ (unless $E$ itself is $\bot$). So, at the end of the stage, $E$ satisfies condition 1 of Definition 6.3. None of the subsequent steps make $E$ violate that condition, so $F$, too, satisfies that condition. Similarly, a routine examination of the situation reveals that Stage 2 (resp. 3, …, resp. 8) of the Purification procedure makes $E$ satisfy condition 2 (resp. 3, …, resp. 8) of Definition 6.3, and $E$ continues to satisfy that condition throughout the rest of the stages. So, $F$ is pure.

Case 4: Immediate from Lemma 6.4.   $\Box$

7 The soundness and completeness of CL17

Theorem 7.1

A closed cirquent $E$ is valid if (soundness) and only if (completeness) $\mbox{{\bf CL17}}\vdash E$.

Proof. The soundness part is immediate from clause 1 of Lemma 5.3 and the fact that the axiom $\top$ is valid. The rest of this section is devoted to a proof of the completeness part. Pick an arbitrary closed cirquent $E$, and let $F$ be its purification. We proceed by induction on the rank of $E$.

By clauses 3-4 of Lemma 6.5, $F$ is a pure cirquent whose rank does not exceed that of $E$. We shall implicitly rely on this fact below. In view of $F$’s being pure, after some analysis it is clear that one of the following conditions should be satisfied:

Condition 0.

$F$ is either $\bot$ or a nonlogical literal.

Condition 1.

$F$ is $\top$.

Condition 2.

$F$ is of the form $A_{0}\sqcup^{\mathfrak{c}}A_{1}$.

Condition 3.

$F$ is of the form \mbox{\large\sqcup}^{\mathfrak{c}}xA(x).

Condition 4.

$F$ is of the form $A_{0}\sqcap^{\mathfrak{c}}A_{1}$, and neither $A_{0}$ nor $A_{1}$ contains the cluster $\mathfrak{c}$.

Condition 5.

$F$ is of the form \mbox{\large\sqcap}^{\mathfrak{c}}xA(x), and $A(x)$ does not contain the cluster $\mathfrak{c}$.

Condition 6.

$F$ is of the form $A_{1}\vee\cdots\vee A_{n}$ ($n\geq 2$), where each disjunct is either a nonlogical literal, or $\sqcup$-rooted, or $\sqcup$-rooted; besides, for no atom $A$ do we have that both $A$ and $\neg A$ are among $A_{1},\cdots,A_{n}$.

Condition 7.

$F$ is of the form $B_{1}\wedge\cdots\wedge B_{m}$ ($m\geq 2$), where at least one conjunct $B_{e}$ is either (0) a nonlogical literal, or (1) $\sqcup$-rooted, or (2) $\sqcup$-rooted, or (3) satisfies Condition 6 in the role of $F$.

Assume $E$ is valid. We want to show that then $E$ is provable. For this, in view clause 1 of Lemma 6.5, it is sufficient to show that $F$ is provable. Keep in mind that, by clause 2 of Lemma 6.5, $F$ is valid. This immediately rules out Condition 0, because, of course, neither $\bot$ nor nonlogical literals are valid. So, we only need to show that $F$ is provable in each of the following seven cases:

Case 1: $F$ is $\top$ as in Condition 1. Then $F$ is an axiom and hence provable.

Case 2: $F$ is $A_{0}\sqcup^{\mathfrak{c}}A_{1}$ as in Condition 2. Let $\cal M$ be a logical solution of $F$. Consider the work of $\cal M$ in the scenario where the environment does not move until $\cal M$ makes the move $\mathfrak{c}.i$ for one of $i\in\{0,1\}$. Sooner or later $\cal M$ has to make such a move, for otherwise $F$ would be lost due to being $\sqcup^{\mathfrak{c}}$-rooted. Since in the games that we deal with the order of moves is irrelevant, without loss of generality we may assume that the move $\mathfrak{c}.i$ is made by $\cal M$ before any other moves. Let $D$ be the result of replacing in $F$ all subcirquents of the form $X_{0}\sqcup^{\mathfrak{c}}X_{1}$ by $X_{i}$. Observe that, after the move $\mathfrak{c}.i$ is made, in any scenario that may follow, $\cal M$ has to continue and win $D$. This means that $\cal M$ is a logical solution of (not only $F$ but also) $D$. Thus, $D$ is valid. The rank of $D$ is of course smaller than that of $F$. Hence, by the induction hypothesis, $D$ is provable. Then so is $F$ because it follows from $D$ by Chor-choosing.

Case 3: $F$ is \mbox{\large\sqcup}^{\mathfrak{c}}xA(x) as in Condition 3. This case is rather similar to the preceding one. Let $\cal M$ be a logical solution of $F$. Consider the work of $\cal M$ in the scenario where the environment does not move until $\cal M$ makes the move $\mathfrak{c}.a$ for some constant $a$. Sooner or later $\cal M$ has to make such a move, for otherwise $F$ would be lost due to being \mbox{\large\sqcup}^{\mathfrak{c}}-rooted. As in case 2, we may assume that the move $\mathfrak{c}.a$ is made before any other moves. Let $D$ be the result of replacing in $F$ all subcirquents of the form \mbox{\large\sqcup}^{\mathfrak{c}}yX(y) by $X(a)$. After the move $\mathfrak{c}.a$ is made, in any scenario that may follow, $\cal M$ has to continue and win $D$. This means that $\cal M$ is a logical solution of $D$. The rank of $D$ is smaller than that of $F$. Hence, by the induction hypothesis, $D$ is provable. Then so is $F$, as it follows from $D$ by Chexists-choosing.

Case 4: $F=A_{0}\sqcap^{\mathfrak{c}}A_{1}$ is as in Condition 4. By clause 2 of Lemma 5.3, both $A_{0}$ and $A_{1}$ are valid, because $F$ follows from either one by Chand-splitting. Both $\mbox{Rank}(A_{0})$ and $\mbox{Rank}(A_{1})$ are smaller than $\mbox{Rank}(F)$. Hence, by the induction hypothesis, both $A_{0}$ and $A_{1}$ are provable. Therefore, by Chand-splitting, so is $F$.

Case 5: F=\mbox{\large\sqcap}^{\mathfrak{c}}xA(x) is as in condition 5. Let $c$ be a constant not occurring in $F$. By clause 2 of Lemma 5.3, $A(c)$ is valid, because $F$ follows from it by Chall-splitting. The rank of $A(c)$ is smaller than that of $F$. Hence, by the induction hypothesis, $A(c)$ is provable. Therefore, by Chall-splitting, so is $F$.

Case 6: $F=A_{1}\vee\cdots\vee A_{n}$ is as in Condition 6. Not all of the cirquents $A_{1},\ldots,A_{n}$ can be literals, for otherwise $F$ would be automatically lost under an interpretation that makes all those literals false, contrary to our assumption that $F$ is valid. With this observation in mind, without loss of generality, we may assume that, for some $k,m$ with $1\leq k+m\leq n$, the first $k$ cirquents $A_{1},\cdots,A_{k}$ are of the form $B_{0}^{1}\sqcup^{\mathfrak{b}_{1}}B_{1}^{1}$, …, $B_{0}^{k}\sqcup^{\mathfrak{b}_{k}}B_{1}^{k}$, the next $m$ cirquents are of the form \mbox{\large\sqcup}^{\mathfrak{c}_{1}}x_{1}C_{1}(x_{1}),\cdots,\mbox{\large\sqcup}^{\mathfrak{c}_{m}}x_{m}C_{m}(x_{m}), and the remaining $n-k-m$ cirquents are literals. Let $\cal M$ be a logical solution of $F$. Consider the work of $\cal M$ in the scenario where the environment does not move until $\cal M$ makes either (a) the move $\mathfrak{b}_{j}.i$ for some $j\in\{1,\cdots,k\}$ and $i\in\{0,1\}$, or (b) the move $\mathfrak{c}_{j}.a$ for some $j\in\{1,\cdots,m\}$ and $a\in\mathbb{N}$. At some point, $\cal M$ should indeed make such a move, for otherwise $F$ would be lost under an(y) interpretation which makes all of the literal cirquents $A_{k+m+1},\cdots,A_{n}$ false. In case (a), let $D$ be the result of replacing in $F$ every subcirquent of the form $X_{0}\sqcup^{\mathfrak{b}_{j}}X_{1}$ by $X_{i}$; in case (b), let $D$ be the result of replacing in $F$ every subcirquent of the form \mbox{\large\sqcap}^{\mathfrak{c}_{j}}yX(y) by $X(a)$. With some analysis left to the reader, $\cal M$ can be seen to be a logical solution of $D$. Thus, $D$ is valid. The rank of $D$ is smaller than that of $F$ and hence, by the induction hypothesis, $D$ is provable. But then so is $F$, because it follows from $D$ by Choosing.

Case 7: $F=B_{1}\wedge\cdots\wedge B_{m}$ and $B_{e}$ are is as in Condition 7. The validity of $F$, of course, implies that $B_{e}$, as one of its $\wedge$-conjuncts, is also valid. This rules out the possibility that $B_{e}$ is a nonlogical literal, because, as we observed earlier, a nonlogical literal cannot be valid. Therefore we are left with one of the following three possible subcases, corresponding to subconditions (1), (2) and (3) of Condition 7:

Subcase 7.1: $B_{e}$ is of the form $C_{0}\sqcup^{\mathfrak{c}}C_{1}$. The argument given for Subcase 5.1 in the proof of Theorem 7.6 of [8] goes through without any changes.

Subcase 7.2: $B_{e}$ is of the form \mbox{\large\sqcup}^{\mathfrak{c}}xC(x). Let $\cal M$ be a logical solution of $F$. Consider the work of $\cal M$ in the scenario where the environment does not move until $\cal M$ makes the move $\mathfrak{c}.a$ for some constant $a$ (otherwise $F$ would be lost). Let $D$ be the result of replacing in $F$ every subcirquent of the form \mbox{\large\sqcup}^{\mathfrak{c}}yX(y) by $X(a)$. Then, as in Case 3, $\cal M$ can be seen to be a logical solution of $D$, meaning that $D$ is valid. The rank of $D$ is smaller than that of $F$ and hence, by the induction hypothesis, $D$ is provable. But then so is $F$, because it follows from $D$ by Chexists-choosing.

Subcase 7.3: $B_{e}$ satisfies Condition 6 in the role of $F$. This case is very similar to Case 6 and, almost literally repeating our reasoning in the latter, we find that $F$ is provable.   $\Box$

8 The decidability of CL17

Theorem 8.1

CL17* is decidable. Namely, the algorithm DECISION described below accepts a closed cirquent $E$ if $\mbox{{\bf CL17}}\vdash E$ and rejects if $\mbox{{\bf CL17}}\not\vdash E$.*

Proof. Consider an arbitrary closed cirquent $E$. The algorithm DECISION given below is a recursive one. It terminates because every recursive call strictly decreases the rank of the cirquent that is being processed. This is how the algorithm acts on input $E$:

First, using the Purification algorithm, DECISION constructs the purification $F$ of $E$. Note that, in view of Theorem 7.1, “provable” and “valid” can (and will) be used interchangeably; additionally, by clause 2 of Lemma 6.5, so can be “$E$” and “$F$” when we talk about their provability or computability. As pointed out in the proof of Theorem 7.1, $F$ should satisfy one of the eight Conditions listed in that proof.

If $F$ is $\bot$ or a nonlogical literal as in Condition 0, it is invalid, and we let DECISION reject $E$.

If $F$ is $\top$ as in Condition 1, then it is valid, and we let DECISION accept $E$.

Assume $F$ is $A_{0}\sqcup^{\mathfrak{c}}A_{1}$ as in Condition 2. Let $D_{i}$ ($i\in\{0,1\}$) be the result of replacing in $F$ all subcirquents of the form $X_{0}\sqcup^{\mathfrak{c}}X_{1}$ by $X_{i}$. DECISION recursively calls itself on $D_{0}$ and then on $D_{1}$ to figure out whether these cirquents are valid/provable. The ranks of both $D_{0}$ and $D_{1}$ are smaller than the rank of $F$ and hence, in view of clause 4 of Lemma 6.5, smaller than the rank of $E$, as promised in the first paragraph of the present proof. If at least one of $D_{0},D_{1}$ turns out to be provable, we let DECISION accept $E$, because $F$ follows from either cirquent by (one or more applications of) Chor-choosing. Otherwise, if both $D_{0},D_{1}$ turn out to be invalid, we let DECISION reject $E$ because, as (in fact) observed within Case 2 of the proof of Theorem 7.1, if $F$ was valid, then so would be either $D_{0}$ or $D_{1}$.

For the subsequent cases, we merely state how DECISION acts. A verification of the adequacy of the corresponding acceptance/rejection decisions is left to the reader.

Assume $F$ is \mbox{\large\sqcup}^{\mathfrak{c}}xA(x) as in Condition 3. Let $\{a_{1},\ldots,a_{s}\}$ be all constants occurring in $F$, and let $a_{s+1}$ be a constant not occurring in $F$.222In fact, there is no need for considering $a_{s+1}$ unless $s=0$, but let us be generous. The same comment applies to our treatment of the cases of $F$ being as in Condition 6 or Condition 7(2). DECISION runs itself on each of the cirquents $A(a_{1}),\cdots,A(a_{s+1})$. If all of these are rejected, then DECISION rejects $E$, otherwise it accepts $E$.

Assume $F=A_{0}\sqcap^{\mathfrak{c}}A_{1}$ is as in Condition 4. DECISION runs itself on $A_{0}$ and then on $A_{1}$. If both are accepted, DECISION accepts $E$, otherwise it rejects $E$.

Assume F=\mbox{\large\sqcap}^{\mathfrak{c}}xA(x) is as in Condition 5. Let $c$ be a constant not occurring in $F$. DECISION calls itself on $A(c)$ and generates the same acceptance/rejection decision for $E$ as the call does for $A(c)$.

Assume $F=A_{1}\vee\cdots\vee A_{n}$ is as in Condition 6. Let $B_{0}^{1}\sqcup^{\mathfrak{b}_{1}}B_{1}^{1}$, …, $B_{0}^{k}\sqcup^{\mathfrak{b}_{k}}B_{1}^{k}$ and \mbox{\large\sqcup}^{\mathfrak{c}_{1}}x_{1}C_{1}(x_{1}), …, \mbox{\large\sqcup}^{\mathfrak{c}_{m}}x_{m}C_{1}(x_{m}) be as in Case 6 of the proof of Theorem 7.1. Let $a_{1},\ldots,a_{s}$ be all constants occurring in $F$, and let $a_{s+1}$ be a constant not found in $F$. For $i\in\{1,\cdots,k\}$ and $j\in\{0,1\}$, let $D_{i}^{j}$ be the result of replacing in $F$ all subcirquents of the form $X_{0}\sqcup^{\mathfrak{b}_{i}}X_{1}$ by $X_{j}$. Further, for $i\in\{1,\cdots,m\}$ and $j\in\{1,\cdots,s+1\}$, let $G_{i}^{j}$ be the result of replacing in $F$ all subcirquents of the form \mbox{\large\sqcap}^{\mathfrak{c}_{i}}yX(y) by $X(a_{j})$. DECISION calls itself on each of the cirquents $D_{1}^{0},\cdots,D_{k}^{0}$, $D_{1}^{1},\cdots,D_{k}^{1}$,   $G_{1}^{1},\cdots,G_{m}^{1}$,  $\cdots$,  $G_{1}^{s+1},\cdots,G_{m}^{s+1}$. If all calls reject their arguments, then DECISION rejects $E$, otherwise it accepts $E$.

Finally, assume $F=B_{1}\wedge\cdots\wedge B_{m}$ and $B_{e}$ are as in Condition 7.

Assume $A_{e}$ is of the form $C_{0}\sqcup^{\mathfrak{c}}C_{1}$ as in Condition 7(1). For $i\in\{0,1\}$, let $D_{i}$ be the result of replacing in $F$ all subcirquents of the form $X_{0}\sqcup^{\mathfrak{c}}X_{1}$ by $X_{i}$. DECISION runs itself on $D_{0}$ and $D_{1}$. If both cirquents are rejected, then DECISION rejects $E$, otherwise it accepts $E$.

Assume $A_{e}$ is of the form \mbox{\large\sqcup}^{\mathfrak{c}}xC(x) as in Condition 7(2). Let $a_{1},\ldots,a_{s}$ be all constants occurring in $F$, and let $a_{s+1}$ be a constant not found in $F$. For each $j\in\{1,\ldots,s+1\}$, let $D_{j}$ be the result of replacing in $F$ all subcirquents of the form \mbox{\large\sqcup}^{\mathfrak{c}}yX(y) by $X(a_{j})$. DECISION runs itself on each of the arguments $D_{1},\ldots,D_{s+1}$. If all $s+1$ cirquents are rejected, DECISION rejects $E$, otherwise it accepts $E$.

Assume $A_{e}$ is as in Condition 7(3). With $A_{e}$ in the role of $F$, DECISION acts exactly as in the above case of $F$ satisfying Condition 6.   $\Box$