Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics

TL;DR

This paper provides a completeness proof for the basic STIT logic Ldm and derives the independence of agents axiom for Xstit, enhancing the theoretical foundations of temporal STIT logics.

Contribution

It offers the first completeness proof for Ldm relative to irreflexive temporal Kripke frames and formalizes the independence of agents axiom for Xstit.

Findings

Completeness proof for Ldm with irreflexive temporal frames

Derivation of independence of agents axiom for Xstit

Strengthened theoretical understanding of temporal STIT logics

Abstract

This paper is an appendix to the paper "Cut-free Calculi and Relational Semantics for Temporal STIT logics" by Berkel and Lyon, 2019. It provides the completeness proof for the basic STIT logic Ldm (relative to irreflexive, temporal Kripke STIT frames) as well as gives the derivation of the independence of agents axiom for the logic Xstit.

Full text

Appendix 0.A Completeness of $\mathsf{Ldm}$

We give the definitions and lemmas sufficient to prove the completeness of $\mathsf{Ldm}$ relative to $\mathsf{Tstit}$ frames [4, 2]. We make use of the canonical model of $\mathsf{Ldm}$ (obtained by standard means [3, 1]) to construct a $\mathsf{Tstit}$ model. A truth-lemma is then given relative to this model, from which, completeness follows as a corollary.

Definition 1 ($\mathsf{Ldm}$-CS, $\mathsf{Ldm}$-MCS)

A set $\Theta\subset\mathcal{L}_{\mathsf{Ldm}}$ is a $\mathsf{Ldm}$ consistent set ($\mathsf{Ldm}$-CS) iff $\Theta\not\vdash_{\mathsf{Ldm}}\bot$. We call a set $\Theta\subset\mathcal{L}_{\mathsf{Ldm}}$ a $\mathsf{Ldm}$ maximally consistent set ($\mathsf{Ldm}$-MCS) iff $\Theta$ is a $\mathsf{Ldm}$-CS and for any set $\Theta^{\prime}$ such that $\Theta\subset\Theta^{\prime}$, $\Theta^{\prime}\vdash_{\mathsf{Ldm}}\bot$.

Lemma 1 (Lindenbaum’s Lemma [3])

Every $\mathsf{Ldm}$-CS can be extended to a $\mathsf{Ldm}$-MCS.

Definition 2 (Present and Future Pre-Canonical $\mathsf{Tstit}$ Model)

The present pre-canonical $\mathsf{Tstit}$ model is the tuple $M^{\mathsf{pres}}=(W^{\mathsf{pres}},\mathcal{R}^{\mathsf{pres}}_{\Box},$ $\{\mathcal{R}^{\mathsf{pres}}_{i}|i\in Ag\},V^{\mathsf{pres}})$ defined below left, and the future pre-canonical $\mathsf{Tstit}$ model is the tuple $M^{\mathsf{fut}}=(W^{\mathsf{fut}},\mathcal{R}^{\mathsf{fut}}_{\Box},\{\mathcal{R}^{\mathsf{fut}}_{i}|i\in Ag\},V^{\mathsf{fut}})$ defined below right:

• •

$W^{\mathsf{pres}}$ is the set of all $\mathsf{Ldm}$-MCSs;

• •

$\mathcal{R}^{\mathsf{pres}}_{\Box}wu$ iff for all $\Box\phi\in w$, $\phi\in u$;

• •

$\mathcal{R}^{\mathsf{pres}}_{i}wu$ iff for all $[i]\phi\in w$, $\phi\in u$;

• •

$V^{\mathsf{pres}}(p)=\{w\in W|p\in w\}$.

• •

$W^{\mathsf{fut}}=W^{\mathsf{pres}}$;

• •

$\mathcal{R}^{\mathsf{fut}}_{\Box}(w)=\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(w)$;

• •

$\mathcal{R}^{\mathsf{fut}}_{i}(w)=\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(w)$;

• •

$V^{\mathsf{fut}}(p)=V^{\mathsf{pres}}(p)$.

Definition 3 (Canonical Temporal Kripke STIT Model)

We define the canonical temporal Kripke STIT model to be the tuple $M^{\mathsf{Ldm}}=(W^{\mathsf{Ldm}},\mathcal{R}^{\mathsf{Ldm}}_{\Box},$ $\{R^{\mathsf{Ldm}}_{i}|i\in Ag\},\mathcal{R}^{\mathsf{Ldm}}_{Ag},\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}},\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{H}},$ $V^{\mathsf{Ldm}})$ such that:

• •

$W^{\mathsf{Ldm}}=W^{\mathsf{pres}}\times\mathbb{N}$111Note that we choose to write each world $(w,j)\in W^{\mathsf{Ldm}}$ as $w^{j}$ to simplify notation. Moreover, we write $\phi\in w^{j}$ to mean that the formula $\phi$ is in the $\mathsf{Ldm}$-MCS $w$ associated with $j$.;

• •

$\mathcal{R}^{\mathsf{Ldm}}_{\Box}w^{j}u^{j}$ iff (i) $\mathcal{R}^{\mathsf{pres}}_{\Box}wu$ and $j=0$, or (ii) $\mathcal{R}^{\mathsf{fut}}_{\Box}wu$ and $j>0$;

• •

$\mathcal{R}^{\mathsf{Ldm}}_{i}w^{j}u^{j}$ iff (i) $\mathcal{R}^{\mathsf{pres}}_{i}wu$ and $j=0$, or (ii) $\mathcal{R}^{\mathsf{fut}}_{i}wu$ and $j>0$;

• •

$\mathcal{R}^{\mathsf{Ldm}}_{Ag}(w^{j})=\bigcap_{1\leq i\leq n}\mathcal{R}^{\mathsf{Ldm}}_{i}(w^{j})$;

• •

$\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}=\{(w^{j},w^{k})|w^{j},w^{k}\in W^{\mathsf{Ldm}}\text{ and }j<k\}$;

• •

$\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{H}}=\{(u^{i},w^{i})|(w^{i},u^{i})\in\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}\}$;

• •

$V^{\mathsf{Ldm}}(p)=\{w^{j}\in W^{\mathsf{Ldm}}|w\in V^{\mathsf{pres}}(p)\}$.

Lemma 2

For all $\alpha\in\{\Box,Ag\}\cup Ag$, if $\mathcal{R}^{\mathsf{Ldm}}_{\alpha}w^{j}u^{k}$ for $j,k\in\mathbb{N}$, then $j=k$.

Proof

Follows by definition of the canonical $\mathsf{Tstit}$ model.

Lemma 3

For all $j\in\mathbb{N}$ with $k\geq 1$, $(w^{j},u^{j})\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}$ iff $(w^{j+k},u^{j+k})\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}$.

Proof

This follows from the fact that $u^{0}\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}(w^{0})$ iff $u\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(w)$ iff $u\in\mathcal{R}^{\mathsf{fut}}_{i}(w)$ for each $i\in Ag$ iff $u\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{fut}}_{i}(w)$ iff $u^{k}\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{Ldm}}_{i}(w^{k})$ for any $k>0$.

Lemma 4 ([3])

(i) For all $\mathsf{x}\in\{\mathsf{pres},\mathsf{fut},\mathsf{Ldm}\}$, $\mathcal{R}^{\mathsf{x}}_{\Box}wu$ iff for all $\phi$, if $\phi\in u$, then $\Diamond\phi\in w$. (ii) For all $\mathsf{x}\in\{\mathsf{pres},\mathsf{fut},\mathsf{Ldm}\}$, $\mathcal{R}^{\mathsf{x}}_{i}wu$ iff for all $\phi$, if $\phi\in u$, then $\langle i\rangle\phi\in w$.

Lemma 5 (Existence Lemma [3])

(i) For any world $w^{j}\in W^{\mathsf{Ldm}}$, if $\Diamond\phi\in w^{j}$, then there exists a world $u^{j}\in W^{\mathsf{Ldm}}$ such that $\mathcal{R}^{\mathsf{Ldm}}_{\Box}w^{j}u^{j}$ and $\phi\in u^{j}$. (ii) For any world $w^{j}\in W^{\mathsf{Ldm}}$, if $\langle i\rangle\phi\in w^{j}$, then there exists a world $u^{j}\in W^{\mathsf{Ldm}}$ such that $\mathcal{R}^{\mathsf{Ldm}}_{i}w^{j}u^{j}$ and $\phi\in u^{j}$.

Lemma 6

The Canonical Model is a temporal Kripke STIT model.

Proof

We prove that $M^{\mathsf{Ldm}}$ has all the properties of a $\mathsf{Tstit}$ model:

• •

By lemma 1, the $\mathsf{Ldm}$ consistent set $\{p\}$ can be extended to a $\mathsf{Ldm}$-MCS, and therefore $W^{\mathsf{pres}}$ is non-empty. Since $\mathbb{N}$ is non-empty as well, $W^{\mathsf{pres}}\times\mathbb{N}=W^{\mathsf{Ldm}}$ is a non-empty set of worlds.

• •

We argue that $\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ is an equivalence relation between worlds of $W^{\mathsf{Ldm}}$, and omit the arguments for $\mathcal{R}^{\mathsf{Ldm}}_{i}$ and $\mathcal{R}^{\mathsf{Ldm}}_{Ag}$, which are similar. Suppose that $w^{j}\in W^{\mathsf{Ldm}}$. We have two cases to consider: (i) $j=0$, and (ii) $j>0$. (i) Standard canonical model arguments apply and $\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ is an equivalence relation between all worlds of the form $w^{0}\in W^{\mathsf{Ldm}}$ (See [3] for details). (ii) If we fix a $j>0$, then $\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ will be an equivalence relation for all worlds of the form $w^{j}\in W^{\mathsf{Ldm}}$ since the intersection of equivalence relations produces another equivalence relation. Last, since $\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ is an equivalence relation for each fixed $j\in\mathbb{N}$, and because each $W^{\mathsf{pres}}\times\{j\}\subset W^{\mathsf{Ldm}}$ is disjoint from each $W^{\mathsf{pres}}\times\{j^{\prime}\}\subset W^{\mathsf{Ldm}}$ for $j\neq j^{\prime}$, we know that the union all such equivalence relations will be an equivalence relation.

• (C1)

Let $i$ be in $Ag$ and assume that $(w^{j},u^{j})\in\mathcal{R}^{\mathsf{Ldm}}_{i}$. We split the proof into two cases: (i) $j=0$, or (ii) $j>0$. (i) Assume that $\Box\phi\in w^{0}$. Since $w$ is a $\mathsf{Ldm}$-MCS, it contains the axiom $\Box\phi\rightarrow[i]\phi$, and so, $[i]\phi\in w$ as well. Since $(w,u)\in\mathcal{R}^{\mathsf{pres}}_{i}$ (because $j=0$), we know that $\phi\in u$ by the definition of the relation; therefore, $(w,u)\in\mathcal{R}^{\mathsf{pres}}_{\Box}$, which implies that $(w^{0},u^{0})\in\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ by definition. (ii) The assumption that $j>0$ implies that $u\in\mathcal{R}^{\mathsf{fut}}_{i}(w)$ $=\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(w)=\mathcal{R}^{\mathsf{fut}}_{\Box}(w)$ by definition, which implies that $(w^{j},u^{j})\in\mathcal{R}^{\mathsf{Ldm}}_{\Box}$.

• (C2)

Let $u^{j}_{1},...,u^{j}_{n}\in W^{\mathsf{Ldm}}$ and assume that $\mathcal{R}^{\mathsf{Ldm}}_{\Box}u^{j}_{i}u^{j}_{k}$ for all $i,k\in\{1,...,n\}$. We split the proof into two cases: (i) $j=0$, or (ii) $j>0$. (i) We want to show that there exists a world $w^{j}\in W^{\mathsf{Ldm}}$ such that $w^{j}\in\bigcap_{1\leq i\leq n}\mathcal{R}^{\mathsf{Ldm}}_{i}(u^{j}_{i})$. Let $\hat{w}^{j}=\bigcup_{1\leq i\leq n}\{\phi|[i]\phi\in u^{j}_{i}\}$. Suppose that $\hat{w}^{j}$ is inconsistent to derive a contradiction. Then, there are $\psi_{1}$,…,$\psi_{k}$ such that $\vdash_{\mathsf{Ldm}}\bigwedge_{1\leq l\leq k}\psi_{i}\rightarrow\bot$. For each $i\in Ag$, we define $\Phi_{i}=\{\psi_{l}|[i]\psi_{l}\in u^{j}_{i}\}\subseteq\{\psi_{1},...,\psi_{k}\}$. Observe that for each $i\in Ag$, $[i]\bigwedge\Phi_{i}\in u^{j}_{i}$ because $\bigwedge[i]\Phi_{i}\in u^{j}_{i}$ and $\vdash_{\mathsf{Ldm}}\bigwedge[i]\Phi_{i}\rightarrow[i]\bigwedge\Phi_{i}$. Since by assumption $\mathcal{R}^{\mathsf{Ldm}}_{\Box}u^{j}_{i}u^{j}_{k}$ for all $i,k\in\{1,...,n\}$, this means that for any $u^{j}_{m}$ we pick (with $1\leq m\leq n$), $\Diamond[i]\bigwedge\Phi_{i}\in u^{j}_{m}$ for each $i\in Ag$ by lemma 4; hence, $\bigwedge_{i\in Ag}\Diamond[i]\bigwedge\Phi_{i}\in u^{j}_{m}$. By the $(\mathsf{IOA})$ axiom, this implies that $\Diamond\bigwedge_{i\in Ag}[i](\bigwedge\Phi_{i})\in u^{j}_{m}$. By lemma 5, there must exist a world $v^{j}$ such that $\mathcal{R}^{\mathsf{Ldm}}_{\Box}u^{j}_{m}v^{j}$ and $\bigwedge_{i\in Ag}[i](\bigwedge\Phi_{i})\in v^{j}$. But then, since $\vdash_{\mathsf{Ldm}}[i](\bigwedge\Phi_{i})\rightarrow\bigwedge\Phi_{i}$ by reflexivity, $\vdash_{\mathsf{Ldm}}\bigwedge_{i\in Ag}(\bigwedge\Phi_{i})\leftrightarrow\bigwedge_{1\leq i\leq k}\psi_{i}$, and $\vdash_{\mathsf{Ldm}}\bigwedge_{1\leq i\leq k}\psi_{i}\rightarrow\bot$, it follows that $\bot\in v^{j}$, which is a contradiction since $v^{j}$ is a $\mathsf{Ldm}$-MCS. Therefore, $\hat{w}^{j}$ must be consistent and by lemma 1, it may be extended to a $\mathsf{Ldm}$-MCS $w^{j}$. Since for each $[i]\phi\in u^{j}_{i}$, $\phi\in w^{j}$, we have that $w\in\mathcal{R}^{\mathsf{pres}}_{i}(u_{i})$ for each $i\in Ag$. Hence, $w\in\bigcap_{1\leq i\leq n}\mathcal{R}^{\mathsf{pres}}_{i}(u_{i})$, and so, $w^{j}\in\bigcap_{1\leq i\leq n}\mathcal{R}^{\mathsf{Ldm}}_{i}(u^{j}_{i})$. (ii) Suppose that $j>0$, so that $t^{j}\in\mathcal{R}^{\mathsf{Ldm}}_{\Box}(s^{j})$ iff $t\in\mathcal{R}^{\mathsf{fut}}_{\Box}(s)$ = $\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(s)$. By assumption then, $u^{j}_{m}\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(u^{j}_{k})=\mathcal{R}^{\mathsf{fut}}_{i}(u^{j}_{k})$ for all $k,m\in\{1,...,n\}$ and each $i\in Ag$. Hence, $u^{j}_{m}\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{fut}}_{i}(u^{j}_{k})$ for all $k,m\in\{1,...,n\}$. If we therefore pick any $u^{j}_{k}$, it follows that $u^{j}_{k}\in\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{fut}}_{i}(u^{j}_{i})$, meaning that the intersection $\bigcap_{1\leq i\leq n}\mathcal{R}^{\mathsf{Ldm}}_{i}(u^{j}_{i})$ is non-empty.

• (C3)

Follows by definition.

• •

$\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$ is a transitive and serial by definition, and $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{H}}$ is the converse of $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$ by definition as well.

• (C4)

For all $u^{j},u^{k},u^{l}\in W^{\mathsf{Ldm}}$, suppose that $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}u^{j}u^{k}$ and $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}u^{j}u^{l}$. Then, $j<k$ and $j<l$, and since $\mathbb{N}$ is linearly ordered, we have that $k<l$, $k=l$, or $k>l$, implying that $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}u^{k}u^{l}$, $u^{k}=u^{l}$, or $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}u^{l}u^{k}$.

• (C5)

Similar to previous case.

• (C6)

Suppose that $(u^{j},v^{j+k})\in\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}\circ\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ with $k\geq 1$. By definition of $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$, $u^{j+k}$ is the only element in $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}(u^{j})$ associated with $j+k$, and so, $(u^{j+k},v^{j+k})\in\mathcal{R}^{\mathsf{Ldm}}_{\Box}$ (By lemma 2 no other $u^{j+k^{\prime}}$ with $k^{\prime}\neq k$ can relate to $v^{j+k}$ in $\mathcal{R}^{\mathsf{Ldm}}_{\Box}$.). Since $k\geq 1$, $v^{j+k}\in\mathcal{R}^{\mathsf{Ldm}}_{\Box}(u^{j+k})$ iff $v\in\mathcal{R}^{\mathsf{fut}}_{\Box}(u)=\bigcap_{i\in Ag}\mathcal{R}^{\mathsf{pres}}_{i}(u)$ iff $v^{0}\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}(u^{0})$. By lemma 3, $(u^{j},v^{j})\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}$. This implies that, and since $(v^{j},v^{j+k})\in\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$ by definition, we have that $(u^{j},v^{j+k})\in\mathcal{R}^{\mathsf{Ldm}}_{Ag}\circ\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$.

• (C7)

Follows from the definition of the $\mathcal{R}^{\mathsf{Ldm}}_{\mathsf{G}}$ relation.

• •

Last, it is easy to see that the valuation function $V^{\mathsf{Ldm}}$ is indeed a valuation function.

Lemma 7 (Truth-Lemma)

For any formula $\phi$, $M^{\mathsf{Ldm}},w^{0}\models\phi$ iff $\phi\in w^{0}$.

Proof

Shown by induction on the complexity of $\phi$ (See [3]).

Appendix 0.B $\mathsf{G3Xstit}$ Derivation of IOAx Axiom

We make use of the system of rules $(\mathsf{IOA_{X}})$, to derive the $\mathsf{Xstit}$ IOA axiom in $\mathsf{G3Xstit}$.

[TABLE]

[TABLE]

[TABLE]