11institutetext: 1Department of Engineering Science, University of Oxford,
Oxford, UK
2Department of Computing, Imperial College London, London, UK
3School of Computer Science, University of Birmingham, Birmingham, UK
11email<EMAIL_ADDRESS>
#  $\rm{IterMask^{2}}$: Iterative Unsupervised Anomaly Segmentation via
Spatial and Frequency Masking for Brain Lesions in MRI

Ziyun Liang1 Xiaoqing Guo1 J. Alison Noble1 Konstantinos Kamnitsas1,2,3

###### Abstract

Unsupervised anomaly segmentation approaches to pathology segmentation train a
model on images of healthy subjects, that they define as the ‘normal’ data
distribution. At inference, they aim to segment any pathologies in new images
as ‘anomalies’, as they exhibit patterns that deviate from those in ‘normal’
training data. Prevailing methods follow the ‘corrupt-and-reconstruct’
paradigm. They intentionally corrupt an input image, reconstruct it to follow
the learned ‘normal’ distribution, and subsequently segment anomalies based on
reconstruction error. Corrupting an input image, however, inevitably leads to
suboptimal reconstruction even of normal regions, causing false positives. To
alleviate this, we propose a novel iterative spatial mask-refining strategy
$\rm{IterMask^{2}}$. We iteratively mask areas of the image, reconstruct them,
and update the mask based on reconstruction error. This iterative process
progressively adds information about areas that are confidently normal as per
the model. The increasing content guides reconstruction of nearby masked
areas, improving reconstruction of normal tissue under these areas, reducing
false positives. We also use high-frequency image content as an auxiliary
input to provide additional structural information for masked areas. This
further improves reconstruction error of normal in comparison to anomalous
areas, facilitating segmentation of the latter. We conduct experiments on
several brain lesion datasets and demonstrate effectiveness of our method.
Code is available at: https://github.com/ZiyunLiang/IterMask2

###### Keywords:

Unsupervised Anomaly Segmentation Brain Lesions

##  1 Introduction

Anomaly segmentation aims to identify patterns that deviate from a ‘normal’
distribution, defined as the distribution of training data. Such algorithms
can be used for unsupervised pathology segmentation, where ‘normal’ (training)
data are images of healthy tissue, while ‘anomaly’ refers to any pathology.
These segmentation methods are termed unsupervised because they do not require
any ‘anomalous’ images with pathology nor their manual segmentations for
training - they are trained using solely ’normal’ images (without
pathologies). They can then be used to segment _any_ anomalies (pathologies)
in new data. This offers an alternative to the predominant supervised learning
paradigm. In the context of brain lesion segmentation, the focus of this
study, the common approach is supervised training of a model using manual
segmentations for a _specific_ pathology [10, 9, 8, 20]. These models cannot
segment other types of pathology. Moreover, it is challenging to train
supervised models for rare diseases due to the scarcity of training data, and
they are impractical for workflows where the type of pathology that may be in
a scan is unknown beforehand. Unsupervised anomaly segmentation can instead
enable development of models that can identify _any_ pathology and enable
applications such as automatic screening for incidental findings [19].

Related Work: The most prevalent unsupervised anomaly segmentation methods are
reconstruction-based. During training, some distortion is applied to the input
image and the model learns the ‘normal’ data distribution by learning to
reconstruct the image. During inference, anomalies that are not seen during
training are challenging to reconstruct, resulting in high reconstruction
errors that are used to segment anomalies. For precise anomaly segmentation,
reconstruction errors need to be high on anomalous and low on normal areas.

Reconstruction-based methods that leverage AutoEncoder (AE) [1, 4] or
Variational AutoEncoder (VAE) [4, 17, 22] use compression as distortion and
train a model to reconstruct the image. Another type of reconstruction-based
method follows the ‘corrupt and reconstruct’ paradigm: the input is corrupted
during _inference_ , usually by adding a type of noise, and the model is
tasked to reconstruct it. Such state-of-the-art methods use diffusion models
[18, 5], which corrupt inputs with Gaussian noise. In both above approaches,
increasing input distortion (compression or noise) amplifies reconstruction
error of anomalies, since the model has not learned their appearance during
training and fails to reconstruct them. This however poses a _sensitivity-
precision trade-off_ , because more distortion also increases reconstruction
error of normal areas, causing false positives [6]. [5] proposes to address
this trade-off by first generating a mask that covers all anomalies, and then
by iteratively reconstructing the masked area with a diffusion model. This
relates to our work that also uses an iterative process, but differs
conceptually. In that method, the initial mask, which can be suboptimal, is
not refined throughout iterations. Furthermore, their generative model does
not have any auxiliary guidance for reconstructing the masked content, which
hinders faithful reconstruction of normal tissues beneath the mask. Our method
effectively addresses these points as we will demonstrate. Recently, cross-
modality translation has been proposed as an intermediate step for
reconstruction [12]. A model is trained for translating normal tissues between
MRI modalities. It is assumed that during inference the model will fail to
translate anomalies, enabling their segmentation. This approach, however,
requires multi-modal data. Finally, promising results are achieved by
denoising methods [11]. Unlike previously discussed approaches, the input is
corrupted by adding noise only during _training_ (not inference) and a model
is trained to remove it. During inference, it is assumed anomalies will be
perceived as noise and will be removed. For this, noise added during training
must model the appearance of anomalies and thus requires prior knowledge of
their appearance. This is impractical when developing a model for segmenting
‘any’ pathology as herein.

The sensitivity-precision trade-off associated with input corruption in
previous works motivates our study: Can we leverage input corruption to
amplify anomaly reconstruction error for its segmentation, while avoiding
information loss in normal areas to improve their reconstruction and reduce
false positives, without prior knowledge about appearance of anomaly?

Contributions: This work introduces $\rm{IterMask^{2}}$, a novel iterative
unsupervised anomaly segmentation method that integrates spatial and frequency
masking. We distort the input using spatial masking and reconstruct masked
areas via a model trained solely on normal data. We iteratively refine the
spatial masks, uncovering areas where low reconstruction error indicates
normality with high confidence. This gradually re-introduces information about
normal areas to further improve the reconstruction of neighbouring normal
areas, reduces false positives, and shrinks the mask towards containing solely
the anomaly. To further guide the reconstruction of masked normal areas, we
also propose providing structural information in the form of high-frequency
image components (low-frequency masking) as additional input. This facilitates
more faithful reconstruction of normal areas, whose appearance is predictable
from training, in contrast to anomalies whose structure and appearance are
unexpected. We conducted extensive experiments on several brain lesion
datasets that demonstrate the effectiveness of our method.

Figure 1: Overview of proposed method. (a) The frequency masking strategy that
provides structural information for an image via its high frequency
components. (b) Training of the reconstruction model. Random spatial masking
is applied to input image x. High image frequencies from step (a) are given as
auxiliary input $\textbf{x}_{c}$ to the model. (c) shows the iterative mask
refinement process during inference. The mask $\textbf{m}_{t}$ of iteration t
gradually shrinks toward the anomaly with the guidance of spatially unmasked
area $\textbf{x}_{m}$ and high image frequencies $\textbf{x}_{c}$.

##  2 Method

Overview of our method is shown in Fig. 1. The method follows the ‘corrupt and
reconstruct’ paradigm. To mitigate the sensitivity-precision trade-off of this
type of method (Sec. 1), we propose an iterative spatial mask refinement
process that uses spatial masking as corruption to amplify reconstruction
errors on anomalies while minimizing information loss in normal areas by
iteratively shrinking a spatial mask toward the anomaly. The mask shrinking
process gradually introduces more information about normal-tissue appearance
to the model (Fig. 1(c)). In each iteration, the spatially unmasked (ideally
normal) area guides the reconstruction of the spatially masked area to shrink
towards anomalies. Areas where the error map indicates confidence are
considered normal and are removed from the mask for next iterations. Given the
vast diversity of human brain structures, however, reconstructing masked areas
without guidance would likely lead to significant reconstruction errors even
for normal tissue areas, causing false positives. Therefore, we further
propose extracting structural information from the image and using it as
auxiliary input to the network to guide the reconstruction of masked areas.
The structural information is high-frequency image components from the Fourier
domain, as shown in Fig.1(a). The training process is shown in Fig.1(b). Below
we describe these components in detail.

###  2.0.1 Iterative Spatial Mask Refinement for Inference

During inference, the model aims to segment any pathology in a test dataset of
brain scans $D_{te}=\left\\{\mathbf{x}^{i}\right\\}^{N}_{i=1}$. Assuming that
the model was trained on data containing only healthy tissues, which define
the ‘normal’ distribution, at inference pathologies are to be segmented as
‘anomalous’ areas with patterns deviating from the normal data distribution.
For this, we use model $f$ that reconstructs spatially masked image areas.
Given an input image $\mathbf{x}$ that we aim to segment, an initial mask
$\textbf{m}_{1}$ is created that covers the entire brain. We will shrink the
mask iteratively, with $\textbf{m}_{t}$ being the mask at iteration $t$. The
masked area is covered with Gaussian noise $\epsilon$, while the unmasked area
is copied from the input image. Therefore, the input to the model is
$\hat{\mathbf{x}}_{t}=\mathbf{m}_{t}\times\epsilon+(1-\mathbf{m}_{t})\times\mathbf{x}$.
The model reconstructs the image giving output
$\mathbf{x}_{t}^{\prime}=f(\hat{\mathbf{x}}_{t},\mathbf{x}_{f})$. Here,
auxiliary input $\mathbf{x}_{f}$ is high-frequency image content, described in
the next part of this section. We then compute the error map between
$\mathbf{x}_{t}^{\prime}$ and original image via $L_{2}$ distance
$\mathbf{e}_{t}=\lVert\mathbf{x}_{t}^{\prime}-\mathbf{x}\rVert_{2}$. Since we
are constantly shrinking the mask towards anomalies, we only consider the
error under masked area,
$\mathbf{e}_{t}^{\prime}=\mathbf{e}_{t}\times\textbf{m}_{t}$. To determine how
to shrink the mask for the next iteration, we compare
$\mathbf{e}_{t}^{\prime}$ with threshold $\tau$. Pixels below $\tau$ are
considered confidently normal as per the model and are removed from the mask.
A detailed analysis on $\tau$ can be found in Section 3. The first iteration
is treated as a special case for convenience. Mask $\textbf{m}_{2}$ for the
second iteration is calculated using the 40th percentile of the first
iteration’s error map $\mathbf{e}_{1}^{\prime}$ as threshold $\tau$, unmasking
40% of the brain as healthy, for faster mask convergence. The iterative
process terminates automatically when the mask shrinks less than 1%.

###  2.0.2 Frequency Masking:

Frequency domain analysis is fundamental in medical imaging, such as for MRI
reconstruction, image denoising and more. Low frequencies of an image’s
Fourier spectrum capture the mean image intensity (DC signal) and intensities
of large image components. High frequencies, on the other hand, capture fine
details like edges, boundaries between tissues, and fine outlines of
structures [7]. Amplitude captures low-level statistics while phase is
necessary for restructuring the Fourier components back to the original image
[16, 15].

Our method aims to reconstruct areas of an image masked in the spatial domain.
To guide the reconstruction process of masked areas and enable more faithful
reconstruction of normal tissues, we provide structural image information to
the model in the form of high-frequency and phase image components. This
reduces false positives by lowering reconstruction error of normal tissue
without accompanied decrease for anomalous areas, because the model has not
learned how to recreate appearance of anomalies from their high frequency
components.

Given a 2D image x (slice of 3D scan) with size $H\times W$, we use the
Discrete Fourier Transform $\mathcal{F}$ to map the input image to the
frequency domain, obtaining:
$\mathcal{F}(\textbf{x})(a,b)=\sum_{h=0}^{H-1}\sum_{w=0}^{W-1}e^{-i2\pi(\frac{ah}{H}+\frac{bw}{W})}\textbf{x}(h,w)$,
where $\textbf{x}(h,w)$ is the spatial pixel value, and the output is complex
frequency value. Amplitude and phase are computed by
$\mathcal{A}=\left|\mathcal{F}(\textbf{x})(a,b)\right|$ and
$\phi=tan^{-1}\frac{Im(\mathcal{F}(\textbf{x})(a,b))}{Re(\mathcal{F}(\textbf{x})(a,b))}$,
where $Im$ and $Re$ refers to imaginary and real of the complex value
respectively. To capture high-level structural information, we use a high-
frequency filter to mask out low-frequency amplitude while keeping all the
phase information. Our high-pass filter for amplitude masking is:

$N(u,v)=\left\\{\begin{aligned} 1,&\quad if\quad d((c_{u},c_{v}),(u,v))<r\\\
0,&\quad else\end{aligned}\right.,\quad\mathcal{A}_{m}=\mathcal{A}\times N$
(1)

Finally, the masked amplitude and phase are combined by $A_{m}*e^{j*\phi}$
before inverse Fourier transform $\textbf{x}_{f}=\mathcal{F}^{-1}(\textbf{x})$
map it back to image space.

###  2.0.3 Spatial Random Masking for Training:

To realize the aforementioned process, we train a UNet as model $f$, which
takes spatially masked images from the training set
$D_{tr}=\left\\{\mathbf{x}^{i}\right\\}^{N}_{i=1}$ as input and outputs the
reconstructed result, with the high image frequencies $x_{f}$ as auxiliary
input. As there are no anomalies in training, we generate randomly shaped
masks for training. For this, we first select a random point
$(\mu_{x},\mu_{y})$ in brain area and generate a multivariate 2D Gaussian
distribution with the selected point as center. The probabilistic density
function of the Gaussian distribution is
$p(x,y)=\frac{1}{2\pi\sigma^{2}}e^{-[(x-\mu_{x})^{2}+(y-\mu_{y})^{2}]/(2\sigma^{2})}$,
where $(x,y)$ is the position. We sample the covariance $\sigma$ for
generating a Gaussian distribution with a dense region that won’t cover the
whole brain. Then, the probabilistic density function $p(x,y)$ is used as the
probability to sample masked patches from the image. The patches have random
side lengths $l={4,8,16}$, and the probability of a patch sampled at position
$(x,y)$ is $\frac{p(x,y)}{\sum_{x,y=1:X,Y}p(x,y)}$. After sampling around 1000
patches, random-shaped masks $\mathbf{m}_{r}$ are generated as shown in
Fig.1(b). For input image x, masked input to the model is
$\hat{\textbf{x}}=\epsilon\times\mathbf{m}_{r}+\mathbf{x}\times(1-\mathbf{m}_{r})$,
where $\epsilon$ is Gaussian noise. The model’s output is reconstruction
$x^{\prime}=f(\hat{\textbf{x}},x_{f})$. The training loss is the
reconstruction error $L=\lVert x^{\prime}-\mathbf{x}\rVert_{2}$.

Note that we treat as a special case the first iteration of the iterative
process described previously in this section, because the whole image x is
masked for $t=1$. For this, we train a second UNet separately. This model
receives as input only the high-frequency image $\textbf{x}_{f}$ and is
trained to reconstruct whole input x.

##  3 Experiment

Setup: We evaluate our method by training our model on healthy (i.e. ‘normal’)
2D slices and segment brain pathologies at test time. We use the BraTS2021
dataset [3, 2] with 1251 tumor cases, ATLAS v2.0 [13] with 655 stroke lesion
cases, and SSIM of ISLES 2015 [14] with 28 stroke lesions. For BraTS, we use
the same data pre-processing and selection process as described in [12]. For
ATLAS and ISLES, we perform skull-strip and apply z-score intensity
normalization as pre-processing. All lesion labels are merged into a single
class.

Results: To evaluate segmentation quality, we use the dice coefficient (DSC),
sensitivity, and precision. To evaluate the reconstruction performance in
‘normal’ areas, we measure the structural similarity by computing the SSIM
score between the original image and the reconstructed image after excluding
the anomaly regions. We compare our method to a variety of baseline methods,
including the autoencoder-based method (AE) [4], diffusion model-based method
(DDPM) [18], diffusion model with iterative resampling AutoDDPM [5], modality
translation Cyclic-UNet [12], and denoising autoencoder DAE [18]. In Cyclic-
UNet, the middle modalities used are T1 (FLAIR as input) and FLAIR
(otherwise).

Table 1: Performance for different anomaly segmentation methods on all
modalities of BraTS. Grey-shaded cells use the best threshold per-image. Best
in bold.

Modality | FLAIR | T1CE | T2 | T1
---|---|---|---|---
Metrics | DSC | Sens. | Prec. | SSIM | DSC | Sens. | Prec. | SSIM | DSC | Sens. | Prec. | SSIM | DSC | Sens. | Prec. | SSIM
AE[4] | 33.4 | 54.0 | 27.0 | 0.941 | 32.3 | 50.1 | 26.4 | 0.957 | 30.2 | 62.8 | 21.1 | 0.937 | 28.5 | 94.9 | 17.4 | 0.953
DDPM[18] | 60.7 | 57.8 | 69.8 | 0.980 | 37.9 | 35.2 | 46.2 | 0.984 | 36.4 | 33.6 | 44.2 | 0.984 | 29.4 | 32.1 | 31.5 | 0.977
AutoDDPM[5] | 55.5 | 57.5 | 58.7 | 0.937 | 36.9 | 58.9 | 28.9 | 0.903 | 29.7 | 53.0 | 22.3 | 0.907 | 33.5 | 61.1 | 24.7 | 0.910
Cycl.UNet[12] | 65.0 | 63.4 | 73.9 | 0.864 | 42.6 | 47.5 | 42.9 | 0.923 | 49.5 | 48.8 | 53.4 | 0.831 | 37.0 | 45.8 | 35.2 | 0.926
DAE[11] $\left[0,+\infty\right]$ | 79.7 | 79.1 | 84.5 | 0.926 | 36.7 | 42.0 | 36.2 | 0.844 | 69.6 | 68.1 | 75.3 | 0.903 | 29.5 | 61.2 | 20.5 | 0.860
DAE $\left[-\infty,0\right]$ | 28.5 | 94.9 | 17.3 | 0.875 | 34.7 | 37.9 | 39.3 | 0.966 | 28.5 | 94.9 | 17.4 | 0.885 | 47.9 | 53.7 | 50.9 | 0.958
DAE$\left[-\infty,+\infty\right]$ | 73.7 | 72.9 | 80.5 | 0.926 | 46.3 | 47.9 | 51.5 | 0.969 | 60.4 | 58.5 | 69.1 | 0.897 | 44.5 | 48.0 | 47.5 | 0.964
$\rm{IterMask^{2}}$ | 80.2 | 81.3 | 83.3 | 0.985 | 61.7 | 59.1 | 70.9 | 0.997 | 71.2 | 74.4 | 72.9 | 0.994 | 58.5 | 56.6 | 67.6 | 0.996
DAE[11] $\left[0,+\infty\right]$ | 84.2 | 83.1 | 87.0 | 0.926 | 42.1 | 52.5 | 42.8 | 0.844 | 74.5 | 72.1 | 80.1 | 0.903 | 35.3 | 64.3 | 28.3 | 0.860
$\rm{IterMask^{2}}$ | 85.9 | 85.7 | 87.4 | 0.991 | 67.7 | 66.4 | 76.4 | 0.997 | 78.3 | 75.6 | 84.0 | 0.995 | 64.9 | 65.2 | 71.4 | 0.995

We first evaluated performance for segmenting tumors as anomalies across all
modalities of the BraTS dataset. As shown in white-shaded parts of Tab.1, our
method exhibits promising performance compared to existing methods that do not
include prior information during training (i.e. AE, DDPM, AutoDDPM,
Cycl.-UNet), improve dice by 15.2%, 19.1%, 21.7%, 21.5% in FLAIR, T1CE, T2,
and T1 modalities respectively. DAE (shown in the $\left[0,+\infty\right]$ row
shaded white in Tab.1) demonstrates promising performance in FLAIR and T2
modalities, where tumors are hyper-intense, but fails to outperform other
baselines methods in T1CE and T1. This is due to hyper-intense noise being
used as prior during training (i.e. by learning to remove noise of range
$\left[0,+\infty\right]$). We further tested DAE with different intensity
priors by adjusting the intensity of added noise. In our method, without
introducing prior intensity information, we outperform DAE with all kinds of
noise in the dice score. More specifically, we compared our method to DAE when
the intensity prior matches with the anomaly ($\left[-\infty,0\right]$ range
of noise for T1 and $\left[-\infty,+\infty\right]$ for T1CE). We improved dice
by 0.5% and 1.6% in FLAIR and T2 with hyper-intense noise, and 15.4% and 10.6%
in T1CE and T2, where the noise intensity is similar to normal tissues. In
terms of reconstruction performance, our method improves SSIM to 0.985 in
FLAIR, 0.997 in T1CE, 0.994 in T2, and 0.996 in T1, showing our iterative
mask-shrinking approach can reconstruct normal areas better than other
existing methods. Fig.2 shows the qualitative result of our proposed method
compared to baselines.

Table 2: Performance on ISLES and ATLAS datasets. Best marked in bold.

Modality | ISLES FLAIR | ATLAS T1
---|---|---
Metrics | DSC | Sens. | Prec. | SSIM | DSC | Sens. | Prec. | SSIM
AE[4] | 21.5 | 0.475 | 0.167 | 0.791 | 11.9 | 40.7 | 8.6 | 0.954
DDPM[18] | 44.0 | 50.3 | 43.9 | 0.937 | 20.2 | 22.6 | 26.5 | 0.987
AutoDDPM[5] | 41.1 | 52.6 | 42.9 | 0.862 | 12.7 | 47.4 | 9.2 | 0.892
Cycl.UNet[12] | 53.4 | 50.5 | 59.4 | 0.842 | - | - | - | -
DAE[11] | 51.8 | 61.9 | 52.5 | 0.914 | 11.1 | 33.4 | 32.7 | 0.995
$\rm{IterMask^{2}}$ | 55.1 | 59.8 | 58.0 | 0.964 | 35.3 | 34.3 | 41.7 | 0.996
DAE[11] | 56.5 | 66.8 | 55.6 | 0.905 | 11.1 | 33.4 | 32.7 | 0.995
$\rm{IterMask^{2}}$ | 59.6 | 69.1 | 61.7 | 0.956 | 47.5 | 57.7 | 54.2 | 0.989

Table 3: Ablation study. $DS_{S,M,L}$ represents Dice score of small, medium
and large lesions.

Modality | BraTS FLAIR
---|---
Metrics | DSC | Sens. | Prec. | $\rm{DS_{S}}$ | $\rm{DS_{M}}$ | $\rm{DS_{L}}$
-freq | 64.2 | 69.4 | 63.6 | 20.7 | 63.4 | 72.1
-spat | 75.1 | 73.8 | 79.6 | 46.6 | 77.9 | 77.0
DAE[11] | 79.7 | 79.1 | 84.5 | 47.3 | 81.5 | 83.0
$\rm{IterMask^{2}}$ | 80.2 | 81.3 | 83.3 | 55.6 | 80.8 | 83.6
DAE[11] | 84.2 | 83.1 | 87.0 | 60.6 | 85.3 | 87.0
$\rm{IterMask^{2}}$ | 85.9 | 85.7 | 87.4 | 65.7 | 86.3 | 88.7

We further evaluated our method on stroke lesion segmentation in the ISLES and
ATLAS datasets, as shown in the white shaded parts in Tab. 2. Our method shows
superior performance for almost all the evaluated metrics compared to
baselines, demonstrating the generalizability of IterMask2 to different
anomalies.

Ablation Study: We assess the effectiveness of the iterative spatial mask
refinement and frequency-masking as in Tab.3. Respectively, we removed
frequency guidance after the initial step (‘-freq’ row) and we used high image
frequencies as input to generate a single-step prediction (removing the
iterative spatial mask refinement process) (‘-spat’ row). Dice score drops by
16.0% and 5.1% respectively, showing the effectiveness of both components.

Figure 2: Visualization result for FLAIR(BraTS).

Figure 3: Sensitivity Analysis.

Sensitivity Analysis: We first analyze the sensitivity of our model to the
mask shrinking threshold $\tau$ in the iterative spatial mask refinement
process. We choose $\tau$ from the healthy validation set’s error map obtained
by applying random masks in the same way as training. As shown in Fig. 3, we
experimented with $\tau$ ranging from 60-100 percentiles of the error map’s
masked area on all modalities of BraTS. Observe that our model demonstrates
stability across a broad spectrum of $\tau$, showcasing a notable level of
fault tolerance. This is credited to our way of computing the final
segmentation, where we use the last iteration’s reconstruction rather than
directly using the final mask. So the algorithm has some degree of fault
tolerance when the mask is larger than the anomaly. In Tab.1 2 3, $\tau$ is
set at 80 percentile of the error map in BraTS and ISLES, and 70 in ATLAS,
values found adequate in preliminary experiments prior to this analysis (thus
not over-optimized). Furthermore, we analyzed sensitivity of our algorithm to
the frequency masking radius $r$. In the experiment, we set high image
frequencies as input to reconstruct images in a single step, showing their
influence on the reconstruction process. Observe from Fig.3 that the model’s
performance is stable to radius from 10-25 in all the modalities of BraTS. In
all our reported experiments, we set the radius to 15, similar to the setting
in [21].

Human-AI collaboration: The threshold $\tau$ is an adjustable parameter,
providing clinicians with the flexibility to interactively adjust the
segmentation if the result using the optimized threshold gives unsatisfactory
results. Moreover, our model’s mask-shrinking process offers an intuitive
interface for human interaction by showing the intermediate decision process.
Therefore, we tested our model by incrementally raising $\tau$ value during
the shrinking process and selected the iteration with the optimal performance
per image for evaluation, obtaining improved performance, as shown in gray-
shaded cells of Tab.1 2 3. We further compared our models’ performance with
the best baseline method’s optimal performance (DAE), also optimizing the
threshold per image when choosing the final segmentation. We found that our
model constantly achieves better performance on all datasets, revealing the
promising potential to interact with clinicians. Furthermore, we categorized
the tumor size into small (size<200), medium, and large (size>800),
demonstrating human collaboration has the potential to notably improve
performance in detecting small anomalies(as shown in gray-shaded units in
Tab.3). When the anomaly is small, the model can prompt clinician
intervention, potentially improving prediction accuracy with minimal human
effort.

##  4 Conclusion

This paper introduces a novel unsupervised anomaly segmentation algorithm
$\rm{IterMask^{2}}$ for segmentation of brain lesions in MRI. The process uses
iterative spatial mask refinement and is guided by structural information from
high-frequency image components. Extensive experiments on brain tumor and
stroke lesion datasets demonstrated the effectiveness of the method in
comparison to previous works. Given the very promising results, future work
could seek to extend the framework for processing 3D images instead of slices
processed herein.

##  5 Acknowledgement

ZL is supported by a scholarship provided by the EPSRC Doctoral Training
Partnerships programme [EP/W524311/1]. The authors acknowledge UKRI grant
reference [EP/X040186/1] and EPSRC grant [EP/T028572/1]. The authors also
acknowledge the use of the University of Oxford Advanced Research Computing
(ARC) facility in carrying out this
work(http://dx.doi.org/10.5281/zenodo.22558).

## References

  * [1] Atlason, H.E., Love, A., Sigurdsson, S., Gudnason, V., Ellingsen, L.M.: Unsupervised brain lesion segmentation from mri using a convolutional autoencoder. In: Medical Imaging 2019: Image Processing. vol. 10949, pp. 372–378. SPIE (2019)
  * [2] Baid, U., Ghodasara, S., Mohan, S., Bilello, M., Calabrese, E., Colak, E., Farahani, K., Kalpathy-Cramer, J., Kitamura, F.C., Pati, S., et al.: The rsna-asnr-miccai brats 2021 benchmark on brain tumor segmentation and radiogenomic classification. arXiv preprint arXiv:2107.02314 (2021)
  * [3] Bakas, S., Akbari, H., Sotiras, A., Bilello, M., Rozycki, M., Kirby, J.S., Freymann, J.B., Farahani, K., Davatzikos, C.: Advancing the cancer genome atlas glioma mri collections with expert segmentation labels and radiomic features. Scientific data 4(1), 1–13 (2017)
  * [4] Baur, C., Denner, S., Wiestler, B., Navab, N., Albarqouni, S.: Autoencoders for unsupervised anomaly segmentation in brain mr images: a comparative study. Medical Image Analysis 69, 101952 (2021)
  * [5] Bercea, C.I., Neumayr, M., Rueckert, D., Schnabel, J.A.: Mask, stitch, and re-sample: Enhancing robustness and generalizability in anomaly detection through automatic diffusion models. arXiv preprint arXiv:2305.19643 (2023)
  * [6] Bercea, C.I., Rueckert, D., Schnabel, J.A.: What do aes learn? challenging common assumptions in unsupervised anomaly detection. In: International Conference on Medical Image Computing and Computer-Assisted Intervention. pp. 304–314. Springer (2023)
  * [7] Chappell, M.: Principles of Medical Imaging for Engineers. Springer International Publishing (2019)
  * [8] Havaei, M., Davy, A., Warde-Farley, D., Biard, A., Courville, A., Bengio, Y., Pal, C., Jodoin, P.M., Larochelle, H.: Brain tumor segmentation with deep neural networks. Medical image analysis 35, 18–31 (2017)
  * [9] Isensee, F., Jäger, P.F., Full, P.M., Vollmuth, P., Maier-Hein, K.H.: nnu-net for brain tumor segmentation. In: Brainlesion: Glioma, Multiple Sclerosis, Stroke and Traumatic Brain Injuries: 6th International Workshop, BrainLes 2020, Held in Conjunction with MICCAI 2020, Lima, Peru, October 4, 2020, Revised Selected Papers, Part II 6. pp. 118–132. Springer (2021)
  * [10] Kamnitsas, K., Ledig, C., Newcombe, V.F., Simpson, J.P., Kane, A.D., Menon, D.K., Rueckert, D., Glocker, B.: Efficient multi-scale 3d cnn with fully connected crf for accurate brain lesion segmentation. Medical image analysis 36, 61–78 (2017)
  * [11] Kascenas, A., Pugeault, N., O’Neil, A.Q.: Denoising autoencoders for unsupervised anomaly detection in brain mri. In: International Conference on Medical Imaging with Deep Learning. pp. 653–664. PMLR (2022)
  * [12] Liang, Z., Anthony, H., Wagner, F., Kamnitsas, K.: Modality cycles with masked conditional diffusion for unsupervised anomaly segmentation in mri. In: International Conference on Medical Image Computing and Computer-Assisted Intervention. pp. 168–181. Springer (2023)
  * [13] Liew, S.L., Lo, B.P., Donnelly, M.R., Zavaliangos-Petropulu, A., Jeong, J.N., Barisano, G., Hutton, A., Simon, J.P., Juliano, J.M., Suri, A., et al.: A large, curated, open-source stroke neuroimaging dataset to improve lesion segmentation algorithms. Scientific data 9(1), 320 (2022)
  * [14] Maier, O., Menze, B.H., Von der Gablentz, J., Häni, L., Heinrich, M.P., Liebrand, M., Winzeck, S., Basit, A., Bentley, P., Chen, L., et al.: Isles 2015-a public evaluation benchmark for ischemic stroke lesion segmentation from multispectral mri. Medical image analysis 35, 250–269 (2017)
  * [15] Oppenheim, A., Lim, J., Kopec, G., Pohlig, S.: Phase in speech and pictures. In: ICASSP’79. IEEE International Conference on Acoustics, Speech, and Signal Processing. vol. 4, pp. 632–637. IEEE (1979)
  * [16] Oppenheim, A.V., Lim, J.S.: The importance of phase in signals. Proceedings of the IEEE 69(5), 529–541 (1981)
  * [17] Pawlowski, N., Lee, M.C., Rajchl, M., McDonagh, S., Ferrante, E., Kamnitsas, K., Cooke, S., Stevenson, S., Khetani, A., Newman, T., et al.: Unsupervised lesion detection in brain ct using bayesian convolutional autoencoders (2018)
  * [18] Pinaya, W.H., Graham, M.S., Gray, R., Da Costa, P.F., Tudosiu, P.D., Wright, P., Mah, Y.H., MacKinnon, A.D., Teo, J.T., Jager, R., et al.: Fast unsupervised brain anomaly detection and segmentation with diffusion models. In: International Conference on Medical Image Computing and Computer-Assisted Intervention. pp. 705–714. Springer (2022)
  * [19] Rowley, P., Paukner, M., Eisenmenger, L., Field, A., Davidson, R., Johnson, S., Asthana, S., Chin, N., Prabhakaran, V., Bendlin, B., et al.: Incidental findings from 16,400 brain mri examinations of research volunteers. American Journal of Neuroradiology 44(4), 417–423 (2023)
  * [20] Stollenga, M.F., Byeon, W., Liwicki, M., Schmidhuber, J.: Parallel multi-dimensional lstm, with application to fast biomedical volumetric image segmentation. Advances in neural information processing systems 28 (2015)
  * [21] Xie, J., Li, W., Zhan, X., Liu, Z., Ong, Y.S., Loy, C.C.: Masked frequency modeling for self-supervised visual pre-training. arXiv preprint arXiv:2206.07706 (2022)
  * [22] Zimmerer, D., Isensee, F., Petersen, J., Kohl, S., Maier-Hein, K.: Unsupervised anomaly localization using variational auto-encoders. In: Medical Image Computing and Computer Assisted Intervention–MICCAI 2019: 22nd International Conference, Shenzhen, China, October 13–17, 2019, Proceedings, Part IV 22. pp. 289–297. Springer (2019)


sentence $\varphi$ of $\mathcal{L}_{\in}$ is valid in
$\mathbf{V}^{(\mathbb{A})}/\\!\sim$ if and only if it is valid in the algebra-
valued model $\mathbf{V}^{(\mathbb{A})}$, i.e.,
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi$ iff
$\mathbf{V}^{(\mathbb{A})}\models\varphi$. Then, as a corollary of Theorem
3.17, we get the following theorem.

######  Theorem 5.5.

Let $(\mathbb{A},D)$ be an ultra-designated $\mathsf{Cobounded}$-algebra.
Then, $\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\overline{\mathsf{ZF}}$.

In the case of building quotient models out of Boolean-valued models, first
the interpretation of the predicate symbols $\in$ and $=$ is given and only
then a definition of the validity of the rest of the formulas is provided.
Contrary to this order, in this paper, we first define the validity of all
formulas in Definition 5.3 and only later we provide the full interpretation
of $\in$ and $=$, which includes also the case of non-validity.

######  Definition 5.6.

We define the following binary relations on
$\mathbf{V}^{(\mathbb{A})}/\\!\sim$. For any
$u,v\in\mathbf{V}^{(\mathbb{A})}$,

$\displaystyle(i)$
$\displaystyle\left\\{\begin{array}[]{ll}R_{=}([u],[v])&\mbox{iff
}~{}\mathbf{V}^{(\mathbb{A})}\models u=v,\\\ R_{\neq}([u],[v])&\mbox{iff
}~{}\mathbf{V}^{(\mathbb{A})}\models\neg(u=v),\end{array}\right.$
$\displaystyle(ii)$
$\displaystyle\left\\{\begin{array}[]{ll}R_{\in}([u],[v])&\mbox{iff
}~{}\mathbf{V}^{(\mathbb{A})}\models u\in v,\\\ R_{\notin}([u],[v])&\mbox{iff
}~{}\mathbf{V}^{(\mathbb{A})}\models\neg(u\in v).\end{array}\right.$

######  Observation 5.7.

Applying Theorem 3.14, one can prove that the relations $R_{=}([u],[v])$,
$R_{\neq}([u],[v])$, $R_{\in}([u],[v])$, and $R_{\notin}([u],[v])$ are well-
defined.

As expected, the interpretations of the predicate symbols $=$ and $\in$ in the
quotient space $\mathbf{V}^{(\mathbb{A})}/\\!\sim$ are the binary relations
$R_{=}$ and $R_{\in}$, respectively. But, the construction differs from the
classical case when non-satisfaction is considered. In Theorem 5.9 and Theorem
5.10, we discuss this issue in full detail.

To keep the expressions simple, for any two elements
$[u],[v]\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$ we shall abbreviate
$(x=y)([u],[v])$, $\neg(x=y)([u],[v])$, $(x\in y)([u],[v])$, and
$\neg(x=y)([u],[v])$ as $[u]=[v]$, $[u]\neq[v]$, $[u]\in[v]$, and
$[u]\notin[v]$, respectively. Then, using Definition 5.3 and Definition 5.6 we
get the following fact.

######  Fact 5.8.

For any $[u],[v]\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$,

$\displaystyle(i)$
$\displaystyle\left\\{\begin{array}[]{ll}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]=[v]&\mbox{iff
}R_{=}([u],[v])\\\
\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\neq[v]&\mbox{iff
}R_{\neq}([u],[v]);\end{array}\right.$ $\displaystyle(ii)$
$\displaystyle\left\\{\begin{array}[]{ll}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\in[v]&\mbox{iff
}R_{\in}([u],[v]);\\\
\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\notin[v]&\mbox{iff
}R_{\notin}([u],[v]);\end{array}\right.$

######  Theorem 5.9.

For any ultra-designated $\mathsf{Cobounded}$-algebra $(\mathbb{A},D)$ and a
pair of elements $[u]$ and $[v]$ of $\mathbf{V}^{(\mathbb{A})}/\\!\sim$,

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\neq[v]\mbox{ iff
}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models[u]=[v].$

###### Proof.

Consider any two elements $[u],[v]$ of $\mathbf{V}^{(\mathbb{A})}/\\!\sim$.
Then,

$\displaystyle\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models[u]=[v]$
$\displaystyle\mbox{ iff}~{}([u],[v])\notin R_{=},$ $\displaystyle\mbox{by
Fact}~{}\ref{fact: satisfactions of atomic formulas}(i)$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}\not\models u=v,$ $\displaystyle\mbox{by
Definition}~{}\ref{Definition: Quotient space identity and belongniness}(i)$
$\displaystyle\mbox{ iff}~{}\llbracket u=v\rrbracket=\mathbf{0},$
$\displaystyle\mbox{since }\llbracket
u=v\rrbracket\in\\{\mathbf{0},\mathbf{1}\\}$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}\models\neg(u=v),$ since
$\mathbf{0}^{*}=\mathbf{1}\in D$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\neq[v],$ by Definition
5.6(i) and Fact 5.8(i).

∎

As a corollary we obtain that the two (class) relations $R_{=}$ and $R_{\neq}$
are disjoint. Moreover, it is easy to see that $R_{=}^{c}$, the complement of
$R_{=}$, is the class $R_{\neq}$. On the other hand, the two class relations
$R_{\in}$ and $R_{\notin}$ are exhaustive but not necessarily exclusive. This
is the content of the following theorem.

######  Theorem 5.10.

Let $(\mathbb{A},D)$ be an ultra-designated $\mathsf{Cobounded}$-algebra.
Then,

  1. (i)

for any $[u],[v]\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$, if
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models[u]\in[v]$, then
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\notin[v]$,

  2. (ii)

if $D\setminus\\{\mathbf{1}\\}\neq\varnothing$ then there exist
$[u],[v]\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$ such that
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\in[v]$ and
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\notin[v]$ both hold.

###### Proof.

(i) Consider $[u],[v]\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$ so that
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models[u]\in[v]$. By Fact 5.8(ii),
$([u],[v])\notin R_{\in}$, which implies that
$\mathbf{V}^{(\mathbb{A})}\not\models u\in v$, by Definition 5.6(ii). Hence,
$\llbracket u\in v\rrbracket\notin D$. Therefore by the definition of
designated $\mathsf{Cobounded}$-algebra, $\llbracket\neg(u\in
v)\rrbracket=\llbracket u\in v\rrbracket^{*}=\mathbf{1}\in D$. This leads to
the fact that $\mathbf{V}^{(\mathbb{A})}\models\neg(u\in v)$, i.e.,
$([u],[v])\in R_{\notin}$, i.e.,
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\notin[v]$.

(ii) Let us fix an element $a\in D\setminus\\{\mathbf{1}\\}$. By definition we
have $a^{*}=a$. Now consider any element $u\in\mathbf{V}^{(\mathbb{A})}$ and
fix the element $v\in\mathbf{V}^{(\mathbb{A})}$, where $v=\\{\langle
u,a\rangle\\}$. Then,

$\llbracket u\in v\rrbracket=(v(u)\wedge\llbracket
u=u\rrbracket)=(a\wedge\mathbf{1})=a\in D.$

Moreover, $\llbracket\neg(u\in v)\rrbracket=a^{*}=a\in D$. Hence, we get that
$\mathbf{V}^{(\mathbb{A})}\models(u\in v)\wedge\neg(u\in v)$, i.e.,
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\in[v]$ and
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models[u]\notin[v]$ both hold. ∎

The theorem above shows that, if there exists an element in the designated set
other than the top element, then $R_{\in}\cap R_{\notin}\neq\varnothing$.

######  Theorem 5.11.

Let $(\mathbb{A},D)$ be an ultra-designated $\mathsf{Cobounded}$-algebra.
Then, for a sequence $\vec{[u]}=([u_{1}],[u_{2}],...)$ in
$\mathbf{V}^{(\mathbb{A})}/\\!\sim$ we have the following:

  1. (i)

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\varphi\rightarrow\psi)(\vec{[u]})$
iff $\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models\varphi(\vec{[u]})$ or
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\psi(\vec{[u]})$,

  2. (ii)

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\varphi\wedge\psi)(\vec{[u]})$
iff $\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi(\vec{[u]})$ and
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\psi(\vec{[u]})$,

  3. (iii)

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\varphi\vee\psi)(\vec{[u]})$ iff
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi(\vec{[u]})$ or
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\psi(\vec{[u]})$,

  4. (iv)

if $\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models\varphi(\vec{[u]})$, then
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\neg\varphi(\vec{[u]})$,

  5. (v)

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\forall x_{k}\varphi)(\vec{[u]})$
iff
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi\big{(}\vec{[u]}(d/k)\big{)}$,
for all $d\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$, where $\vec{[u]}(d/k)$ is
identified with the sequence $([u_{1}],\ldots,[u_{k-1}],d,[u_{k+1}],\ldots)$,
and

  6. (vi)

$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\exists x_{k}\varphi)(\vec{[u]})$
iff
$\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi\big{(}\vec{[u]}(d/k)\big{)}$,
for some $d\in\mathbf{V}^{(\mathbb{A})}/\\!\sim$.

###### Proof.

Since $D$ is an ultrafilter of $\mathbb{A}$, by Lemma 2.12 we have that
$\mathbf{A}\setminus D=\\{\mathbf{0}\\}$, where $\mathbf{A}$ is the underlying
set of $\mathbb{A}$.

$\displaystyle(i)~{}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\varphi\rightarrow\psi)(\vec{[u]})$
$\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}~{}\models(\varphi\rightarrow\psi)(\vec{u})$
$\displaystyle\mbox{
iff}~{}\llbracket(\varphi\rightarrow\psi)(\vec{u})\rrbracket\in D$
$\displaystyle\mbox{
iff}~{}\llbracket(\varphi\rightarrow\psi)(\vec{u})\rrbracket\neq\mathbf{0},\mbox{
since}~{}\mathbf{A}\setminus D=\\{\mathbf{0}\\}$ $\displaystyle\mbox{
iff}~{}\big{(}\llbracket\varphi(\vec{u})\rrbracket\Rightarrow\llbracket\psi(\vec{u})\rrbracket\big{)}\neq\mathbf{0}$
$\displaystyle\mbox{
iff}~{}\llbracket\varphi(\vec{u})\rrbracket=\mathbf{0}\mbox{
or}~{}\llbracket\psi(\vec{u})\rrbracket\neq\mathbf{0}$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}\not\models\varphi(\vec{u})\mbox{
or}~{}\mathbf{V}^{(\mathbb{A})}\models\psi(\vec{u}),\mbox{
applying}~{}\mathbf{A}\setminus D=\\{\mathbf{0}\\}$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\not\models\varphi(\vec{[u]})\mbox{
or}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\psi(\vec{[u]}).$

The proofs of (ii), (iii), and (iv) can also be done similar to (i), using
Lemma 2.12.

$\displaystyle(v)~{}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models(\forall
x_{k}\varphi)(\vec{[u]})$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}~{}\models(\forall x_{k}\varphi)(\vec{u})$
$\displaystyle\mbox{
iff}~{}\bigwedge_{v\in\mathbf{V}^{(\mathbb{A})}}\llbracket\varphi\big{(}\vec{u}(v/k)\big{)}\rrbracket\in
D,$ where $\vec{u}(v/k)$ is the sequence
$(u_{1},\ldots,u_{k-1},v,u_{k+1},\ldots)$ $\displaystyle\mbox{
iff}~{}\llbracket\varphi\big{(}\vec{u}(v/k)\big{)}\rrbracket\in D,\mbox{ for
all}~{}v\in\mathbf{V}^{(\mathbb{A})},$ the forward direction is immediate, for
the other direction $\displaystyle\qquad\mbox{ we use property (iii) of
Definition \ref{Definition: MTV algebra} and}~{}\mathbf{A}\setminus
D=\\{\mathbf{0}\\}$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}\models\varphi\big{(}\vec{u}(v/k)\big{)},\mbox{
for all}~{}v\in\mathbf{V}^{(\mathbb{A})}$ $\displaystyle\mbox{
iff}~{}\mathbf{V}^{(\mathbb{A})}/\\!\sim~{}\models\varphi\big{(}\vec{[u]}(d/k)\big{)},\mbox{
for all}~{}d\in\mathbf{V}^{(\mathbb{A})}/\\!\sim.$

(vi) It can be proved as (v), because for any subset $\\{a_{i}~{}:~{}i\in
I\\}$ of $\mathbf{A}$, $\bigvee\limits_{i\in I}a_{i}\in D$ implies that there
exists $j\in I$ such that $a_{j}\in D$ as $\mathbf{A}\setminus
D=\\{\mathbf{0}\\}$. ∎

Observe that only the property (iv) of Theorem 5.11 is not expressed as a
necessary and sufficient condition. Indeed, the missing direction of property
(iv) fails. For a concrete example, consider the formula $\varphi(x,y):=x\in
y$ and use Theorem 5.10(ii). Moreover, we conclude this section, by pointing
out that the same exact sentences $\varphi$ and $\psi$ of Lemma 4.6 witness
that the underlying logic of the set theory having a model
$\mathbf{V}^{(\mathbb{A})}/\\!\sim$ is paraconsistent.

##  6\. Comparison with other models of paraconsistent set theories

In this section, we compare the paraconsistent models we developed in this
paper with models of paraconsistent set theories that we find in the
literature. In particular, we will address the models produced by Priest’s
model-theoretic approach given that they are the only paraconsistent models of
set theory in which all $\mathsf{ZF}$-axioms are valid. We will argue that our
approach overcomes the limits of Priest’s model-theoretic approach to
paraconsistent set theory. In short we will argue that in the models presented
in this paper $\mathsf{ZF}$ holds consistently and not only paraconsistently.
By this we mean that in our models $\mathsf{ZF}$ are only valid and not, also,
not valid. In this sense, those presented here are the first proper (from a
classical perspective) paraconsistent models of $\mathsf{ZF}$.

The model-theoretic approach has been put forward in [Priest, 2006, Section
18.4] and [Priest, 2017, Section 11]. In order to keep things short, we will
assume some familiarity with these papers. The basic idea of the model-
theoretic approach of Priest consists in finding an equivalence relation which
allows us to collapse a model of $\mathsf{ZF}$ into a model of
$\mathsf{NLP}_{=}+\mathsf{ZF}$666By $\mathsf{NLP}_{=}$ we denote the set
theory that we obtain by combining the axioms of naïve set theory, i.e.,
Extensionality and Comprehension with the logical axioms of LP=, where LP=
denotes the first-order version of the Logic of Paradox, LP extended with a
binary predicate $=$, where $x=y$ receives value $\mathbf{1}$ or $\frac{1}{2}$
just in case $x$ equals $y$ (in the meta-theory). and which, moreover,
contains a large fragment of the cumulative hierarchy as an inner model.
Priest proposes two equivalence relations: the type-lift and the Hamkins type-
lift.

Let us sketch one of these constructions. In the case of the type-lift, we
start with a model of ZF with two inaccessible cardinals, say, $\kappa_{1}$
and $\kappa_{2}$. While everything is preserved below $V_{\kappa_{1}}$, on the
other hand, everything is collapsed between $V_{\kappa_{1}}$ and
$V_{\kappa_{2}}$. The resulting object of such a collapse, call it $a$, is
what witnesses the paraconsistency of the model. Instead, the standard
hierarchy below $\kappa_{1}$ is responsible for the validity of ZF in a
cumulative hierarchy. Applying this construction we obtain the following
important result.

######  Theorem 6.1 ([Priest, 2006]).

Suppose that $\mathcal{M}$ is a classical model of $\mathsf{ZF}$ containing
two inaccessible cardinals $\kappa_{1}$ and $\kappa_{2}$. Then there is an LP-
model $\mathcal{M}^{\sim}=\langle D^{\sim},I^{\sim}\rangle$ such that:

  1. (i)

$\mathcal{M}^{\sim}$ is a model of _ZF_ $+$ $\mathsf{NLP}_{=}$ and

  2. (ii)

$\mathcal{M}^{\sim}$ contains a model $\mathcal{N}$ where $\mathcal{N}$ is a
classical model of $\mathsf{ZF}$.

For completeness, let us very briefly address the Hamkins type-lift. An
important fact about this second construction is that Theorem 6.1 also holds
for it. The Hamkins type-lift models constitutes an improvement over the type-
lift models given that different sets witness different instances of
$\mathsf{Comprehension}$ thus providing more discriminating models; which was
not the case for the models obtained by means of the type-lift. Although we
have an advance on the set theoretical side, however, this new construction
manifests a decisive drawback on the logical side. Indeed, the treatment of
identity is highly non-standard, since Leibniz’s law of indiscernibility of
identicals fails in the models obtained by the Hamkins type-lift construction.
On the other hand, for any $\mathbf{V}^{(\mathbb{A})}/\\!\sim$, Leibniz’s law
of indiscernibility of identicals holds. This provides a classical treatment
for the notion of identity, as witnessed by Theorem 3.14. For this reason, we
concentrate on the comparison between our models and the original Priest’s
type-lift models.

Before presenting the point of difference between the models presented in this
paper and the type-lift ones, it is worth reporting Priest’s view, who was not
completely satisfied with the type-lift constructions.

> Clearly, the collapsed model just constructed is not a very interesting
> one.The much over worked $a$ is the witness set for every condition. But it
> suffices to establish that there are interpretations of both ZF and naive
> set theory. ([Priest, 2017], p. 48)

We believe that the models discussed here fares better than Priest’s in
providing a paraconsistent version of $\mathsf{ZF}$ for the following reasons.

  1. (1)

The paraconsistency of the present models does not come from a single set on
top of the hierarchy, but it is widespread in the cumulative hierarchy and
witnessed by many different sets along the hierarchy (see Theorem 4.7). In a
slogan, we can say that these algebra-valued models provide a paraconsistent
cumulative hierarchy, while Priest’s ones a cumulative hierarchy together with
a paraconsistent set (which is somewhat isolated from the rest).

  2. (2)

The models presented in this paper do not validate the axiom of (unrestricted)
Comprehension. Thus, the corresponding set theory is different from that of
Priest’s models. This is an important point from a classical perspective,
since these results show how close we can get to a classical cumulative
hierarchy, but with a non-classical logic.

  3. (3)

Not only the axioms of ZF are all valid in any
$\mathbf{V}^{(\mathbb{A})}/\\!\sim$, but it is also important to observe that
their negation do not hold in these models. In this case, we can say that ZF
holds _consistently_. This is a trivial observation in the classical context,
which, however, is not obvious in a paraconsistent context. For example, in
the models obtained by a type-lifting construction the Separation Schema holds
together with its negation. In this case we can say that $\mathsf{ZF}$ holds
_paraconsistently_.

This last point has been objects of criticism. Very recently Incurvati wrote
the following.

> Indeed, as Priest (2017: 98) points out, once inconsistent sets enter the
> picture, it can be shown that if ZF’s Separation Schema is true, it is both
> true and false. What this brings to light is that the paraconsistent set
> theorist needs, after all, to say more about what the universe of sets looks
> like. It is not enough to simply suppose that it contains some paradigmatic
> inconsistent sets and has the cumulative hierarchy as an inner model.
> ([Incurvati, 2020], p.126)

We believe that the structures built in this paper address exactly the issue
raised by the above quotation. Not only we have paraconsistent models where
$\mathsf{ZF}$ holds consistently, but the similarity these structures bear
with V leave no mystery with respect to what they look like: a very familiar
cumulative hierarchy.

Since these new structures satisfy both requirements of being paraconsistent
and being non-trivial models of $\mathsf{ZF}$, i.e., validating these axioms
consistently (as witnessed by the validity of Theorem 3.11 and Theorem 4.5),
we can claim that they are the first example of non-trivial paraconsistent
models of $\mathsf{ZF}$.

##  7\. Generalising the approach

We end the paper with a few questions that the present approach to non-
classical models of set theory suggests. Besides the construction of non-
trivial paraconsistent models of set theory in which $\mathsf{ZF}$ hold
consistently, this paper introduces a novelty in the algebra-valued
constructions: the change of the interpretation function. We applied this idea
here to the construction of paraconsistent models of $\mathsf{ZF}$, but
nothing prevents us to generalise the technique to fit other logical
environments.777Some interesting preliminary results have been obtain with
respect to Heyting-valued models. We leave to a next time a full discussion of
this other case. Table 1 and Table 2 give an overview of the study made in
this paper, which help to analyze the open questions raised in this section.

| Axioms of $\mathsf{ZF}$ | Axioms of $\overline{\mathsf{ZF}}$ | $\mathsf{LL}_{\varphi}$ | $\mathbf{L}(\llbracket\cdot\rrbracket,\mathbf{V}^{(\mathbb{A})})$
---|---|---|---|---
$\llbracket\cdot\rrbracket_{\mathrm{BA}}$ | Valid | Valid | Valid | Not known in general.
|  |  |  | Classical, for atomic Boolean algebras.
$\llbracket\cdot\rrbracket_{\mathrm{PA}}$ | Valid | Valid | Valid | Not known in general.
|  |  |  | Classical, for atomic Boolean algebras.
Table 1. With respect to Boolean-valued models, $\mathbf{V}^{(\mathbb{A})}$. | Axioms of $\mathsf{ZF}$ | Axioms of $\overline{\mathsf{ZF}}$ | $\mathsf{LL}_{\varphi}$ | $\mathbf{L}(\llbracket\cdot\rrbracket,\mathbf{V}^{(\mathbb{A})})$
---|---|---|---|---
$\llbracket\cdot\rrbracket_{\mathrm{BA}}$ |  $\mathrm{NFF}$-$\mathsf{ZF}$ is valid |  $\mathrm{NFF}$-$\mathsf{ZF}+\overline{\mathsf{Extensionality}}$ | Fails for some $\varphi$ | Paraconsistent
|  | is valid |  |
$\llbracket\cdot\rrbracket_{\mathrm{PA}}$ | $\mathsf{ZF}-\mathsf{Extensionality}$ | Valid | Valid | Paraconsistent
| is valid |  |  |
Table 2. With respect to ultra-designated $\mathsf{Cobounded}$-algebra valued
models, $\mathbf{V}^{(\mathbb{A})}$, where $\mathbb{A}$ has more than two
elements.

The first one deals with the scope of the validity of the Zermelo-Fraenkel
axioms and their correct formulation. Indeed, notice that
$\llbracket\cdot\rrbracket_{\mathrm{BA}}$ only provides Boolean-valued models
of $\mathsf{ZF}$, while $\llbracket\cdot\rrbracket_{\mathrm{PA}}$ both Boolean
and ultra-designated $\mathsf{Cobounded}$-algebra-valued models of
$\overline{\mathsf{ZF}}$. From this perspective both
$\llbracket\cdot\rrbracket_{\mathrm{PA}}$ and $\overline{\mathsf{ZF}}$ are
more inclusive since they capture a larger class of models for Zermelo-
Fraenkel set theory.

Question 1 Is there a maximal class $\mathcal{X}$ of algebras and a couple
$(\mathsf{ZF}^{X},\llbracket\cdot\rrbracket_{\mathrm{X}})$, with
$\mathsf{ZF}^{X}$ an axiomatic system classically equivalent to $\mathsf{ZF}$
and $\llbracket\cdot\rrbracket_{\mathrm{X}}$ an interpretation function, such
that
$\mathbf{V}^{(\mathbb{X},~{}\llbracket\cdot\rrbracket_{\mathrm{X}})}\models\mathsf{ZF}^{X}$,
for $\mathbb{X}\in\mathcal{X}$?

Notice that there is no obvious reason why this attempt of maximising the
class of models that validate an appropriate version of $\mathsf{ZF}$ should
yield a unique result. If this is indeed the case, however, we would obtain an
interesting relativization of the notion of independence.

Question 2 Assume that there exist two couples
$(\mathsf{ZF}^{X},\llbracket\cdot\rrbracket_{\mathrm{X}})$ and
$(\mathsf{ZF}^{Y},\llbracket\cdot\rrbracket_{\mathrm{Y}})$ that define two
maximal but incompatible classes of models $\mathcal{M}_{\mathcal{X}}$ and
$\mathcal{M}_{\mathcal{Y}}$, each validating the appropriate version of
$\mathsf{ZF}$ and both extending the class of Boolean-valued models. Then, is
it possible to find a sentence in the pure language of set theory,
$\mathcal{L}_{\in}$, that is independent from $\mathsf{ZF}^{X}$ but not from
$\mathsf{ZF}^{Y}$? In other terms, is it possible to show that the notion of
independence is not absolute?

An interesting aspect of the above question is that it does not necessarily
need a non-classical logical environment. As a matter of fact, once we start
modifying the interpretation function, we can raise the same issue in a purely
classical context.

Question 2∗ Is there an assignment function
$\llbracket\cdot\rrbracket_{\mathrm{BA}^{\prime}}$ from a
$\mathcal{L}_{\mathbb{B}}$-language into a Boolean algebra $\mathbb{B}$, such
that all $\mathsf{ZF}$ axioms receive value $\mathbf{1}$, but where there are
formulas in the pure language of set theory, $\mathcal{L}_{\in}$, which
receive value $\mathbf{1}$ under
$\llbracket\cdot\rrbracket_{\mathrm{BA}^{\prime}}$, but not under
$\llbracket\cdot\rrbracket_{\mathrm{BA}}$?

Another interesting question about these non-classical models is whether they
can be used to produce (possibly new) classical models.

Question 3888We thank Joel D. Hamkins for this interesting suggestion. Is it
possible to define a two step iteration in which the first step is non-
classical, but the second is classical? More concretely, is it possible to
find a Boolean algebra $\mathbb{B}$ within a ultra-designated
$\mathsf{Cobounded}$-algebra-valued model
$\mathbf{V}^{(\mathbb{T},~{}\llbracket\cdot\rrbracket_{\mathrm{PA}})}$ and to
build from there a Boolean-valued model
$\big{(}\mathbf{V}^{(\mathbb{T},~{}\llbracket\cdot\rrbracket_{\mathrm{PA}})}\big{)}^{(\mathbb{B},~{}\llbracket\cdot\rrbracket_{\mathrm{BA}})}$?
If this is the case, is it possible to obtain this new Boolean-valued model as
a Boolean-valued extension of $\mathbf{V}$? In other terms, is
$\big{(}\mathbf{V}^{(\mathbb{T},~{}\llbracket\cdot\rrbracket_{\mathrm{PA}})}\big{)}^{(\mathbb{B},~{}\llbracket\cdot\rrbracket_{\mathrm{BA}})}$
a new classical model?

Finally, it would be interesting to precisely determine the extension of the
class of models that we investigated in this paper.

Question 4 Is there an algebraic way to describe the class of structures that
validate $\overline{\mathsf{ZF}}$ under
$\llbracket\cdot\rrbracket_{\mathrm{PA}}$?

Acknowledgments. The first author acknowledges support from the FAPESP grant.
n. 2017/23853-0. The second author wants to acknowledge FAPESP for providing
him a Visiting Researcher grant (n. 2016/25891-3) to spend one year at the
Philosophy Department of the University of Campinas. The third author
acknowledges support from FAPESP, Jovem Pesquisador grant (n. 2016/25891- 3),
and from CNPq grant (n. 301108/2019-6).

## References

  * [Antos et al., 2015] Antos, C., Friedman, S., Honzik, R., and Ternullo, C. (2015).  Multiverse conceptions in set theory.  Synthese, 192(8):2463–2488.
  * [Bell, 2005] Bell, J. (2005).  Set theory. Boolean valued models and independence proofs.  Oxford Science Pubblications.
  * [Grayson, 1977] Grayson, R. J. (1977).  Heyting-valued models for intuitionistic set theory.  In Fourman, M. P., Mulvey, C. J., and Scott, D. S., editors, Applications of sheaves, Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra and Analysis, volume 753, pages 402–414. Berlin: Springer.
  * [Incurvati, 2020] Incurvati, L. (2020).  Conceptions of Set and the Foundations of Mathematics.  Cambridge University Press.
  * [Jockwich et al., 2022] Jockwich, S., Tarafder, S., and Venturi, G. (2022).  Ideal Objects for Set Theory.  Journal of Philosophical Logic, page Online First.
  * [Jockwich-Martinez and Venturi, 2021a] Jockwich-Martinez, S. and Venturi, G. (2021a).  Non-classical models of $\mathrm{ZF}$.  Studia Logica, 109:509–537.
  * [Jockwich-Martinez and Venturi, 2021b] Jockwich-Martinez, S. and Venturi, G. (2021b).  On negation for non-classical set theories.  Journal of Philosophical Logic, 50:549–570.
  * [Löwe et al., 2021] Löwe, B., Passmann, R., and Tarafder, S. (2021).  Constructing illoyal algebra-valued models of set theory.  Algebra Universalis, 82(46).
  * [Löwe and Tarafder, 2015] Löwe, B. and Tarafder, S. (2015).  Generalized algebra-valued models of set theory.  Review of Symbolic Logic, 8(1):192–205.
  * [Maddy, 2016] Maddy, P. (2016).  Set-theoretic foundations.  In Caicedo, A. E., Cummings, J., Koellner, P., and Larson, P. B., editors, Foundations of Mathematics. American Mathematical Society.
  * [Priest, 2006] Priest, G. (2006).  In Contradiction: A Study of the Transconsistent.  Oxford University Press.
  * [Priest, 2017] Priest, G. (2017).  What if? the exploration of an idea.  Australasian Journal of Logic, 14(1).
  * [Tarafder, 2022] Tarafder, S. (2022).  Non-classical foundation of set theory.  The Journal of Symbolic Logic, 87(1):347 – 376.
  * [Tarafder and Chakraborty, 2016] Tarafder, S. and Chakraborty, M. K. (2016).  A paraconsistent logic obtained from an algebra-valued model of set theory.  In Beziau, J. Y., Chakraborty, M. K., and Dutta, S., editors, New Directions in Paraconsistent Logic, 5th WCP, volume 152, pages 165–183. New Delhi: Springer.
  * [Tarafder and Venturi, 2021] Tarafder, S. and Venturi, G. (2021).  Independence proofs in non-classical set theories.  Review of Symbolic Logic, First view:1–32.
  * [Tarafder and Venturi, 2022] Tarafder, S. and Venturi, G. (2022).  ZF between classicality and non-classicality.  Studia Logica, 110:189–218.
  * [Venturi, 2016] Venturi, G. (2016).  Forcing, multiverse and realism.  In Boccuni, F. and Sereni, A., editors, Objectivity, Knowledge and Proof. _FIlMat_ Studies in the Philosophy of Mathematics, pages 211–241. Springer.