Material dialogues for first-order logic in constructive type theory: extended version

Abstract

Dialogues are turn-taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model-theoretic semantics of first-order logic. Furthermore, we prove that completeness with regard to intuitionistic material dialogues fails in both constructive and classical settings. As an alternative, we propose material dialogues played over Kripke structures. These Kripke material dialogues exhibit constructive completeness when restricting to the negative fragment. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.

1. Introduction

Logical dialogues were introduced by Lorenzen (1960, 1961), a philosopher and constructive mathematician active throughout the latter half of the twentieth century. They are a result of his search for a constructively acceptable account of mathematics, beginning with his work on operative mathematics (Lorenzen 1955). Logical dialogues are turn-taking games which model a debate in which the proponent defends the validity of a formula against the criticisms of an opponent. The games’ moves are modeled after speech acts: asserting formulas and questioning assertions made by the opposing player. In this, they differ from the more wide-spread logical games in the style of Hintikka (1968), in which a formula is reduced to its atoms by both players, the turn order being determined by the syntactical structure of the formula. Although logical dialogues were initially put forward as a semantics for intuitionistic logic, they can also capture classical logic (see e.g. Lorenz 1961).

Any dialogue begins with the proponent asserting a formula to be discussed. The players then take turns, starting with the opponent. The player at turn can choose between two possible moves: Either they can attack an assertion made by the opposing player or they can defend against such an attack, usually by asserting another formula. Some attacks require the attacking player to assert a formula while carrying out the attack, in which case the assertion in question is called an admission. As an example, attacking the asserted formula $\varphi \to \psi$ requires the attacker to admit $\varphi$ while attacking. To defend against the attack on $\varphi \to \psi$ , the attacked player must assert $\psi$ . As in many games, finite plays are won by the player who made the last move. Infinite plays are always won by the opponent. To prevent the opponent from winning by stalling indefinitely, for example through repeated attacks on the proponent’s initial assertion, additional restrictions are imposed on the opponent’s legal moves. The most common such restriction is to only allow the opponent to react to the proponent’s previous move (see Krabbe 2006 for a survey of alternative restrictions).

Meaning of logical connectives in dialogues is captured by attacks and defenses which allow the players to break down assertions into subformulas. However, this approach does not directly extend to atomic formulas. There are two different methods for treating atomic formulas in logical dialogues. Material dialogues, the variant originally proposed by Lorenzen (1960, 1961), permit attacks on atomic formulas. To defend against such an attack, the attacked player is required to demonstrate the validity of the atomic formula. In Lorenzen’s original formulation, this meant deriving a word according to a grammar, a remainder of his operative semantics of mathematics (Lorenzen 1955). Formal dialogues, which were put forward in the dissertation of Lorenzen’s student (Lorenz 1961), treat atomic formulas without appealing to their ‘underlying meaning’, i.e. by purely syntactic means. In this setting, atomic formulas cannot be attacked by either player and an additional restriction is imposed on the proponent: They may only assert those atomic formulas which the opponent has asserted previously. Historically, the study of logical dialogues after Lorenzen’s and Lorenz’ initial work has been focused on formal dialogues due to their greater simplicity (see Krabbe 2006). Sørensen and Urzyczyn (2007) have demonstrated that the winning strategies of formal dialogues for propositional logic are structurally similar to sequent calculus derivations, a result which has been extended to first-order logic in Forster et al. (2020).

If one fixes the ‘demonstration’ of atomic formulas in a material dialogue to be its satisfaction in a previously agreed upon first-order structure, this induces a model-theoretic notion of satisfaction and, by quantifying over all models, validity. In this article, we study the arising semantics of first-order logic in the constructive setting of the calculus of inductive constructions (Coquand and Huet 1986; Paulin-Mohring 1993). This work extends previous investigations into the constructivity of completeness theorems for various semantics of first-order logic, including formal dialogues for intuitionistic first-order logic, in Forster et al. (2020, 2021). The article’s results concerning classical material dialogues (Section 3) have been mechanized using the Coq interactive theorem prover, the mechinzation being located at Kirst (2022b). The results concerning intuitionistic logic in Sections 4 and 5 have so far not been mechanized.

1.1 Outline and contributions

This section summarizes the article’s results. Section 2 covers some basic definitions and results we rely on throughout the article. We close with a brief discussion of various questions arising from this article in Section 6. Note that our use of “soundness” and “completeness” may be somewhat unusual. When speaking of the soundness of a semantics, the intended meaning is the soundness of some suitable deduction system with regard to said semantics (and similarly for “completeness”). While non-standard, this terminology allows us to be more concise about the results derived in this article.

This article is an extended version of the conference article (Wehr and Kirst 2022a ). The present article adds the treatment of Kripke material dialogues (Section 5) and brings the information on constructive reverse mathematics of first-order completeness theorems up-to-date.

Classical material dialogues In Section 3, we define material dialogues for classical first-order logic. We prove their soundness with regard to a cut-free, classical sequent calculus. Notably, classical material dialogues are sound on any first-order structure, whereas classical Tarski semantics require the underlying structure to satisfy all instances of the law of the excluded middle (LEM), a property not necessarily given for all structures in a constructive setting. This means that, informally speaking, the ‘classicality’ of classical material dialogues rests within their rules of engagement, not the underlying first-order structures. We further prove that classical material validity entails exploding classical Tarski validity, a constructively stricter notion than standard classical Tarski validity. We then use the constructive completeness of exploding classical Tarski validity (Veldman 1976) to deduce the same for classical material dialogues. Notably, we obtain completeness for the full syntax of first-order logic fully constructively. The analogous result for Tarski semantics is equivalent to a non-constructive principle called WLEMS in Herbelin and Kirst (2023). The results of Section 3 have been mechanized in Coq, the mechanization being located at Wehr and Kirst (2022b ).

Intuitionistic material dialogues In Section 4, we analyze material dialogues for first-order logic with the usual rules of dialogues of intuitionistic logics. We prove that standard Tarski validity on the fragment $\mathfrak{F}^\texttt{D}$ given below entails intuitionistic material validity.

\begin{align*} a, b : \mathfrak{A} & ::= \bot ~|~ P\,\overline{t} ~|~ a \wedge b ~|~ a \vee b ~|~ \exists x. a \\ \varphi, \psi : \mathfrak{F}^\texttt{D} & ::= a ~|~ \varphi \wedge \psi ~|~ \varphi \vee \psi ~|~ a \to \psi ~|~ \forall x. \varphi ~|~ \exists x. \varphi\end{align*}

This means that proving completeness with regard to intuitionistic material dialogues is tantamount to disproving non-constructive principles on the meta-level. As such principles are consistent with most constructive theories, completeness cannot be established without additional axioms. In fact, intuitionistic and classical material dialogues completely coincide under the full LEM. The natural material rendition of intuitionistic dialogues is thus ill-suited as a semantics of intuitionistic first-order logic. The results of Section 4 have not been mechanized.

Kripke material dialogue In view of the results in Section 4, we propose an alternative dialogical semantics in Section 5. As classical material dialogues could be considered ‘classical dialogues played on the canonical structure for classical semantics’, we consider its natural analogue: intuitionistic dialogues played on Kripke structures, the canonical structure for intuitionistic semantics. We demonstrate their suitability by deriving many of the same results for them as for the classical material dialogues of Section 3. We prove them sound with regard to a cut-free intuitionistic sequent calculus. Furthermore, we show that Kripke material validity entails exploding Kripke validity. We extend the constructive completeness of exploding Kripke models for the $\forall,\to,\bot$ -fragment (Herbelin and Lee 2009) to Kripke material dialogues. The results of Section 5 have not been mechanized.

2. Preliminaries

2.1 The calculus of inductive constructions

The results of this article are all derived within the Calculus of Inductive Constructions CIC, the constructive type theory underlying the interactive theorem prover Coq (Coquand and Huet 1986; Paulin-Mohring 1993). The CIC consists of a predicative hierarchy of type universes $\mathbb{T}_i$ above an impredicative universe $\mathbb{P}$ of propositions. Each type universe contains an empty type, products $A \times B$ , sums $A + B$ , function types $A \to B$ , dependent products $\Pi a : A.B(a),$ and dependent sums $\Sigma a : A. B(a)$ . In $\mathbb{P}$ , we denote them by their respective Curry-Howard correspondents $\bot, \wedge, \vee, \to, \forall,\exists$ . Allowing unrestricted elimination from $\mathbb{P}$ into the $\mathbb{T}_i$ results in an inconsistency. However, this restriction can be lifted for some types in $\mathbb{P}$ , including types of at most one constructor, such as $\bot$ and the equality type $=\, \colon \Pi A. A \to A \to \mathbb{P}$ with a sole constructor of type $\forall (a : A).~a = a$ .

We make use of various inductive types. The natural numbers ( $n : \mathbb{N} ::= 0 ~|~S\,n$ ) are defined in the usual fashion of Peano. Now fix some type A. Option types ( $\mathcal{O}(A) ::= \ulcorner a \urcorner ~|~ \emptyset$ ) are used to model optional parameters of type A in later definitions, i.e. $\emptyset$ denotes the absence of the parameter and $\ulcorner a \urcorner$ denotes the presence of a parameter $a : A$ . Members of list types ( $l : \mathcal{L}(A) ::= []~|~ a :: l$ ) are finite sequences of values of type A, [] denoting the empty list and $a :: l$ denoting a given list $l : \mathcal{L}(A)$ extended by a value $a : A$ . We write $[a_1, ..., a_n]$ for the list $a_1 :: (... :: (a_n :: []))$ , denote list membership by $a \in l$ and take $l {+\hspace{-0.55em}+\,} l'$ to be the list appending operation.

2.2 First-order predicate logic

2.2.1 Syntax with de Bruijn binders

Fix a signature $\Sigma$ of functions symbols f and predicate symbols P, denoting their arities by $|f|$ and $|P|$ , respectively. The associated term and formula languages are defined below. Here, the right columns ascribe types to the variables used in the definitions.

\begin{align*} \mathfrak{T} & ::= n ~|~ f\,\vec{t} & n : \mathbb{N}, f : \Sigma, \vec{t} : \mathfrak{T}^{|f|} \\ \varphi : \mathfrak{F} & ::= \dot{\bot} ~|~ P\,\vec{t} ~|~ \varphi \dot{\,\wedge\,} \psi ~|~ \varphi \dot{\,\vee\,} \psi ~|~ \varphi \dot{\,\to\,} \psi ~|~ \dot{\,\forall\,} \varphi ~|~ \dot{\,\exists\,} \varphi & P : \Sigma, \vec{t} : \mathfrak{T}^{|P|}\end{align*}

To aid in the distinction between meta- and object-level syntax, we write small dots over the connectives of the latter. Negation is defined as $\dot{\neg\,} \varphi := \varphi \dot{\,\to\,} \dot{\bot}$ .

Observe the absence of variables as part of the quantifiers. This is because we employ syntax with de Bruijn binders, a notion developed by de Bruijn as part of the implementation of the AUTOMATH theorem prover (de Bruijn 1972). In a fully formal setting, such as the mechanization accompanying this article (Wehr and Kirst 2022b ), they allow for the treatment of syntax, binders and substitutions with much greater ease than the common named binders approach. Even though definitions using named binders tend to be easier understood, we have decided to follow our mechanization, presenting this article in the de Bruijn-style. Adapting the material to named binders would require drastic changes to most definitions and proof strategies, leaving the article disconnected from the formalization and the assurance of correctness it provides.

In de Bruijn syntax, the variables are represented by natural numbers $n : \mathbb{N}$ , called de Bruijn indices. Such an index indicates its binding quantifier by counting the number of quantifiers between it and said binding quantifier in the syntax tree. For an example consider the formula $\dot{\,\forall\,} x.( P\,x \dot{\,\to\,} \dot{\,\forall\,} z. Q\,x\,z)$ which is represented by $\dot{\,\forall\,} (P\,0\dot{\,\to\,} \dot{\,\forall\,} Q\,1\,0)$ in de Bruijn syntax. Fig. 1 depicts the references described by the indices. Observe that the variable x is represented by different indices depending on its position in the syntax tree.

Figure 1. De Bruijn representation of $\forall x. P\,x \to \forall z. Q\,x\,z$ .

Indexes pointing ‘beyond’ the quantifiers of a formula are taken to be free variables. In $P\,0 \dot{\,\to\,} \dot{\,\forall\,} Q\,1\,2$ , the indexes 0 and 1 refer to the same free variable whereas 2 refers to the ‘next’ free variable. In a formula $\dot{\,\forall\,} \varphi$ , stripping away the quantifier ‘reveals’ a new fresh variable in $\varphi$ , referred to by 0 at the top-level. If this variable is supposed to be fresh, as for example required in the $\dot{\,\forall\,}$ R-rule of a sequent calculus, the indexes of free variables in other formulas must be ‘shifted’ by 1. This shifting operation ${\uparrow \hspace{-0.3em} \varphi}$ plays a key role in the definitions of proof systems and dialogue rules in this article. It is defined in terms of a recursive operation $\text{shift}_n$ on terms and formulas with shorthand ${\uparrow \hspace{-0.3em} \varphi} := \text{shift}_0\,\varphi$ . Below, $\bigcirc \in \{\dot{\,\wedge\,}, \dot{\,\vee\,},\dot{\,\to\,}\}$ and $\Box \in \{\dot{\,\forall\,}, \dot{\,\exists\,}\}$ . Note especially the increase of k in the quantifier case.

\begin{align*} \text{shift}_k\,\dot{\bot} := \dot{\bot}\quad\quad \text{shift}_k\,(P\,\vec{t}) := P\,\overrightarrow{(\text{shift}_k\,t)}\quad\quad \text{shift}_k\,(\varphi \bigcirc \psi) := (\text{shift}_k\,\varphi) \bigcirc (\text{shift}_k\,\psi) \end{align*}

\begin{align*} \text{shift}_k\,(\Box \varphi) := \Box (\text{shift}_{k + 1}\,\varphi)\quad\quad \text{shift}_k\,(f\,\vec{t}) := f\,\overrightarrow{(\text{shift}_k\,t)}\quad\quad \text{shift}_k\,m := \begin{cases} m & m < k \\ m + 1 & \text{otherwise} \end{cases}\end{align*}

We write $\varphi[t]$ to denote the result of substituting a term t for the free variable denoted by 0 at the top-level of $\varphi$ . While the substitution operation behaves as one would expect, it is rather intricate to define, which is why we refer curious readers to, e.g. Abadi et al. (1991).

2.2.2 Model-theoretic semantics

A structure $\textbf{S}$ consists of a type X, a predicate interpretation $P^\textbf{S} : X^{|P|} \to \mathbb{P}$ for each $P : \Sigma$ , a function interpretation $f^\textbf{S} : X^{|f|} \to X$ for each $f : \Sigma$ and an absurdity interpretation $\dot{\bot}^\textbf{S} : \mathbb{P}$ . A model consists of a structure $\textbf{S}$ together with an assignment $\rho : \mathbb{N} \to X$ . The term evaluation function $t^\rho$ in a model $\textbf{S}, \rho$ is defined as $n^\rho := \rho\,n$ and $(f\,\vec{t})^\rho := f^\textbf{S}\,\vec{t}^\rho$ . The Tarski satisfaction relation $\rho \vDash \varphi$ is defined below. We often write $\textbf{S}$ for X, e.g. writing $s : \textbf{S}$ instead of $s : X$ .

\begin{align*} \rho \vDash P\,\vec{t} ~~:\Leftrightarrow ~~ & P^\textbf{S}\,\vec{t}^\rho & \rho \vDash \varphi \dot{\,\to\,} \psi ~~:\Leftrightarrow ~~ & \rho \vDash \varphi \to \rho \vDash \psi \\ \rho \vDash \varphi \dot{\,\wedge\,} \psi ~~:\Leftrightarrow ~~ & \rho \vDash \varphi \wedge \rho \vDash \psi & \rho \vDash \varphi \dot{\,\vee\,} \psi ~~:\Leftrightarrow ~~ & \rho \vDash \varphi \vee \rho \vDash \psi \\ \rho \vDash \dot{\,\forall\,} \varphi ~~:\Leftrightarrow ~~ & \forall s : \textbf{S}.~~ s \cdot \rho \vDash \varphi & \rho \vDash \dot{\,\exists\,} \varphi ~~:\Leftrightarrow ~~ & \exists s : \textbf{S}.~~ s \cdot \rho \vDash \varphi \\ \rho \vDash \dot{\bot} ~~:\Leftrightarrow ~~ & \dot{\bot}^\textbf{S}\end{align*}

Here, we write $s \cdot \rho$ with $s : \textbf{S}$ for the assignment extension operation which is defined as below.

\[ (s \cdot \rho)(0) := s \qquad \qquad (s \cdot \rho)(S\,n) := \rho(n)\]

Note that below the quantifier, the indices of all variables not bound by that quantifier are incremented. This ensures that each variable refers to the correct element in $s \cdot \rho$ in the definition above.

For a finite context $\Gamma,$ we write $\rho \vDash \Gamma$ if $\rho \vDash\varphi$ for all $\varphi \in \Gamma$ . A structure $\textbf{S}$ is classical if for all assignments $\rho$ and formulas $\varphi$ it satisfies the principle of double-negation elimination ( $\rho \vDash \dot{\neg\,} \dot{\neg\,} \varphi \dot{\,\to\,} \varphi$ ). A structure $\textbf{S}$ is exploding if for all assignments $\rho$ and formulas $\varphi$ it satisfies the principle of explosion ( $\rho \vDash\dot{\bot} \dot{\,\to\,} \varphi$ ). A structure $\textbf{S}$ is standard if $\dot{\bot}^\textbf{S}$ is contradictory (i.e. $\neg \dot{\bot}^\textbf{S}$ holds). Observe that all standard structures are exploding. An entailment between a finite context $\Gamma$ and a formula $\varphi$ is valid in classical exploding structures, written $\Gamma \vDash^E \varphi$ , if for all classical, exploding structures $\textbf{S}$ and all assignments $\rho$ it is the case that $\rho \vDash \Gamma$ entails $\rho \vDash \varphi$ . Validity of entailments in classical standard structures, $\Gamma\vDash^S \varphi$ , is defined analogously.

A Kripke frame is a pair $(K, \leq)$ . That is, a type K of worlds and a reachability preorder $\leq : K \to K \to\mathbb{P}$ on that type which is proof irrelevant, i.e. $H = H'$ for any $H, H' : k\leq k'$ . A Kripke structure consists of a Kripke frame $(K,\leq)$ , a family $\textbf{S} : \Pi k : K. \mathbb{S}$ of structures and a family of functions $\iota : \Pi k, k' : K. k \leq k' \to \textbf{S}_k \to \textbf{S}_{k'}$ . Writing $P^k$ as a shorthand for $P^{\textbf{S}_k}$ , we require that $P^k\,\overline{s}$ entails $P^{k'}\,(\iota(k \leq k')(\overline{s}))$ and furthermore $\iota(k' \leq {k}'')(\iota(k \leq k')(s)) = \iota(k \leq k'')(s)$ for all $s : \textbf{S}_k$ . To aid readability, we denote environments by $\rho^k : \mathbb{N} \to \textbf{S}_k$ , the superscript indicating its codomain. For $k : K$ and $s : \textbf{S}_k$ we write $s^{k'}$ for $\iota\,(k \leq k')\,s$ where applicable, extending this to environments via $\rho^{k'} := \iota(k \leq k') \circ \rho^k$ if $\rho^k$ is clear from the context. A Kripke model consists of a Kripke structure, a world k and an environment $\rho^k$ . Given a Kripke model, we define a relation $\rho^k \Vdash\varphi$ , denoting that $\varphi$ is forced at a world k under the k-environment $\rho^k$ as below.

\begin{align*} \rho^k \Vdash P\,\overline{t} ~~:\Leftrightarrow ~~ & P^k\,\overline{t}^\rho & \rho^k \Vdash \varphi \dot{\,\to\,} \psi ~~:\Leftrightarrow ~~ & \forall k \leq k'.~~ \rho^{k'} \Vdash \varphi ~~\to~~ \rho^{k'} \Vdash \psi \\ \rho^k \Vdash \varphi \dot{\,\wedge\,} \psi ~~:\Leftrightarrow ~~ & \rho^k \Vdash \varphi \wedge \rho^k \Vdash \psi & \rho^k \Vdash \varphi \dot{\,\vee\,} \psi ~~:\Leftrightarrow ~~ & \rho^k \Vdash \varphi \vee \rho^k \Vdash \psi \\ \rho^k \Vdash \dot{\,\exists\,} x. \varphi ~~:\Leftrightarrow ~~ & \exists s : \textbf{S}_k.~~ s \cdot \rho^k \Vdash \varphi & \rho^k \Vdash \dot{\,\forall\,} x. \varphi ~~:\Leftrightarrow ~~ & \forall k \leq k', s : \textbf{S}_{k'}.~~ s \cdot \rho^{k'} \Vdash \varphi \\ \rho^k \Vdash \dot{\bot} ~~:\Leftrightarrow ~~ & \dot{\bot}^k\end{align*}

For a finite context $\Gamma,$ we write $\rho^k \Vdash \Gamma$ if $\rho^k \Vdash\varphi$ for all $\varphi \in \Gamma$ . A Kripke structure is exploding or standard if all $\textbf{S}_k$ are such. A formula $\varphi$ is valid in exploding Kripke structures in a context $\Gamma$ , written $\Gamma \vDash_K^{E} \varphi$ , if for all exploding Kripke structures, all worlds $k : K$ and all k-environments $\rho^k$ we have that $\rho^k \Vdash \Gamma$ entails $\rho^k \Vdash \varphi$ . We denote validity in standard models with $\Gamma \vDash_K^{E} \varphi$ . Validity of entailments in standard Kripke structures, $\Gamma\vDash^S_K \varphi$ , is defined analogously.

2.2.3 Proof systems

Denote by $\Gamma \Rightarrow_K \Delta$ the derivability of the sequent $\Gamma\Rightarrow \Delta$ in the sequent calculus for classical first-order logic defined below. The system’s presentation is somewhat non-standard as the principal formulas of derivation rules are not removed from $\Gamma$ and $\Delta$ . This is convenient when proving soundness as it parallels the requirements imposed on the proponent when attacking and defending.

Similarly, denote by $\Gamma \Rightarrow_J \delta$ derivability of $\Gamma \Rightarrow\delta$ in the sequent calculus for intuitionistic first-order logic defined below. The comments regarding treatment of formulas in $\Gamma$ and the quantifier rules above also apply to this system.

The following two results are taken from the literature, relying on ideas from Veldman (1976):

Theorem 1. The following hold in constructive settings when restricting $\Gamma$ and $\varphi$ to the $\dot{\,\forall\,},\dot{\to},\dot{\bot}$ -fragment of, respectively classical and intuitiomstic, first-order logic:

1. (1) Herbelin and Ilik (2016) : $\Gamma \vDash^E \varphi$ entails $\Gamma \Rightarrow_K \varphi$

2. (2) Herbelin and Lee (2009) : $\Gamma \vDash^E_K \varphi$ entails $\Gamma \Rightarrow_J \varphi$

3. Classical Material Dialogues

We begin by defining formally the material dialogues for classical first-order logic. Fix a standard structure $\textbf{S}$ the dialogue will be played over. Material dialogues are a turn-taking game between two players. To win, the proponent must defend the satisfaction of some formula in a model, whereas the opponent must challenge the proponent’s claims in such a way that the proponent cannot respond. The dialogues we consider are so-called E-dialogues which restrict the opponent to only ever react to the proponent’s directly preceding move, whereas the proponent may always respond to any of the opponent’s previous moves. There exists another dialogue variant, which lightens the restriction to the opponent to only being able to react to each proponent attack and admission only once, to prevent ‘stalling’-tactics. The notion of satisfaction induced by both variants is identical (see e.g. Felscher 1985; Forster et al. 2021). We chose to work with E-dialogues because they allow for simpler constructions and arguments. However, all results in this article extend to D-dialogues via the aforementioned equivalence.

We model the dialogue game as a state transition system. A triple $(\rho, A, C): (\mathbb{N} \to \textbf{S}) \times \mathcal{L}(\mathfrak{F}) \times \mathcal{L}(\mathbf{A})$ is called a dialogue state. Together $\textbf{S}, \rho$ form the ambient model. The list A contains all of the opponent’s assertions and C records all attacks that the opponent has leveled against the proponent. Each round begins with the proponent making a move, indicated by a transition $ (\rho, A, C) \leadsto_p (\rho', A', C') ;\, m$ from a dialogue state to a dialogue state and a proponent move $m : \mathbf{M}$ . This is followed by an opponent move, indicated by a transition $(\rho', A', C') ;\, m \leadsto_o (\rho'', A'', C'')$ from a state and proponent move to a further state. We continue by defining the two transition relations $ \leadsto_p $ and $ \leadsto_o $ .

The type $\textbf{D}$ of defenses, defined below, features three different kinds of defenses: $D_A\,\varphi$ denotes the act admitting of the formula $\varphi$ , $D_W\,\varphi\,s$ denotes admitting ‘ $\varphi[s]$ ’ where $s : \textbf{S}$ . Lastly, $D_M\,\varphi$ means claiming to be able to demonstrate that $\varphi$ holds. Note that $D_M\,\varphi$ is only ever instantiated with atomic $\varphi$ .

\[\textbf{D} ::= D_A\,\varphi ~|~ D_W\,\varphi\,s ~|~ D_M\,\varphi \qquad \qquad \varphi : \mathfrak{F}, s : \textbf{S} \]

The type $\mathbf{A}$ contains all attacks. One writes $a \rhd \varphi$ if $a : \mathbf{A}$ is an attack on $\varphi$ . Each $a : \mathbf{A}$ has an associated set $\mathcal{D}_{a}$ of defenses against a. Both $\mathbf{A}$ and the associated $\mathcal{D}_{a}$ are laid out below. The shifting operation ${\uparrow \hspace{-0.3em} \varphi}$ is extended to attacks in a point-wise manner, i.e. ${\uparrow \hspace{-0.3em} (A_L\,\varphi)}= A_L\,{\uparrow \hspace{-0.3em} \varphi}$ , such that ${\uparrow \hspace{-0.3em} a} \rhd {\uparrow \hspace{-0.3em} \varphi}$ whenever $a \rhd \varphi$ .

\begin{align*} A_{\bot} \rhd \dot{\bot} \qquad & \qquad \mathcal{D}_{A_{\bot}} = \{D_M\,\dot{\bot}\} \\ \qquad A_P\,\vec{t} \rhd P\,\vec{t} \qquad & \qquad \mathcal{D}_{A_P\,\vec{t}} = \{D_M\,P\,\vec{t}\} \\ \qquad A_{\to} \,\varphi\,\psi \rhd \varphi \dot{\,\to\,} \psi \qquad & \qquad \mathcal{D}_{A_{\to} \, \varphi \, \psi} = \{D_A\,\psi\} \\ \qquad A_{\vee}\,\varphi\,\psi \rhd \varphi \dot{\,\vee\,} \psi \qquad & \qquad \mathcal{D}_{A_{\vee}\,\varphi\,\psi} = \{D_A\,\varphi, D_A \,\psi\} \\ A_L\,\varphi \rhd \varphi \dot{\,\wedge\,} \psi \qquad & \qquad \mathcal{D}_{A_L\,\varphi} = \{D_A\,\varphi\} \\ A_R\,\psi \rhd \varphi \dot{\,\wedge\,} \psi \qquad & \qquad \mathcal{D}_{A_R\,\psi} = \{D_A\,\psi\} \\ \qquad A_s\,\varphi \rhd \dot{\,\forall\,} \varphi \qquad & \qquad \mathcal{D}_{A_s \,\varphi} = \{D_W\,\varphi\,s\} \\ A_{\exists}\,\varphi \rhd \dot{\,\exists\,} \varphi \qquad & \qquad \mathcal{D}_{A_{\exists}\,\varphi} = \{ D_W\,\varphi\,s ~|~ s : \textbf{S} \} \end{align*}

Some attacks force the attacker to admit a formula. This is formalized by a function $\mathsf{adm}\, : \mathbf{A} \to \mathcal{O}(\mathfrak{F})$ where $\mathsf{adm}\,a =\ulcorner \varphi \urcorner$ means that $\varphi$ must be admitted when attacking with a and $\mathsf{adm}\,a = \emptyset$ means no admission need be made. The admission obligations are $\mathsf{adm}\,(A_\to\,\varphi\,\psi) = \ulcorner \varphi \urcorner$ and $\mathsf{adm}\,a = \emptyset$ for all other attacks $a : \mathbf{A}$ .

Each round begins by the proponent making a move $m : \mathbf{M}$ , as detailed below: Either challenging one of the opponent’s assertions $(P\hspace{-0.22em}A\,a)$ or defending against a challenge previously issued by the opponent, either by asserting a formula $(P\hspace{-0.14em}D\,\varphi)$ or by demonstrating that an atomic formula holds in the ambient model $(P\hspace{-0.14em}M\,\varphi)$ . The function $\mathsf{move} : \textbf{D} \to \mathbf{M}$ maps defenses to the proponent move that needs to be made to carry out said defense.

\[ m : \mathbf{M} := P\hspace{-0.22em}A\,a ~|~ P\hspace{-0.14em}D\,\varphi ~|~ P\hspace{-0.14em}M\,\varphi\]

\begin{align*} \mathsf{move}\,(D_A\,\varphi) = P\hspace{-0.14em}D\,\varphi\quad\quad \mathsf{move}\,(D_W\,\varphi\,s) = P\hspace{-0.14em}D\,\varphi\quad\quad \mathsf{move}\,(D_M\,\varphi) = P\hspace{-0.14em}M\,\varphi\end{align*}

The effect of a proponent’s defense d on the game state is defined via a function $d^P$ as below. Crucially, the shifting of admissions in A and attacks in C ensures that references to free variables are not ‘disturbed’ by the update of $\rho$ .

\[ d^P\,(\rho, A, C) = \begin{cases} (s \cdot \rho, {\uparrow \hspace{-0.3em} A}, {\uparrow \hspace{-0.3em} C}) & \text{ if } d = D_W\,\varphi\,s \\ (\rho, A, C) & \text{otherwise} \end{cases}\]

Defenses need to be justified by the ambient model. While $D_A\,\varphi$ and $D_W\,\varphi\,s$ are always justified, $D_M\,\varphi$ requires $\rho \vDash \varphi$ to hold. All of the previous notations enable a compact definition of the state transitions the proponent may induce by making a move.

The opponent must react to the proponent’s previous move. If the proponent defended by asserting a formula, they must issue a new challenge by attacking said assertion (OA). If the proponent attacked one of their assertions, they can either defend against said attack (OD) or counter the attack, attacking the admission made by the proponent while attacking (OC). If the proponent demonstrated the validity of an atomic formula in the ambient model, the opponent cannot respond at all. The operation $d^O$ is defined analogously to $d^P$ and is used to define the transition steps the opponent can induce by making a move. In a slight abuse of notation, we write $c :: A$ , where c is an attack, for $\psi :: A$ if $\mathsf{adm}\,c = \ulcorner \psi \urcorner$ and A if $\mathsf{adm}\,c = \emptyset$ .

A state can be won if the proponent can ensure the play always eventually ends. This is defined as an inductive predicate which is very similar to the inductive well-foundedness predicate used in type theory. A derivation of $\text{Win}\,s$ can be viewed as a winning strategy for the proponent starting from the state s: The first premise prescribes a move $s \leadsto_p s'\,;\,m$ which the proponent should play and the second premise provides the proponent with winning strategies continuing after any possible opponent reaction to the prescribed proponent move. As $\text{Win}\,s$ is an inductive predicate, its derivations must be well-founded and thus cannot have any infinite branches, meaning a proponent “following” a winning strategy $\text{Win}\,s$ must eventually be prescribed a move $s \leadsto_p s'\,;\,m$ whose resulting state s’ does not allow for opponent reactions, making the second premise vacuously true and the state s’ trivially winning for the proponent.

\begin{align*} \frac{s \leadsto_p s'\,;\,m \qquad \quad \forall s''.~s'\,;m \leadsto_o s'' \to \text{Win}\,s''}{\text{Win}\,s}\end{align*}

This notion of winnability extends to formulas $\varphi$ , denoted $\text{Win}\,(\rho, A, C,\varphi)$ , which holds if for all attacks $c \rhd \varphi$ it is the case that $\text{Win}\,\,(\rho, c :: A, c :: C)$ . A formula $\varphi$ is dialogically entailed in a context $\Gamma$ , written $\Gamma \vDash^D\varphi$ , if for all standard structures $\textbf{S}$ and assignments $\rho : \textbf{V} \to\textbf{S}$ it is the case that $\text{Win}\,(\rho, \Gamma, [], \varphi)$ .

Example 1. Sketched below is a strategy establishing $\text{Win}\,(\rho, [P \dot{\,\to\,} Q, P], [A_Q])$ and thus $\text{Win}\,(\rho, [P \dot{\,\to\,} Q, P], [], Q)$ . The proponent first attacks $P \dot{\,\to\,} Q$ . In both branches, the opponent can only continue if an atomic formula is satisfied by the ambient model. The proponent can thus carry out a ‘demonstration’ ( $P\hspace{-0.14em}M$ ) of said atomic formula, winning the play. This strategy can be played on any model $\textbf{S}, \rho$ , meaning it suffices to establish $P \dot{\,\to\,} Q, P \vDash^D Q$ .

We continue by proving the classical material dialogues sound with regard to the cut-free classical sequent calculus from Section 2.2. This is the easiest soundness result to obtain because of the structural similarity between winning strategies for dialogues and cut-free sequent calculus derivations demonstrated in Sørensen and Urzyczyn (2007). Recall also that the proofs in this article work with the de Bruijn syntax. The results in this section were mechanized in Coq (Wehr and Kirst 2022b ).

The majority of the soundness proof is straightforward. A slight difficulty arises from the differing treatment of quantifiers by material dialogues and sequent calculi. Compare a typical L $\forall$ -rule with the state transition caused by the proponent attacking the admission $\dot{\,\forall\,} \varphi$ with $A_{t^\rho}\,\varphi$ and the opponent responding defending, both given below. While the sequent calculus simply instantiates the formula via a substitution $\varphi[t]$ , material dialogues carry out the instantiation via the assignment, requiring shifting of the admissions and challenges.

\[ [L\forall]\frac{\dot{\,\forall\,} \varphi \in \Gamma \quad \Gamma, \varphi[t] \Rightarrow_K \Delta}{\Gamma \Rightarrow_K \Delta} \quad \quad (\rho, \Gamma, C) \leadsto_{po}(t^\rho \cdot \rho, \varphi :: {\uparrow \hspace{-0.3em} \Gamma}, {\uparrow \hspace{-0.3em} C})\]

To prove soundness, one needs to show that these two methods of instantiation are ‘essentially the same’. For this, we introduce congruence relations on different aspects of dialogues: Given assignments $\rho, \rho'$ and formulas $\varphi, \varphi'$ , we define an equivalence relation $\rho, \varphi \equiv \rho', \varphi'$ which holds if $\varphi$ and $\varphi'$ are equal up to term evaluations in the respective assignments. The definition is given below, in which $\varphi \Box \psi$ is a place-holder for all binary connectives and $\Box\varphi$ for both quantifiers.

\begin{align*} \frac{}{\rho, \dot{\bot} \equiv \rho', \dot{\bot}}\quad \quad \frac{t_i^\rho = t_i'^{\rho'} \text{ for all } i}{\rho, P\,\vec{t} \equiv \rho', P\,\vec{t'}}\quad \quad \frac{\rho, \varphi \equiv \rho', \varphi' \quad \rho, \psi \equiv \rho', \psi'}{\rho, \varphi \Box \psi \equiv \rho', \varphi' \Box \psi'}\end{align*}

\begin{align*} \frac{\forall d.~d \cdot \rho, \varphi \equiv d \cdot \rho', \varphi'}{\rho, \Box \varphi \equiv \rho', \Box \varphi'}\end{align*}

This congruence can be extended to attacks and defenses and it can be shown that these relations do indeed ‘act as congruences’ (see the mechanization for details). The following lemma is crucial to the proof of soundness.

Lemma 1. Let $(\rho, A, C)$ and $(\rho', A', C')$ be dialogue states such that $\rho, A \equiv \rho', A'$ and $\rho, C \equiv \rho', C'$ . If $\text{Win}\,(\rho, A, C)$ then $\text{Win}\,(\rho', A', C')$ .

In the following, and many other proofs in this article, we describe the construction of $\text{Win}\,s$ by describing a winning strategy for the proponent. As noted above, this naturally corresponds to a unique $\text{Win}\,s$ derivation.

Theorem 2 (Soundness). Let $\Gamma$ , $\varphi$ be such that $\Gamma \Rightarrow_K \varphi$ . Then $\Gamma \vDash^D \varphi$ .

Proof. For this, it suffices to show that for any standard structure $\textbf{S}$

\begin{align*} \Gamma \Rightarrow_K \Delta \to \forall \rho, A, C.&~(\forall \delta \in \Delta.\exists c \in C.~c \rhd \delta \wedge (\forall \psi.~ \mathsf{adm}\,c = \ulcorner \psi \urcorner \to \psi \in A)) \\ & \to \Gamma \subseteq A \to \text{Win}\,(\rho, A, C) \end{align*}

because it allows one to conclude $\text{Win}\,(\rho, c :: \Gamma, [c])$ for any $c \rhd \varphi$ , and thus $\text{Win}\,(\rho, \Gamma, [], \varphi)$ , from $\Gamma \Rightarrow_K \varphi$ . We prove the claim per induction on $\Gamma \Rightarrow_K \Delta$ and only spell out an exemplary subset of the cases. For a full proof, the reader may consult the accompanying mechanization (Wehr and Kirst 2022b ).

• Ax: Then, $P\,\overline{t} \in \Gamma$ and $P\,\overline{t} \in \Delta$ . The proponent thus first attacks the admission $P\,\overline{t}$ , forcing the opponent to demonstrate $P^\textbf{S}\,\overline{t}^\rho$ . With this, the proponent can now justify the defense against the challenge against $P\,\overline{t} \in \Delta$ , leaving the opponent without any way of responding and thus winning the dialogue.

• L $\bot$ : Then, $\dot{\bot} \in \Gamma$ . Then, the proponent can attack $\bot$ , forcing the opponent to demonstrate $\bot$ . Then, a winning strategy exist by the principle of explosion.

• L $\to$ : Then, $\varphi \dot{\,\to\,} \psi \in \Gamma,$ and we obtain inductive hypotheses for $\Gamma \Rightarrow_K \varphi, \Delta$ and $\Gamma, \psi \Rightarrow_K \Delta$ . The proponent thus attacks the admission $\varphi \dot{\,\to\,} \psi$ . The opponent has two ways of responding to this attack:

  • - If the opponent defends against the attack by admitting $\psi,$ then the proponent can win by playing the strategy obtained from the inductive hypothesis on $\Gamma, \psi \Rightarrow_K \Delta$ .

  • - If the opponent counters, attacking the admission $\varphi$ with some challenge $c \rhd \varphi$ then the proponent can win by playing the strategy obtained from the inductive hypothesis on $\Gamma \Rightarrow_K \varphi, \Delta$ .

• R $\to$ : Then, $\varphi \dot{\,\to\,} \psi \in \Delta,$ and we have an IH for $\Gamma, \varphi \Rightarrow_K \psi, \Delta$ . The proponent thus defends against the challenge on $\varphi \dot{\,\to\,} \psi$ to which the opponent must respond with a challenge $c \rhd \psi$ . The proponent can thus win by playing according to the IH as $\varphi$ has already been admitted per our assumption.

• L $\forall$ : Then, $\dot{\,\forall\,} \varphi \in \Gamma,$ and we have an IH for $\Gamma, \varphi[t] \Rightarrow_K \Delta$ for some term t. The proponent thus attacks $\forall \varphi$ with $A_{t^\rho}\,\varphi$ against which the opponent must defend with $D_W\,\varphi\,t^\rho$ . The state resulting from this is $(t^\rho \cdot \rho, \varphi :: {\uparrow \hspace{-0.3em} A}, {\uparrow \hspace{-0.3em} C})$ . However, the IH only yields a winning strategy for the state $(\rho, \varphi[t] :: A, C)$ . We can now apply Lemma 1 as $t^\rho \cdot \rho, \varphi :: {\uparrow \hspace{-0.3em} A} \equiv \rho, \varphi[t] :: A$ and $t^\rho \cdot \rho, {\uparrow \hspace{-0.3em} C} \equiv \rho, C$ to transform the winning strategy provided by the IH into the desired form.

• R $\forall$ : Then, $\dot{\,\forall\,} \varphi \in \Delta,$ and we have an IH for ${\uparrow \hspace{-0.3em} \Gamma} \Rightarrow_K \varphi, {\uparrow \hspace{-0.3em} \Delta}$ . The proponent thus defends with $D_W\,\varphi\,s$ for some $s : \textbf{S}$ and the opponent responds with some challenge $c \rhd \varphi$ . This results in the state $(s \cdot \rho, c :: {\uparrow \hspace{-0.3em} A}, c :: {\uparrow \hspace{-0.3em} C})$ for which the IH directly provides a winning strategy.

We continue by proving completeness. We first prove that material validity entails validity on all classical, exploding models. This is extended to traditional completeness in Theorem 4 by use of completeness for classical exploding models on the $\forall,\to,\bot$ -fragment (Theorem 1) and a negative translation.

Lemma 2. For any $\Gamma$ and $\varphi$ , $\Gamma \vDash^D \varphi$ entails $\Gamma \vDash^E \varphi$ .

Proof. Fix a classical, exploding structure $\textbf{S}$ . We extend Tarski satisfaction to defenses via

\[ \rho \vDash D_A\,\varphi :\Leftrightarrow \rho \vDash \varphi ~~\text{ and }~~ \rho \vDash D_W\,\varphi\,s :\Leftrightarrow s \cdot \rho \vDash \varphi ~~\text{ and }~~ \rho \vDash D_M\,\varphi :\Leftrightarrow \rho \vDash \varphi. \]

Furthermore, we define an auxiliary predicate $\Gamma \vDash_\rho \bigvee \mathcal{D}$ on contexts $\Gamma$ , assignments $\rho$ and sets of defenses $\mathcal{D}$ . $\Gamma \vDash_\rho \bigvee \mathcal{D}$ is the “Tarski-correspondent” of a winning strategy, as captured by (1) below. Intuitively states that under the assignment $\rho$ , $\Gamma$ entails the disjunction of all semantic interpretations of $\mathcal{D}$ . Two technical deviations from this intuition are required to carry out the proof: First, to connect $\Gamma \vDash_\rho \bigvee \mathcal{D}$ to the notion of formula satisfaction $\rho \vDash \alpha$ , the statement is relativized to formula consequences $\alpha$ of $\bigvee \mathcal{D}$ . Second, to account for the context extensions induced by $D_W\,\varphi\,s$ , the notion is generalized to all finite extensions $\vec{s} \cdot \rho$ of $\rho$ .

\[\Gamma \vDash_\rho \bigvee \mathcal{D} ~:\Leftrightarrow~ \rho \vDash \Gamma \to \forall \vec{s} : \textbf{S}, \alpha.~ (\forall d \in \mathcal{D}.~ \rho \vDash d \to (\vec{s} \cdot \rho) \vDash \alpha) \to (\vec{s} \cdot \rho) \vDash \alpha\]

The proof relies on the two intermediate results below, whose proofs are rather routine. We refer the curious reader to the mechanization (Wehr and Kirst 2022b ) or to Section 5 in which very similar results are proven for Kripke material dialogues. (1) is proven by induction on the $\text{Win}\,$ -predicate and (2) is proven per case distinction on $\varphi$ . Here, $\hat{\textbf{S}}$ denotes the standard structure with $\dot{\bot}^{\hat{\textbf{S}}} = \bot$ which is otherwise exactly the same as $\textbf{S}$ .

1. (1) $\text{Win}\,(\rho, \Gamma, C)$ in $\hat{\textbf{S}}$ entails $\Gamma \vDash_\rho \bigvee (\bigcup_{c \in C}\mathcal{D}_{c})$ in $\textbf{S}$

2. (2) If $(c :: \Gamma) \vDash_\rho \bigvee (\mathcal{D}_{c} \cup \mathcal{D})$ for all $c \rhd \varphi$ then $\Gamma \vDash_\rho \bigvee (\{D_A\,\varphi\} \cup \mathcal{D})$ in $\textbf{S}$

Now assume $\Gamma \vDash^D \varphi$ and a classical, exploding $\textbf{S}, \rho$ with $\rho \vDash \Gamma$ . Per assumption $\text{Win}\,(\rho, \Gamma, [], \varphi)$ in $\hat{\textbf{S}}$ meaning $(c :: \Gamma) \vDash_\rho \bigvee \mathcal{D}_{c}$ in $\textbf{S}$ for all $c \rhd \varphi$ by (1) and thus $\Gamma \vDash_\rho \bigvee \{D_A \varphi\}$ by (2). By picking $\varphi$ as $\alpha,$ we then obtain $\rho \vDash \varphi$ in $\textbf{S}$ as desired.

Recall that the constructive completeness result for exploding Tarski structures in Herbelin and Ilik (2016), recalled in Theorem 1, is restricted to the $\dot{\,\forall\,}, \dot{\to}, \dot{\bot}$ -fragment of first-order logic. To conclude completeness for material dialogues on the full syntax of first-order logic, we thus employ a negative translation which is given below:

\begin{align*} \bot^M := \bot\quad\quad (P\,\vec{s})^M := P\,\vec{s}\quad\quad (\varphi \wedge \psi)^M := \neg (\varphi^M \to \neg \psi^M)\quad\quad (\varphi \vee \psi)^M := \neg \varphi^M \to \psi^M \end{align*}

\begin{align*} (\forall \varphi)^M := \forall \varphi^M\quad\quad (\exists \varphi)^M := \neg (\forall \neg \varphi^M)\quad\quad (\varphi \to \psi)^M := \varphi^M \to \psi^M\end{align*}

Furthermore, a dialogical analogue of cut-admissibility is required to derive completeness on the full syntax. A formula $\varphi$ can be cut if for any $\textbf{S}, \rho, \Gamma, \Gamma', C$ with $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \varphi :: \Gamma', C)$ and $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C, \varphi)$ we also have that $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C)$ . The proofs below rely on the congruence principles Lemma 1. As we believe that spelling out all applications of the principle obscures the simple ideas behind the proof, we opt to leave applications of Lemma 1 implicit where possible. Readers interested in the proofs in full detail may take a look at the Coq mechanization (Wehr and Kirst 2022b ).

The proofs of Lemma 3 and Theorem 3 in the following, as well as proofs in later sections of this article, proceed per induction on strategies, i.e. derivations of the Win-predicate. In the CIC, every inductively defined type admits an induction principle derived from the clauses of the inductive definition. We shall give a presentation of the induction principle corresponding to the Win-predicate. Fix a predicate $P : (\textbf{V} \to \textbf{S}) \times\mathcal{L}(\mathfrak{F}) \times \mathcal{L}(\mathbf{A}) \to \mathbb{P}$ , i.e. a function mapping states to propositions. The induction principle is as follows:

\[ (\forall s.~s \leadsto_p s'\,;\,m \to (\forall s''.~s'\,;\,m \leadsto_o s'' \to \text{Win}\,s'' \wedge P\,s'') \to P\,s) \to \forall s.~\text{Win}\,s \to P\,s\]

That is, if for every state s and proponent move $s \leadsto_p s'\,;\,m$ such that after any opponent reaction $s'\,;\,m \leadsto_o s''$ there exists a winning strategy $\text{Win}\,s''$ and $P\,s''$ is already known to holds, it can be proven that $P\,s$ holds, then $P\,s$ holds for every winnable state. As an example, the proof of Lemma 3 is carried out as an induction using the following predicate.

\begin{align*} P(\rho, \Gamma, C^*) :\Leftrightarrow &~ \forall C, c, C', n.~C^* = C {+\hspace{-0.55em}+\,} c :: C' \to c \rhd \uparrow^n\varphi \to \\ &~ (\forall d \in \mathcal{D}_{c}.~\rho \text{ justifies } d \to \text{Win}\,(d^O(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C'))) \to \\ &~ \text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')\end{align*}

Lemma 3. Let $\varphi$ be such that all formulas of smaller complexity can be cut. Fix $c \rhd \varphi$ such that $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} c :: C')$ and for all $d \in \mathcal{D}_{c}$ justified under $\rho$ we have $\text{Win}\,(d^O(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C'))$ . Then, $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')$ .

Proof. Intuitively, the proponent of $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')$ mimics the proponent of $\text{Win}\,(\rho, \gamma, C {+\hspace{-0.55em}+\,} c :: C')$ until the latter defends against c. In the critical cases $D_A$ and $D_W$ , the admitted formula must be of lower complexity than $\varphi$ , for which a winning strategy may be obtained by the assumed lower cut-elimination result.

Formally, we prove a slight generalization of the claim: Instead of just $c \rhd \varphi$ , we consider any n and $c \rhd (\uparrow^n\varphi)$ such that $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} c :: C')$ and for all $d \in \mathcal{D}_{c}$ justified under $\rho$ we have $\text{Win}\,(d^O(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C'))$ . The second subcase of the PA-case below illustrates why this generalization is necessary. We then proceed per induction on $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} c :: C')$ and begin by performing a case distinction on the proponent’s move in $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} c :: C')$ .

PA: The proponent uses $a \rhd \psi$ on $\psi \in \Gamma$ . Then, the proponent of $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')$ copies that move. There are two possible opponent responses.

• - In the case of $\mathsf{adm}\,a = \ulcorner \theta \urcorner$ , the opponent may counter with some $c' \rhd \theta$ . Then, the proponent copies the strategy obtained from the inductive hypothesis upon the same counter.

• - The opponent may defend with some $d \in \mathcal{D}_{a}$ . Then, the proponent copies the strategy obtained for the inductive hypothesis upon the same defense.

This case only becomes involved if the defense is some $D_W\,\psi\,s$ , meaning the resulting state becomes $(s \cdot \rho, \psi :: {\uparrow \hspace{-0.3em} \Gamma}, {\uparrow \hspace{-0.3em} C} {+\hspace{-0.55em}+\,} {\uparrow \hspace{-0.3em} C'})$ . To obtain a suitable winning strategy from the inductive hypothesis $P(s \cdot \rho, \psi :: {\uparrow \hspace{-0.3em} \Gamma}, {\uparrow \hspace{-0.3em} C} {+\hspace{-0.55em}+\,} {\uparrow \hspace{-0.3em} C'})$ as defined above, C and C’ must be instantiated with ${\uparrow \hspace{-0.3em} C}$ and ${\uparrow \hspace{-0.3em} C'}$ , respectively. Then, the parameters c and n must be instantiated with ${\uparrow \hspace{-0.3em} c}$ and $n + 1$ for the premise on the second line of $P(s \cdot \rho, \psi :: {\uparrow \hspace{-0.3em} \Gamma}, {\uparrow \hspace{-0.3em} C} {+\hspace{-0.55em}+\,} {\uparrow \hspace{-0.3em} C'})$ to be provable. Once these instantiations have been made, the argument proceeds smoothly. However, it is crucial that $c \rhd \varphi$ is generalized to $c \rhd \uparrow^n\varphi$ . Other cases of this proof and Theorem 3 require similar shifts from $c \rhd \uparrow^n \varphi$ to ${\uparrow \hspace{-0.3em} c} \rhd \uparrow{n + 1} \varphi$ when $D_W$ -instances are encountered but we shall elide these to ease readability. The full details can be found in the mechanization (Wehr and Kirst 2022b ).

PD: Then there is a $c' \in C {+\hspace{-0.55em}+\,} c :: C'$ and the proponent defends with some $d \in \mathcal{D}_{c}$ . There are two cases to distinguish:

• $c' \in C {+\hspace{-0.55em}+\,} C':$ Then, the proponent of $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')$ copies the defense. If d is not $D_M\,\varphi$ for some $\varphi$ , then the opponent attacks the formula $\psi$ admitted by d with some $a \rhd \psi$ . The proponent then plays according to the strategy obtained from the inductive hypothesis upon $a \rhd \psi$ .

• $c' = c:$ Per assumption we have $\text{Win}\,(d^O\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C'))$ . Then, we perform a case distinction on the form of d.

• $d = D_M\,\varphi:$ Then, $\text{Win}\,(d^O(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')) = \text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C'),$ and we are done.

• $d = D_A\,\psi:$ The assumption thus is $\text{Win}\,(\rho, \psi :: \Gamma, C {+\hspace{-0.55em}+\,} C')$ . From the inductive hypothesis, we obtain $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C', \psi)$ . As $D_A\,\psi \in \mathcal{D}_{c}$ and $c \rhd (\uparrow^n\varphi)$ we know that $\psi$ is of lower complexity than $\varphi$ , meaning it can be cut and we thus obtain $\text{Win}\,(\rho, \Gamma, C {+\hspace{-0.55em}+\,} C')$ .

• $d = D_W\,\psi\,s:$ This case is analogous to that for $d = D_A\,\psi$ with a few more applications of Lemma 1.

Theorem 3 (Cut-admissibility). All formulas can be cut.

Proof. The proof proceeds per induction on formula complexity. Thus, pick a $\varphi$ such that all formulas of lower complexity can be cut. We show that for all n,

\[\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \uparrow^n \varphi :: \Gamma', C) \to \text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C, \uparrow^n \varphi) \to \text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C) \]

per induction on $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \uparrow^n \varphi :: \Gamma', C)$ which subsumes the fact that $\varphi$ can be cut. We perform a case distinction on the proponent move.

• $P\hspace{-0.22em}A\,a$ Then, the proponent attacks some $\psi \in \Gamma {+\hspace{-0.55em}+\,} \uparrow^n\varphi :: \Gamma'$ with $a \rhd \psi$ . We distinguish two cases.

• $\psi \in \Gamma {+\hspace{-0.55em}+\,} \Gamma':$ Then, the proponent of $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C)$ copies that attack and proceeds per inductive hypothesis.

• $\psi = \uparrow^n \varphi:$ Then, $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C, \uparrow^n\varphi)$ yields $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', a :: C)$ and the inductive hypothesis means that for all $d \in \mathcal{D}_{a}$ we have that $\text{Win}\,(d^O\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C))$ . We may thus apply Lemma 3 to deduce $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C)$ .

• $P\hspace{-0.14em}D\,\psi:$ Then, there is some $c \in C$ and some $d \in \mathcal{D}_{c}$ which the proponent may perform.The proponent of $\text{Win}\,(\rho, \Gamma {+\hspace{-0.55em}+\,} \Gamma', C)$ thus copies that defense and proceeds per inductive hypothesis.

Combining Theorem 3 with the negative translation above yields completeness on the full syntax of first-order logic.

Theorem 4 Completeness. For any $\Gamma$ and $\varphi$ , $\Gamma \vDash^D \varphi$ entails $\Gamma \Rightarrow_K \varphi$ .

Proof. First of all, $\Gamma \vDash^D \varphi$ entails $\Gamma^M \vDash^D \varphi^M$ . This follows from the provability of $\varphi \,\dot{\leftrightarrow}\, \varphi^M$ , soundness (Theorem 2), and cut-admissibility for material dialogues (Theorem 3). We can now apply Lemma 2 to obtain $\Gamma^M \vDash^E \varphi^M$ , which entails $\Gamma^M \Rightarrow_K \varphi^M$ by Theorem 1. It is well known that this entails $\Gamma \Rightarrow_K \varphi$ .

Observe that Theorem 4 was developed fully constructively. This is noteworthy because similar results often make use of unconstructive principles. For example, the naive method of extending completeness from the $\dot{\,\forall\,},\dot{\to},\dot{\bot}$ -fragment directly to the full syntax for classical, standard Tarski models uses LEM (Forster et al. 2021). Moreover, it has been sown by Herbelin and Kirst (2023) that the non-constructive principle WLEMS ( $\forall p:\mathbb N\to\mathbb P.\,\neg\neg (\forall n. \, \neg p\,n\lor \neg \neg p\,n)$ , at the intersection of weak excluded middle and double-negation is necessary, to obtain completeness for full classical first-order logic. This should be taken as an indication that material dialogues are exceptionally well-suited as a semantics for classical first-order logic in a constructive setting.

4. Intuitionistic Material Dialogues

One of the striking features of dialogue games is that classical dialogue semantics can often be transformed into intuitionistic dialogue games by a simple change in the rules governing the interactions between proponent and opponent (see e.g. Krabbe 2006; Lorenz 1961): The proponent may only ever defend against the opponent’s most recent attack. This is an analogue to restricting the right-hand formula set $\Delta$ of sequents $\Gamma \Rightarrow \Delta$ to at most one formula to ‘transform’ classical sequent calculi into intuitionistic ones. The adjusted version of the proponent move transition relation $ \leadsto_p $ for the arising intuitionistic material dialogues is given below. Note that in this section, in a slight abuse of notation, $\text{Win}\,(\rho, A, C)$ and $\Gamma \vDash^D \varphi$ refer to dialogues played according to these intuitionistic rules. Further note that the rule PA remains unchanged when compared to classical material dialogues.

This version of intuitionistic material dialogues does not admit a constructive completeness proof. To demonstrate this, we define the following fragment of first-order logic:

\begin{align*} a, b : \mathfrak{A} & ::= \bot ~|~ P\,\vec{t} ~|~ a \dot{\,\wedge\,} b ~|~ a \dot{\,\vee\,} b ~|~ \dot{\,\exists\,} a & P : \Sigma, \vec{t} : \mathfrak{T}^{|P|} \\ \varphi, \psi : \mathfrak{F}^\texttt{D} & ::= a ~|~ \varphi \dot{\,\wedge\,} \psi ~|~ \varphi \dot{\,\vee\,} \psi ~|~ a \dot{\,\to\,} \psi ~|~ \dot{\,\forall\,} \varphi ~|~ \dot{\,\exists\,} \varphi &\end{align*}

$\mathfrak{A}$ is the fragment of first-order logic which allows attacking ‘blindly’, i.e. the same attack pattern can be used on these formulas in every winning strategy. The fragment $\mathfrak{A}$ does not include $a \dot{\,\to\,} b$ as attacking it requires being able to defend a and $\dot{\,\forall\,} x. a$ as attacking it requires a (finite) choice of $s: \textbf{S}$ . Unless specified otherwise, we are working in a fixed standard structure $\textbf{S}$ . The results of this section have not been mechanized.

Lemma 4. For any $a : \mathfrak{A}$ and any $\rho, A, C$ with $a \in A$ one may assume $\rho \vDash a$ to deduce $\text{Win}\,(\rho, A, C)$ , i.e. $(\rho \vDash a \to \text{Win}\,(\rho, A, C)) \to \text{Win}\,(\rho, A, C)$ .

Proof. Per induction on the structure of a. Suppose $\rho \vDash a$ entails $\text{Win}\,(\rho, a :: A, C)$ we show $\text{Win}\,(\rho, a :: A, C)$ . Where appropriate, we implicitly make use of the fact that $\text{Win}\,(\rho, A, C)$ entails $\text{Win}\,(\vec{s} \cdot \rho, A', \uparrow^n\,C)$ where $\vec{s} : \textbf{S}$ , $|\vec{s}| = n$ and $\uparrow^n A \subseteq A'$ .

• $a = P\,\vec{t}:$ Then, the proponent attacks $P\,\vec{t}$ , forcing the opponent to demonstrate $\rho \vDash P\,\vec{t}$ . The proponent may then continue according to the assumption.

• $a = \dot{\bot}:$ The proponent attacks $\dot{\bot}$ and wins.

• $a = b \dot{\,\wedge\,} c:$ The proponent starts by attacking $b \dot{\,\wedge\,} c$ with $A_L$ and $A_R$ , leaving us to prove that $\text{Win}\,(\rho, b :: c :: A, C)$ . Applying the IH for b and c means we may assume $\rho \vDash b$ and $\rho \vDash c$ to prove $\text{Win}\,(\rho, b :: c :: A, C)$ . As we thus know $\rho \vDash b \dot{\,\wedge\,} c,$ the proponent can proceed per assumption.

• $a = b \dot{\,\vee\,} c:$ The proponent attacks $b \dot{\,\vee\,} c$ , leaving $\text{Win}\,(\rho, d :: b \vee c :: A, C)$ for $d \in \{b, c\}$ . Applying the IH for d allows us to assume $\rho \vDash d$ , meaning the proponent can continue per assumption in either case.

• $a = \dot{\,\exists\,} b:$ The proponent attacks $\dot{\,\exists\,} b$ , leaving $\text{Win}\,(s \cdot \rho, b :: {\uparrow \hspace{-0.3em} (\dot{\,\exists\,} b :: A), {\uparrow \hspace{-0.3em} C}})$ . Per IH on b we may assume $s \cdot \rho \vDash b$ and thus $\rho \vDash \dot{\,\exists\,} b$ , continuing per assumption.

Theorem 5. Pick $\varphi : \mathfrak{F}^\texttt{D}$ , then $\rho \vDash \varphi$ entails $\text{Win}\,(\rho, A, C, \varphi)$ for any A and C.

Proof. Proof per induction on $\varphi$ .

• $\varphi : \mathfrak{A} :$ We only handle $\varphi = P\vec{t}$ and $\varphi = \dot{\bot}$ as the other cases are subsumed by other cases of this proof. If $\rho \vDash \dot{\bot}$ we are done. If $\varphi = P\vec{t,}$ then the only possible challenge is $A_P\,\vec{t}$ to which the proponent responds by demonstrating $\rho \vDash P\vec{t}$ .

• $\varphi = \psi \dot{\,\wedge\,} \theta:$ Then we know $\rho \vDash \varphi$ and $\rho \vDash \psi$ . The possible challenges are $A_L$ and $A_R$ , defending against which leaves $\text{Win}\,(\rho, A, A_X :: C, \theta)$ for some $\xi \in \{\varphi, \psi\}$ . Either case holds per IH for $\xi$ .

• $\varphi = \psi \dot{\,\vee\,} \theta:$ Then, we know $\rho \vDash \xi$ for $\xi \in \{\psi, \theta\}$ . The proponent thus defends against $A_\vee$ by admitting $\xi$ and proceeds per IH for $\xi$ .

• $\varphi = a \dot{\,\to\,} \psi:$ Then, we know $\rho \vDash a$ entails $\rho \vDash \psi$ . In attacking, the opponent will admit a, leaving $\text{Win}\,(\rho, a :: A, A_\to\,a\,\psi:: C)$ . We apply Lemma 4, allowing us to assume $\rho \vDash a$ to prove $\text{Win}\,(\rho, a :: A, A_\to\,a\,\psi :: C)$ . The proponent thus defends by admitting $\psi$ and proceeds per IH on $\psi$ as $\rho \vDash \psi$ per assumption.

• $\varphi = \dot{\,\forall\,} \psi:$ We know that $s \cdot \rho \vDash \psi$ for any $s : \textbf{S}$ . The challenge will be $A_s\,\psi$ for some $s : \textbf{S}$ . The proponent reacts by admitting $\psi(s)$ , proceeding per IH.

• $\varphi = \dot{\,\exists\,} \psi:$ Then, $s \cdot \rho \vDash \psi$ for some $s : \textbf{S}$ . The only possible challenge is $A_\exists\,\psi$ to which the proponent responds by admitting $\psi$ with s as the witness, proceeding per IH.

Theorem 5 can be made sense of in the following way: It is known that CIC is consistent with various non-intuitionistic intermediate logics whose axiom schemes lie partially in $\mathfrak{F}^\texttt{D}$ , e.g. classical logic ( $a \dot{\,\vee\,} \dot{\neg\,}a$ ) and Gödel-Dummett logic LC ( $(a \dot{\,\to\,} b) \dot{\,\vee\,} (b \dot{\,\to\,} a)$ ) for $a, b :\mathfrak{A}$ . By Theorem 5, it is thus consistent with CIC that these parts of the axiom schemes are dialogically valid according to the rules investigated in this section. However, this means that completeness of these dialogues with regard to some intuitionistic deduction system cannot be proven: If it could, that would mean it was consistent that parts of these non-intuitionistic axiom schemata, e.g. $P \dot{\,\vee\,} \dot{\neg\,} P$ , were provable intuitionistically, which we know not to be the case.

Under the full law of the excluded middle, one can obtain an even stronger result: intuitionistic and classical dialogical validity, as defined here, fully coincide. This result relies on the following lemma:

Lemma 5. Assuming LEM, the following holds for any $\varphi$ in any standard $\textbf{S}$

1. (1) $\forall \rho, A, C.~ \varphi \in A \to \rho \vDash \dot{\neg\,} \varphi \to \text{Win}\,(\rho, A, C)$

2. (2) $\forall \rho, A, C.~ \rho \vDash \varphi \to \text{Win}\,(\rho, A, C, \varphi)$

Proof. We show prove both claims per simultaneous induction on $\varphi$ . For most cases, 2. is the same as in Theorem 5 in which case we omit it. We write IHi for the inductive hypothesis for part i of Lemma 5.

• $\varphi = P\,\vec{t}:$ (1) The proponent may force the opponent to demonstrate $\rho \vDash P\,\vec{t}$ by attacking $P\,\vec{t} \in A$ , contradicting $\rho \vDash \neg P\,\vec{t}$ .

• $\varphi = \dot{\bot}:$ (1) The proponent may win by attacking $\dot{\bot} \in A$ .

• $\varphi = \psi \dot{\,\to\,} \theta:$ (1) Suppose $\rho \vDash \dot{\neg\,} (\psi \dot{\,\to\,} \theta)$ , meaning $\rho \vDash \psi$ and $\rho \vDash \dot{\neg\,} \theta$ . The proponent then attacks $\psi \dot{\,\to\,} \theta \in A$ . If the opponent counters the attack, the proponent can win by playing the strategy obtained by IH2 on $\rho \vDash \psi$ . If the opponent admits $\theta$ , then the proponent plays according to IH1 on $\rho \vDash \dot{\neg\,} \theta$ .

  • (2) Suppose $\rho \vDash \psi \dot{\,\to\,} \theta$ . The opponent attacks $\psi \dot{\,\to\,} \theta$ with $A_\to\,\psi\,\theta$ , admitting $\psi$ . By the law of the excluded middle, either $\rho \vDash \psi$ or $\rho \vDash \dot{\neg\,} \psi$ . In the latter case, the proponent can now proceed per IH2 on $\rho \vDash \dot{\neg\,} \psi$ . In the former case, we have $\rho \vDash \theta$ per assumption and the proponent can proceed by admitting $\theta$ and playing along IH1 on $\rho \vDash \theta$ .

• $\varphi = \psi \dot{\,\wedge\,} \theta:$ (1) Suppose $\rho \vDash \dot{\neg\,} (\psi \dot{\,\wedge\,} \theta)$ , meaning $\rho \vDash \dot{\neg\,} \psi$ or $\rho \vDash \dot{\neg\,} \theta$ . The proponent attacks the side of the contradicted formula of $\psi \dot{\,\wedge\,} \theta \in A$ and proceeds per IH1.

• $\varphi = \psi \dot{\,\vee\,} \theta:$ (1) Suppose $\rho \vDash \dot{\neg\,} (\psi \dot{\,\vee\,} \theta)$ , meaning $\rho \vDash \dot{\neg\,} \psi$ and $\rho \vDash \dot{\neg\,} \theta$ . By attacking $\psi \dot{\,\vee\,} \theta \in A$ , the proponent thus forces the opponent to admit either clause, being able to proceed via IH1 in either case.

• $\varphi = \dot{\,\forall\,} \psi:$ (1) If $\rho \vDash \dot{\neg\,} \dot{\,\forall\,} \psi$ that means there is an $s : \textbf{S}$ with $s \cdot \rho \vDash \dot{\neg\,} \psi$ . The proponent thus attack $\dot{\,\forall\,} \psi$ with $A_s \,\psi$ and proceeds per IH1.

• $\varphi = \dot{\,\exists\,} \psi:$ (1) Suppose $\rho \vDash \dot{\neg\,} \dot{\,\exists\,} \psi$ , meaning $s \cdot \rho \vDash \dot{\neg\,} \psi$ for any $s : \textbf{S}$ . Then the proponent attacks $\dot{\,\exists\,} \psi \in A$ and proceeds per IH1.

Theorem 6. Under LEM, classical and intuitionistic dialogical validity agree.

Proof.

• $\leftarrow:$ This is the case – even without the law of excluded middle – as every intuitionistic winning strategy is also a classical winning strategy on the same state.

• $\to:$ Suppose $\Gamma \vDash^D \varphi$ classically. By Lemma 2 this means $\Gamma \vDash^E \varphi$ . As every standard structure is exploding and under the LEM every structure is classical, this means $\varphi$ is valid under $\Gamma$ in every standard structure. By Lemma 5 this entails that $\Gamma \vDash^D \varphi$ intuitionistically.

Note that the failure of completeness is not simply due to the ‘wrong choice of rules’ for intuitionistic dialogues. While there are examples of the proponent restriction failing to turn classical dialogues intuitionistic (see e.g. Wolff 2022), we do not believe this to be the case in this instance. Formal dialogues for intuitionistic first-order logic, which are obtained from their classical counterparts via that very restriction, are constructively sound and complete (Felscher 1985; Forster et al. 2020; Lorenz 1961). Rather, we believe the cause of failure lies in the difference between formal and material dialogues: their treatment of atomic formulas.

5. Kripke Material Dialogues

In the previous section, we demonstrated that intuitionistic material dialogues fail to capture intuitionistic first-order logic. Classical material dialogues can be seen as classical dialogues played on the canonical notion of model for classical first-order logic: Tarski models. In that vein, we present intuitionistic dialogues played on Kripke models as a semantics for intuitionistic first-order logic. While these stray far from the ideas of Lorenzen, they admit a constructive completeness proof restricted to the $\dot{\,\forall\,},\dot{\to},\dot{\bot}$ -fragment.

A Kripke material dialogue is played on a Kripke structure $(K, \leq, \textbf{S}_{-}, \iota)$ . The game states of Kripke material dialogues are dependent pairs $(k, \rho^k, A, C) :\Sigma k : K,~(\mathbb{N} \to \textbf{S}_k) \times \mathcal{L}(\mathfrak{F}) \times \mathcal{L}(\mathbf{A})$ representing material dialogue states ‘at a world k in K’. Mirroring the clauses of $\Vdash$ for $\to$ and $\forall$ , opponent attacks in Kripke dialogues may ‘move’ the game state along $\leq$ in K. To express this, we define a predicate $a \mid k \mapsto k'$ with $A_\to\,\varphi\,\psi \mid k \mapsto k'$ and $A_s\,\varphi \mid k \mapsto k'$ hold whenever $k \leq k'$ and $a \mid k \mapsto k$ holds for all other attacks a. The definitions of valid moves and their effects on the game state are largely analogous to intuitionistic material dialogues. In a slight abuse of notation, we use the same notation for describing dialogues as in Sections 3 and 4 to denote concepts relating to Kripke material dialogues. Note that the definitions of $d^P$ and $d^O$ are essentially the same as for the previous material dialogues, leaving the world unchanged.

The definition of $\text{Win}\,(k, \rho, A, C)$ remains unchanged. To account for attacks ‘moving’ the state along $k \leq k'$ , $\text{Win}\,(k,\rho, A, C, \varphi)$ now is a shorthand for the statement that $\text{Win}\,(k', \rho, a :: A, a :: C)$ for any $a \rhd \varphi$ with $a \mid k \mapsto k'$ . We then define $\Gamma \vDash ^D \varphi$ the same as before.

The results of this section have not been mechanized. We first prove that Kripke material dialogues are sound with regard to the intuitionistic sequent calculus $\Gamma \Rightarrow_J \delta$ given in Section 2.2. Note that this proof of soundness requires a similar notion of congruences as the Lemma 1 used in proving soundness of classical material dialogues.

Lemma 6. Suppose $\text{Win}\,(k, \rho, A, C)$ and $\rho, A \equiv \rho', A'$ and $\rho, C \equiv \rho', C'$ for some $\rho'$ , A’ and C’. Then $\text{Win}\,(k, \rho', A', C')$ .

Theorem 7 (Soundness). Suppose $\Gamma \Rightarrow_J \delta$ then $\Gamma \vDash^D \delta$ .

Proof. It suffices to prove that $\Gamma \Rightarrow_J \delta $ entails $\forall k, \rho, C.~\text{Win}\,(k, \rho, \Gamma, \delta)$ for all exploding Kripke structures. We proceed per induction on $\Gamma \Rightarrow_J \delta$ . We only treat a few exemplary cases.

Ax: The only possible challenge is $A_P\,\overline{t}$ . Then, the proponent attacks the $P\,\overline{t} \in \Gamma$ , forcing the opponent to demonstrate $P^k\,\overline{t}^\rho$ . Then, the proponent can defend against $A_P\,\overline{t}$ by demonstrating the same fact, thereby winning the dialogue.

L $\bot$ : The proponent attacks $\dot{\bot} \in \Gamma$ , forcing the proponent to demonstrate $\bot$ . The existence of a winning strategy then follows from the principle of explosion.

L $\to$ : The proponent thus attacks $\varphi \dot{\,\to\,} \psi \in \Gamma$ . If the opponent counters, the proponent plays according to the IH on $\Gamma \Rightarrow_J \varphi$ . If the opponent defends, the proponent plays according to the IH on $\Gamma, \psi \Rightarrow_J \delta$ .

R $\to$ : Then, the challenge is $A_\to\,\varphi\,\psi$ , leaving us to prove $\text{Win}\,(k', \rho, \varphi :: \Gamma, A_\to\,\varphi\,\psi :: C)$ for some $k \leq k'$ . As $\varphi :: \varphi :: \Gamma \subseteq \varphi :: \Gamma$ , the proponent may defend and continue playing according to the weakened inductive hypothesis.

L $\forall$ : The proponent attacks $\dot{\,\forall\,} \varphi \in \Gamma$ choosing $t^\rho : \textbf{S}_k$ as the witness. Once the opponent defends, the game state is $\text{Win}\,(k, t^\rho \cdot \rho, \varphi :: {\uparrow \hspace{-0.3em} \Gamma}, {\uparrow \hspace{-0.3em} (c :: C)})$ . By applying Lemma 6, the proponent may continue to play according to the IH as $\rho, \varphi[t] :: \Gamma \equiv t^\rho \cdot \rho, \varphi :: {\uparrow \hspace{-0.3em} \Gamma}$ and $\rho, c :: C \equiv t^\rho \cdot \rho, {\uparrow \hspace{-0.3em} (c :: C)}$ .

R $\forall$ : Then, the challenge is $A_s \,\varphi$ for some $s : \textbf{S}_{k'}$ and $A_s \,\varphi \mid k \mapsto k'$ . The proponent can then defend and continue playing according to the IH on ${\uparrow \hspace{-0.3em} \Gamma} \Rightarrow_J \varphi$ .

Completeness is also proven with a strategy analogous to that for classical material dialogues in Section 3. We first prove that Kripke dialogical validity entails exploding Kripke validity. We then use a prior result from Herbelin and Lee (2009) to deduce completeness for the $\forall,\to,\bot$ -fragment.

We extend the forcing relation to defenses as follows

\begin{align*} \rho^k \Vdash D_A\,\varphi ~:\Leftrightarrow~ \rho^k \Vdash \varphi\quad\quad \rho^k \Vdash D_W\,\varphi\,s ~:\Leftrightarrow~ s \cdot \rho^k \Vdash \varphi\quad\quad \rho^k \Vdash D_M\,\varphi ~:\Leftrightarrow~ \rho^k \Vdash \varphi\end{align*}

and define an auxiliary predicate on contexts $\Gamma$ , k-environments $\rho$ and challenges c

\[\Gamma \Vdash_\rho^k \bigvee \mathcal{D}_{c} ~:\Leftrightarrow~ \forall k \leq k', \vec{s} : S_{k'}, \alpha.~ \rho^{k'} \Vdash \Gamma \to (\forall d \in \mathcal{D}_{c}.~\rho^{k'} \Vdash d \to \vec{s} \cdot \rho^{k'} \Vdash \alpha) \to \vec{s} \cdot \rho^{k'} \Vdash \alpha\]

$\Gamma \Vdash_\rho^k \bigvee \mathcal{D}_{c}$ should be read as $\Gamma$ semantically entailing the disjunction of the semantic interpretations of defenses against c under the k-environment $\rho$ .

Lemma 7. If for some $\varphi$ we have $(c :: \Gamma) \Vdash_\rho^k \bigvee \mathcal{D}_{c}$ for all $c \rhd \varphi,$ then $\rho^k \Vdash \Gamma$ entails $\rho^k \Vdash \varphi$ .

Proof. Assume $({\star})~ \forall c \rhd \varphi.~(c :: \Gamma) \Vdash_\rho^k \bigvee \mathcal{D}_{c}$ and $\rho^k \Vdash \Gamma$ . We proceed per case distinction on $\varphi$ .

• $\varphi = \dot{\bot}:$ Follows from $({\star})$ with $c = A_\bot$ .

• $\varphi = P\,\overline{t}:$ Follows from $({\star})$ with $c = A_P\,\overline{t}$ .

• $\varphi = \psi \dot{\,\to\,} \theta:$ Let $k \leq k'$ and suppose $\rho^{k'} \Vdash \psi$ . As this means $\rho^{k'} \Vdash \psi :: \Gamma$ , $\rho^{k'} \Vdash \theta$ follows from $({\star})$ with $c = A_\to\,\psi\,\theta$ .

• $\varphi = \psi \dot{\,\wedge\,} \theta:$ Apply $({\star})$ with $A_L\,\psi$ and $A_R\,\theta$ to obtain $\rho^k \Vdash \psi$ and $\rho^k \Vdash \theta$ , yielding $\rho^k \Vdash \psi \dot{\,\wedge\,} \theta$ .

• $\varphi = \psi \dot{\,\vee\,} \theta:$ Apply $({\star})$ with $A_\vee\,\psi\,\theta$ . This leaves us proving that $\rho^k \Vdash \psi$ and $\rho^k \Vdash \theta$ each entail $\rho^k \Vdash \psi \dot{\,\vee\,} \theta$ , which is clear.

• $\varphi = \dot{\,\forall\,} \psi:$ Let $k \leq k'$ and $s : \textbf{S}_{k'}$ , we need to prove that $s \cdot \rho^{k'} \Vdash \psi$ . For this, we apply $({\star})$ with $A_s\,\psi$ and $\vec{s} = s$ .

• $\varphi = \dot{\,\exists\,} \psi:$ Apply $({\star})$ with $A_\exists\,\psi$ . This leaves us proving that for $s : \textbf{S}_k$ , $s \cdot \rho^k \Vdash \psi$ entails $\rho^k \Vdash \dot{\,\exists\,} \psi$ , which is clear.

Recall that for any structure $\textbf{S}$ , we denote by $\hat{\textbf{S}}$ the standard structure with $\dot{\bot}^{\hat{\textbf{S}}} = \bot$ which is otherwise exactly the same as $\textbf{S}$ .

Lemma 8. Let $(K, \leq, \textbf{S}_{-}, \iota)$ be exploding. Suppose $\text{Win}\,(k, \rho, \Gamma, c :: C)$ over $(K, \leq, \hat{\textbf{S}}_{-}, \iota)$ then $\Gamma \Vdash_\rho^k \bigvee \mathcal{D}_{c}$ over $(K, \leq, \textbf{S}_{-}, \iota)$ .

Proof. We proceed per induction on $\text{Win}\,(k, \rho, \Gamma, c :: C)$ . Fix $k \leq k'$ , $\vec{s} : S_{k'}$ and suppose $\rho^{k'} \Vdash \Gamma$ and furthermore that $\rho^{k'} \Vdash d$ entails $\vec{s} \cdot \rho^{k'} \Vdash \alpha$ for all $d \in \mathcal{D}_{c}$ . We perform a case distinction on the proponent’s move.

• $PA:$ The proponent attacks some $\varphi \in \Gamma$ . We perform a case distinction on $\varphi$ .

• $\varphi = \dot{\bot}:$ Then, $\rho^{k'} \Vdash \dot{\bot}$ per assumption and thus $\rho^{k'} \Vdash \alpha$ as the structure is exploding.

• $\varphi = P\,\overline{t}:$ Apply the IH for the opponent defending by demonstrating $\rho^{k'} \Vdash P\,\overline{t}$ , which holds per assumption.

• $\varphi = \psi \dot{\,\to\,} \theta:$ First apply Lemma 7 to the IH upon the opponent countering to obtain $\rho^{k'} \Vdash \psi$ . We can then apply the IH obtained upon the opponent admitting $\theta$ as $\rho^{k'} \Vdash \psi :: \Gamma$ .

• $\varphi = \psi \dot{\,\wedge\,} \theta:$ To apply the IH, either $\rho^k \Vdash \psi$ or $\rho^k \Vdash \theta$ must be shown, depending on the proponent’s attack. Both hold as $\rho^k \Vdash \psi \dot{\,\wedge\,} \theta$ per assumption.

• $\varphi = \psi \dot{\,\vee\,} \theta:$ As $\rho^{k'} \Vdash \psi \dot{\,\vee\,} \theta$ per assumption, either $\rho^{k'} \Vdash \psi$ or $\rho^{k'} \Vdash \theta$ . In either case, we can apply the IH upon the opponent admitting the respective formula.

• $\varphi = \dot{\,\forall\,} \psi:$ The proponent chooses some $s : \textbf{S}_k$ . As $\rho^{k'} \Vdash \dot{\,\forall\,} \psi$ we have $s \cdot \rho^{k'} \Vdash \psi$ . Denote by $\uparrow_{\vec{s}} \alpha$ the renaming of $\alpha$ in which every strictly index less than $|\vec{s}|$ remains the same and any other index is increased by one. By applying the IH upon the opponent admitting this, we can then obtain $\vec{s} \cdot s \cdot \rho^{k'} \Vdash \uparrow_{\vec{s}} \alpha$ which is equivalent to $\vec{s} \cdot \rho^{k'} \Vdash \alpha$ by design of the $\uparrow_{\vec{s}}$ -operation.

• $\varphi = \dot{\,\exists\,} \psi:$ As $\rho^{k'} \Vdash \dot{\,\exists\,} \psi$ there must be some $s : \textbf{S}_{k'}$ such that $s \cdot \rho^{k'} \Vdash \psi$ . By applying the IH upon the opponent admitting this, we can then obtain $\vec{s} \cdot s \cdot \rho^{k'} \Vdash \uparrow_{\vec{s}} \alpha$ meaning $\vec{s} \cdot \rho^{k'} \Vdash \alpha$ .

• $PD:$ The proponent defends against c via some $d \in \mathcal{D}_{c}$ . We conclude $\vec{s} \cdot \rho^{k'} \Vdash \alpha$ from the assumption by showing $\rho^{k'} \Vdash d$ . If $d = P_M\,\varphi$ then $\rho^k \Vdash \varphi$ and thus $\rho^{k'} \Vdash \varphi$ must hold for the proponent move to have been legal. In the other two cases, an application of Lemma 7 to the IH yields $\rho^{k'} \Vdash d$ .

Lemma 9. For any $\Gamma$ and $\varphi$ , $\Gamma \vDash^D \varphi$ entails $\Gamma \vDash_K^E \varphi$ .

Proof. Assume $\Gamma \vDash^D \varphi$ and fix an exploding Kripke structure $(K, \leq, \textbf{S}_{-}, \iota)$ , a world $k : K$ and an environment $\rho^k$ such that $\rho^k \Vdash \Gamma$ . As $\Gamma \vDash^D \varphi$ , we know that $\text{Win}\,(\rho^k, \Gamma, [], \varphi)$ in $(K, \leq, \hat{\textbf{S}}_{-}, \iota)$ . Then by Lemma 8 we know $c :: \Gamma \Vdash_{\rho^k}^k \mathcal{D}_{c}$ in $(K, \leq, \textbf{S}_{-}, \iota)$ for every $c \rhd \varphi$ . With Lemma 7 we may thus conclude $\rho^k \Vdash \varphi$ as desired.

Theorem 8 (Completeness.) When restricting to the $\dot{\,\forall\,}, \dot{\to}, \dot{\bot}$ -fragment, $\Gamma \vDash^D \varphi$ entails $\Gamma \Rightarrow_J \varphi$ .

Proof. By Lemma 9, we know $\Gamma \vDash^E_K \varphi$ . Herbelin and Lee (2009) prove that this entails $\Gamma \Rightarrow_J \varphi$ .

Similarly to the case of classical first-order logic at the end of Section 3, it is a current subject of investigation which non-constructive principles are needed to extend the completeness result for the intuitionistic case to the full syntax. Concretely, we expect that the aforementioned principle WLEMS is necessary in any case and possibly even sufficient.

6. Discussion

Mechanization of active research While researching for this article, we mechanized the results from Section 3 in the interactive theorem prover Coq. The mechanization can be found at Wehr and Kirst (2022b ). Mechanizing the results of Section 3 revealed some mistakes concerning the binding structure in our initial definition of the rules for material dialogues which, albeit being minor, invalidated both soundness and completeness. We missed these mistakes while working ‘on paper’ and believe it would have taken much longer to discover them without the mechanization. Having machine checked the definitions in Section 3 gave us sufficient confidence in the correctness of the technical details of material dialogues to work solely on paper for the remainder of the article.

It should also be noted that the mechanization took up only about a quarter of the overall time spent researching for this project, in large part due to building on top of the a large preexisting mechanization from Forster et al. (2021). Notably, this mechanization already included mechanizations of the results from Herbelin and Ilik (2016), Herbelin and Lee (2009). We believe this might be a worthwhile trade-off between the time requirement of a full mechanization of all results and the room for error in working solely on paper. To this end, a library aimed at easing the mechanization of results concerning first-order logic in Coq has since been prepared by Kirst et al. (2022).

Proof strategies for Completeness We prove completeness by relating dialogical validity to validity in a model-theoretic semantics and appealing to a preexisting completeness result. This is the quickest way to obtain completeness in the framework set up by Forster et al. (2021). For classical material dialogues, we believe it would also be possible to obtain a direct constructive completeness proof with regard to natural deduction on the basis of a Henkin construction.

Benefits of Material Dialogues When working with Tarski semantics in CIC, one’s attention needs to be restricted to classical structures (as defined in Section 2). Many structures of interest such as the standard model of Peano arithmetic is not provably classical in constructive settings and can thus not be studied in a Tarski setting. In contrast, Section 3 demonstrates that classical material dialogues embody classical logic regardless of the classicality of the underlying structure. It thus seems like a promising basis on which to carry out model-theoretic investigations of classical first-order logic in constructive settings. However, we have not yet investigated these possibilities more deeply.

Faithfulness to Lorenzen’s material dialogues We attempted to be as faithful to Lorenzen’s definitions from Lorenzen (1960, 1961) as possible while implementing material dialogues played over first-order structures. Arguably, this second aspect already is in conflict with Lorenzen’s ideas as he placed a lot of value in the ‘underlying game’ for settling atomic propositions to be of a discrete nature, something completely lost in our formulation. However, all the attacks and defenses for the connectives of first-order logic are exactly as they are in Lorenzen’s work. Notably, our usage of a structure defined, standard constant $\dot{\bot}^\textbf{S}$ is very similar to Lorenzen’s definitions which propose to fix some unwinnable game as a stand-in for a ‘demonstration’ of $\dot{\bot}$ . Because of the addition of the Kripke frame and allowing opponent attacks to ‘move’ the game state along it, Kripke material dialogues stray very far from what is described by Lorenzen (1960, 1961).

Classical Kripke Dialogues The analysis of Kripke dialogues for intuitionistic first-order logic raises the question of how Kripke dialogues played according to classical rules would behave. While we chose not to pursue this question further, we believe that Kripke dialogues with classical rules should behave similarly to the classical material dialogues of Section 3. Concretely, we believe their validity entails classical exploding Tarski validity because every classical exploding Tarski structure can also be viewed as an equivalent one-world Kripke structure. The more critical property is soundness: We believe that the ‘independence of the classicality of the structure’ already demonstrated by the soundness proof for classical material dialogues should extend to even work on Kripke structures.