# Set Reconstruction on the Hypercube

Luke Pebody

###### Abstract.

Given an action of a group $G$ on a set $S$, the $k$-deck of a subset $T$ of
$S$ is the multiset of all subsets of $T$ of size $k$, each given up to
translation by $G$.

For a given subset $T$, the reconstruction number of $T$ is the minimum $k$
such that the $k$-deck uniquely identifies $T$ up to translation by $G$, and
the reconstruction number of the action $G:S$ is the maximum reconstruction
number of any subset of $S$.

The concept of reconstruction number extends naturally to multisubsets $T$ of
$S$ and in [2], the author calculated the multiset-reconstruction number of
all finite abelian groups. In particular, it was shown that the multiset-
reconstruction number of $\mathbb{Z}_{2}^{n}$ was $n+1$. This provides an
upper bound of $n+1$ to the reconstruction number of $\mathbb{Z}_{2}^{n}$. The
author also showed a lower bound of $\lfloor\frac{n+1}{2}\rfloor$ in the same
paper.

The purpose of this note is to close the gap. The reconstruction number of
$\mathbb{Z}_{2}^{n}$ is

$\lfloor n+1-\log_{2}(n+1-\log_{2}(n))\rfloor.$

##  1\. Introduction and Definitions

Given a set $S$ and non-negative integer $k$, denote by $S^{(k)}$ the set of
subsets of $S$ of size $k$. Given an action on a group $G$ of a set $S$, the
$k$-deck of a subset $T$ is the multiset of all subsets of $T$ of size $k$,
each given up to translation by $G$:

$\mathrm{deck}_{k}(G)=\\{\\{gU:g\in G\\}:U\in T^{(k)}\\}.$

Say that subsets $T_{1}$ and $T_{2}$ are $k$-indistinguishable if
$\mathrm{deck}_{i}(T_{1})=\mathrm{deck}_{i}(T_{2})$ for all $i\leq k$ and
$k$-distinguishable otherwise. In particular, for any subset $T$ of $G$, any
element $g$ of $G$ and any integer $k$, $gT$ and $T$ are $k$-indistinguishable
and sets $T_{1}$ and $T_{2}$ are $k$-indistinguishable if and only for all
$i\leq k$, there is a bijection $\phi_{i}:T_{1}^{(i)}\to T_{2}^{(i)}$ such
that for all $U\in T_{1}^{(i)}$ there exists a $g$ such that $\phi_{i}U=gU$.

For subsets $T_{1}$ and $T_{2}$ say that the distinguishing number of $T_{1}$
and $T_{2}$, denoted by $d_{G:S}(T_{1},T_{2})$, is the smallest number $k$
such that $T_{1}$ and $T_{2}$ are $k$-distinguishable. If there is no such $k$
(and so $T_{1}$ and $T_{2}$ are translates), the distinguishing number is
$\infty$.

For a subset $T$ of $S$, say that the reconstruction number $r_{G:S}(T)$ is
the smallest number $k$ such that for any subset $U$ of $S$, if $T$ and $U$
are $k$\- indistinguishable then $U$ is a translate $gT$ of $T$, and the
reconstruction number $r(G:S)$ is the maximum value of $r_{G:S}(T)$ for any
subset $T\subseteq S$.

One can extend the definition of reconstruction from sets to multisets. Let a
multiset from $S$ be a map $\phi:S\to\mathbb{N}$ from $S$ to the non-negative
integers $\mathbb{N}$, and then define the $k$-deck of $\phi$ to be the map
$\mathrm{deck}_{k}\phi:S^{k}\to\mathbb{N}$ defined by

$\mathrm{deck}_{k}(s_{1},s_{2},\ldots,s_{k})=\sum_{g\in
G}\phi(gs_{1})\phi(gs_{2})\ldots\phi(gs_{k}).$

Given this definition of a $k$-deck, we can define $k$-distinguishable and
$k$-indistinguishable as before, and for a multiset $\phi$ from $G$, say that
the multiset reconstruction number $\mathrm{rm}_{G:S}(\phi)$ is the smallest
number $k$ such that for any multiset $\psi$ from $G$, if $\phi$ and $\psi$
are $k$-indistinguishable, then $\psi$ is a translate $g\phi$ (defined by
$g\phi(s)=\phi(g^{-1}s)$) of $\phi$. Finally, define the multiset
reconstruction number $\mathrm{rm}(G:S)$ to be the maximum value of
$\mathrm{rm}_{G:S}(\phi)$ for any multiset $\phi$ from $G$.

One of the first general results in this area was in [1], where the authors
showed that the reconstruction number of a group action $r(G:S)$ was bounded
above by $\log_{2}(|G|)$.

In this paper we will focus on the action of an abelian group acting on itself
by multiplication. For the specific case of the cyclic group acting on itself
by multiplication, it was proved in [3] that the reconstruction number of
$r(Z_{n})$ was at most equal to 9 times the number of prime factors of $n$ and
was equal to 3 for prime $n$. This was improved upon in [2] where the multiset
reconstruction number was calculated for every abelian group and, thereby, it
was shown that $r(\mathbb{Z}_{n})\leq 6$.

We will focus on the group $\mathbb{Z}_{2}^{n}$ which we will identify both,
where necessary, with the $n$-dimensional vector space over the field of 2
elements and with the power set of the $n$ element set. In [2], it was shown
that the multiset reconstruction number of $\mathbb{Z}_{2}^{n}$ is $n+1$, from
which it follows that $r(\mathbb{Z}_{2}^{n})\leq n+1$. In the same paper, a
lower bound was provided of $\frac{n+1}{2}$. In this paper we will show that
the reconstruction number is equal to $\lfloor
n+1-\log_{2}(n+1-\log_{2}(n))\rfloor.$ This expression may seem a tad
unwieldy, but comes from the following fact.

######  Theorem 1.

For positive integers $n$ and $k$, the statements

$k\leq\lfloor n+1-\log_{2}(n+1-\log_{2}(n))\rfloor$

and

$2^{n+1-k}\geq k$

are equivalent.

###### Proof.

Let us suppose that $t$ is the unique non-negative integer that $2^{t}+t\leq
n<2^{t+1}+t+1$. Then if we set $k=n-t$, we see that $2^{n+1-k}=2^{t+1}\geq
n-t=k$, but if we set $k=n+1-t$, we see that $2^{n+1-k}=2^{t}<n+1-t=k+1$.
Since $2^{n+1-k}$ is decreasing in $k$, it follows that $2^{n+1-k}\geq k$ if
and only if $k\leq n-t$.

Further, if $2^{t}+t\leq n<2^{t+1}$, then $\log_{2}(n)$ is between $t$ and
$t+1$, so $n+1-\log_{2}(n)$ is between $2^{t}$ and $2^{t+1}$. Similarly, if
$2^{t+1}\leq n<2^{t+1}+t+1$, then $\log_{2}(n)$ is between $t+1$ and $t+2$, so
$n+1-\log_{2}(n)$ is between $2^{t}$ and $2^{t+1}$.

It follows that $\lfloor n+1-\log_{2}(n+1-\log_{2}(n))\rfloor=n-t$. ∎

In Section 2, we will show that if $2^{n+1-k}\geq k$ then the reconstruction
number of $\mathbb{Z}_{2}^{n}$ is at least $k$, and in Sections 3 and 4, we
will show the converse.

##  2\. Lower Bound

To prove our lower bound, we provide a method for creating sets which are not
easily distinguishable.

######  Theorem 2.

Suppose that $G$ contains a subgroup $H$, and that set $A$ is the union of
sets $A_{1},\ldots,A_{k}$ such that for each $i$, $A_{i}$ is contained in a
distinct coset $g_{i}H$ of $H$.

Suppose likewise that set $B$ is the union of sets $B_{1},\ldots,B_{k}$ such
that for each $i$, $B_{i}$ is contained in a distinct coset $g^{\prime}_{i}H$
of $H$.

Suppose finally that for each $1\leq i\leq k$, $A\setminus A_{i}$ and
$B\setminus B_{i}$ are translates. Then $A$ and $B$ are not
$k-1$-distinguishable.

###### Proof.

Let $g_{1},g_{2},\ldots,g_{i}$ (with $i<k$) be elements of $G$, and for set
$S\subseteq G$ denote by $f(S)$ the number of elements $g$ of $G$ for which
$gg_{1},gg_{2},\ldots,gg_{i}\in S$.

Let $t$ be the number of distinct cosets of $H$ in which
$g_{1},g_{2},\ldots,g_{i}$ lie. Note that $t\leq i<k$. Then for any $g$,
$gg_{1},gg_{2},\ldots,gg_{i}$ lie in $t$ cosets of $H$. Therefore each version
$gg_{1},gg_{2},\ldots,gg_{i}$ contained in $A$ is contained in exactly $k-t$
of the sets $A\setminus A_{j}$.

Thus $(k-t)f(A)=\sum_{i}f(A\setminus A_{i})=\sum_{i}f(B\setminus
B_{i})=(k-t)f(B)$ and hence $f(A)=f(B)$.

Since this is true for all $g_{1},g_{2},\ldots,g_{i}$ with $i\leq k$, it
follows that $A$ and $B$ are not $(k-1)$-distinguishable. ∎

Now we show how to find sets satisfying the properties of Theorem 2

######  Corollary 3.

For positive integer $k\geq 3$, suppose that abelian group $G$ contains a
subgroup $H$ of index at least $k$. Suppose also that subgroup $H$ has $k$
cosets of subgroups $h_{i}H_{i}$ such that the intersection of the cosets is
empty:

$\bigcap\limits_{i}h_{i}H_{i}=\emptyset,$

and all of the smaller intersections are not empty:

$\forall j\bigcap\limits_{i\neq j}h_{i}H_{i}\neq\emptyset.$

Then the reconstruction number of $G$ is at least $k$.

###### Proof.

Since $\bigcap\limits_{i}h_{i}H_{i}$ is different from $\bigcap\limits_{i\neq
j}h_{i}H_{i}$ for all $j$, it follows that the cosets $h_{i}H_{i}$ are
distinct. Further, since for all pairs $i,j$, $h_{i}H_{i}\cap
h_{j}H_{j}\neq\emptyset$, it follows that the subgroups $H_{i}$ and $H_{j}$
are distinct.

Choose $k$ distinct cosets $g_{1}H,g_{2}H,\ldots,g_{k}H$ of $H$ in $G$, and
then for $1\leq i\leq k$, let $A_{i}=g_{i}H_{i}$ and let
$B_{i}=g_{i}h_{i}H_{i}$. Finally let $A$ be the disjoint union of the $A_{i}$
and $B$ be the disjoint union of the $B_{i}$.

Choose $1\leq i\leq k$, and let $x$ be any element of $\bigcap\limits_{j\neq
i}h_{j}H_{j}$. Then for all $j\neq i$,
$xA_{j}=xg_{j}H_{j}=g_{j}xH_{j}=g_{j}h_{j}H_{j}=B_{j}$, and so $x(A\setminus
A_{i})=\bigcup_{j\neq i}xA_{j}=\bigcup_{j\neq i}B_{j}=B\setminus B_{i}.$

Thus the sets $A_{i}$ and $B_{i}$ satisfy the condition of Theorem 2, and
hence $A$ and $B$ are not $k-1$-distinguishable. Further, we will show that
$A$ and $B$ are not translates.

Suppose otherwise, then there exists $g\in G$ such that $gA=B$. Since cosets
of $H$ are preserved by the map $x\to gx$, it follows that this map must map
each $A_{i}$ to some $B_{j}$. However, if $i\neq j$ then $A_{i}$ and $B_{j}$
are cosets of different subgroups $H_{i}$ and $H_{j}$ which means one cannot
be mapped to the other.

Thus for each $i$, it follows that $gg_{i}H_{i}=g_{i}h_{i}H_{i}$, from which
it follows (since $G$ is abelian) that $g\in h_{i}H_{i}$ for all $i$. This is
a contradiction, as

$\bigcap\limits_{i}h_{i}H_{i}=\emptyset.$

It follows that $A$ and $B$ are not $k-1$-distinguishable, and are not
translates, so $G$ must have reconstruction number of at least $k$. ∎

To conclude we will show the existence of cosets with this intersection
property.

######  Lemma 4.

The hypercube $\mathbb{Z}_{2}^{k-1}$ contains $k$ cosets of subgroups with
empty intersection, such that the intersection of any $k-1$ of them is not
empty.

###### Proof.

Representing the elements of $\mathbb{Z}_{2}^{k-1}$ as sequences
$(x_{1},x_{2},\ldots,x_{k-1})$ of elements of $\mathbb{Z}_{2}$, we can take
our $k$ cosets $x_{1}=0$, $x_{1}=x_{2}$, $x_{2}=x_{3}$, …, $x_{k-2}=x_{k-1}$
and $x_{k-1}=1$.

Clearly no vector satisfies all of these conditions, but if you remove any one
condition, they can be satisfied. ∎

This concludes the work for the lower bound.

######  Corollary 5.

If positive integers $n,k$ have $2^{n+1-k}\geq k$ then the reconstruction
number of $\mathbb{Z}_{2}^{n}$ is at least $k$.

###### Proof.

For $k\geq 3$, this follows directly from Corollary 3 and Lemma 4.
$\mathbb{Z}_{2}^{k-1}$ is a subset of $\mathbb{Z}_{2}^{n}$ of index
$2^{n+1-k}$, so if this is at least $k$, the conditions of Lemma 4 apply.

For $k=1$ and $k=2$, the conditions are that $2^{n-1}\geq 1$ and $2^{n-2}\geq
2$, which are both equivalent to $n\geq 2$.

For $n\geq 2$ and for any two non-zero elements $a,b$ of $\mathbb{Z}_{n}^{2}$
the sets $\\{0,a\\}$ and $\\{0,b\\}$ are non-translates that are not
1-distinguishable so $\mathbb{Z}_{n}^{2}$ has reconstruction number at least
2. ∎

##  3\. The Fourier Transform

Given elements $x=(x_{1},x_{2},\ldots,x_{n})$ and
$y=(y_{1},y_{2},\ldots,y_{n})$ of $\mathbb{Z}_{2}^{n}$, define
$<x,y>=(-1)^{x_{1}y_{1}+x_{2}y_{2}+\ldots+x_{n}y_{n}}$. Then, given a mapping
$f:\mathbb{Z}_{2}^{n}\to\mathbb{Z}$ the Fourier transform
$\hat{f}:\mathbb{Z}_{2}^{n}\to\mathbb{Z}$ is defined by
$\hat{f}(x)=\sum_{y\in\mathbb{Z}_{2}^{n}}f(y)<x,y>$.

It is a well-known property of the Fourier Transform (which we will use in the
proof of Theorem 10) that applying the Fourier Transform twice just multiplies
the original map by the size of the group: $\hat{\hat{f}}(x)=2^{n}f(x)$.

Given a multiset $f$ from $\mathbb{Z}_{2}^{n}$ and a linear map
$\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{k}$, denote by $\theta f$ the
multiset from $\mathbb{Z}_{2}^{k}$ defined by

$\theta f(x)=\sum_{z:\theta z=x}f(z).$

For every linear map $\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{k}$, there
is a dual map $\theta^{*}:\mathbb{Z}_{2}^{k}\to\mathbb{Z}_{2}^{n}$ with the
property that for every $x\in\mathbb{Z}_{2}^{n}$ and $y\in\mathbb{Z}_{2}^{k}$,
$<\theta x,y>=<x,\theta^{*}y>$. The dual map gives a clean description of the
Fourier transform of linear images of multisets.

######  Lemma 6.

Given a multiset $f$ from $\mathbb{Z}_{2}^{n}$ and a linear map
$\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{k}$ with dual $\theta^{*}$, the
Fourier transform of the image $\theta f$ is given by

$\hat{\theta f}(x)=\hat{f}\theta^{*}x.$

###### Proof.

$\displaystyle\hat{\theta f}(x)$
$\displaystyle=\sum_{y\in\mathbb{Z}_{2}^{k}}\theta f(y)<x,y>$
$\displaystyle=\sum_{y\in\mathbb{Z}_{2}^{k}}\sum_{z:\theta z=y}f(z)<x,y>$
$\displaystyle=\sum_{z\in\mathbb{Z}_{2}^{n}}f(z)<x,\theta z>$
$\displaystyle=\sum_{z\in\mathbb{Z}_{2}^{n}}f(z)<\theta^{*}x,z>$
$\displaystyle=\hat{f}\theta^{*}x.$

∎

There is a similar easy to describe effect of translation on the Fourier
Transform.

######  Lemma 7.

Given a multiset $f$ from $\mathbb{Z}_{2}^{n}$ and an element
$z\in\mathbb{Z}_{2}^{n}$, the Fourier transform of the translate $z+f$ is
given by

$\hat{(z+f)}x=\hat{f}x<x,z>.$

###### Proof.

$\displaystyle\hat{(z+f)}x$
$\displaystyle=\sum_{y\in\mathbb{Z}_{2}^{n}}(z+f)(y)<x,y>$
$\displaystyle=\sum_{y\in\mathbb{Z}_{2}^{n}}f(z+y)<x,y>$
$\displaystyle=\sum_{y^{\prime}\in\mathbb{Z}_{2}^{n}}f(y^{\prime})<x,z+y^{\prime}>$
$\displaystyle=\sum_{y^{\prime}\in\mathbb{Z}_{2}^{n}}f(y^{\prime})<x,z><x,y^{\prime}>$
$\displaystyle=<x,z>\sum_{y^{\prime}\in\mathbb{Z}_{2}^{n}}f(y^{\prime})<x,y^{\prime}>$
$\displaystyle=<x,z>\hat{f}x.$

∎

It is proved in [2] that the reconstruction number of a given multiset can be
described in terms of the Fourier transform.

######  Theorem 8.

The $k$-deck of $f$ gives exactly the same information as knowing all values
$\prod_{i=1}^{k}\hat{f}(x_{i})$ for all sequences $(x_{1},x_{2},\ldots,x_{k})$
with $x_{1}+x_{2}+\ldots+x_{k}=0$.

We can use this to show the effect of linear maps on distinguishability.

######  Theorem 9.

For any multisets $f,g$ on $\mathbb{Z}_{2}^{n}$ and integer $k\geq 2$:

  1. (1)

If $f$ and $g$ are $k$-indistinguishable then for any linear map $\theta$ from
$\mathbb{Z}_{2}^{n}$ to any target space, $\theta f$ and $\theta g$ are
$k$-indistinguishable.

  2. (2)

If $f$ and $g$ are $k$-distinguishable, then there exists a linear map
$\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{k-1}$ such that $\theta f$ and
$\theta g$ are $k$-distinguishable.

###### Proof.

By Theorem 8, $f$ and $g$ being $k$-indistinguishable is equivalent to

$\hat{f}(x_{1})\ldots\hat{f}(x_{i})=\hat{g}(x_{1})\ldots\hat{g}(x_{i})$

for all sequences $x_{1},\ldots,x_{i}$ with $i\leq k$ and
$x_{1}+\ldots+x_{i}=0$.

Suppose $f$ and $g$ are $k$-indistinguishable, and let
$\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{p}$ be any linear map. Then by
Lemma 6, for any sequence $x_{1},\ldots,x_{i}\in\mathbb{Z}_{2}^{p}$ with
$i\leq k$ and $x_{1}+\ldots+x_{i}=0$,

$\displaystyle\hat{\theta f}(x_{1})\ldots\hat{\theta f}(x_{i})$
$\displaystyle=\hat{f}(\theta^{*}x_{1})\ldots\hat{f}(\theta^{*}x_{i})$
$\displaystyle=\hat{g}(\theta^{*}x_{1})\ldots\hat{g}(\theta^{*}x_{i})$
$\displaystyle=\hat{\theta g}(x_{1})\ldots\hat{\theta g}(x_{i}),$

so $\theta f$ and $\theta g$ are $k$-indistinguishable.

Similarly, for $k$-distinguishable $f$ and $g$, there exists a sequence
$x_{1},\ldots,x_{i}$ with $i\leq k$, $x_{1}+\ldots+x_{i}=0$ and

$\hat{f}(x_{1})\ldots\hat{f}(x_{i})\neq\hat{g}(x_{1})\ldots\hat{g}(x_{i}).$

Then define map $\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{k-1}$ in terms of
its duel by $\theta^{*}e_{j}=x_{j}$ for $j<i$ and $\theta^{*}e_{j}=0$ for
$j\geq i$. Note that $\theta^{*}(e_{1}+\ldots+e_{i-1})=x_{i}$.

Thus if we let $y_{j}=e_{j}$ for $j<i$ and $y_{i}=e_{1}+\ldots+e_{i-1}$, then
$y_{1},\ldots,y_{i}$ are a sequence with $i\leq k$, $y_{1}+\ldots+y_{i}=0$ and

$\hat{\theta f}(y_{1})\ldots\hat{\theta f}(y_{i})\neq\hat{\theta
g}(y_{1})\ldots\hat{\theta g}(y_{i}),$

so $\theta f$ and $\theta g$ are $k$-distinguishable. ∎

##  4\. Structure of maximally indistinguishable multisets on
$\mathbb{Z}_{2}^{k-1}$

For this section, we will investigate the nature of multisets from
$\mathbb{Z}_{2}^{k-1}$ which have distinguishing number $k$. We will give
concrete examples of such multisets now.

For distinct non-negative integers $a,b$ and positive integers
$a_{1},\ldots,a_{k-1}$, denote by $f_{(a,b),(a_{1},\ldots,a_{k-1})}$ the
multiset defined by

$f((x_{1},x_{2},\ldots,x_{k-1}))=\begin{cases}a+\sum a_{i}x_{i}\textrm{ if
}\sum x_{i}\textrm{ is even}\\\ b+\sum a_{i}x_{i}\textrm{ if }\sum
x_{i}\textrm{ is odd}\\\ \end{cases}$

We note that the Fourier Transform of $f_{(a,b),(a_{1},\ldots,a_{k-1})}$ takes
a particularly simple form. Since the all-ones vector
$e_{1}+e_{2}+\ldots+e_{k-1}$ will come up quite a lot this section, denote it
by $h$.

######  Theorem 10.

The Fourier Transform of $f_{(a,b),(a_{1},\ldots,a_{k-1})}$ is given by

$\hat{f}_{(a,b),(a_{1},\ldots,a_{k-1})}(x)=\begin{cases}2^{k-2}(a+b+\sum
a_{i})\textrm{ if }x=0\\\ 2^{k-2}a_{i}\textrm{ if }x=e_{i}\\\
2^{k-2}(a-b)\textrm{ if }x=h\\\ 0\textrm{ otherwise }\end{cases}$

###### Proof.

Let $g:\mathbb{Z}_{2}^{k-1}\to\mathbb{Z}$ denote the right hand side of the
equation in the statement. Then for any $x\in\mathbb{Z}_{2}^{k-1}$

$\displaystyle\hat{g}(x)$
$\displaystyle=\sum_{y\in\mathbb{Z}_{2}^{k-1}}f(y)<x,y>$
$\displaystyle=2^{n-2}((a+b+\sum
a_{i})<x,0>+\sum_{i}a_{i}<x,e_{i}>+(a-b)<x,h>).$

Now for all $x$, $<x,0>=1$, $1+<x,e_{i}>=2x_{i}$ and $<x,h>$ is 1 if
$\sum_{i}x_{i}$ is even and -1 if $\sum_{i}x_{i}$ is odd. It follows that

$\displaystyle\hat{g}(x)$ $\displaystyle=\begin{cases}2^{k-1}(a+\sum
a_{i}x_{i})\textrm{ if }\sum x_{i}\textrm{ is even}\\\ 2^{k-1}(b+\sum
a_{i}x_{i})\textrm{ if }\sum x_{i}\textrm{ is odd}\\\ \end{cases}$
$\displaystyle=2^{n-1}f(x)$

Then $g$ has the same fourier transform has $\hat{f}$ and so must be equal to
$\hat{f}$. ∎

Then it follows that $f_{(a,b),(a_{1},\ldots,a_{k-1})}$ has a twin from which
it has high distinguishing number.

######  Corollary 11.

For distinct non-negative integers $a,b$ and positive integers
$a_{1},\ldots,a_{k-1}$, the multisets $f_{(a,b),(a_{1},\ldots,a_{k-1})}$ and
$f_{(b,a),(a_{1},\ldots,a_{k-1})}$ have distinguishing number $k$.

###### Proof.

By Theorem 10, the fourier transforms
$g_{1}=\hat{f}_{(a,b),{a_{1},\ldots,a_{k-1}})}$ and
$g_{2}=\hat{f}_{(b,a),{b_{1},\ldots,b_{k-1}})}$ have identical support
$\\{0,e_{1},e_{2},\ldots,e_{k-1},h\\}$ and are equal except at $x=h$ for which
we have $g_{1}(-x)=g_{2}(-x)$.

By Theorem 8, the distinguishing number of the two multisets is equal to the
length of the minimum 0-sum sequence $x_{1},\ldots,x_{t}$ for which

$g_{1}(x_{1})\ldots g_{1}(x_{t})\neq g_{2}(x_{1})\ldots g_{2}(x_{t}).$

Clearly any such sequence must contain $h$ an odd number of times, leaving a
1-coordinate in each location that must be made up by a copy of $e_{i}$. Thus
the shortest such sequence has length $k$ and is
$e_{1}+e_{2}+\ldots+e_{k-1}+h=0$. ∎

We will show that up to translation and linear maps on $\mathbb{Z}_{2}^{k-1}$,
these are the only pairs of multisets of distinguishing number $k$. Say that
two multisets $f_{1}$ and $f_{2}$ from $\mathbb{Z}_{2}^{k-1}$ of
distinguishing number $k$ are in standard position if

$\hat{f}_{1}e_{1}\ldots\hat{f}_{1}e_{k-1}\hat{f}_{1}7\neq\hat{f}_{2}e_{1}\ldots\hat{f}_{2}e_{k-1}\hat{f}_{2}h.$

######  Theorem 12.

For $k\geq 3$, if $f_{1}$ and $f_{2}$ are two multisets on
$\mathbb{Z}_{2}^{k-1}$ of distinguishing number $k$, then there exists a
bijective group homomorphism
$\theta:\mathbb{Z}_{2}^{k-1}\to\mathbb{Z}_{2}^{k-1}$ such that $\theta f_{1}$
and $\theta f_{2}$ are in standard position.

###### Proof.

By Theorem 8, there is a 0-sum sequence of length $k$, $x_{1},\ldots,x_{k}$
for which

$\hat{f}_{1}(x_{1})\ldots\hat{f}_{1}(x_{k})\neq\hat{f}_{2}(x_{1})\ldots\hat{f}_{2}(x_{k}),$

and there is no shorter such sequence.

In particular this means that $x_{1},\ldots,x_{k}$ cannot be split into two
shorter 0-sum sequences (for they would both have equal sums), so
$x_{1},\ldots,x_{k-1}$ must be linearly independent and therefore must span
$\mathbb{Z}_{2}^{k-1}$. As such there is a bijective group homomorphism
$\theta:\mathbb{Z}_{2}^{k-1}\to\mathbb{Z}_{2}^{k-1}$ for which
$\theta^{*}e_{i}=x_{i}$ for all $1\leq i\leq k-1$.

Then by Lemma 6, if we denote $\theta f_{1}$ and $\theta f_{2}$ by $g_{1}$ and
$g_{2}$, we have

$\hat{g}_{1}(e_{1})\ldots\hat{g}_{1}(e_{k-1})\hat{g}_{1}(h)\neq\hat{g}_{2}(e_{1})\ldots\hat{g}_{2}(e_{k-1})\hat{g}_{2}(h),$

and there is no shorter such sequence. ∎

######  Theorem 13.

For $k\geq 3$, if $f_{1}$ and $f_{2}$ are two multisets on
$\mathbb{Z}_{2}^{k-1}$ of distinguishing number $k$ in standard position, then
there exist distinct non-negative integers $a,b$ , positive integers
$a_{1},\ldots,a_{k-1}$ and elements $x_{1},x_{2}\in\mathbb{Z}_{2}^{k-1}$ such
that

$\displaystyle x_{1}+f_{1}$ $\displaystyle=f_{(a,b),(a_{1},\ldots,a_{k-1})}$
$\displaystyle x_{2}+f_{2}$ $\displaystyle=f_{(b,a),(a_{1},\ldots,b_{k-1})}$

###### Proof.

We know that

$\hat{f}_{1}(e_{1})\ldots\hat{f}_{1}(e_{k-1})\hat{g}_{1}(h)\neq\hat{f}_{2}(e_{1})\ldots\hat{f}_{2}(e_{k-1})\hat{g}_{2}(h),$

and there is no shorter such sequence. In particular, note that for all
$x\in\mathbb{Z}_{2}^{k-1}$, $x+x=0$ is a shorter sequence, so
$\hat{g}_{1}(x)^{2}=\hat{g}_{2}(x)^{2}$.

Now let $x$ be any element of $\mathbb{Z}_{2}^{k-1}$ other than
$\\{0,e_{1},e_{2},\ldots,e_{k-1},h\\}$, and let $I=\\{i:1\leq i\leq
k-1,x_{i}=1\\}$ be the set of 1 coordinates of $x$. Note that by the choice of
$x$, $2\leq p\leq k-2$. As such, it follows that $\\{e_{i}:i\in
I\\}\cup\\{x\\}$ and $\\{e_{i}:i\notin I\\}\cup\\{h,x\\}$ are both 0-sum
subsets of length at most $k-1$, and so it follows that

$\displaystyle\prod_{i\in I}\hat{g}_{1}(e_{i})\hat{g}_{1}(x)$
$\displaystyle=\prod_{i\in I}\hat{g}_{2}(e_{i})\hat{g}_{2}(x)\textrm{ and }$
$\displaystyle\prod_{i\notin I}\hat{g}_{1}(e_{i})\hat{g}_{1}(h)\hat{g}_{1}(x)$
$\displaystyle=\prod_{i\notin
I}\hat{g}_{2}(e_{i})\hat{g}_{2}(h)\hat{g}_{2}(x).$

Multiplying these together we get

$\prod_{i}\hat{g}_{1}(e_{i})\hat{g}_{1}(h)\hat{g}_{1}(x)^{2}=\prod_{i}\hat{g}_{1}(e_{i})\hat{g}_{2}(h)\hat{g}_{2}(x)^{2}.$

Since we know that $\hat{g}_{1}(x)^{2}=\hat{g}_{2}(x)^{2}$ and

$\hat{g}_{1}(e_{1})\ldots\hat{g}_{1}(e_{k-1})\hat{g}_{1}(h)\neq\hat{g}_{2}(e_{1})\ldots\hat{g}_{2}(e_{k-1})\hat{g}_{2}(h),$

it follows that $\hat{g}_{1}(x)=\hat{g}_{2}(x)=0.$

To summarize, $\hat{g}_{1}$ and $\hat{g}_{2}$ have no support outside of
$\\{0,e_{1},\ldots,e_{k-1},h\\}$, we have
$\hat{g}_{1}(x)^{2}=\hat{g}_{2}(x)^{2}$ for all $x$ and

$\hat{g}_{1}(e_{1})\ldots\hat{g}_{1}(e_{k-1})\hat{g}_{1}(h)\neq\hat{g}_{2}(e_{1})\ldots\hat{g}_{2}(e_{k-1})\hat{g}_{2}(h).$

Now let $x_{1}=\sum_{\hat{g}_{1}e_{i}<0}e_{i}$ and
$x_{2}=\sum_{\hat{g}_{2}e_{i}<0}$. Then for all $i$, $\hat{g_{1}+x_{1}}e_{i}$
and $\hat{g_{1}+x_{2}}e_{i}$ are positive numbers with the same square, and so
are equal.

Thus $\hat{g_{1}+x_{1}}$ and $\hat{g_{2}+x_{2}}$ are of the form given in
Theorem 10 except that we have not shown that $a,b$ are necessarily non-
negative, or that any of $a,b,a_{1},\ldots,a_{k-1}$ are necessarily integers.

To that end, note that $a=g_{1}+x_{1}(0)$, $b=g_{2}+x_{2}(0)$ (and so they are
indeed non-negative integers), and $a_{i}=g_{1}+x_{1}(e_{i})-g_{2}+x_{2}(0)$,
so is integral. ∎

It follows that if we have $k$-distinguishable multisets, some element must
appear $k$ times.

######  Theorem 14.

For integers $k\geq 2$, if multisets $f$ and $g$ on $\mathbb{Z}_{2}^{k-1}$
have distinguishing number $k$, some element appears with multiplicity at
least $k$ in $f$ or $g$.

###### Proof.

By Theorem 13, $f$ and $g$ are translates of a linear image of some pair
$f_{(a,b),(a_{1},\ldots,a_{k-1})}$ and $f_{(b,a),(b_{1},\ldots,b_{k-1})}$. The
multiplicity of $h$ in these two multisets is $a+a_{1}+\ldots+a_{k-1}$ and
$b+a_{1}+\ldots+a_{k-1}$. Since each $a_{i}$ is a positive integer, and $a$
and $b$ are distinct non-negative integers, one of these numbers is at least
$k$. ∎

This now allows us to prove our upper bound.

######  Corollary 15.

For positive integers $n$ and $k$, if the reconstruction number of
$\mathbb{Z}_{2}^{n}$ is at least $k$, then $2^{n+1-k}\geq k$.

###### Proof.

Suppose that the reconstruction number of $\mathbb{Z}_{2}^{n}$ is $t\geq k$.
Then there exists two sets $S_{1},S_{2}\subseteq\mathbb{Z}_{2}^{n}$ that are
$t$-distinguishable, but not $t-1$-distinguishable.

Then by Theorem 9, there exists a map
$\theta:\mathbb{Z}_{2}^{n}\to\mathbb{Z}_{2}^{t-1}$ such that the multisets
$\theta S_{1},\theta S_{2}$ from $\mathbb{Z}_{2}^{t-1}$ are
$t$-distinguishable, but not $t-1$-distinguishable.

Finally, by Theorem 14, there must be some element of $\mathbb{Z}_{2}^{t-1}$
that appears in $\theta S_{1}$ or $\theta S_{2}$ at least $t$ times. Since
each element of $\mathbb{Z}_{2}^{t-1}$ only has $2^{n+1-t}$ inverse images, it
follows that $2^{n+1-t}\geq t$.

Since $t\geq k$, we must have $2^{n+1-k}\geq 2^{n+1-t}\geq t\geq k$. ∎

Tying everything together, we now have proved the precise value of the
reconstruction number of the hypercube.

######  Corollary 16.

The reconstruction number of $\mathbb{Z}_{2}^{n}$ is

$\lfloor n+1-\log_{2}(n+1-\log_{2}(n))\rfloor.$

###### Proof.

By Corollaries 5 and 15, the reconstruction number of $\mathbb{Z}_{2}^{n}$ is
the maximum value of $k$ for which if $2^{n+1-k}\geq k$. By Theorem 1, this is
$\lfloor n+1-\log_{2}(n+1-\log_{2}(n))\rfloor.$ ∎

## References

  * [1] NOGA ALON, YAIR CARO, ILIA KRASIKOV, and YEHUDA RODITTY.  Combinatorial reconstruction problems.  Journal of Combinatorial Theory, Series B, 47:153–161, 10 1989\.
  * [2] LUKE PEBODY.  The reconstructibility of finite abelian groups.  Combinatorics, Probability and Computing, 13:867–892, 11 2004.
  * [3] JAMIE RADCLIFFE and ALEX SCOTT.  Reconstructing subsets of $\mathbb{Z}_{n}$.  Journal of Combinatorial Theory, Series A, 83:169–187, 8 1998.


11institutetext: Technical University of Munich, Boltzmannstr. 3, 85748
Garching, Germany 11email<EMAIL_ADDRESS>
# Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set
Theory

Lukas Stevens  0000-0003-0222-6858

###### Abstract

Using Isabelle/HOL, we verify the state-of-the-art decision procedure for
multi-level syllogistic with singleton (MLSS for short), which is a
quantifier-free fragment of set theory. We formalise its syntax and semantics
as well as a sound and complete tableau calculus for it. We also provide an
executable specification of a decision procedure that exhaustively applies the
rules of the calculus and prove its termination. Furthermore, we extend the
calculus with a lightweight type system that paves the way for an integration
of the procedure into Isabelle/HOL.

###### Keywords:

Decision procedures Semantic tableaux Interactive theorem proving Set theory

##  1 Introduction

In Isabelle/HOL, there are specialised procedures for dealing with e.g.
natural numbers, linear arithmetic, and metric spaces. Some of these
procedures have been verified in Isabelle/HOL, such as a procedure for
Presburger arithmetic [12] that was later extended to mixed real-integer
arithmetic [11]. This procedure, though, uses reflection to work on goals in
Isabelle/HOL, which, during execution, either sacrifices speed by going
through the simplifier or requires trusting the code generator. More recently,
Stevens and Nipkow [25] presented a verified decision procedure for orders
that produces certificates. This approach offers efficient execution by using
generated code as well as soundness because the certificates are replayed
through Isabelle’s inference kernel.

This paper focuses on another ubiquitous structure in mathematics, namely
sets. To the best of our knowledge, we present the first formally verified
decision procedure for (a fragment of) set theory. In particular, we consider
a quantifier-free fragment which Cantone and Zarba [9] call multi-level
syllogistic with singleton (MLSS). The fragment includes the usual set
operations of union, intersection, difference, membership, equality and, in
addition, it allows the construction of singleton sets.

Since MLSS admits a tableau calculus, generating certificates will be
straightforward. Like with the aforementioned order solver, this paves the way
for an integration of the decision procedure into Isabelle, adding to its
growing body of verified decision procedures.

###  1.1 Contributions

We present a formalisation in Isabelle/HOL of a tableau calculus for MLSS due
to Cantone and Zarba [9][7, Chapter 14]. We prove soundness and completeness
of the calculus and give an abstract specification of a decision procedure
that exhaustively applies the rules of the calculus. To obtain total
correctness of the procedure, we prove its termination. Additionally, we
naively refine the abstract to an executable specification from which we can
generate code. The formalisation initially follows the paper but offers a more
thorough account of some important details:

  * •

We deliver the omitted proof of Lemma 2 in the paper [9], a key building block
for the completeness proof of the calculus.

  * •

The formal proof of completeness reveals that the calculus lacks a rule for
eliminating double negation.

  * •

We derive an explicit upper bound for the number of formulas in a tableau
branch.

In the context of Isabelle/HOL, there is one crucial aspect that requires us
to modify the calculus in the paper: the calculus works under the assumption
that every variable is a set; however, this is not the case in Isabelle/HOL,
e.g. consider the expression n $\in$ A where n is a natural number. We call
these variables urelements. To deal with them, we extend the calculus with a
lightweight type system and a verified inference algorithm that identifies the
urelements.

The modification of the calculus required non-trivial changes to the
completeness proof. Here, the formalisation was instrumental because Isabelle
immediately revealed which proofs had been broken. This illustrates the
usefulness of ITPs for developing logic calculi: they allow us to confidently
make modifications without compromising correctness.

All in all, the formalisation amounts to over 6000 lines of theory. It is part
of the _Archive of Formal Proofs_ (AFP) [24]. The entry provides an overview
theory MLSS_Proc_All.thy that highlights the (mostly syntactic) differences
between paper and formalisation and references the constants and theorems that
are introduced in this paper.

###  1.2 Related Work

Since the literature on decidable fragments of set theory is vast, we only
focus on MLSS here. Ferro et al. [14] were the first to show the decidability
of the fragment. Subsequent work [6] found the decision problem to be NP-
complete. To obtain a practical decision procedure, Cantone [4] proposed a
tableau calculus, which was later improved by Beckert and Hartmer [1]. Both of
these procedures construct a model during execution that guides the proof
search. Beckert and Hartmer also cover an extension of the calculus with
uninterpreted functions, which Cantone and Zarba [10] later revisited while
avoiding the construction of a model during execution. In this paper, we
consider a version of the latter procedure due to Cantone and Zarba [9] that
is specialised to MLSS and where the branching rules of the calculus are set
up to guarantee the mutual exclusivity of the branches. Later extensions of
the calculus added certain interpreted functions, such as monotone functions
[8] and the inverse of a function [5]. The latter extension notably includes
the Cartesian product. Those extensions, though, did not improve upon the
tableau calculus for MLSS.

There is a large body of work at the intersection of ITPs and tableau methods,
but to keep with this paper’s theme we only consider formalisations of
correctness here. For first-order logic, there are abstract completeness
proofs using the _Beth-Hintikka style_ of possibly infinite derivation trees
[3] as well as the _Henkin style_ of maximally consistent sets [17]. Both are
abstract enough to be instantiated with a wide range of concrete calculi. A
more concrete formalisation [19] verifies a sequent calculus for first-order
logic whose completeness proof is via a translation to semantic tableau.

Beyond completeness, we target decidability, which is more attainable for
propositional logic. There is a verified tableau calculus for the modal logic
S5 [2] in Lean and one for hybrid logic [18] in Isabelle/HOL. Both of these do
not prove termination but there is a formalisation of a tableau calculus for
the temporal logic CTL in Coq [13] that does.

###  1.3 Notation

Isabelle/HOL [21] conforms to everyday mathematical notation for the most
part. We establish notation and in particular some essential data types
together with their primitive operations that are specific to Isabelle/HOL.

We write t :: ’a to specify that the term t has the type ’a and ’a
$\Rightarrow$ ’b for the space of total functions from type ’a to type ’b.

Sets with elements of type ’a have the type ’a set. The cardinality of a set A
is denoted by |A| and the image of A under f by f ‘ A.

We use ’a list to describe the type of lists, which are constructed using the
empty list [] constructor or the infix cons constructor #, and are appended
with the infix operator @. The function set converts a list into a set.

We remark that $\longleftrightarrow$ is equivalent to $=$ on the type of
Booleans bool and $\equiv$ is definitional equality of the meta-logic of
Isabelle/HOL, which is called Isabelle/Pure. Meta-implication is denoted by
$\Longrightarrow$ and a chain of implications A${}_{\text{1}}$
$\Longrightarrow$ $\cdots$ $\Longrightarrow$ A${}_{\text{k}}$
$\Longrightarrow$ C can be abbreviated by $\llbracket$
A${}_{\text{1}}$;$\,\ldots\,$;A${}_{\text{k}}$ $\rrbracket$ $\Longrightarrow$
C.

##  2 Syntax and Semantics of MLSS

###  2.1 Syntax

At the heart of MLSS, we have the type of set terms, which is the disjoint
union of the empty set and variables as well as the operations union,
intersection, difference, and the singleton set represented by the constructor
Single. We keep the type of variables abstract by making it a parameter of the
set term data type. The only restriction on the type of variables is that it
needs to be infinite. Isabelle/HOL’s data type package automatically defines a
function that gives us the set of variables in a set term, which we name vars.
In what follows, we will overload the function vars to also work on set atoms,
formulas, and branches.

⬇

datatype (vars: ’a) pset_term =

$\emptyset$ | Var ’a | Single (’a pset_term)

| ’a pset_term $\sqcup_{\text{s}}$ ’a pset_term

| ’a pset_term $\sqcap_{\text{s}}$ ’a pset_term

| ’a pset_term $-_{\text{s}}$ ’a pset_term

We can combine two set terms to form a set atom by using the membership or the
equality operator.

⬇

datatype (vars: ’a) pset_atom =

’a pset_term $\in_{\text{s}}$ ’a pset_term

| ’a pset_term $=_{\text{s}}$ ’a pset_term

With the above operators we can also represent the subset operator
$\sqsubseteq_{\text{s}}$ and enumerate finite sets: s $\sqsubseteq_{\text{s}}$
t is equivalent to s $\sqcup_{\text{s}}$ t $=_{\text{s}}$ t and a finite set
of elements {t${}_{\text{1}}$,$\ldots$,t${}_{\text{k}}$} can be expressed by
Single t1 $\sqcup_{\text{s}}$ $\ldots$ $\sqcup_{\text{s}}$ Single tk.

We use the propositional fragment of formulas due to Nipkow [20] with set
atoms as propositional atoms to form the quantifier-free fragment MLSS of set
theory.

⬇

datatype (atoms: ’a) fm =

A ’a

| $\boldsymbol{\neg}\>$(’a fm)

| ’a fm $\boldsymbol{\land}$ ’a fm

| ’a fm $\boldsymbol{\lor}$ ’a fm

type_synonym ’a pset_fm = ’a pset_atom fm

We will often drop the atom constructor A to reduce clutter. Additionally, we
use s $\notin_{\text{s}}$ t and s $\neq_{\text{s}}$ t to denote
$\boldsymbol{\neg}\>$A (s $\in_{\text{s}}$ t) and $\boldsymbol{\neg}\>$A (s
$=_{\text{s}}$ t), respectively.

Similarly to vars, we get the function atoms :: ’a fm $\Rightarrow$ ’a set for
free that retrieves all set atoms in a formula. We combine these functions to
extract all the variables occurring in a set formula.

⬇

definition vars $\phi$ $\equiv$ $\bigcup$(vars ‘ atoms $\phi$)

Likewise, we fix the constant subterms :: ’b $\Rightarrow$ ’a pset_term set
that is polymorphic in its argument type ’b. We overload this constant to
return the set terms that are subterms of a set term, set atom, or formula,
respectively. Lastly, we introduce the function subfms :: ’a fm $\Rightarrow$
’a fm set that computes the subformulas of a formula. The functions subterms
and subfms are implemented in the expected way.

###  2.2 Semantics

The original paper [9] bases the semantics of MLSS on the von Neumann
hierarchy of sets $\mathcal{V}$. We instead use the hierarchy of _hereditarily
finite sets_ (HF sets) which fulfil all the same axioms as $\mathcal{V}$ –
that is, the axioms of ZF – except for the axiom of infinity. In particular,
the membership relation is well-founded. The HF sets, as we will see, are
sufficient to construct a model for any satisfiable MLSS formula. In contrast
to $\mathcal{V}$, the HF sets are directly representable in Isabelle/HOL, and
indeed, an AFP entry [23] formalises them. The entry defines a type hf that
comes with the following functionality:

  * •

The function HF :: hf set $\Rightarrow$ set that converts a finite set of HF
sets into an HF set.

  * •

The usual set operations such as equality ($=$), membership
($\boldsymbol{\in}$), union ($\sqcup$), intersection ($\sqcap$), and
difference ($-$) are defined.

  * •

Finally, the empty set coincides with the ordinal $0$, so it is denoted by 0
:: hf.

Equipped with the above, we define the interpretation functions

  * •

I${}_{\text{st}}$ :: (’a $\Rightarrow$ hf) $\Rightarrow$ ’a pset_term
$\Rightarrow$ hf and

  * •

I${}_{\text{sa}}$ :: (’a $\Rightarrow$ hf) $\Rightarrow$ ’a pset_atom
$\Rightarrow$ hf

in the standard way, i.e. by mapping each syntactic construct to the
corresponding operation on HF sets and interpreting variables with respect to
a given valuation function M :: ’a $\Rightarrow$ hf. For the concrete
definition we refer to the formalisation.

We write M $\models$ $\phi$ for the judgement that the formula $\phi$ holds
under the valuation function M. The implementation of $\models$ coincides with
the interpretation function of Nipkow [20]. As usual, we call a formula $\phi$
_satisfiable_ if there exists a model M with M $\models$ $\phi$. Otherwise, we
say that $\phi$ is _unsatisfiable_.

##  3 A Tableau Calculus for MLSS

We formalise the tableau calculus for MLSS as described by Cantone and Zarba
[9]. Inspired by the formalisation of a tableau calculus for hybrid logic by
From [16], we use lists to represent the branches of the tableau tree. Note
that we add formulas to the front of the list during branch expansion, so last
b for a branch b is always the formula we are trying to disprove with the
tableau. We sometimes call this formula the _initial formula_.

⬇

type_synonym ’a branch = ’a pset_fm list

We lift the functions vars and subterms to branches in the expected way.

In the standard tableau calculus for propositional logic as Fitting [15]
describes it, a branch is called _closed_ if it contains both the negation of
a formula and the formula itself; conversely, it is called _open_ if it is not
closed. For MLSS, we extend the notion of closedness with three additional
rules; the first two are straightforward while the last one states that a
branch is closed when the branch contains a membership cycle t${}_{\text{0}}$
$\in_{\text{s}}$ t${}_{\text{1}}$, t${}_{\text{1}}$ $\in_{\text{s}}$
t${}_{\text{2}}$, $\ldots$, t${}_{\text{k}}$ $\in_{\text{s}}$
t${}_{\text{0}}$.

⬇

inductive bclosed :: ’a branch $\Rightarrow$ bool where

$\llbracket$ $\phi$ $\in$ set b; $\boldsymbol{\neg}\>$$\phi$ $\in$ set b
$\rrbracket$ $\Longrightarrow$ bclosed b

| (t $\in_{\text{s}}$ $\emptyset$) $\in$ set b $\Longrightarrow$ bclosed b

| (t $\neq_{\text{s}}$ t) $\in$ set b $\Longrightarrow$ bclosed b

| $\llbracket$ member_cycle cs; set cs $\subseteq$ set b$\rrbracket$
$\Longrightarrow$ bclosed b

abbreviation bopen b $\equiv$ $\neg$ bclosed b

A tableau is called _closed_ if all of its branches are closed.

###  3.1 Linear Expansion Rules

Table 1: Linear expansion rules.table]tab:lexpands All rules except the double negation rule coincide with the original paper [9]. For brevity, we omit the rules for $\sqcap_{\text{s}}$ and $-_{\text{s}}$. Propositional Rules |  | Rules for $\sqcup_{\text{s}}$
---|---|---
|  p $\boldsymbol{\land}$ q |  $\Longrightarrow$ |  p, q
---|---|---
$\boldsymbol{\neg}\>$(p $\boldsymbol{\lor}$ q) |  $\Longrightarrow$ |  $\boldsymbol{\neg}\>$p, $\boldsymbol{\neg}\>$q
p $\boldsymbol{\lor}$ q, $\boldsymbol{\neg}\>$p |  $\Longrightarrow$ |  q
p $\boldsymbol{\lor}$ q, $\boldsymbol{\neg}\>$q |  $\Longrightarrow$ |  p
$\boldsymbol{\neg}\>$(p $\boldsymbol{\land}$ q), p |  $\Longrightarrow$ |  $\boldsymbol{\neg}\>$q
$\boldsymbol{\neg}\>$(p $\boldsymbol{\land}$ q), q |  $\Longrightarrow$ |  $\boldsymbol{\neg}\>$p
$\boldsymbol{\neg}\>$($\boldsymbol{\neg}\>$p) |  $\Longrightarrow$ |  p
|  |  s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$ |  $\Longrightarrow$ |  s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$, s $\notin_{\text{s}}$ $\text{t}_{\text{2}}$
---|---|---
s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ |  $\Longrightarrow$ |  s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$
s $\in_{\text{s}}$ $\text{t}_{\text{2}}$ |  $\Longrightarrow$ |  s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$
s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$
$\text{t}_{\text{2}}$,
s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$ |  $\Longrightarrow$ |  s $\in_{\text{s}}$ $\text{t}_{\text{2}}$
s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$
$\text{t}_{\text{2}}$,
s $\notin_{\text{s}}$ $\text{t}_{\text{2}}$ |  $\Longrightarrow$ |  s $\in_{\text{s}}$ $\text{t}_{\text{1}}$
s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$, s $\notin_{\text{s}}$ $\text{t}_{\text{2}}$ |  $\Longrightarrow$ |  s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$
Rules for $\sqcap_{\text{s}}$ |  | Rules for $-_{\text{s}}$
| $\vdots$
---
|  | $\vdots$
---
Rules for Single |  | Rules for $=_{\text{s}}$
|  |  $\Longrightarrow$ |  s $\in_{\text{s}}$ Single s
---|---|---
s $\in_{\text{s}}$ Single t |  $\Longrightarrow$ |  s $=_{\text{s}}$ t
s $\notin_{\text{s}}$ Single t |  $\Longrightarrow$ |  s $\neq_{\text{s}}$ t
|  |  $\text{t}_{\text{1}}$ $=_{\text{s}}$ $\text{t}_{\text{2}}$, l |  $\Longrightarrow$ |  l{$\text{t}_{\text{2}}$/$\text{t}_{\text{1}}$}
---|---|---
$\text{t}_{\text{1}}$ $=_{\text{s}}$ $\text{t}_{\text{2}}$, l |  $\Longrightarrow$ |  l{$\text{t}_{\text{1}}$/$\text{t}_{\text{2}}$}
s${}_{\text{1}}$ $\in_{\text{s}}$ t, s${}_{\text{2}}$ $\notin_{\text{s}}$ t |  $\Longrightarrow$ |  s${}_{\text{1}}$ $\neq_{\text{s}}$ s${}_{\text{2}}$

The calculus considers two kinds of branch expansion rules: _linear_ and
_branching_ rules. As the name suggests, branching rules lead to the creation
of new branches in the tableau while linear rules only extend a branch b with
new formulas b’ = [$\psi_{1}$,$\ldots$,$\psi_{n}$], which we denote by b’
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b. LABEL:tab:lexpands
shows the linear expansion rules. Note that in the first two rules for
$=_{\text{s}}$, l is a literal occurring in the branch. Furthermore, the term-
for-term substitution l{s/t} is restricted to the top-level set terms of l,
i.e. the set terms that occur directly under one of the atom constructors
$\in_{\text{s}}$ or $=_{\text{s}}$; for example, given the literal

⬇

l = $\boldsymbol{\neg}\>$((s $\sqcup_{\text{s}}$ u) $-_{\text{s}}$ s
$=_{\text{s}}$ s $\sqcup_{\text{s}}$ u)

we have

⬇

= ($\boldsymbol{\neg}\>$((s $\sqcup_{\text{s}}$ u) $-_{\text{s}}$ s
$=_{\text{s}}$ s $\sqcup_{\text{s}}$ u)){t/s $\sqcup_{\text{s}}$ u}

= $\boldsymbol{\neg}\>$((s $\sqcup_{\text{s}}$ u) $-_{\text{s}}$ s
$=_{\text{s}}$ t).

A more crucial restriction of the linear rules is that no new subterm may be
created by their application; for instance, the second rule for
$\sqcup_{\text{s}}$ is

⬇

s $\in_{\text{s}}$ t${}_{\text{1}}$ $\Longrightarrow$ s $\in_{\text{s}}$
t${}_{\text{1}}$ $\sqcup_{\text{s}}$ t${}_{\text{2}}$,

which formally represents

⬇

(s $\in_{\text{s}}$ t${}_{\text{1}}$) $\in$ set b $\Longrightarrow$ [s
$\in_{\text{s}}$ t${}_{\text{1}}$ $\sqcup_{\text{s}}$ t${}_{\text{2}}$]
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b,

and may only be used under the condition t${}_{\text{1}}$ $\sqcup_{\text{s}}$
t${}_{\text{2}}$ $\in$ subterms (last b). The purpose of this restriction is
to prevent unbounded expansion of the branch. In fact, we give an explicit
upper bound for the number of formulas in a branch in Section 7.

Due to boundedness, repeated expansion with linear rules eventually results in
a _linearly saturated_ branch, i.e. a branch where no application of linear
rules would produce new formulas.

⬇

definition lin_sat b $\equiv$ $\forall$b’. b’
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b $\longrightarrow$
set b’ $\subseteq$ set b

Finally, we remark that the original paper [9] is missing the last
propositional rule dealing with double negation. This rule is required for
completeness, though, considering that the branch
[$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$p, p,
$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$p
$\boldsymbol{\land}$ p] is saturated — neither linear nor branching rules
apply — and open, but there clearly is no model for the initial formula
$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$$\boldsymbol{\neg}\>$p
$\boldsymbol{\land}$ p.

###  3.2 Branching Rules

Table 2: Branching expansion rules.table]tab:bexpands We write $\phi$ for last b here. All rules coincide with the original paper [9] so we only show an illustrative subset. Rule |  Precondition |  Subsumption condition
---|---|---
p $\boldsymbol{\neg}\>$p |  p $\boldsymbol{\lor}$ q $\in$ set b |  p $\in$ set b $\lor$ $\boldsymbol{\neg}$ p $\in$ set b
s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$ |  (s $\in_{\text{s}}$ $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$) $\in$ set b $\text{t}_{\text{1}}$ $\sqcup_{\text{s}}$ $\text{t}_{\text{2}}$ $\in$ subterms $\phi$ |  (s $\in_{\text{s}}$ $\text{t}_{\text{1}}$) $\in$ set b $\lor$ (s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$) $\in$ set b
$\vdots$ |  $\vdots$ |  $\vdots$
Var x $\in_{\text{s}}$ $\text{t}_{\text{1}}$ Var x $\notin_{\text{s}}$ $\text{t}_{\text{2}}$ Var x $\notin_{\text{s}}$ $\text{t}_{\text{1}}$ Var x $\in_{\text{s}}$ $\text{t}_{\text{2}}$ |  ($\text{t}_{\text{1}}$ $\neq_{\text{s}}$ $\text{t}_{\text{2}}$) $\in$ set b $\text{t}_{\text{1}}$ $\in$ subterms $\phi$ $\text{t}_{\text{2}}$ $\in$ subterms $\phi$ x $\notin$ vars b |  $\exists$s. (s $\in_{\text{s}}$ $\text{t}_{\text{1}}$) $\in$ set b $\land$ (s $\notin_{\text{s}}$ $\text{t}_{\text{2}}$) $\in$ set b $\lor$ $\exists$s. (s $\notin_{\text{s}}$ $\text{t}_{\text{1}}$) $\in$ set b $\land$ (s $\in_{\text{s}}$ $\text{t}_{\text{2}}$) $\in$ set b

After running out of linear rules to apply, only the branching rules shown in
LABEL:tab:bexpands remain. A rule is applicable if its _precondition_ is met
and, to prevent unnecessary branching, if it is not subsumed as indicated by
the _subsumption condition_. These rules create multiple branches in the
tableau, so we represent the different possibilities bs’ to expand a branch b
as a set and write bs’
$\mathrel{\includegraphics{./symbols/lefttrianglebar.pdf}}$ b. Accordingly, we
get a new branch b’ @ b in the tableau for each b’ $\in$ bs’.

A linearly saturated branch where no further branching is possible is called a
_saturated_ branch.

⬇

definition sat b $\equiv$ lin_sat b $\land$ ($\nexists$bs’. bs’
$\mathrel{\includegraphics{./symbols/lefttrianglebar.pdf}}$ b)

Note that even branching rules are defined such that they never create new
subterms, except for the last rule that adds a new variable to the branch.
These variables serve to manifest an inequality; hence, we call them
_witnesses_.

⬇

definition wits b $\equiv$ vars b - vars (last b)

##  4 A Decision Procedure for MLSS

The mechanics of the decision procedure are typical for a procedure based on a
tableau calculus: it decides the satisfiability of a given formula $\phi$ by
determining whether the formula has a closed tableau. More specifically, it
initialises the tableau with the singleton branch [$\phi$] and checks whether
this branch can be expanded to a closed tableau.

We only discuss the abstract specification here and refer the reader to the
formalisation for the executable specification. The implementation uses a
couple of features of Isabelle/HOL’s function package: instead of defining the
function via pattern matching, we specify the equations of the function as
conditional rewrite rules. This requires us to prove that the assumptions of
the equations are non-overlapping, which is done by automation. The other
concern is that Isabelle/HOL requires functions to be total, so a recursive
function needs to terminate for it to be well-defined; nevertheless, the
termination proof is separated from the definition of the function for
modularity. The function package maintains the soundness of the definition by
introducing a so-called domain predicate mlss_proc_branch_dom which
characterises the arguments for which the function terminates. Each equation
of the function is guarded by an assumption that the predicate holds for the
argument. In Section 7, we will show that the domain predicate holds for the
context in which the function mlss_proc_branch is called in. Before we go into
more detail on how the termination is proved, we discuss the definition of the
function, as shown below.

⬇

function mlss_proc_branch :: ’a branch $\Rightarrow$ bool where

$\neg$ lin_sat b $\Longrightarrow$ mlss_proc_branch b =

mlss_proc_branch ((SOME b’. b’
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b $\land$

set b $\subset$ set (b’ @ b)) @ b)

| $\llbracket$ lin_sat b; bclosed b $\rrbracket$ $\Longrightarrow$
mlss_proc_branch b = True

| $\llbracket$ $\neg$ sat b; bopen b; lin_sat b $\rrbracket$ $\Longrightarrow$
mlss_proc_branch b =

($\forall$b’ $\in$ (SOME bs. bs
$\mathrel{\includegraphics{./symbols/lefttrianglebar.pdf}}$ b).
mlss_proc_branch (b’ @ b))

| $\llbracket$ lin_sat b; sat b $\rrbracket$ $\Longrightarrow$
mlss_proc_branch b = bclosed b

definition mlss_proc :: ’a pset_fm $\Rightarrow$ bool where

mlss_proc $\phi$ $\equiv$ mlss_proc_branch [$\phi$]

The purpose of the function is to determine whether we can expand a given
branch to a closed tableau. As stated before, we first use linear expansion
rules in order to prevent premature branching; to this end, we recursively
expand the branch with linear rules until the branch is linearly saturated.
Note that we use Hilbert’s $\varepsilon$-operator in the form of SOME111In the
formalisation, the function mlss_proc_branch is actually parametrised by
choice functions to allow for refinement. to choose some rule that actually
adds new formulas to the branch. As soon as the branch is linearly saturated,
we terminate if the branch is closed as the second equation shows. Otherwise,
we choose an applicable branching rule and recursively check whether all newly
created branches can be closed. The final equation applies once no further
branch expansion is possible, in which case we just test for closedness of the
branch.

The procedure mlss_proc then calls mlss_proc_branch with a singleton branch
[$\phi$] to determine the satisfiability of a given formula $\phi$.

Thus, we use mlss_proc_branch is only on branches that result from applying
the expansion rules. We call this kind of branch _well-formed_. In the
definition below, the expression b’
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}^{*}$ b denotes that b’
is one of the branches that results from applying (potentially zero) expansion
rules to b.

⬇

definition wf_branch b $\equiv$ $\exists$$\phi$. b
$\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}^{*}$ [$\phi$]

We use this notion in Section 7 to state an upper bound for the cardinality of
well-formed branches. The upper bound justifies the termination of the
decision procedure. Before we come to that, though, we prove soundness and
completeness in Section 6 and 5, respectively. In Section 7, we also show that
both properties easily transfer to mlss_proc, which, together with
termination, establishes that it is a decision procedure.

##  5 Completeness of the Calculus

For completeness of the calculus, we need to show that every unsatisfiable
formula has a closed tableau or, conversely, that the formula is satisfiable
if there is a saturated and open branch in the tableau. To facilitate
inductive reasoning, we show a stronger statement by constructing a model M
such that M $\models$ $\phi$ for all $\phi$ $\in$ set b. At the core of the
model, there is a _realisation_ function that maps set terms to sets of type
hf. A subset of the witnesses, which we call _pure_ witnesses, receives
special treatment from the realisation function for reasons that will become
apparent in Section 5.1. The collection of set terms of a branch can thus be
partitioned into two collections, as defined below.

⬇

definition pwits :: ’a branch $\Rightarrow$ ’a set where

pwits b $\equiv$ {c $\in$ wits b. $\forall$t $\in$ subterms (last b).

AT (Var c $=_{\text{s}}$ t) $\notin$ set b $\land$ AT (t $=_{\text{s}}$ Var c)
$\notin$ set b}

definition subterms’ :: ’a branch $\Rightarrow$ ’a pset_term set where

subterms’ b $\equiv$ subterms (last b) $\cup$ Var ‘ (wits b - pwits b)

We aim to construct a syntactic model that we derive from the membership
literals s $\in_{\text{s}}$ t in the branch. To this end, we construct a graph
whose vertices are the disjoint union of the sets above and there is an edge
from s to t in the graph if, and only if, s $\in_{\text{s}}$ t is in b. Note
that we use Noschinski’s graph library [22] which represents a graph as a
record of vertices, arcs (directed edges), and two functions tail and head
that map an arc to its source and target vertex, respectively.

⬇

definition bgraph b $\equiv$ let vs = Var ‘ pwits b $\cup$ subterms’ b

in $\llparenthesis$ verts = vs, arcs = {(s, t). (s $\in_{\text{s}}$ t) $\in$
set b},

tail = fst, head = snd $\rrparenthesis$

The realisation function is defined relative to this graph. As mentioned
before, the realisation function treats the pure witnesses differently than
the rest of the set terms. The function evaluates terms in the latter set in
accordance to the structure of the graph, i.e. the realisation of a vertex is
defined as the union of the realisations of the parent vertices. For the
former set, we choose a function I that assigns the pure witnesses pairwise
distinct sets with cardinality greater than that of the vertices. We can
always choose such a function since we assume an infinite universe of
variables. Then, we return the singleton set HF {I x}, which, together with
the cardinality constraint, guarantees that realisations are distinct between
pure witnesses themselves as well as between pure witnesses and set terms. The
notation u $\rightarrow_{\text{G}}$ s in the definition below indicates that
there is an edge from u to s in the graph G.

⬇

abbreviation parents G s $\equiv$ {u. u $\rightarrow_{\text{G}}$ s}

function realise :: ’a pset_term $\Rightarrow$ V where

x $\in$ Var ‘ pwits b $\Longrightarrow$ realise x = HF {I x}

| x $\in$ subterms’ b

$\Longrightarrow$ realise t = HF {realise ‘ parents (bgraph b) s}

| x $\notin$ verts G $\Longrightarrow$ realise x = 0

Again, we need to ensure that the assumptions of the equations are non-
overlapping and that the function terminates. The former is taken care of by
automation, leaving us to prove termination. The assumption that b is open
implies that there are no membership cycles, thus bgraph b is acyclic.
Furthermore, the graph is finite by definition. Thus, we can use the
cardinality of the set of ancestors as a measure that decreases in each
recursive call.

Before we prove that the realisation function constitutes a model in Section
5.2, we will first explain the significance of the pure witnesses.

###  5.1 Characterisation of the Pure Witnesses

Recall that the pure witnesses of a branch b are those witnesses that are not
related to other subterms in last b by equality. In the context of a well-
formed branch, we can strengthen this characterisation to any set term and, in
addition, we also get that there is no membership literal where a pure witness
is on the right-hand side. Intuitively speaking, the realisation of a pure
witness does not depend on the realisation of any other set term.

⬇

lemma lemma_2:

assumes wf_branch b and c $\in$ pwits b

shows (Var c $=_{\text{s}}$ t) $\notin$ set b and (t $=_{\text{s}}$ Var c)
$\notin$ set b

and (t $\in_{\text{s}}$ Var c) $\notin$ set b

So why are pure witnesses treated differently? According to the definition of
realise, it would evaluate the pure witnesses would to the empty set 0 :: hf,
were they not treated separately. To see that this is a problem, consider the
branch b = [Var s $\neq_{\text{s}}$ Var t, Var t $\neq_{\text{s}}$ Var u]
which expands to several open and saturated branches, one of which is

⬇

[Var x $\neq_{\text{s}}$ Var y, Var x $\in_{\text{s}}$ Var s, Var x
$\notin_{\text{s}}$ Var t,

[Var x $\neq_{\text{s}}$ Var y, Var y $\in_{\text{s}}$ Var t, Var y
$\notin_{\text{s}}$ Var u] @ b

for some fresh x and y. Assigning both Var x and Var y a value of 0 would
contradict the literal Var x $\neq_{\text{s}}$ Var y. To prevent this, we
assign the pure witnesses pairwise different values.

The proof of lemma_2 is more technical than interesting so we refer the reader
to the formalisation.

###  5.2 Realisation of an Open Branch

Remember that for completeness, we need to show that the realisation function
for an open and saturated branch b actually constitutes a model for all
formulas in the branch. We start by verifying that the realisation function
models all literals in the branch; more formally, the following propositions
hold:

  1. (1)

We have realise s $\boldsymbol{\in}$ realise t if it holds that s
$\in_{\text{s}}$ t is in b.

  2. (2)

We have realise s $=$ realise t if s $=_{\text{s}}$ t is in b.

  3. (3)

We have realise s $\neq$ realise t if s $\neq_{\text{s}}$ t is in b.

  4. (4)

We have realise s $\boldsymbol{\notin}$ realise t if it holds that s
$\notin_{\text{s}}$ t is in b.

To illustrate the usefulness of lemma_2, we prove Proposition (2). The proofs
of all propositions translate well into Isabelle, so we refer to the original
paper [9] for the remaining proofs.

######  Proof (Proof of Proposition (2))

Assume that s $=_{\text{s}}$ t is in b. If there exists a c $\in$ pwits b
where s = Var c or t = Var c, we arrive at a contradiction due to lemma_2.
Therefore, both s $\in$ subterms’ b and t $\in$ subterms’ b must hold. Now,
assume for contradiction that realise s $\neq$ realise t. Without loss of
generality — the other case is symmetric — we obtain an e such that e
$\boldsymbol{\in}$ realise s and e $\boldsymbol{\notin}$ realise t.
Considering that s $\in$ subterms’ b and the definition of realise, we obtain
a d with e = realise d and d $\rightarrow_{\text{bgraph b}}$ s. This, in turn,
yields that d $\in_{\text{s}}$ s must be in b. Together with the assumption (s
$=_{\text{s}}$ t) $\in$ set b and the saturation of b, it follows that d
$\in_{\text{s}}$ t must also be in b. But then we have realise d
$\boldsymbol{\in}$ realise t $\longleftrightarrow$ e $\boldsymbol{\in}$
realise t using Proposition (1), which is a contradiction to the assumption e
$\boldsymbol{\notin}$ realise t.

We now lower the results on literals to set terms. All of the proofs are
straightforward so we refer the reader to the formalisation.

  1. (a)

It holds that realise $\emptyset$ = 0.

  2. (b)

Let $\star_{\text{s}}$ $\in$ {$\sqcup_{\text{s}}$, $-_{\text{s}}$,
$\sqcap_{\text{s}}$}. If the term s $\star_{\text{s}}$ t occurs in subterms b,
then

realise (s $\star_{\text{s}}$ t) = realise s $\star$ realise t.

  3. (c)

If Single t $\in$ subterms b, then

realise (Single t) = HF {realise t}.

The final step for obtaining a proper model is to connect the realisation
function to the semantics as defined in Section 2. For set terms, we can use
the Propositions (a)–(c) to prove the lemma below by induction on t.

⬇

lemma assumes t $\in$ subterms b

shows I${}_{\text{st}}$ ($\lambda$x. realise (Var x)) t = realise t

Lifting the above result to formulas yields the coherence of b, as the
original paper [9] calls it. The proof is a tedious but straightforward
induction on the the size of the formulas.

⬇

lemma coherence:

assumes $\phi$ $\in$ set b shows ($\lambda$x. realise (Var x)) $\models$
$\phi$

The coherence property finishes the proof of completeness of the calculus as
it gives us a model for every formula in an open and saturated branch.

##  6 Soundness of the Calculus

A tableau calculus is sound if the corresponding formula is unsatisfiable for
any closed tableau. We prove the following two properties to establish
soundness:

  1. (1)

It is impossible to satisfy all formulas in a closed branch simultaneously.

  2. (2)

The expansion rules maintain satisfiability.

We formalise the first property in Isabelle below.

⬇

lemma bclosed_sound:

assumes bclosed b shows $\exists$$\phi$ $\in$ set b. M $\not\models$ $\phi$

###### Proof

It is clear that, for any s, neither does M model s $\in$ $\emptyset$ nor s
$\neq_{\text{s}}$ s. Furthermore, no model can satisfy both $\phi$ and
$\boldsymbol{\neg}\>$$\phi$ at the same time. Lastly, a membership cycle is
impossible since the membership relation of hf is well-founded.

We are left with showing that both linear and branching expansion rules
preserve satisfiability. As for the linear rules, a straightforward proof by
case analysis on b’ $\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b
suffices to obtain the lemma below.

⬇

lemma lexpands_sound:

assumes b’ $\mathrel{\includegraphics{./symbols/lefttriangle.pdf}}$ b and
$\phi$ $\in$ set b’ and $\bigwedge$$\psi$. $\psi$ $\in$ set b
$\Longrightarrow$ M $\models$ $\psi$

shows M $\models$ $\phi$

A similar argument would work for the branching rules if it were not for the
last rule adding new variables. Those variables need to be assigned specific
values; hence, we modify the model as shown in the proof below.

⬇

lemma bexpands_sound:

assumes bs’ $\mathrel{\includegraphics{./symbols/lefttrianglebar.pdf}}$ b and
$\bigwedge$$\psi$. $\psi$ $\in$ set b $\Longrightarrow$ M $\models$ $\psi$

shows $\exists$M’. $\exists$b’ $\in$ bs’. $\forall$$\psi$ $\in$ set (b’ @ b).
M’ $\models$ $\psi$

###### Proof

We only consider the case where bs’
$\mathrel{\includegraphics{./symbols/lefttrianglebar.pdf}}$ b was proved by
applying the last branching expansion rule to s $\neq_{\text{s}}$ t for some s
and t. We have

⬇

bs’ = {[Var x $\in_{\text{s}}$ s, Var x $\notin_{\text{s}}$ t], [Var x
$\in_{\text{s}}$ t, Var x $\notin_{\text{s}}$ s]}

for some fresh variable x. Since s $\neq_{\text{s}}$ t is in b, we have that
I${}_{\text{st}}$ M s $\neq$ I${}_{\text{st}}$ M t because M is a model.
Without loss of generality, this inequality manifests itself through some y
with y $\boldsymbol{\in}$ I${}_{\text{st}}$ M s and y $\boldsymbol{\notin}$
I${}_{\text{st}}$ M t. We update M to map x to y to obtain the assignment M’.
Note that M’ is still a model for formulas in b because x is fresh with
respect to b. Furthermore, it is also a model for the first branch in bs’,
which finishes the proof.

##  7 Total Correctness of the Decision Procedure

We first demonstrate the termination of the procedure for well-formed
branches, i.e. every well-formed branch is in the domain of mlss_proc_branch.
To this end, we derive an upper bound for the number of distinct formulas in a
branch whose proof we omit here for brevity. We should point out that this
bound is not to be construed as the complexity of the procedure as it may
create exponentially many branches in general.

⬇

lemma card_wf_branch_ub:

assumes wf_branch b

shows |set b| $\leq$ 2 * |subfms (last b)| + 16 * |subterms (last
b)|${}^{\text{4}}$

Remember that mlss_proc_branch only applies a linear expansion rule to a
branch if the application results in new formulas. Moreover, the subsumption
conditions of the branching expansion rules ensure that each of the newly
created branches contain new formulas. Ultimately, we conclude that the
procedure must terminate for well-formed branches because the number of
formulas increases in each step but is also bounded.

⬇

lemma assumes wf_branch b shows mlss_proc_branch_dom b

The above lemma allows us to utilise the computation induction rule of
mlss_proc_branch on well-formed branches, which we use to prove soundness and
completeness. As both proofs are essentially an application of soundness,
respectively completeness, of the calculus, we refer the reader to the
formalisation.

⬇

lemma mlss_proc_branch_complete:

fixes b :: ’a branch

assumes wf_branch b and $\neg$ mlss_proc_branch b

assumes infinite (UNIV :: ’a set)

shows $\exists$M. M $\models$ last b

lemma mlss_proc_branch_sound:

assumes wf_branch b and $\forall$$\psi$ $\in$ set b. M $\models$ $\psi$

shows $\neg$ mlss_proc_branch b

To finish the proof of total correctness, note that every singleton branch is
trivially well-formed; thus, termination, completeness, and soundness easily
transfer to mlss_proc.

⬇

theorem mlss_proc_complete:

fixes $\phi$ :: ’a pset_fm

assumes $\neg$ mlss_proc $\phi$ and infinite (UNIV :: ’a set)

shows $\exists$M. M $\models$ $\phi$

theorem mlss_proc_sound:

assumes M $\models$ $\phi$ shows $\neg$ mlss_proc $\phi$

##  8 Dealing with Urelements

In the introduction, we stated the goal of integrating mlss_proc as a tactic
into Isabelle. For this to work, we must map every branch expansion rule to a
corresponding theorem in Isabelle/HOL. This is straightforward for all
expansion rules except for the last branching expansion rule. To illustrate,
suppose that we are to disprove a statement of the form

⬇

s $\neq$ (t :: ’a) $\land$ s $\in$ (A :: ’a set) $\cup$ B $\land$ $\ldots$

in Isabelle/HOL. By way of reification, we convert this to a formula of the
shape

⬇

s’ $\neq_{\text{s}}$ t’ $\boldsymbol{\land}$ s’ $\in_{\text{s}}$ A’
$\sqcup_{\text{s}}$ B’ $\boldsymbol{\land}$ $\ldots$

in our set syntax for some s’, t’, A’, and B’. When we apply the decision
procedure to this formula, it might return a tableau proof that contains an
application of the last branching rule to (s’ $\neq_{\text{s}}$ t’) $\in$ set
b. This results in two branches, one of which is [Var x $\in_{\text{s}}$ s’,
Var x $\notin_{\text{s}}$ t’] @ b; however, there is no matching rule in
Isabelle/HOL since s and t are not sets.

|  |  |  |  | $\Gamma$ $\vdash$ t : l
---|---|---|---|---
$\Gamma$ $\vdash$ $\emptyset$ n : Suc n |  | $\Gamma$ $\vdash$ Var x : $\Gamma$ x |  | $\Gamma$ $\vdash$ Single t : Suc l
|  $\star_{\text{s}}$ $\in$
{$\sqcup_{\text{s}}$,$\,\sqcap_{\text{s}}$,$\,-_{\text{s}}$} $\Gamma$ $\vdash$
s : l $\Gamma$ $\vdash$ t : l l $\neq$ 0
---
$\Gamma$ $\vdash$ s $\star_{\text{s}}$ t : l
|  $\Gamma$ $\vdash$ s : l $\Gamma$ $\vdash$ t : l |  |  $\Gamma$ $\vdash$ s : l $\Gamma$ $\vdash$ t : Suc l
---|---|---
$\Gamma$ $\vdash$ s $=_{\text{s}}$ t |  | $\Gamma$ $\vdash$ s $\in_{\text{s}}$ t
Figure 1: The type system for set terms and atoms.figure]fig:types

To deal with this problem, we formalise a lightweight type system as displayed
in LABEL:fig:types. The type of a set term in this system is just a natural
number which we call level. Intuitively speaking, the level l means that the
corresponding term t in Isabelle/HOL has type

$\texttt{'a}\ \underbrace{\texttt{set}\ \ldots\ \texttt{set}}_{\texttt{l}\
\text{times}}$

for some ’a. Note that the constructor $\emptyset$ now receives an additional
argument indicating the level of each instance of $\emptyset$.

Moreover, the typing judgement extends to set atoms by matching up the levels
of its component set terms.

Ultimately, we define $\Gamma$ $\vdash$ $\phi$ $\equiv$ $\forall$a $\in$ atoms
$\phi$. $\Gamma$ $\vdash$ a in order to type formulas.

We can now define the urelements with respect to a formula. An urelement is a
set term whose corresponding type in Isabelle/HOL might not be a set.

⬇

definition urelem :: ’a pset_fm $\Rightarrow$ ’a pset_term $\Rightarrow$ bool
where

urelem $\phi$ t $\equiv$ $\exists\Gamma$. $\Gamma$ $\vdash$ $\phi$ $\land$
$\Gamma$ $\vdash$ t : 0

Using this definition, we make two changes to the specification of the
calculus:  (1) First and foremost, we require that neither s nor t is an
urelement in the precondition of the last branching expansion rule.  (2) As
mentioned above, we add an argument to the $\emptyset$ constructor. This
argument is only used for the typing judgement; it has no impact on the
semantics.

Soundness, of course, is not affected by these changes but we have to make a
few amendments to maintain completeness:  (1) The first equation of realise
now also must account for the urelements. In particular, it has to ensure that
urelements receive pairwise different values unless they are related through
equality atoms. This does not affect pure witnesses since they can not be
related through equality atoms due to lemma_2.  (2) We must adjust the
completeness proof in those places where it directly refers to the definition
of realise to account for the case where a given term is an urelement.  (3)
The completeness theorem receives the additional assumption that $\Gamma$
$\vdash$ $\phi$ holds for the initial formula $\phi$.  (4) For the
completeness proof, we must show that the typing judgement is invariant under
branch expansion.

The modifications above ensure that the proof can be replayed through
Isabelle/HOL. To actually use the calculus, we must determine the urelements
of the initial formula $\phi$, though. In other words, we have to implement an
inference algorithm for our lightweight type system. The algorithm is, in
essence, a simplified version of Hindley-Milner type inference so it has the
same two phases: it generates constraints using syntax directed rules and then
passes them to a constraint solver.

Since we are only interested in the level of a term, we can encode all
constraints into the theory of $0$, the successor function S, and equality
(but no disequality). Note that constraints of the form l $\neq$ 0 can be
replaced by l $=$ S i with i being a fresh variable. A solver for this theory
is straightforward to implement and verify; nevertheless, we have to be
careful that it computes the minimum assignment $\Gamma$ from variables to
levels that fulfils the constraints. This guarantees that a set term t is not
an urelement if, and only if, $\Gamma$ t $>$ 0. Conversely, all terms s with
$\Gamma$ s $=$ 0 are urelements.

##  9 Conclusion and Future Work

We developed a formalisation of a tableau calculus for a quantifier-free
fragment of set theory called MLSS based on a paper by Cantone and Zarba [9].
The formalisation includes an abstract description of a decision procedure
that builds on the calculus. To make the decision procedure compatible with
Isabelle/HOL, we extended the calculus with a lightweight type system while
maintaining completeness. We also refined the abstract specification to an
executable specification from which code can be generated.

In future work, we plan to implement an efficient executable specification in
the style of a worklist algorithm. This specification should also generate
certificates that can be replayed through Isabelle’s inference kernel to
facilitate the integration of the procedure into Isabelle.

####  9.0.1 Acknowledgements

The author thanks Kevin Kappelmann and Tobias Nipkow for their comments on a
draft version of this paper and the anonymous referees for their thorough
reviews.

## References

  * Beckert and Hartmer [1998] Beckert, B., Hartmer, U.: A tableau calculus for quantifier-free set theoretic formulae. Automated Reasoning with Analytic Tableaux and Related Methods p. 93–107 (1998), doi:10.1007/3-540-69778-0_16
  * Bentzen [2021] Bentzen, B.: A Henkin-style completeness proof for the modal logic S5. In: Baroni, P., Benzmüller, C., Wáng, Y.N. (eds.) Logic and Argumentation - 4th International Conference, Lecture Notes in Computer Science, vol. 13040, pp. 459–467, Springer (2021), doi:10.1007/978-3-030-89391-0\\_25
  * Blanchette et al. [2017] Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning 58(1), 149–179 (2017), doi:10.1007/s10817-016-9391-3
  * Cantone [1997] Cantone, D.: A fast saturation strategy for set-theoretic tableaux. In: Galmiche, D. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 122–137, Springer (1997), doi:10.1007/BFb0027409
  * Cantone et al. [2010] Cantone, D., Longo, C., Asmundo, M.N.: A decision procedure for a two-sorted extension of multi-level syllogistic with the cartesian product and some map constructs. In: Faber, W., Leone, N. (eds.) Italian Conference on Computational Logic, CEUR Workshop Proceedings, vol. 598, CEUR-WS.org (2010), URL http://ceur-ws.org/Vol-598/paper11.pdf
  * Cantone et al. [1990] Cantone, D., Omodeo, E.G., Policriti, A.: The automation of syllogistic. Journal of Automated Reasoning 6(2), 173–187 (1990), ISSN 0168-7433, doi:10.1007/BF00245817
  * Cantone et al. [2001] Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing - From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science, Springer (2001), doi:10.1007/978-1-4757-3452-2
  * Cantone et al. [2003] Cantone, D., Schwartz, J.T., Zarba, C.G.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. Electronic Notes in Theoretical Computer Science 86(1), 49–60 (2003), doi:10.1016/S1571-0661(04)80652-2, international Workshop on First-Order Theorem Proving
  * Cantone and Zarba [1998] Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) Automated Deduction in Classical and Non-Classical Logics, Selected Papers, Lecture Notes in Computer Science, vol. 1761, pp. 126–136, Springer (1998), doi:10.1007/3-540-46508-1\\_8
  * Cantone and Zarba [1999] Cantone, D., Zarba, C.G.: A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. In: Murray, N.V. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 1617, pp. 97–112, Springer (1999), doi:10.1007/3-540-48754-9\\_12
  * Chaieb [2006] Chaieb, A.: Verifying mixed real-integer quantifier elimination. In: Furbach, U., Shankar, N. (eds.) International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, vol. 4130, pp. 528–540, Springer (2006), doi:10.1007/11814771\\_43
  * Chaieb and Nipkow [2005] Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 3835, pp. 367–380, Springer (2005), doi:10.1007/11591191\\_26
  * Doczkal and Smolka [2014] Doczkal, C., Smolka, G.: Completeness and decidability results for CTL in Coq. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, pp. 226–241, Springer International Publishing (2014), doi:10.1007/978-3-319-08970-6_15
  * Ferro et al. [1980] Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Communications on Pure and Applied Mathematics 33(5), 599–608 (1980), doi:10.1002/cpa.3160330503
  * Fitting [1996] Fitting, M.: Semantic Tableaux and Resolution. Springer New York, New York, NY (1996), doi:10.1007/978-1-4612-2360-3_3
  * From [2019] From, A.H.: Formalizing a Seligman-style tableau system for hybrid logic. Archive of Formal Proofs (December 2019), ISSN 2150-914x, https://isa-afp.org/entries/Hybrid_Logic.html, Formal proof development
  * From [2023] From, A.H.: Synthetic completeness. Archive of Formal Proofs (January 2023), ISSN 2150-914x, https://isa-afp.org/entries/Synthetic_Completeness.html, Formal proof development
  * From et al. [2020] From, A.H., Blackburn, P., Villadsen, J.: Formalizing a Seligman-style tableau system for hybrid logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning, pp. 474–481, Springer International Publishing, Cham (2020), doi:10.1007/978-3-030-51074-9_27
  * From et al. [2021] From, A.H., Schlichtkrull, A., Villadsen, J.: A sequent calculus for first-order logic formalized in Isabelle/HOL. In: Monica, S., Bergenti, F. (eds.) Proceedings of the 36th Italian Conference on Computational Logic, CEUR Workshop Proceedings, vol. 3002, pp. 107–121, CEUR-WS.org (2021), URL http://ceur-ws.org/Vol-3002/paper7.pdf
  * Nipkow [2008] Nipkow, T.: Linear quantifier elimination. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, pp. 18–33, Springer (2008), doi:10.1007/978-3-540-71070-7_3
  * Nipkow et al. [2002] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
  * Noschinski [2013] Noschinski, L.: Graph theory. Archive of Formal Proofs (April 2013), ISSN 2150-914x, https://isa-afp.org/entries/Graph_Theory.html, Formal proof development
  * Paulson [2013] Paulson, L.C.: The hereditarily finite sets. Archive of Formal Proofs (November 2013), ISSN 2150-914x, https://isa-afp.org/entries/HereditarilyFinite.html, Formal proof development
  * Stevens [2023] Stevens, L.: Mlss decision procedure. Archive of Formal Proofs (May 2023), ISSN 2150-914x, https://isa-afp.org/entries/MLSS_Decision_Proc.html, Formal proof development
  * Stevens and Nipkow [2021] Stevens, L., Nipkow, T.: A verified decision procedure for orders in Isabelle/HOL. In: Hou, Z., Ganesh, V. (eds.) Automated Technology for Verification and Analysis, pp. 127–143, Springer International Publishing (2021), doi:10.1007/978-3-030-88885-5_9