# Efficient Verification-Based Face Identification

Amit Rozner∗1 Barak Battash∗1 Ofir Lindenbaum1 and Lior Wolf2
1 Faculty of Engineering, Bar Ilan University 2 School of Computer Science,
Tel Aviv University ∗ These authors contributed equally.

###### Abstract

We study the problem of performing face verification with an efficient neural
model $f$. The efficiency of $f$ stems from simplifying the face verification
problem from an embedding nearest neighbor search into a binary problem; each
user has its own neural network $f$. To allow information sharing between
different individuals in the training set, we do not train $f$ directly but
instead generate the model weights using a hypernetwork $h$. This leads to the
generation of a compact personalized model for face identification that can be
deployed on edge devices. Key to the method’s success is a novel way of
generating hard negatives and carefully scheduling the training objectives.
Our model leads to a substantially small $f$ requiring only 23k parameters and
5M floating point operations (FLOPS). We use six face verification datasets to
demonstrate that our method is on par or better than state-of-the-art models,
with a significantly reduced number of parameters and computational burden.
Furthermore, we perform an extensive ablation study to demonstrate the
importance of each element in our method.

##  I Introduction

Face recognition is often tackled as a multiclass classification task in which
a different class represents each identity. However, this paradigm leads to
fixed identities based on those observed during training. A more general
approach is to perform matching using the learned representation [1]. This
basic form of transfer learning has proven scalable and relatively efficient
[2].

Sometimes, however, the resources needed to compute the representation are
infeasible, e.g., for edge devices with limited resources. Common restrictions
involve limited memory footprint and energy consumption. Various edge devices
require different types of optimizations. For example, mobile phones, laptops,
and tablets require energy consumption optimization to achieve enhanced
battery life, which is a top priority for such devices [3]. Additional
challenges are often faced in IP cameras, smart doors, and other internet-of-
things (IoT) devices with low compute and memory resources [4, 5].

The prevailing approach for addressing the face recognition challenge involves
employing a large overparameterized deep neural network (DNN). Such a network
is proficient at converting a facial image into a vector within an embedding
space. Each identity has at least one face image, represented using an
embedding vector in the database. During the inference phase, each facial
image must undergo processing through an extensive DNN to generate an
embedding vector, facilitating subsequent comparisons with vectors stored in
the database. Consequently, the computational expense of the inference
operation is influenced directly by the complexity of the DNN. Prior research
efforts have proposed using more lightweight DNN architectures to mitigate
this computational burden. In this research project, we are interested in the
face verification setting, in which we want to learn a model specific to one
or a few identities.

In such cases, it makes sense to consider a verification-based paradigm, in
which one trains much smaller networks, each designed to identify a specific
individual, thus simplifying the face identification problem. Suppose the
number of individuals in the gallery is not large. In this case, this ensemble
of binary classifiers may be more efficient than the representation-based
approach, especially on edge devices, such as mobile phones, where only a
single user is enrolled in the system.

Training multiple binary classifiers, however, has an inherent limitation in
that the benefit of knowledge sharing is mainly lost. Face identification
requires invariance to pose, illumination, expression, background, and other
factors. When training a deep multiclass classifier, this invariance is
manifested in the various layers, and learning to be pose-invariant on the
images of one person, for example, can be beneficial for identifying others.
Further, the binary classifier needs to be trained for each enrolled user.
This results in a prolonged “sign-up” process with additional computational
costs. Fine-tuning deep neural networks using a single or a few user images is
challenging, even if the backbone is pre-trained.

Some knowledge sharing is possible through shared layers in the ensemble of
binary classifiers. However, knowledge sharing occurs at all levels (both low-
level vision and high-level). Moreover, due to the application demands, the
binary networks need to be of low capacity, and sharing some of the layers
would reduce the ability to adapt to the new identities.

In this work, we suggest an alternative solution in which a hypernetwork [6]
$h$ is trained to generate, given a single image $x^{i}_{enroll}$ of a person
$i$, the weights $\theta^{i}$ of a verification network $f(\theta^{i})$ that
identifies the specific individual $i$. Our model is trained using weighted
binary cross-entropy loss, and we introduce a new method for effective hard
negative mining. The new scheme, termed $K$-means centered sampling (KCS),
helps our model learn a more discriminative function by constructing batches
containing similar identities. We benchmark our method using six publicly
available datasets and demonstrate that it can dramatically reduce the number
of parameters while maintaining highly competitive results.

In the following sections, we detail the background of our work II as well as
its related research III. Then, we provide a detailed description of our
method in section IV. Following this, we present the experiments we conducted
in section V, which is followed by a discussion VI and conclusions VII
sections.

##  II Background

Facial recognition involves recognizing a person enrolled in a database by
their facial image. The two main tasks in facial recognition are face
verification (one-to-one matching 1:1) and face identification (one-to-many
matching 1:N). Face verification involves comparing two facial images from a
database and another non-database image (query image). Then, the system
decides whether the person in the query image is of the same identity as in
the database image. Face identification involves authenticating a person’s
identity, considering multiple identities in the database. Since face
verification involves a 1-to-1 matching, it is often a more straightforward
task, which requires less computational effort and provides higher accuracy
than identification.

Face identification is used for surveillance [7], access control [8, 9], law
enforcement [10], etc. It often involves a large amount of identities in the
database. This may require the model to run on designated hardware with high
power and computing capabilities. For some applications, edge devices are
power consumption bounded by battery and/or heat limitations. Thus, using huge
and power-demanding models is less common in real-world applications. This
issue can sometimes be mitigated by offloading the DNN computations to the
cloud, which produces more significant latency and additional costs. Face
verification is commonly used in granting access to personal mobile devices,
tablets, or computers, payment verification, and more. Despite the significant
difference between the two tasks, the standard way of solving them is
typically based on the same framework.

Deep learning is the main driver behind modern face recognition systems. Many
systems are based on a deep neural network $h_{bb}$, which projects an input
face image $x_{enroll}$ to an embedding vector
$e_{enroll}=h_{bb}(x_{enroll})$, where $e_{enroll}\in R^{d}$ and $d$ is the
embedding dimension. Face recognition consists of two phases: enrollment and
authentication. In the enrollment stage, a face image of a person $i$ is fed
to $h_{bb}$, generating a unique feature vector $e^{i}_{enroll}$ based on
their unique facial characteristics. $e^{i}_{enroll}$ is then stored in a
database $D\in R^{N\times d}$, where $N$ is the number of faces stored in the
database.

The difference between identification and verification tasks can be formally
defined by $N$, where $N>1$, and $N=1$ are used in identification and
verification, respectively. For authentication, a face image $x_{auth}$ is fed
to the feature extractor $e_{auth}=h_{bb}(x_{auth})$, where $e_{auth}$ is the
embedding vector of $x_{auth}$. For the verification task, $e_{auth}$ is
compared to $e^{i}_{enroll}$ using a predefined distance metric, such as the
L2 distance, cosine similarity, or similar. Suppose the distance between the
two embedding vectors is lower than a threshold. In that case, the face is
authenticated as belonging to the same identity, i.e., $x_{auth}$ is an image
of person $i$. For identification, the authentication is performed in two
phases. The initial search is typically performed using a $K$-Nearest-
Neighbours [11] algorithm or similar that identifies the closest embedding
$e^{nearest}_{enroll}$ and performs verification between
$e^{nearest}_{enroll}$ and $e_{auth}$ using the threshold scheme discussed
above.

Since DNNs attempt to embed a large set of diverse faces, the required network
size is very demanding. We argue that a paradigm shift in this approach may
prove beneficial. Instead of generating embeddings for each input face image,
developing a more compact DNN that can authenticate the identity of a specific
given face would be advantageous. This simplified approach may significantly
reduce model size, minimizing the need for cloud computing and significantly
decreasing power consumption, thereby positively impacting battery life.

##  III Related Work

###  III-A Deep Embedding Neural Networks for Facial Recognition

In recent years, DNNs have been widely used for face recognition tasks.
Schroff et al. [12] used a Triplet loss to improve performance on challenging
facial recognition datasets. Additional progress was made by Liu et al. [13],
who suggested an improvement to the well-known Softmax loss, termed L-Softmax
loss. It encourages intra-class compactness and inter-class separation between
the learned embedding features. Liu et al. [14] introduced the concept of an
angular margin loss combined with the standard Softmax loss function. Removing
the Softmax and applying a Cosine margin loss to the target logit helped Wang
et al. [15] to achieve superior performance over its predecessors. ArcFace
[16] used a geodesic distance over a hypersphere, showing improved
discriminative power and a stable training process. Using image quality
estimation by the embedding norm, Kim et al. [17] claimed that adapting the
ArcFace by each sample’s quality will lead to significant gains. Their
proposed loss, termed AdaFace, achieved state-of-the-art (SOTA) results on
challenging low-quality and high-quality datasets.

###  III-B Face Recognition on Edge Devices

Edge devices do not have the power and computing abilities required to run
SOTA facial recognition models, such as [18, 19]. This has led to the
development of efficient neural networks designed to minimize memory and power
consumption while maintaining high accuracy. Creating such efficient models
requires considerable effort and may involve methods such as pruning [20, 21],
quantization [22], and hardware-aware neural architecture search [23]. In
recent years, researchers have made significant progress in developing
efficient facial recognition models, downscaling them to sizes as small as
half a million parameters [24].

Several attempts were made to convert lightweight generic computer vision
models for facial recognition tasks to mitigate this issue. An early attempt
was made by Chen et al. [25] using a modified MobileNetV2 [26] architecture
trained for the face verification task with the ArcFace [16] loss. They
achieved real-time yet competitive results using less than 1M parameters.
Subsequently, Martindez-Diaz et al. [24] suggested multiple architectures that
resemble ShuffleNetV2 [27] with a parameter range from 0.5M to 4.5M. Then,
Martinez-Diaz et al. [28] introduced MobileFaceNetV1, which utilized separable
convolution to decrease the computational complexity, and ProxylessFaceNAS,
which added the inverted residual block to its neural architecture space, thus
increasing efficiency. Recently, Hoo et al. [29] achieved further parameter
reduction by using modified ConvNeXt [30] blocks. While former works used
convolutional neural networks (CNNs), Hoo et al. [31] introduced attention
modules, achieving further progress. Another approach by George et al. [32]
combines CNN with Transformer architectures and a low-rank linear layer to
reach further SOTA results when training on the WebFace12M dataset [33].

###  III-C HyperNetwork Neural Network Architecture

HyperNetwork, a term introduced in [6], is a general name for a neural network
model that predicts the weights of another neural network, usually referred to
as a target network or a primary network. The target network performs the
actual task for which the training was done. Since its inception, it has been
a highly successful architecture for many learning tasks, such as uncertainty
estimation via Bayesian inference [34], generating weights for DNNs of related
tasks, i.e., continual learning [35], enabling better compression in resource-
limited use cases compared to embedding neural networks [36, 37, 38], training
multiple target DNNs faster [39], and more [40, 41]. We want to use a
hypernetwork as a facial recognition classifier, where the target model will
be deployed on the edge.

##  IV Method

Our method consists of two main parts: a single hypernetwork $h$ located on
the cloud (while not obligatory), which generates weights $\theta^{i}$ for a
personal neural network $f(\theta^{i})$, where $i$ is the user ID. Each user’s
interaction with hypernetwork $h$ is a one-time occasion only during
enrollment. The hypernetwork $h$ comprises two blocks: $h_{gen}$ and $h_{bb}$,
in the following manner:

$h=h_{gen}\circ h_{bb}.$ (1)

The first is a pre-trained face recognition embedding model $h_{bb}$, which is
frozen for the entire training process. This block helps us extract face
features using a strong pretrained DNN. The second part, $h_{gen}$, is a DNN
that receives face information produced by $h_{bb}$ and generates weights
$\theta^{i}$ for a user’s personal model $f(\theta^{i})$. Next, we rigorously
define each component in our system while describing the three phases:
enrollment, inference, and training. Although the training phase is the first
chronologically, we start from the enrollment and inference phases to better
motivate our novel suggested paradigm.

###  IV-A Enrollment Phase

The enrollment phase is the process of inserting an identity $i$ into the
database. This enables comparing new unknown images to the enrolled identity
and making decisions, such as granting access to a location or software at
inference time. In the enrollment phase, unlike standard face recognition
methods, our DNN does not generate and save embeddings in a database but
generates a tiny DNN that is sent to the users’ edge devices. In more detail,
a user enrolls to the system by taking one facial image
$\hat{x}^{i}_{enroll}\in\mathbb{R}^{H\times W\times 3}$, where $H,W$ are the
input width and height, and 3 is the color dimension. The image is pre-
processed using standard face alignment, as in [17]. The preprocessed image,
$x^{i}_{enroll}\in\mathbb{R}^{h\times w\times 3}$, is sent to the feature
extractor $e^{i}=h_{bb}(x^{i}_{enroll})$, which is a frozen pre-trained face
recognition model that outputs an embedding tensor $e^{i}\in\mathbb{R}^{d}$,
where $d$ is the embedding dimension and depends on the pre-trained model. The
generative network $h_{gen}$ is given $e^{i}$, which represents the user face
characteristics as an input and is capable of transforming $e^{i}$ into
personal neural network weights $\theta^{i}$ that are highly discriminative:

$\theta^{i}=h_{gen}\circ h_{bb}(x^{i}_{enroll}),$ (2)

where $\theta^{i}$ helps construct the private model :$f(x,\theta^{i})$, and
$x$ is some input facial image.

###  IV-B Inference Phase

The inference phase describes the actions of the model when a data stream is
fed to it. Our inference phase is conducted on the user edge device and
requires only the computational burden of $f(\theta^{i})$. A facial image is
streamed to the model for verification. Then, it is preprocessed in the same
manner as in the enrollment phase. The preprocessed image
$x_{stream}\in\mathbb{R}^{h\times w\times 3}$ is then utilized using
$y=f(x_{stream},\theta^{i})$. The output, $y$, is a binary decision on whether
$x_{stream}$ is an image of user $i$.

Figure 1: Illustration of the inference phase of our method. Enrollment is
performed once per user $i$, using a single facial image $x^{i}_{enroll}$. The
enrollment output is a set of weights $\theta^{i}$ of $f$, designed to fit
low-power devices. In the streaming phase, face images $x_{stream}$ are
presented to $f$, which then decides whether those belong to person $i$. In
the stream phase, $h$ is discarded; thus, the main computational burden is
mitigated.

###  IV-C Training Phase

Training (Fig 3) starts by taking an input batch consisting of $nB$ samples
from $B$ different identities. Without loss of generality, the following
descriptions illustrate the case of balanced sampling, i.e., the number of
samples per identity $n$ is constant across the batch. This removes bias
towards a specific individual within the batch. Our method also applies to
unbalanced sampling, where the constant $n$ can be replaced by a per-user
$n^{i}$. Let us first define an input training batch
$X=\\{x^{1}_{1},..,x^{1}_{n},x^{2}_{1},..,x^{2}_{n},..,x^{B}_{1},..x^{B}_{n}\\}\in\mathbb{R}^{n\times
B\times 3\times h\times w}$, where the superscript represents the identity and
the subscript denotes the sample index in the batch running from 1 to $n$. At
each training iteration, the goal of $h(X)$ is to generate a weights tensor
$\vec{\theta}$, which is $n\times B$ concatenated weight sets corresponding to
the input images. Each sample in $j\in X$ results in a weight set $\theta_{j}$
such that $f(x,\theta_{j})$ will recognize only the images of the same
identity as the identity of image $j$. Let us define an identity mapper that
inputs a sample index $j$ and outputs an identity index, formally:
$M:j\in[0,nB)\rightarrow i$. Next, we can define the target matrix
$Y\in\mathbb{R}^{nB\times nB}$, where each row represents the target for
sample $j$ as follows

$Y_{j,k}=\begin{cases}1&M(k)==M(j),\\\ 0&o.w,\end{cases}$ (3)

with $k\in[0,nB)$. The prediction is constructed in two phases. First, the
weight matrix for the batch is created

$\vec{\theta}=h(X).$ (4)

$\vec{\theta}\in\mathbb{R}^{nB\times p}$ where $p$ denotes the number of
parameters in $f$. Then, the weights are used to build the personal model for
each sample. The second prediction phase can be denoted in a batch form as

$\hat{Y}=f(X,\vec{\theta}).$ (5)

Where $\hat{Y}\in\mathbb{R}^{nB\times nB}$. We then use the weighted binary
cross entropy loss function:

$\displaystyle L_{bce}=\frac{1}{nB}\sum^{nB-1}_{j=0}\sum^{nB-1}_{k=0}-[\lambda
Y_{j,k}log\hat{Y}_{j,k}+$ (6) $\displaystyle(1-\lambda)(1-Y_{j,k})$
$\displaystyle log(1-\hat{Y}_{j,k})].$

Where $\lambda$ is a factor that compensates for the scarcity of similar
identity samples, i.e., since each batch contains $B$ identities, the ratio
between positive and negative targets will be $1:B$, $\lambda$ formally
defined as:

$\lambda=1-\frac{\beta}{B}.$ (7)

For $\beta=1$, we get classic weighted binary cross-entropy, with ”perfect”
balancing between the classifiers’ classes. Nevertheless, $\beta$ should be
higher than 1 to reduce future false positives. We used $\beta=2$, but future
experiments should attempt even higher values of $\beta$.

Since the $h$ solution space is enormous, i.e., the amount of $\theta$ that
$h$ can generate to solve the current batch classification problem,
regularizing the output of $h$ is crucial to the generalization of $h$. We
propose a weight decay equivalent objective on this set of target models to
regularize the weights $\theta^{i}$ generated by the hypernetwork $h$. The
goal is to penalize $h$ when generating large weights, which causes the model
to become more noise-sensitive and generalize poorly [42]. The objective is
defined as:

$L_{norm}=\frac{1}{nB}\sum_{j=0}^{n-1}\sum_{0=1}^{B-1}\|h(x_{j}^{i})\|_{2}^{2}.$
(8)

We evaluate the effect of this regularization in the ablation study performed
in Section V. Our full objective is a weighted sum of the former losses

$L=L_{bce}+\alpha_{norm}L_{norm}\,,$ (9)

where $\alpha_{norm}$ is a factor that balances between the two components.

Next, we describe several core components of our training phase.

$K$-means centered sampling We now introduce a novel method for effective hard
negative mining during batch sampling called $K$-means Centered Sampling
(KCS).

In our training, each sample is compared to all other samples in the batch;
thus, let us assume uniform sampling over the identities. The identities of
most samples in the batch are not necessarily similar and, therefore, may be
easy negatives; see Fig. 2. In this case, $h$ will quickly minimize $L$ even
without learning discriminative features. We want each batch to contain
similar identities, forcing $h$ to avoid overfitting and learning robust and
discriminative features. To achieve this, we use $h_{bb}$ to extract an
embedding for each identity, then cluster these into multiple groups using
$K$-means. During training, when employing KCS, batches are sampled from
within each cluster.

|
---|---
(a) | (b)
|
(c) | (d)
Figure 2: Comparing batches obtained with conventional sampling to those
obtained with $K$-means centered sampling (KCS). (a, b) a random batch sampled
during training, (c, d) a random batch sampled during training when using KCS.

Scheduling Training hypernetworks is challenging, especially in fine-grained
classification tasks. We utilize scheduling for three hyperparameters to
accelerate the model’s convergence: batch size, $\alpha_{norm}$, and the epoch
in which we start using KCS. Scheduling aims to help the model warm up and
make the training problem gradually harder. Since the batch size in our
training regime directly affects the difficulty (i.e., the larger the batch,
the more complex), we increase the batch size by a factor of 2 several times
during warm-up until the final batch size is achieved, which is eight times
larger than the initial batch. Smaller values of $\alpha_{norm}$ lead to fewer
constraints on $h_{gen}$ prediction; thus, we start the training with low
$\alpha_{norm}$ and increase it gradually.

KCS is designed to construct batches with examples of similar appearance;
however, we observed that this often prevents model convergence when used from
the initial training phase. To mitigate this, we start by warming up for $T$
iterations using uniform identity sampling and then use KCS during the
following iterations.

Figure 3: The training phase of our method starts with a one-time enrollment
procedure, which is noted by dashed arrows. The weights $\theta$ are generated
for all images in the batch $X$. Then, $f$ is generated for each user using
their specific weights. The streaming phase, noted by regular arrows, may be
performed as often as required using the person-specific model $f$. Each model
$f$ receives $X$ as an input and calculates the binary cross entropy loss with
respect to each model’s user label. The embedding model $h_{bb}$ is not
trainable. The trainable part $h_{gen}$ obtains the gradients for the batch of
$n\times B$ neural networks.

Selection of Architectural Components The architecture of $h_{gen}$ is simple,
comprising elements such as fully connected layers, LayerNorm [43], and GeLU
activation [44]. $f$ predominantly relies on group convolutions for enhancing
efficiency and non-parametric normalization layers. Additional information can
be found in the implementation details subsection.

TABLE I: Accuracy results on six leading face verification datasets. We
present the top-1 accuracy results, the number of parameters of the inference
model, and the number of parameters of the model responsible for the user’s
enrollment. An identical number of parameters indicates that the enrollment
and inference models are identical. We further show the MFLOPS (million
floating point operations) for the inference step.

Model Enroll Param.(M) Infer Param.(M) MFLOPs LFW CA-LFW CP-LFW CFP-FP
AgeDB-30 VGG2-FP EfficientNet-B0 [45] 5.3 5.3 - 99.50 95.32 89.73 93.47 95.45
93.20 GhostFaceNetV1-2 [46] 4.06 4.06 60.29 99.65 95.53 88.57 91.51 96.18 -
MobileFaceNetV1 [28] 3.4 3.4 1100 99.40 94.47 87.17 95.80 96.40 -
ProxylessFaceNAS [28] 3.2 3.2 900 99.20 92.55 84.17 94.70 94.40 -
PocketNetM-256 [47] 1.75 1.75 1099 99.58 95.63 90.03 95.66 97.17 -
PocketNetM-128 [47] 1.68 1.68 1099 99.60 95.67 90.00 95.07 96.78 -
PocketNetS-256 [47] 0.99 0.99 587 99.66 95.50 88.93 94.34 96.35 -
PocketNetS-128 [47] 0.92 0.92 587 99.58 95.48 88.63 94.21 96.10 - ConvFaceNeXt
2A [29] 1.05 1.05 404.57 99.12 92.78 85.45 98.84 93.05 - ConvFaceNeXt PE [29]
1.05 1.05 404.57 99.10 93.32 85.45 98.87 92.95 - ConvFaceNeXt - LCAM [31] 1.05
1.05 406.56 99.20 93.47 86.40 89.49 93.70 90.78 ConvFaceNeXt - L5K [31] 1.05
1.05 406.60 99.23 93.73 86.97 89.61 93.65 90.04 ShuffleMixFaceNet-XS [48] 1.04
1.04 161.9 99.53 - - 91.26 95.62 - DG0 [49] 0.42 0.42 50 99.03 93.67 85.48
87.23 - 88.92 DG1 [49] 0.82 0.82 150 99.60 95.10 88.90 92.51 - 92.32
MixFaceNet-XS [48] 1.04 1.04 161.9 99.60 - - 91.09 95.85 - ShuffleFaceNet 0.5x
[24] 0.5 0.5 66.9 99.23 - - 92.59 93.22 - Ours FaceTransformer[50] 145.1 0.023
5.4 99.52 94.61 89.63 94.96 93.83 92.96 Ours AdaFace[17] 145.1 0.023 5.4 99.55
94.67 90.58 95.56 94.50 93.73

##  V Experiments

Implementation details We use PyTorch [51] as a framework. To show that our
method is backbone agnostic, we will present results using two backbones
(i.e., $h_{bb}$) from different architecture families: Adaface [17] (CNNs) and
FaceTransformer[50] (Transformer). Adaface [17] uses a ResNet101 [52] backbone
pretrained on the MS-Celeb-1M V2 [16] dataset, and it is frozen for the entire
training. We trained $h_{gen}$ using SGD with a learning rate of $1e-3$,
momentum value of 0.9, weight decay of $1e-4$, and 3000 warm-up steps.
$h_{gen}$ consists of 4 linear layers with LayerNorm [43] and GeLU activation
[44]. The variation based on the FaceTransformer [50] was also pretrained on
the MS-Celeb-1M V2 [16] dataset and was frozen for the entire training. We
trained $h_{gen}$ using SGD with a learning rate of $5e-3$ momentum value 0.9,
weight decay of $1e-4$, and 3000 warm-up steps. The output of $h_{bb}$ are
latent vectors $e$ with size:$B\times T\times 512$, where $T$ is the number of
tokens; we therefore first transpose $e$ and then pass it through a series of
$1D$ convolutions till achieving the form of $e\in R^{B\times 512}$, which is
passed through 4 linear layers with LayerNorm [43] and GeLU activation [44]
blocks, which extract $\theta$. We use $K=150$ in $K$-means clustering for
KCS. KCS is initiated after 100k steps. The FLOPs count calculation was
conducted using ’thop’ 111https://pypi.org/project/thop/ and ’pthflops’
222https://pypi.org/project/pthflops/ Python packages.

Mini Batch of NNs On a mini-batch of data Some works that train hypernetworks
[53] use an inner optimization loop to optimize the parameters $\theta$ for
$f$ and use the result as supervision for $h_{gen}$. The downside of this
methodology is that, currently, no framework supports backward propagation on
a batch of neural networks. This forces a loop over all the batch items and
optimization over $\theta_{i}\forall i$ in the batch. As described in this
work, the proposed recipe is different in that it relies on the final
classification signal. This is because $f$ is a tiny neural network that
reduces the concern of vanishing gradients. Nevertheless, at each forward
pass, we need to make a forward and a backward pass-through $nB$ neural
networks $f(\theta)$, with each pass containing $nB$ samples. Looping over
$nB$ neural networks would make the training procedure almost impractical;
thus, we would like to tensorize this procedure. This requires using the
functorch library [54], which enables forward propagation on a batch of
$(nB)^{2}$ images through a batch of $nB$ neural networks, resulting in a fast
and efficient training regime.

Datasets Evaluation of our method is done on six widely accepted facial
recognition benchmarks. Specifically, we use Labeled Faces in the Wild (LFW)
[55] and its later variants CP-LFW [56], and CA-LFW [57]. We also evaluate our
method on CFP-FP [58], AgeDB-30 [59], and VGG2-FP [60]. The MS-Celeb-1M V2
[16] dataset is used to train our models. It is a refined version of the MS-
Celeb-1M [61], containing 5.8M images of 85K identities.

Comparison to other methods We compare our method to 9 leading efficient face
recognition models and their multiple variants. All methods were trained using
the MS-Celeb-1M V2 [16] training set. Some schemes trained on the WebFace260M
dataset [33] were dropped for fair comparison [32].

TABLE II: Ablation study demonstrating the importance of different components
in our method. Training a model with the same structure as the private model
$f$ directly without it being generated by $h$ fails to achieve competitive
results. We do not see a benefit in training multiple $h_{gen}$ input layers,
leading to worse results than using only the embedding layer. Further, KCS has
proved beneficial, improving the results significantly over all datasets.
Lastly, using a larger model has not shown improvement over the minimal
version.

Model Enroll Param.(M) Infer Param.(M) MFLOPs LFW CA-LFW CP-LFW CFP-FP
AgeDB-30 VGG2-FP Avg. Training $f$ directly 0.023 0.023 5.4 90.70 75.17 65.72
68.21 72.70 71.60 74.02 Multiple $h_{gen}$ input layers 147.2 0.023 5.4 99.41
93.48 88.52 95.59 93.90 93.64 94.09 Ours AdaFace[17] w/o KCS 147.2 0.023 5.4
99.23 93.18 88.77 93.51 91.20 92.54 93.07 Ours AdaFace[17] w/o $L_{norm}$
147.2 0.023 5.4 99.29 93.37 89.11 93.61 91.79 92.82 93.33 Ours AdaFace[17]
118.6 0.023 5.4 99.55 94.67 90.58 95.56 94.50 93.73 94.77 Ours AdaFace[17],
larger model 147.4 0.037 5.7 99.50 94.60 90.45 94.80 94.77 93.84 94.66

###  V-A Results

Table LABEL:tab:main_results presents top-1 accuracy results on the six
leading face verification datasets mentioned above. Although our method
requires a large enrollment model, this is used only once per user, and only
the inference model is deployed on the edge device. When comparing inference
model size, i.e., its number of parameters and amount of MFLOPs required, we
can see the significant advantage of our model. Although our model is almost
22 times smaller than its smallest competitor [24], it maintains on par or
better results on all available datasets when the two are compared. Even
compared to more than 100 times larger models, we still obtain state-of-the-
art results on the CFP-FP dataset. For the first time, we demonstrate a method
that dramatically reduces memory requirements while maintaining reasonable
results on multiple benchmarks. Our method is based on a state-of-the-art face
recognition backbone for the initial embedding during enrollment. It is
improved when using the more accurate backbone (AdaFace [17] instead of
FaceTransformer[50]). Still, the improvement is slight, and both backbones are
comparable. A visual overview of the results on the five datasets: LFW, CA-
LFW, CP-LFW, CFP-FP, and AgeDB-30, is shown in Fig. 4, only the methods that
have results on all five datasets are presented. Fig. 4 shows both the top-1
accuracy vs. the number of parameters and the number of floating point
operations in mega-flops. We expect further improvements when using backbones
trained on cleaner and larger datasets, such as subsets of the WebFace260M
dataset [33], similarly to the improvement obtained by Kim et al. [17] when
training on larger datasets.

|
---|---
(a) | (b)
Figure 4: (a) The top1 accuracy average vs. the number of parameters for five
datasets (excluding vgg2-fp) of our models and efficient competing models for
face recognition. (b) the same when comparing accuracy and the number of
operations in mega-flops.

Ablation study Key parts of our method are examined via an ablation study
shown in Table LABEL:tab:ablation. We first tested the option of training $f$
in a direct manner using the AdaFace [17] training scheme. This resulted in a
massive degradation in accuracy, which can be explained by the model
underfitting the dataset due to its small number of parameters. Additional
ablation was done using multiple layers as input for $h_{gen}$. We have not
seen any benefit of using additional feature maps from different layers as
input compared to our main result, which uses only a single embedding layer.
This may be because more input feature maps for weight creation resulted in a
larger $h_{gen}$, which overfitted the data and worsened performance.

Another experiment was done using a model $f$ with a larger number of
parameters, which led to on-par results. We assume that the limiting factor to
our model’s performance is not the number of parameters but the procedure of
generating those; we will discuss the limiting factors of our method and how
to solve them in the Discussion section VI

Lastly, we check the impact of removing our KCS training technique and the
$L_{norm}$ loss term. In both cases, this led to a significant decrease in
accuracy; the largest decrease was on the AgeDB-30 dataset, which is the
hardest benchmark.

##  VI Discussion

Our method suffers from a few limitations. First, it converges quickly to a
decent performance, but obtaining competitive results could be time-consuming.
We suspect that our cosine learning rate scheduler is not optimal for this
optimization task.

Second, from the efficiency viewpoint, increasing the batch size results in a
quadratic increase in training complexity. This happens because each sample is
compared to all other samples in the batch, which is computationally
intensive. Exploring a way of training with a smaller batch size for a longer
time without hurting the convergence quality may prove beneficial.
Alternatively, one can select a subset of the pairs in the batch.

Third, previous works in generative models showed that methods that generate
with iterative updates [62](cite diffusion model works) are better than one-
step generation models, such as GANs [63]. This suggests that generating the
$\theta^{i}$ in a few steps, for example, using a diffusion process, [64] may
be beneficial.

Currently, $f$ has some drawbacks; it could be improved using conventional
normalization methods, such as batch or layer normalization. Future work could
include training on larger datasets, such as WebFace4M/12M [33] or larger.
This will aid us in leveraging larger and stronger $h_{gen}$ architectures.

While our current work focuses on creating a model from a single enrollment
image per user, we could explore using more images if they are available. In
cases where multiple images are available, we can generate multiple enrollment
images, embedding them and then averaging them as an input to $h_{gen}$. Such
an approach can increase the robustness of $f$ to different views, lighting,
and more.

Further improvements may consider data augmentations as a tool to enhance the
input data. For example, using geometric augmentations such as flip, crop,
rotate, or translate the face images to augment the single
image:$x_{enroll}^{i}$ and average the embedding to make the input of
$h_{gen}$ more robust.

##  VII Conclusions

This work presented an efficient paradigm for running efficient DNN on edge,
not by suggesting a more efficient model but by changing the problem scope
being solved. The change we suggested is treating the cases of very small
databases, such as smartphones, tablets, and personal laptops, differently
from large databases. At the core of our work stands the idea of a simpler
problem with a more straightforward solution. Our solution no longer needs a
very general neural network but one that solves a particular problem. This
significantly reduced the number of parameters while achieving on-par accuracy
for multiple datasets. Although this paper focuses on face verification, we
believe our method can also be applied in other fields, such as speaker
identification and keyword spotting.

## References

  * Taigman et al. [2014] Y. Taigman, M. Yang, M. Ranzato, and L. Wolf, “Deepface: Closing the gap to human-level performance in face verification,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2014, pp. 1701–1708.
  * Taigman et al. [2015] ——, “Web-scale training for face identification,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2015, pp. 2746–2754.
  * Ajani et al. [2021] T. S. Ajani, A. L. Imoize, and A. A. Atayero, “An overview of machine learning within embedded and mobile devices–optimizations and applications,” _Sensors_ , vol. 21, no. 13, p. 4412, 2021.
  * Rastegari et al. [2020] M. Rastegari, V. Ordonez, J. Redmon, and A. Farhadi, “Enabling ai at the edge with xnor-networks,” _Communications of the ACM_ , vol. 63, no. 12, pp. 83–90, 2020.
  * Zemlyanikin et al. [2019] M. Zemlyanikin, A. Smorkalov, T. Khanova, A. Petrovicheva, and G. Serebryakov, “512kib ram is enough! live camera face recognition dnn on mcu,” in _Proceedings of the IEEE/CVF International Conference on Computer Vision Workshops_ , 2019, pp. 0–0.
  * Ha et al. [2016] D. Ha, A. Dai, and Q. V. Le, “Hypernetworks,” _arXiv preprint arXiv:1609.09106_ , 2016.
  * Cheng et al. [2018] Z. Cheng, X. Zhu, and S. Gong, “Surveillance face recognition challenge,” _arXiv preprint arXiv:1804.09691_ , 2018.
  * Nag et al. [2018] A. Nag, J. Nikhilendra, and M. Kalmath, “Iot based door access control using face recognition,” in _2018 3rd International conference for convergence in technology (I2CT)_. IEEE, 2018, pp. 1–3.
  * Lee et al. [2020] H. Lee, S.-H. Park, J.-H. Yoo, S.-H. Jung, and J.-H. Huh, “Face recognition at a distance for a stand-alone access control system,” _Sensors_ , vol. 20, no. 3, p. 785, 2020.
  * Lynch [2020] J. Lynch, “Face off: Law enforcement use of face recognition technology,” _Available at SSRN 3909038_ , 2020.
  * Dudani [1976] S. A. Dudani, “The distance-weighted k-nearest-neighbor rule,” _IEEE Transactions on Systems, Man, and Cybernetics_ , no. 4, pp. 325–327, 1976.
  * Schroff et al. [2015] F. Schroff, D. Kalenichenko, and J. Philbin, “Facenet: A unified embedding for face recognition and clustering,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2015, pp. 815–823.
  * Liu et al. [2016] W. Liu, Y. Wen, Z. Yu, and M. Yang, “Large-margin softmax loss for convolutional neural networks,” _arXiv preprint arXiv:1612.02295_ , 2016\.
  * Liu et al. [2017] W. Liu, Y. Wen, Z. Yu, M. Li, B. Raj, and L. Song, “Sphereface: Deep hypersphere embedding for face recognition,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2017, pp. 212–220.
  * Wang et al. [2018] H. Wang, Y. Wang, Z. Zhou, X. Ji, D. Gong, J. Zhou, Z. Li, and W. Liu, “Cosface: Large margin cosine loss for deep face recognition,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2018, pp. 5265–5274.
  * Deng et al. [2019] J. Deng, J. Guo, N. Xue, and S. Zafeiriou, “Arcface: Additive angular margin loss for deep face recognition,” in _Proceedings of the IEEE/CVF conference on computer vision and pattern recognition_ , 2019, pp. 4690–4699.
  * Kim et al. [2022] M. Kim, A. K. Jain, and X. Liu, “Adaface: Quality adaptive margin for face recognition,” in _Proceedings of the IEEE/CVF conference on computer vision and pattern recognition_ , 2022, pp. 18 750–18 759.
  * Han et al. [2022] K. Han, Y. Wang, H. Chen, X. Chen, J. Guo, Z. Liu, Y. Tang, A. Xiao, C. Xu, Y. Xu _et al._ , “A survey on vision transformer,” _IEEE transactions on pattern analysis and machine intelligence_ , vol. 45, no. 1, pp. 87–110, 2022.
  * Khan et al. [2022] S. Khan, M. Naseer, M. Hayat, S. W. Zamir, F. S. Khan, and M. Shah, “Transformers in vision: A survey,” _ACM computing surveys (CSUR)_ , vol. 54, no. 10s, pp. 1–41, 2022.
  * Liu et al. [2020] J. Liu, S. Tripathi, U. Kurup, and M. Shah, “Pruning algorithms to accelerate convolutional neural networks for edge applications: A survey,” _arXiv preprint arXiv:2005.04275_ , 2020.
  * Liang et al. [2021] T. Liang, J. Glossner, L. Wang, S. Shi, and X. Zhang, “Pruning and quantization for deep neural network acceleration: A survey,” _Neurocomputing_ , vol. 461, pp. 370–403, 2021.
  * Gholami et al. [2022] A. Gholami, S. Kim, Z. Dong, Z. Yao, M. W. Mahoney, and K. Keutzer, “A survey of quantization methods for efficient neural network inference,” in _Low-Power Computer Vision_. Chapman and Hall/CRC, 2022, pp. 291–326.
  * Benmeziane et al. [2021] H. Benmeziane, K. E. Maghraoui, H. Ouarnoughi, S. Niar, M. Wistuba, and N. Wang, “A comprehensive survey on hardware-aware neural architecture search,” _arXiv preprint arXiv:2101.09336_ , 2021.
  * Martindez-Diaz et al. [2019] Y. Martindez-Diaz, L. S. Luevano, H. Mendez-Vazquez, M. Nicolas-Diaz, L. Chang, and M. Gonzalez-Mendoza, “Shufflefacenet: A lightweight face architecture for efficient and highly-accurate face recognition,” in _Proceedings of the IEEE/CVF International Conference on Computer Vision Workshops_ , 2019, pp. 0–0.
  * Chen et al. [2018] S. Chen, Y. Liu, X. Gao, and Z. Han, “Mobilefacenets: Efficient cnns for accurate real-time face verification on mobile devices,” in _Biometric Recognition: 13th Chinese Conference, CCBR 2018, Urumqi, China, August 11-12, 2018, Proceedings 13_. Springer, 2018, pp. 428–438.
  * Sandler et al. [2018] M. Sandler, A. Howard, M. Zhu, A. Zhmoginov, and L.-C. Chen, “Mobilenetv2: Inverted residuals and linear bottlenecks,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2018, pp. 4510–4520.
  * Ma et al. [2018] N. Ma, X. Zhang, H.-T. Zheng, and J. Sun, “Shufflenet v2: Practical guidelines for efficient cnn architecture design,” in _Proceedings of the European conference on computer vision (ECCV)_ , 2018, pp. 116–131.
  * Martinez-Diaz et al. [2021] Y. Martinez-Diaz, M. Nicolas-Diaz, H. Mendez-Vazquez, L. S. Luevano, L. Chang, M. Gonzalez-Mendoza, and L. E. Sucar, “Benchmarking lightweight face architectures on specific face recognition scenarios,” _Artificial Intelligence Review_ , pp. 1–44, 2021.
  * Hoo et al. [2022] S. C. Hoo, H. Ibrahim, and S. A. Suandi, “Convfacenext: Lightweight networks for face recognition,” _Mathematics_ , vol. 10, no. 19, p. 3592, 2022.
  * Liu et al. [2022] Z. Liu, H. Mao, C. Wu, C. Feichtenhofer, T. Darrell, and S. Xie, “Convnet for the 2020s. arxiv,” _arXiv preprint arXiv:2201.03545_ , 2022.
  * Hoo et al. [2023] S. C. Hoo, H. Ibrahim, S. A. Suandi, and T. F. Ng, “Lcam: Low-complexity attention module for lightweight face recognition networks,” _Mathematics_ , vol. 11, no. 7, p. 1694, 2023.
  * George et al. [2023] A. George, C. Ecabert, H. O. Shahreza, K. Kotwal, and S. Marcel, “Edgeface: Efficient face recognition model for edge devices,” _arXiv preprint arXiv:2307.01838_ , 2023.
  * Zhu et al. [2021] Z. Zhu, G. Huang, J. Deng, Y. Ye, J. Huang, X. Chen, J. Zhu, T. Yang, J. Lu, D. Du _et al._ , “Webface260m: A benchmark unveiling the power of million-scale deep face recognition,” in _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , 2021, pp. 10 492–10 502.
  * Krueger et al. [2017] D. Krueger, C.-W. Huang, R. Islam, R. Turner, A. Lacoste, and A. Courville, “Bayesian hypernetworks,” _arXiv preprint arXiv:1710.04759_ , 2017.
  * Von Oswald et al. [2019] J. Von Oswald, C. Henning, B. F. Grewe, and J. Sacramento, “Continual learning with hypernetworks,” _arXiv preprint arXiv:1906.00695_ , 2019.
  * Zhao et al. [2020] D. Zhao, S. Kobayashi, J. Sacramento, and J. von Oswald, “Meta-learning via hypernetworks,” in _4th Workshop on Meta-Learning at NeurIPS 2020 (MetaLearn 2020)_. NeurIPS, 2020.
  * Nguyen et al. [2021] P. Nguyen, T. Tran, K. Le, S. Gupta, S. Rana, D. Nguyen, T. Nguyen, S. Ryan, and S. Venkatesh, “Fast conditional network compression using bayesian hypernetworks,” in _Machine Learning and Knowledge Discovery in Databases. Research Track: European Conference, ECML PKDD 2021, Bilbao, Spain, September 13–17, 2021, Proceedings, Part III 21_. Springer, 2021, pp. 330–345.
  * Galanti and Wolf [2020] T. Galanti and L. Wolf, “On the modularity of hypernetworks,” _Advances in Neural Information Processing Systems_ , vol. 33, pp. 10 409–10 419, 2020\.
  * Navon et al. [2020] A. Navon, A. Shamsian, G. Chechik, and E. Fetaya, “Learning the pareto front with hypernetworks,” _arXiv preprint arXiv:2010.04104_ , 2020.
  * Yang et al. [2022] J. Yang, O. Lindenbaum, and Y. Kluger, “Locally sparse neural networks for tabular biomedical data,” in _International Conference on Machine Learning_. PMLR, 2022, pp. 25 123–25 153.
  * Svirsky and Lindenbaum [2023] J. Svirsky and O. Lindenbaum, “Interpretable deep clustering,” _arXiv preprint arXiv:2306.04785_ , 2023.
  * Jia et al. [2022] X. Jia, X. Feng, H. Yong, and D. Meng, “Weight decay with tailored adam on scale-invariant weights for better generalization,” _IEEE Transactions on Neural Networks and Learning Systems_ , 2022.
  * Ba et al. [2016] J. L. Ba, J. R. Kiros, and G. E. Hinton, “Layer normalization,” _arXiv preprint arXiv:1607.06450_ , 2016.
  * Hendrycks and Gimpel [2016] D. Hendrycks and K. Gimpel, “Gaussian error linear units (gelus),” _arXiv preprint arXiv:1606.08415_ , 2016.
  * Tan and Le [2019] M. Tan and Q. Le, “Efficientnet: Rethinking model scaling for convolutional neural networks,” in _International conference on machine learning_. PMLR, 2019, pp. 6105–6114.
  * Alansari et al. [2023] M. Alansari, O. A. Hay, S. Javed, A. Shoufan, Y. Zweiri, and N. Werghi, “Ghostfacenets: Lightweight face recognition model from cheap operations,” _IEEE Access_ , 2023.
  * Boutros et al. [2022] F. Boutros, P. Siebke, M. Klemt, N. Damer, F. Kirchbuchner, and A. Kuijper, “Pocketnet: Extreme lightweight face recognition network using neural architecture search and multistep knowledge distillation,” _IEEE Access_ , vol. 10, pp. 46 823–46 833, 2022.
  * Boutros et al. [2021] F. Boutros, N. Damer, M. Fang, F. Kirchbuchner, and A. Kuijper, “Mixfacenets: Extremely efficient face recognition networks,” in _2021 IEEE International Joint Conference on Biometrics (IJCB)_. IEEE, 2021, pp. 1–8.
  * Zhao et al. [2023] F. Zhao, P. Zhang, R. Zhang, and M. Li, “Dgfacenet: Lightweight and efficient face recognition,” _Engineering Applications of Artificial Intelligence_ , vol. 124, p. 106513, 2023.
  * Zhong and Deng [2021] Y. Zhong and W. Deng, “Face transformer for recognition,” _arXiv preprint arXiv:2103.14803_ , 2021.
  * Paszke et al. [2019] A. Paszke, S. Gross, F. Massa, A. Lerer, J. Bradbury, G. Chanan, T. Killeen, Z. Lin, N. Gimelshein, L. Antiga _et al._ , “Pytorch: An imperative style, high-performance deep learning library,” _Advances in neural information processing systems_ , vol. 32, 2019.
  * He et al. [2016] K. He, X. Zhang, S. Ren, and J. Sun, “Deep residual learning for image recognition,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2016, pp. 770–778.
  * Shamsian et al. [2021] A. Shamsian, A. Navon, E. Fetaya, and G. Chechik, “Personalized federated learning using hypernetworks,” in _International Conference on Machine Learning_. PMLR, 2021, pp. 9489–9502.
  * He and Zou [2021] H. He and R. Zou, “functorch: Jax-like composable function transforms for pytorch,” 2021.
  * Huang et al. [2008] G. B. Huang, M. Mattar, T. Berg, and E. Learned-Miller, “Labeled faces in the wild: A database forstudying face recognition in unconstrained environments,” in _Workshop on faces in’Real-Life’Images: detection, alignment, and recognition_ , 2008.
  * Zheng and Deng [2018] T. Zheng and W. Deng, “Cross-pose lfw: A database for studying cross-pose face recognition in unconstrained environments,” _Beijing University of Posts and Telecommunications, Tech. Rep_ , vol. 5, no. 7, 2018.
  * Zheng et al. [2017] T. Zheng, W. Deng, and J. Hu, “Cross-age lfw: A database for studying cross-age face recognition in unconstrained environments,” _arXiv preprint arXiv:1708.08197_ , 2017.
  * Sengupta et al. [2016] S. Sengupta, J.-C. Chen, C. Castillo, V. M. Patel, R. Chellappa, and D. W. Jacobs, “Frontal to profile face verification in the wild,” in _2016 IEEE winter conference on applications of computer vision (WACV)_. IEEE, 2016, pp. 1–9.
  * Moschoglou et al. [2017] S. Moschoglou, A. Papaioannou, C. Sagonas, J. Deng, I. Kotsia, and S. Zafeiriou, “Agedb: the first manually collected, in-the-wild age database,” in _proceedings of the IEEE conference on computer vision and pattern recognition workshops_ , 2017, pp. 51–59.
  * Cao et al. [2018] Q. Cao, L. Shen, W. Xie, O. M. Parkhi, and A. Zisserman, “Vggface2: A dataset for recognising faces across pose and age,” in _2018 13th IEEE international conference on automatic face & gesture recognition (FG 2018)_. IEEE, 2018, pp. 67–74.
  * Guo et al. [2016] Y. Guo, L. Zhang, Y. Hu, X. He, and J. Gao, “Ms-celeb-1m: A dataset and benchmark for large-scale face recognition,” in _Computer Vision–ECCV 2016: 14th European Conference, Amsterdam, The Netherlands, October 11-14, 2016, Proceedings, Part III 14_. Springer, 2016, pp. 87–102.
  * Dhariwal and Nichol [2021] P. Dhariwal and A. Nichol, “Diffusion models beat gans on image synthesis,” _Advances in neural information processing systems_ , vol. 34, pp. 8780–8794, 2021.
  * Goodfellow et al. [2014] I. Goodfellow, J. Pouget-Abadie, M. Mirza, B. Xu, D. Warde-Farley, S. Ozair, A. Courville, and Y. Bengio, “Generative adversarial nets,” _Advances in neural information processing systems_ , vol. 27, 2014.
  * Lutati and Wolf [2023] S. Lutati and L. Wolf, “Ocd: Learning to overfit with conditional diffusion models,” in _International Conference on Machine Learning_. PMLR, 2023, pp. 23 157–23 169.


# Hybrid Maximal Filter Spaces

David Gonzalez  Department of Mathematics, University of California, Berkeley
<EMAIL_ADDRESS>
###### Abstract.

We introduce a new way of encoding general topology in second order arithmetic
that we call hybrid maximal filter (hybrid MF) spaces. This notion is a
modification of the notion of a proper MF space introduced by Montalbán. We
justify the shift by showing that proper MF spaces are not able to code most
topological spaces, while hybrid MF spaces can code any second countable MF
space. We then answer Montalbán’s question about metrization of well-behaved
MF spaces to this shifted context. To be specific, we show that in stark
contrast to the original MF formalization used by Mummert and Simpson, the
metrization theorem can be proven for hybrid MF spaces within $\text{ACA}_{0}$
instead of needing $\Pi_{2}^{1}-\text{CA}_{0}$.

##  1\. Introduction

In this article we explore the concept of general topology in second order
arithmetic through a new lens. Because a topology is naturally described as a
third order object, it is not clear how to formalize its study in second order
arithmetic. The usual approach involves restricting to topologies with
structure that allows you to see the topology in a second order way. The most
well studied approach looks at separable, complete metric spaces (see: [1],[2]
Chapter 10). However, many theorems of topology lack meaning in this setting.
For example, metrization and the study of not completely metrizable spaces
(like order topologies) are totally excluded.

To remedy the lack of expressive power of metric spaces, there have been two
main explored approaches. The first is studying countable second-countable
(CSC) spaces (eg. [3], [10]). In this setting everything is countable, so all
aspects of the topological space can be captured using only second order
arithmetic. This system has the obvious disadvantage that it only describes
countable spaces. In particular, it is not a good place to study notions such
as connectivity.

The second approach is studying countably based maximal filter (MF) spaces
(e.g. [7]). It is this second approach that we focus on in this article. Here,
a topological space is encoded by a partially ordered set. Each basic open is
given by an element in this partially ordered set, and the points of the space
are given by maximal filters in the partially ordered set. A point is said to
be in a basic open if the element corresponding to that open set is an element
of the point as a maximal filter. This approach has the advantage of defining
a broad class of topological spaces that includes all separable, complete
metric spaces and many spaces that are not metrizable (exactly classified in
[8]). MF spaces as formalized here do have some undesirable properties. For
example, saying a subset of a partially ordered set is a maximal filter can be
as difficult as requiring $\Pi_{1}^{1}-\text{CA}_{0}$ (this is not explicitly
noted [7], but we will see a short proof of it later based on those results).
In other words, it may take $\Pi_{1}^{1}-\text{CA}_{0}$ to declare that a set
encodes a point in your space. For this reason, it can be difficult to compute
relatively simple topological properties in the MF space setting. For example,
Mummert and Simpson [7] showed that the set of pairs of opens such that the
closure of the first is contained in the second may need
$\Pi_{2}^{1}-\text{CA}_{0}$ to compute.

The above results are striking in the high complexity they achieve. They also
bring up a potential concern. The difficulty of recording basic topological
relations may hide the combinatorial core of a theorem or make a construction
seem overly difficult to describe. In this, results proven in the setting of
MF spaces leave a stone unturned: what would the complexity of the result be
without these descriptive difficulties surrounding basic topological notions
like point and containment. For example, the well known result of the
metrization theorem being equivalent to $\Pi_{2}^{1}-\text{CA}_{0}$ in MF
spaces ([7]) ought to be far simpler if we were in a setting where basic
notions were easier to compute.

The coding of an object is often an innocuous part of computability theory.
This is not the case with MF spaces; there are apparent difficulties with the
chosen coding. It is for this reason that alternate codings ought to be
explored, especially if they result in different outcomes for the descriptive
complexity of objects like a complete metric on the space. This is what led
Montalbán to propose the notion of proper MF spaces, and what leads us to
investigate the notion of hybrid MF spaces.

In the next sections we will give the necessary background on reverse
mathematics and MF spaces. After this we will study proper MF spaces in
general to justify the definition of hybrid MF spaces. Next we will give a
proof of the metrization theorem for hybrid MF spaces in $\text{ACA}_{0}$. The
last section will feature some complexity calculations and suggestions for
future work.

##  2\. Background on Reverse Math

Reverse mathematics aims to calibrate a proof to a particular subsystem of
second order arithmetic. Over a weak base system a typical argument shows that
a mathematical theorem implies a stronger system and vice versa. We mention
the following systems in this paper (listed from weakest to strongest).
$\text{RCA}_{0}$ contains $\Delta_{1}^{0}$ comprehension and $\Sigma_{1}^{0}$
induction. In other words, it allows only for the definitions of computable
objects. $\text{ACA}_{0}$ contains arithmetical comprehension and arithmetical
induction. This allows for the definition of arithmetical objects.
$\Pi_{1}^{1}-\text{CA}_{0}$ is $\text{ACA}_{0}$ along with $\Pi_{1}^{1}$
comprehension. $\Pi_{2}^{1}-\text{CA}_{0}$ is $\text{ACA}_{0}$ along with
$\Pi_{2}^{1}$ comprehension. There are many texts that go over the definitions
of these subsystems in detail (see e.g.[11], [2]).

While $\text{RCA}_{0}$ is occasionally mentioned, $\text{ACA}_{0}$ is base
system for this paper. This base system is unusually strong, but this is
typical when working with MF spaces. The reason for this is that in [5] it was
shown that the existence of a maximal filter in a poset is equivalent to
$\text{ACA}_{0}$. As our spaces will be coded by maximal filters in a poset,
it is difficult to account for the case where there are no maximal filters at
all. Furthermore, typical objects like upward closures of sets in a poset
cannot be calculated without $\text{ACA}_{0}$ and this is needed constantly.
In short, one cannot give an honest formalization of MF spaces outside of
$\text{ACA}_{0}$.

Our main result concerns metrization, and it is proven in our base system. We
do not produce a reversal, as such an endeavor is not common when working in a
base system.

One could understand the metrization result through a more structural lens.
The result in [7] shows that given a regular MF space there is a metric on it,
but this metric necessarily uses $\Pi_{2}^{1}$ sets in its definition. Our
metrization result is proven in $\text{ACA}_{0}$, so shows that any regular
hybrid MF space (a concept defined later) has a metric on it and this metric
is arithmetically defined. In short, the subsystems of second order arithmetic
used in this context can be understood as bounds on the complexity of defining
additional metric structure on a given topological space.

##  3\. Background on MF Spaces

This section aims to give the definitions regarding MF spaces established in
[7] that will also be used in this article. There will also be definitions of
a few needed terms from general topology.

######  Definition 1.

Fix a partially ordered set $P$. A pre-filter on $P$ is a non-empty subset $R$
with the property that for every $x,y\in R$ there is a $z\in R$ with $z\geq x$
and $z\geq y$. A filter on $P$ is a pre-filter that is upwards closed. A
maximal filter is a filter that is not strictly contained in any filter.

Given $S\subseteq P$ we let ucl$(S)$ denote the upwards closure of $S$. Note
that if $S$ is a pre-filter then ucl$(S)$ is a filter. We use the concept of
maximal filters to defined a maximal filter space.

######  Definition 2.

Let $P$ be a countable partially ordered set. $MF(P)$ is the set of maximal
filters on $P$. Every $p\in P$ codes a basic open set

$N_{p}:=\\{m\in MF(P)|p\in m\\}.$

A general open set is given by $U\subseteq P$ as follows

$N_{U}:=\bigcup_{p\in U}N_{p}.$

These open sets are called the poset topology on $MF(P)$

Note that in $\text{ACA}_{0}$ one can show that the $N_{U}$ are closed under
unions and finite intersections. In particular, it is justified to call these
sets a topology. Note also that we can code closed sets with the code for the
open set that represents its complement. Concepts that can be defined in a
general topological space carry the same definitions in this context based on
the open sets $N_{U}$. For example, $m\in\text{cl}(N_{U})$ if every $q\in m$
has a common extension with some $p\in U$.

The metrization theorem concerns regular spaces.

######  Definition 3.

An MF space is regular if for every $x\in MF(P)$ and $p\in P$ with $x\in
N_{p}$ there is a $q\in P$ with $n\in N_{q}$ and $\text{cl}(N_{q})\subseteq
N_{p}$.

We will also mention the more technical notion of strong regularity.

######  Definition 4.

An MF space is strongly regular if there is a sequence of subsets $\langle
D_{p}|p\in P\rangle$ with the property that $N_{p}=\bigcup_{q\in R_{p}}N_{q}$
and $\text{cl}(N_{q})\subseteq N_{p}$ whenever $q\in D_{p}$.

Given a strongly regular space, and $p\in P$ we will always use $D_{p}$ to
denote the set in the definition above. In a classical sense it is not
difficult to see that all regular spaces are strongly regular. In fact, one
can make this observation in $\Pi_{2}^{1}-\text{CA}_{0}$ (see [7] Lemma 4.1).
One only must enumerate the set $p,q$ such that $\text{cl}(N_{q})\subseteq
N_{p}$. One of the central insights of [7] is that this set of pairs can in
fact be $\Pi_{2}^{1}$-complete. In other words, showing strong regularity from
regularity requires the strength of $\Pi_{2}^{1}-\text{CA}_{0}$. This insight
is what ultimately leads to showing that the following metrization theorem is
equivalent to $\Pi_{2}^{1}-\text{CA}_{0}$.

######  Definition 5.

MFMT is the statement that every regular MF space is homeomorphic to a
complete separable metric space.

The notion of homeomorphism between an MF space and a complete separable
metric space is similar to the one we use in Definition 20. It is not central
to this exposition, so we omit the exact notion used in [7] here.

We will briefly mention the notion of a normal topological space which is one
in which every pair $N_{p},N_{q}$ with
$\text{cl}(N_{q})\cap\text{cl}(N_{p})=\emptyset$ has $r,t$ such that
$\text{cl}(N_{q})\subseteq N_{r}$, $\text{cl}(N_{p})\subseteq N_{t}$ and
$N_{t}\cap N_{r}=\emptyset$.

The final topology definition that will be used is that of paracompactness.

######  Definition 6.

A cover of a topological space is point finite if every point in the space has
a neighborhood that only intersects finitely many of the elements of the
cover. A topological space is paracompact if every cover admits a point finite
subcover.

The fact that every complete metric space is paracompact was formalized as
Theorem II.7.2 in [11]. We will return to this notion when it is needed at the
end of the final section.

##  4\. Proper MF Spaces and Hybrid MF Spaces

Montalbán [6] made the following definition.

######  Definition 7.

A partial order $P$ defines a proper MF space if for $p,q\in P$, $p\leq q$ if
and only if $N_{p}\subseteq N_{q}$ and if $p$ and $q$ are comparable there is
an $r\in P$ such that $N_{r}=N_{p}\cap N_{q}$.

The hope was that these sorts of spaces would be easier to work with than
general MF spaces. In particular, every MF space would be codeable as a proper
MF space, but issues like definability of points would be simplified. This is
what prompted Montalbán in [6] to ask his 15th question: what is the reverse
mathematical strength of the complete metrization of proper MF spaces?

Unfortunately, we observe below that the notion of a proper MF space is not a
suitable formulation for further study. Contrary to the suspicions of
Montalbán, proper MF spaces cannot code every MF space.

In the proposition below we use $p\wedge q$ to denote the $r$ such that
$N_{r}=N_{p}\cap N_{q}$ in the proper MF space.

######  Proposition 8.

The topology of a proper MF space given by the elements of its poset is a
clopen basis.

###### Proof.

Let $P$ be the partial order that gives rise to the MF space. Consider a basic
open set coded by $y\in P$. Say there is a maximal filter $M\subseteq P$ with
$M\in\partial(N_{y})$. Consider the set

$N:=\\{p\in P|p\in M\lor\exists m\in M~{}p=m\wedge y\\}.$

First note that $N$ does not contain the empty set. This is because every open
set containing $M$ must intersect $N_{y}$. Therefore, any $m\in M$ has a non-
empty meet with $y$.

We claim that $N$ is a pre-filter. Note that for $m,n\in M$, we have that
$m\wedge y,n\wedge y\in N$ so $(m\wedge y)\wedge(n\wedge y)=(m\wedge n)\wedge
y\in N$ as $m\wedge n\in M$. Similarly, $m,n\wedge y\in N$ so $m\wedge(n\wedge
y)=(m\wedge n)\wedge y\in N$ as $m\wedge n\in M$. Of course, $m\wedge n\in
M\subseteq N$. This means that $\text{ucl}(N)$ is a filter. Note that
$\text{ucl}(N)$ contains $M$. By maximality of $M$, this means that
$M=\text{ucl}(N)$. In particular, $y\in M$ and therefore $M\in N_{y}$

This means that the boundary of $N_{y}$ is contained in $N_{y}$, and therefore
it is closed. ∎

######  Example 1.

$[0,1]$ is not a proper MF space.

This follows from Proposition 8 and the fact that $[0,1]$ is connected, so it
cannot have a clopen basis.

One method that this example discounts for finding posets including meet that
code a particular topological space is taking the meet-semilattice of open
sets given to us by the basis of the topology. More explicitly, if we take the
standard countable basis for $[0,1]$ of rational radius balls with rational
centers, this meet-semilattice of open sets does not code $[0,1]$ in the sense
of an MF space. For example, the set of opens containing $1/2$ is not a
maximal filter. In fact, it can be extended to a maximal filter in two
different ways. Either the open rational intervals ending in $1/2$ can be
added or the open rational intervals starting with $1/2$ can be added. It can
be observed that this topology is quite distinct from that of $[0,1]$ as every
rational number is duplicated in this way.

This excursion leads us to the conclusion that the basic open sets in an MF
space actually serve two distinct roles that cannot be unified into a single
object:

  1. (1)

Like in all spaces, they encode topological information via a lattice of open
sets,

  2. (2)

They code points via maximal filters on a selected subposet of the above
lattice.

In many cases the subposet cannot be a an induced subposet as in the example
above. Either this, or the subposet lacks meets or joins. The lattice and
poset are actually quite far apart from each other. It seems natural then that
a more complete description and encoding of an MF space should actually
include both of these objects and how they interact.

This leads to the following "hybrid" approach to the definition of an MF space
in second order arithmetic.

######  Definition 9.

A hybrid MF space is a pseudo-complemented distributive lattice
$(L,\leq_{L},\wedge,\vee,0,1,^{c})$ with a distinguished subposet
$(P,\leq_{p})$ such that:

  1. (1)

$x\leq_{L}y$ for $x,y\in P$ if and only if every maximal filter in $P$
containing $x$ also contains $y$.

  2. (2)

Every non-zero element $x\in L$ is $\leq_{L}$ above infinitely many elements
of $P$. For ease of notation we call this set $B(x)\subseteq P$.

  3. (3)

$x\leq_{L}y$ for $x,y\in L$ if and only if $B(x)\subseteq B(y)$.

  4. (4)

$B(x\wedge y)=B(x)\cap B(y)$.

  5. (5)

$B(x\vee y)=B(x)\cup B(y)$.

  6. (6)

If $B(x\wedge y)=\emptyset$ then $x\wedge y=0$.

  7. (7)

If every maximal filter passes through $B(x\vee y)$ then $x\vee y=1$.

  8. (8)

$B(x^{c})$ is the set of all $y$ such that $x\wedge y=0$.

We say that a maximal filter $M$ is in a basic open $p\in P$ if $p\in M$. For
$x\in L$ we say that $M$ is in $x$ if there is some $p\in P$ with $x\geq_{L}p$
and $p\in M$. $M$ is contained union of basic open sets coded by $W\subseteq
L$ if there is an $x\in W$ with $M$ in $x$.

It can be shown that any partial order $P$ can be upgraded to a hybrid MF
space using $\Pi_{2}^{1}-\text{CA}_{0}$. The most difficult portion is the
definition of $\leq_{L}$ among the elements of $P$. The definition given above
is naturally $\Pi_{2}^{1}$ as $\leq_{L}=\\{(x,y)|\forall M\subseteq
P~{}MaxFilt(M)\to(x\in M\to y\in M)\\}$ and $MaxFilt(M)$ is $\Pi_{1}^{1}$.

To be concrete, it is not difficult to define a hybrid MF representation of
the previously problematic space $[0,1]$. $L$ is given by the collection of
unions of finitely many rational subintervals of $[0,1]$. $P$ is given by the
rational subintervals of $[0,1]$. $\leq_{P}$ is given by the relation that
states that the closure of a an interval sits inside the larger interval (i.e.
the right and left end points are contained in the larger interval). Lemma 4.2
of [7] demonstrates that this representation as an ordinary MF space is as
desired. $\leq_{L}$ is defined by containment which is easily computable.
$\wedge,\vee,0,1$ and c are similarly easy to compute.

The following is essentially immediate from the work of Mummert and Simpson
(e.g. it follows from Lemma 12 below).

######  Lemma 10 ([7]).

The statement that every partial order $P$ can be extended to a hybrid MF-
space is equivalent over $\text{ACA}_{0}$ to $\Pi_{2}^{1}-\text{CA}_{0}$.

The question now becomes what sort of results can be proven in the hybrid
formalism. In the next section we explore Montalbán’s 15th question from [6]
in the hybrid context. We assess the strength of the metrization theorem in a
setting where basic topological definitions are easily definable, as Montalbán
desired.

However, before we move forward we note here some basic properties of the
pseudo-complement that will prove helpful later on. Note that the definition
of pseudo-complement can be naturally extended to open sets coded by reals. We
let $U^{c}=\\{p\in L|\forall q\in Uq\vee p=0\\}$, a set definable in
$\text{ACA}_{0}$. All of these properties are provable in $\text{ACA}_{0}$. In
fact, the proof is quite straightforward and precisely the same as Lemma 4.5
in [7] (a more detailed treatment can be found in [9] Lemma 4.3.11).

######  Lemma 11.

($\text{ACA}_{0}$) Fix an open set $U$ coded by a real number in a hybrid MF
space.

  1. (1)

The entire space is a disjoint union of $\text{cl}(U)$ and $U^{c}$. In
particular, every point is in exactly one of these sets.

  2. (2)

There is no point in both $U$ and $\text{cl}(U^{c})$.

We will use the above lemma freely in the proofs of the next section.

##  5\. Metrization

In MF spaces, there is a deep difference between regular spaces and the made-
for-reverse-math notion of strongly regular spaces. In fact, showing that
regular spaces are strongly regular is equivalent to
$\Pi_{2}^{1}-\text{CA}_{0}$. In hybrid MF spaces, this distinction does not
exist and can be seen in the base theory of $\text{ACA}_{0}$.

######  Lemma 12.

($\text{ACA}_{0}$) Every regular hybrid MF space is strongly regular.

###### Proof.

We only need to form the set of $p,q\in P$ such that
$\text{cl}(N_{p})\subseteq N_{q}$. This is easily done by checking the
condition $p^{c}\vee q=1$. ∎

Another previously discussed aspect of MF spaces is that it is difficult to
define the set of points. In general, the points are $\Pi_{1}^{1}$ to define.

######  Lemma 13.

The predicate $MaxFilt(X)$ which states that $X$ is a maximum filter in a
poset is $\Pi_{1}^{1}$ in general.

###### Proof.

In [7] they show that the set of $p,q$ such that $\text{cl}(N_{q})\subseteq
N_{p}$ can be $\Pi_{2}^{1}$ complete. We can write this set in terms of the
$MaxFilt(X)$ predicate as follows:

$\text{cl}(N_{q})\subseteq N_{p}\iff\forall
X~{}\big{(}MaxFilt(X)\land\forall\ell\in X\exists r~{}r\geq\ell\land r\geq
q\big{)}\to p\in X.$

If the above is $\Pi_{2}^{1}$ complete then $MaxFilt(X)$ must be strictly
$\Pi_{1}^{1}$. ∎

The above is true even if we restrict to case of regular spaces, the matter of
interest in the metrization theorem. A major contrast in the hybrid approach
is that the set of points is definable in the base theory of $\text{ACA}_{0}$
due to the following observation.

######  Lemma 14.

($\text{RCA}_{0}$) There is an arithmetic formula that is true exactly on the
maximal filters of a given regular hybrid MF space.

###### Proof.

We claim that a subset of $P$ is a maximal filter if and only if it is a
filter and for any $p\in P-M$ one of the following 2 cases hold:

  1. (1)

there is an $m\in M$ such that $p\wedge m=\emptyset$,

  2. (2)

for every $r\in D_{p}$ there is an $n\in M$ such that $r\wedge n=\emptyset$.

We first show that if one of these conditions hold of every $p\in P-M$, then
$M$ is maximal. If $M$ was not maximal, there would be a maximal filter $N$
containing some point $p\in P-M$. If Condition 1 holds of this point, then $N$
cannot be a filter as there is $p,m\in N$ with no common extension. This is an
immediate contradiction. Say instead that Condition 2 holds of the point $p$.
As the $r\in D_{q}$ cover $N_{p}$ by construction, in order theoretic terms,
any maximal filter containing $p$ must contain one of the $r\in D_{q}$.
Therefore, $N$ contains one of these $r$. However, $N$ cannot contain such an
$r$ as there is an $n\in M$ such that $r\wedge n=\emptyset$.

We now show that if $M$ is maximal then one of these conditions holds. If $M$
is maximal, then it is a point in the space, and $p$ represents an open set
that does not contain $M$. It is immediate that Condition 1 holds exactly when
$M$ is not in the closure of $N_{p}$. Therefore, we need to check that if $M$
is in the boundary of $N_{p}$, then Condition 2 holds. Consider an $r\in
D_{p}$. As $\text{cl}(N_{r})\subseteq N_{p}$, $M\not\in\text{cl}(N_{r})$.
Therefore, there is $n\in M$ such that $r\wedge n=\emptyset$, as desired. ∎

We will use the arithmetic definition of maximal filter moving forward in the
proof.

We now prove metrizability in the hybrid setting. The outline of the proof is
similar to the one in [7], but there are differing details throughout. These
details are critical as they move the complexity of the proof down from
$\Pi_{2}^{1}-\text{CA}_{0}$ to $\text{ACA}_{0}$. We start with the regularity
implies normality lemma.

######  Lemma 15.

($\text{ACA}_{0}$) Let $X$ be a hybrid MF space. There are functionals
$\nu_{1},\nu_{2}$ with the following property. If $U$ and $V$ are open subsets
of $X$ and $\text{cl}(U)\cap\text{cl}(V)=\emptyset$, then $\nu_{1}(U,V)$ and
$\nu_{2}(U,V)$ are disjoint open subsets of $X$ such that
$\text{cl}(U)\subseteq\nu_{1}(U,V)$ and $\text{cl}(V)\subseteq\nu_{2}(U,V)$.

###### Proof.

For an open set $W$, let $\\{e(W,n)\\}_{n\in\omega}$ be an enumeration of the
union of $D_{p}$ for $p\in W$ in increasing order. Let

$U(n)=e(U^{c},n)\cap\bigcap_{i\leq n}(e(V^{c},i))^{c}$
$V(n)=e(V^{c},n)\cap\bigcap_{i\leq n}(e(U^{c},i))^{c}$

be the corresponding elements of $L$.

Define

$\nu_{1}(U,V)=\\{V(n)\\}_{n\in\omega},$
$\nu_{2}(U,V)=\\{C(n)\\}_{n\in\omega}.$

The classical proof that these functionals have the desired properties now
goes through in $\text{ACA}_{0}$. To be specific, let $x\in\text{cl}(U)$. As
$\text{cl}(U)\cap\text{cl}(V)=\emptyset$, this means that $x\in e(V^{c},n)$
for some $n$. Furthermore, if $x\not\in e(U^{c},i)^{c}$ this means that every
open set containing $x$ intersects $e(U^{c},i)$. However, this means that
$x\in\text{cl}(U^{c},i)\subseteq U^{c}$. This is a contradiction to the fact
that $x\in\text{cl}(U)$. Therefore, $x\in V(n)$ for some $n$. A similar and
symmetric proof demonstrates this point for $V$.

To see that the two open sets are disjoint, note that if $x\in U(n)$ for some
$n$ it is in $e(U^{c},n)$ and each of the $(e(V^{c},i))^{c}$ for $i\leq n$.
This means that $x$ is not in $V(m)$ for $m\leq n$ as $(e(U^{c},m))^{c}\cap
e(U^{c},m)=\emptyset$. Furthermore, $x$ is not in $V(m)$ for $m\geq n$ as
$(e(V^{c},m))^{c}\cap e(V^{c},m)=\emptyset$. This completes the proof.

∎

######  Lemma 16.

($\text{ACA}_{0}$) Fix $p\in P$ and $q\in R_{p}$. Let D be the set of dyadic
rational numbers in the interval $[0,1]$. There is a map $g_{p,q}$ from $D$ to
coded open subsets of $X$ such that $g_{p,q}(0)=\\{q\\}$,
$g_{p,q}(1)=\\{p\\}$, and $\text{cl}(g_{p,q}(k))\subseteq g_{p,q}(k^{\prime})$
whenever $k<k^{\prime}$.

###### Proof.

Let $U_{0}=\\{q\\}$ and $U_{1}=\\{p\\}$. We define the rest of the $U_{k}$ for
dyadic $k$ by induction. Throughout the induction we will maintain that for
dyadic rationals $k<k^{\prime}$, $\text{cl}(U_{k})\subseteq U_{k^{\prime}}$.
Let us note that this is an arithmetic condition. In particular, we can check
if $U_{k}^{c}\cup U_{k^{\prime}}=1$. This means that we can preform our
induction within $\text{ACA}_{0}$.

We assume that the map has already been defined for all dyadic $k$ with
reduced form $\frac{a}{2^{m}}$. We show how to define the map on dyadic $\ell$
with reduced form $\frac{b}{2^{m+1}}$. Select $k<k^{\prime}$ with reduced form
$\frac{a}{2^{m}}$ that are the closest to $\ell$. We have that
$\ell=\frac{k+k^{\prime}}{2}$. By induction, we assume that
$\text{cl}(U_{k})\subseteq U_{k^{\prime}}$. In other words, we have that
$\text{cl}(U_{k})\cap\text{cl}(U_{k^{\prime}}^{c})=\emptyset$, as otherwise
there would be a point in both $U_{k^{\prime}}$ and $U^{c}_{k^{\prime}}$. This
means that we define the $U_{\ell}$ as
$U_{\ell}=\nu_{1}(U_{k},U_{k^{\prime}}^{c})$. By the previous lemma this can
be done in $\text{ACA}_{0}$. Furthermore, we are guaranteed that
$\text{cl}(U_{k})\subseteq U_{\ell}$. Lastly, we claim that
$\text{cl}(U_{\ell})$ is contained in $U_{k^{\prime}}$. Note that
$\nu_{2}(U_{k},U_{k^{\prime}}^{c})$ is an open disjoint from $U_{\ell}$ by
construction. Furthermore, $\nu_{2}(U_{k},U_{k^{\prime}}^{c})$ contains the
closure of $U_{k^{\prime}}^{c}$. Therefore, every point not in
$\nu_{2}(U_{k},U_{k^{\prime}}^{c})$ must be in $U_{k^{\prime}}$, and in
particular every point in $U_{\ell}$ is in $U_{k^{\prime}}$ as required. ∎

The next three results have arguments that are quite similar to those found in
[7] (and indeed they are also quite similar to the classical arguments). There
are not many details different from the argument for ordinary MF spaces and
hybrid MF spaces because the arguments produced in [7] already go through at
the lower complexity level of $\text{ACA}_{0}$. The proofs of these
intermediate lemmas are still produced here, but not in full detail; one ought
to examine [7] Lemmas 4.7-4.10 or [9] Lemmas 4.3.12, 4.3.13, and 4.3.18 for
further details.

######  Lemma 17.

($\text{ACA}_{0}$) There is a sequence $\langle f_{p,q}|p\in P,q\in
R_{p}\rangle$ of continuous functions from $P\to[0,\infty)$ such that for all
$p\in P$ and $q\in R_{p}$ we have $f_{p,q}(N_{q})=0$ and $f_{p,q}(X-N_{p})=1$.

###### Proof.

We can form the set $\langle g_{p,q}|p\in P,q\in R_{p}\rangle$ for all $p$ and
$q$ by the previous lemma. We extend $g_{p,q}$ to all positive dyadic
rationals by letting $g_{p,q}(k)$ be the whole space if $k>1$. As in the
previous lemma, $U_{k}$ is meant to indicate the open set coded by
$g_{p,q}(k)$. Let

$f_{p,q}=\inf\\{k\in D^{+}|x\in U_{k}\\}.$

It is clear that these $f_{p,q}$ satisfy the desired conclusion. This can be
executed in $\text{ACA}_{0}$. $f_{p,q}(x)<k$ if and only if there is some
$k^{\prime}<k$ with $x\in U_{k^{\prime}}$ if and only if there is $r\in P$
with $r\in x\cap U_{k^{\prime}}$. To see $f_{p,q}(x)>k$ you similarly check
for a $k^{\prime\prime}>k$ with $x\in U_{k^{\prime}}^{c}$ which can be seen by
looking for an $r\in P$ with $r\in x\cap U_{k^{\prime\prime}}^{c}$. This is
enough to define the output of $f$. ∎

From this, we get the desired metrizability.

######  Proposition 18.

($\text{ACA}_{0}$) Every hybrid MF space is metrizable.

###### Proof.

Reindex the function from the above lemma to be $f_{n}$ and let

$d(x,y)=\sum_{n\in\omega}2^{-n}|f_{n}(x)-f_{n}(y)|.$

The classical proof of Uryshon’s metrization theorem is straightforward and
shows that this is a metric. ∎

At this point we pause to note that the above development answers Question 4.1
from [7], in a certain sense. They ask what can be said about the reverse
mathematical strength of stating that every strongly regular MF space has a
(not necessarily complete) metric. By moving to a different representation
meant to easily capture topological notions like strong regularity, we are
able to show this in the base theory of $\text{ACA}_{0}$. Or course, in a
stricter sense their question remains open.

We now wish to show that hybrid MF spaces are completely metrizable. It is in
fact this theorem that was shown in [7] to be equivalent to
$\Pi_{2}^{1}-\text{CA}_{0}$.

We use the following lemma to demonstrate this, which states that in
$\text{RCA}_{0}$ every $G_{\delta}$ subset of a completely metrizable space is
completely metrizable.

######  Lemma 19.

($\text{RCA}_{0}$) If $(U_{i})$ is a sequence of open sets in a complete,
separable metric space $(\hat{A},D)$, the there is a complete metric
$d^{\prime}$ such on $\bigcap_{i}U_{i}$ that agrees with the subspace topology
on $\bigcap_{i}U_{i}$. Furthermore, if $D\subseteq\bigcap_{i}U_{i}$ is
computable and dense then this topology is canonically isomorphic to
$\hat{D}$.

###### Proof.

This follows from the classical proof see e.g. [4] Theorem 3.11. More details
for the context of reverse mathematics can be found in [9] Lemma 4.3.18. ∎

Given a hybrid MF space $X$ we let $A\subseteq X$ be a computable dense set
definable in $\text{ACA}_{0}$. Note that this can be found; given non-empty
$p\in P$ we find a maximal filter containing $p$ by recursion. Let $p_{0}=p$,
and let $p_{i+1}$ be the least element of $P$ that has non-zero intersection
with $p_{0},\cdots,p_{i}$ and non-zero intersection with some sequence of
elements in $D_{p_{0}}\times\cdots\times D_{p_{i}}$. By Lemma 14 this is
enough to guarantee that we build a maximal filter in the limit. We show first
that $X$ is isometrically embeddable in $\hat{A}$, the completion of $A$, and
then we show that the image of this embedding is $G_{\delta}$.

To formalize the idea of a continuous map between an MF space and a metric
space we take the following definition.

######  Definition 20.

A continuous function code $F$ between a hybrid MF space based on the poset
$P$ and a complete metric space given by a dense set $A$ is given by a set of
pairs $\langle p,\langle a,r\rangle\rangle\in P\times A\times\mathbb{R}$. $F$
induces a partial function from $MF(P)$ to $\hat{A}$. We say that $F$ is
defined at $m\in MF(P)$ if for every sequence of elements in $m_{i}\in m$
there is $\langle m_{i},\langle a_{i},r_{i}\rangle\rangle\in F$ with $r_{i}\to
0$. Furthermore, for every such $\langle m_{i},\langle
a_{i},r_{i}\rangle\rangle\in F$ with $r_{i}\to 0$, the $a_{i}$ are a Cauchy
sequence in the same equivalence class. In this case we say that $F$ sends $m$
to this unique equivalence class of Cauchy sequences. A coded continuous
function is one that is a total function induced by a continuous function
code.

It is not too difficult to see in ZFC that every continuous function between a
hybrid MF space and a complete metric space is induced by such a code. It is
enough to check that given such a function $f$, $\\{\langle p,\langle
a,r\rangle\rangle\in P\times A\times\mathbb{R}|f(N_{p})\subseteq B_{r}(a)\\}$
is a continuous function code for $f$.

######  Lemma 21.

($\text{ACA}_{0}$) If $X$ is a metrizable countably based hybrid MF space,
there is a separable complete metric space $\hat{A}$ and a continuous, open
bijection $h$ between $X$ and a dense subset of $A$. Furthermore, $h$ is an
isometry.

###### Proof.

Define the metric $d$ on $X$ with Proposition 18. Let $A$ be a countable dense
subset of $X$. For each $p\in P$,

$diam(p):=\sup\\{d(a,b)|a,b\in A\cap N_{p}\\}.$

Let $H$ be the set of all $\langle p,\langle a,r\rangle\rangle$ such that
$diam(p)<r$ and $a\in N_{p}$.

Consider $m$ a maximal filter in $P$. We first find a $\langle m_{i},\langle
a_{i},r_{i}\rangle\rangle\in H$ with $r_{i}\to 0$. Let $b_{i}$ be a sequence
of points in $A$ that converge to $m$. Because $X$ is metrizable, there is
some $p\in m$ such that $diam(p)\leq 2^{-n-1}$. Let $b_{i(n)}$ be such that
$b_{i(n)}\in N_{p}$. This yields that $\langle m_{i},\langle
b_{i},2^{-n}\rangle\rangle\in H$. As $n$ was arbitrary this gives the needed
sequence.

Now consider two distinct $\langle m_{i},\langle
a_{i},r_{i}\rangle\rangle,\langle m_{i}^{\prime},\langle
a_{i}^{\prime},r_{i}^{\prime}\rangle\rangle\in H$. Say that $r_{i}\to 0$ and
$r_{i}^{\prime}\to 0$ and they are both decreasing without loss of generality.
By definition, $d(a_{i},m)<{r_{i}}$ and
$d(a_{i}^{\prime},m)<{r_{i}^{\prime}}$. This means that for all $j\geq i$
$d(a_{i},a_{j})<2{r_{i}}$ and
$d(a_{i}^{\prime},a_{j}^{\prime})<2{r_{i}^{\prime}}$. Or, what is the same,
the sequences are Cauchy. Furthermore,
$d(a_{i},a_{i}^{\prime})<{r_{i}+r_{i}^{\prime}}$ and therefore tends to $0$
too. This means that the sequences $a_{i}$ and $a_{i}^{\prime}$ must be in the
same equivalence class as desired.

It is clear that the $h$ that $H$ codes is an isometry because it is an
isometry on the dense set $A$ shared between the spaces. As $h$ is an
isometry, it is open on its dense image. ∎

We will also use the Paracompactness Lemma from Theorem II.7.2 in [11].

######  Lemma 22.

($\text{RCA}_{0}$) Given a complete, separable metric space $(A,d)$, there is
a computable functional $\Phi$ that, given a sequence of opens $U_{i}$,
returns a point finite refinement $V_{i}$

######  Theorem 23.

($\text{ACA}_{0}$) Every hybrid MF space is completely metrizable.

###### Proof.

We wish to construct a sequence of open subsets of $\hat{A}$ that witness that
$\text{im}(h)$ from Lemma 21 is $G_{\delta}$. From here we will appeal to
Lemma 19 to complete the proof.

By our previous results, we obtain a metric $d$ on $X$ that induces the
topology, along with a set of witnesses $R_{p}$ for $p\in P$ for the strong
regularity of $X$. We construct countable sequences of open sets and will form
a tree of these sequences. The odd entries in the sequences, denoted $W_{i}$,
will be themselves sequences of balls in the metric topology centered on $a\in
A$. The even entries will be elements $q_{i}\in P$ that represent basic open
sets in the MF topology. In this notation, the sequences will look like
$(W_{0},q_{0},\cdots,W_{n},q_{n})$ or $(W_{0},q_{0},\cdots,q_{n},W_{n+1})$. To
define the precise tree we are working with, we put the following restrictions
on the sequences:

  1. (1)

For every $i$ and $q_{i}$, there is a basic open ball $B$ enumerated in
$W_{i}$ such that $N_{q}\subseteq B$.

  2. (2)

For every $i$, $q_{i+1}\leq_{P}q_{i}$.

  3. (3)

For every $i$, $\text{diam}(q_{i})<2^{-i}$.

  4. (4)

$W_{0}$ is an element of the point finite refinement of the canonical
${B(a,1)}_{a\in A}$ covering of $X$.

  5. (5)

$W_{i+1}$ is an element of the point finite refinement of the cover of the
element $W_{i}$ given by the set of $N_{q_{i}}$ such that the $q_{i}$ satisfy
Conditions 1-3.

It is clear that Conditions 1-4 are arithmetic. Condition 5 is also
arithmetic, but requires more explanation. In the statement of Condition 5, it
is implicitly assumed that the set of $N_{q_{i}}$ satisfying Conditions 1-3
cover $W_{i}$. We start by showing this. Consider a point $x\in W_{i}$. Take a
point $a\in A$ with $d(x,a)<2^{-i}$. The set $B(a,2^{-i})\cap W_{i}$ is open,
and is therefore a union of $N_{r}$ for $r\in P$. In particular, for some $c$
with $N_{c}\subseteq B(a,2^{-i})\cap W_{i}$, $x\in N_{c}$. If $i>0$, then the
$W_{i}$ came from a point finite refinement of $q_{i-1}$, so, $W_{i}\subseteq
N_{q_{i-1}}$. This means that, considering $x$ as a filter, $q_{i-1},c\in x$.
Take $q_{i}$ to be a common extension of $q_{i-1}$ and $c$. It can now be see
that $x\in N_{q_{i}}$ with all of the desired properties.

Strictly speaking, we can only apply the paracompactness functional to balls
in the space, not the opens given by the maximal filter space. That being
said, we can obtain a description for $N_{q}$ in terms of balls
arithmetically, which fixes this issue. In particular, given $N_{q}$, let

$U_{q}=\\{B|\exists p\in R_{q}~{}~{}B\cap A\subseteq N_{p}\cap A\\}.$

Mummert shows that $N_{q}=\bigcup_{B\in U_{q}}B$ in Lemma 4.3 of [7]. In terms
of reverse mathematics, when we say "the point finite refinement of the cover
of the element $W_{i}$ given by the set of $N_{q_{i}}$ such that…" we
precisely mean "the point finite refinement of the cover of the element
$W_{i}$ given by the set of $U_{q_{i}}$ such that…"

With this, it should be clear that the above conditions are well defined and,
in fact, arithmetic. Because the satisfaction of these properties is
determined locally by looking at the preceding elements in the finite
sequence, it is clear that the sequences satisfying the conditions form a
countable tree definable in $\text{ACA}_{0}$. We call this tree $T$. We now
define the open sets $C_{i}$ as the union of the $2i+1$st level of $T$. We
claim that $\text{im}(h)=\bigcap_{i}C_{i}$.

We first show that $\text{im}(h)\subseteq\bigcap_{i}C_{i}$. Given
$x\in\text{im}(h)$, we show that $\forall i~{}x\in C_{i}$ by induction.
$C_{0}$ is a cover by definition so it contains $x$. By the argument above, if
$x\in C_{i}$ because $x\in W_{i}$, there is an extension $q_{i}$ with $x\in
N_{q_{i}}$. Furthermore, because the paracompactness functional maintains
covers, $x$ must be in some $W_{i+1}$. Therefore, $x\in C_{i+1}$ as desired.

We now show that $\bigcap_{i}C_{i}\subseteq\text{im}(h)$. Fix
$z\in\bigcap_{i}C_{i}$. We form the tree, $T_{z}$, which contains all
sequences $(W_{0},\cdots,W_{n})$ that are odd projections from elements of $T$
with $x\in W_{n}$. $T_{z}$ is infinite as there are arbitrarily long paths,
because $z\in C_{i}$ for all $i$. However, $T_{z}$ is finitely branching. By
construction, once you fix $W_{i}$ the possible extensions form a point finite
cover, so only finitely many of them contain $z$. This means that only
finitely many of these extensions are in $T_{z}$, as we claimed. By Konig’s
Lemma there is an infinite path through the tree $(W_{i})_{i\in\omega}$. By
definition, $z\in\bigcap_{i}W_{i}$. This corresponds to a sequence $q_{i}$ in
the even projection from the tree $T$ with $z\in\bigcap_{i}q_{i}$. Note that
the $q_{i}$ are arbitrarily small, so $\bigcap_{i}q_{i}$ has only one point.
Now consider $m=\text{ucl}_{L}((q_{i})_{i\in\omega})\subseteq P$. It is not
difficult to see that $m$ is a filter. We now show that it is maximal. If it
was not maximal, there would be an $r\in P-m$ with $c\in D_{r}$ such that for
all $i$ $c\wedge q_{i}\neq\emptyset$. Let
$\varepsilon=d(\bar{N_{c}},\bar{N_{r}^{c}})$, positive by regularity. Take $i$
with $2^{-i}<\varepsilon$ and note that $q_{i}\leq_{L}r$. Therefore, $r\in m$,
a contradiction. This gives that the image of $m$ under $h$ must be $z$.
Therefore, $z\in\text{im}(h)$, as desired.

Lemma 19 completes the proof. ∎

##  6\. Some Complexity Calculations and Future Work

We define a map which demonstrates a few interesting complexity calculations.
These calculations suggest directions for future work.

######  Definition 24.

Given a tree $\mathcal{T}\subseteq\mathbb{N}^{<\mathbb{N}}$ we define
$\Phi(\mathcal{T})\subseteq(\mathbb{N}\cup\\{*\\})^{<\mathbb{N}}$ where $*$ is
a symbol not among $\mathbb{N}$. We take
$\Phi(\mathcal{T})=\\{\sigma^{\frown}*|\sigma\in\mathcal{T}\\}\cup\mathcal{T}$.

Note that given a tree, we can understand it as a partial ordering via the
inclusion relation. In particular, every tree also codes an MF space.
Furthermore, in $\text{ACA}_{0}$ this MF space can be extended to a hybrid MF
space. It is easy to confirm $\leq_{P}$ and $\leq_{L}$ coincide as the maximal
filters are the maximal paths through the tree and the points in the tree just
contain each path that includes them. One can then extend the structure to
include $0,1,\wedge,\vee,^{c}$ in a direct way. In what follows, we consider
trees as a hybrid MF space in the manner described above.

######  Lemma 25.

Every $\mathcal{T}\subseteq\mathbb{N}^{<\mathbb{N}}$ represents a regular
topology.

###### Proof.

It was observed above that $\leq_{P}$ and $\leq_{L}$ coincide in the topology
of $\mathcal{T}$. Furthermore, it can be confirmed that given
$\sigma,\tau\in\mathcal{T}$ their meet is the longest common initial segment
of $\sigma$ and $\tau$. The meet is of $\sigma$ and $\tau$ are then inside of
the poset $P$. This means that $\mathcal{T}$ represents a proper MF space. By
Proposition 8, this means that the basis is clopen.

In other words for $x\in N_{p}$, it is enough to note that
$\text{Cl}(N_{p})\subseteq N_{p}$ to see that there is a witness to regularity
for the pair $x,p$ (namely $p$ itself). ∎

######  Proposition 26.

The set of discrete, regular hybrid MF spaces is $\mathbf{\Pi}_{1}^{1}$
complete.

###### Proof.

First we note that there is a $\mathbf{\Pi}_{1}^{1}$ definition. Being
discrete for a regular space is equivalent to saying there are no limit
points; in other words, no sequence of points converges to any particular
point. This can be expressed as

$\forall
X,\\{Y_{i}\\}_{i\in\omega}\big{(}\mathop{\mathchoice{\bigwedge\mkern-15.0mu\bigwedge}{\bigwedge\mkern-12.5mu\bigwedge}{\bigwedge\mkern-12.5mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}MaxFilt(Y_{i})\land
MaxFilt(X)\big{)}\to\exists p\in P~{}p\in
X\land\mathop{\mathchoice{\bigwedge\mkern-15.0mu\bigwedge}{\bigwedge\mkern-12.5mu\bigwedge}{\bigwedge\mkern-12.5mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}p\not\in
Y_{i}.$

By Lemma 14 , $MaxFilt(X)$ can be expressed as an arithmetic formula, so the
above expression is $\Pi_{1}^{1}$ in $P$ as desired.

We now note that $\Phi(\mathcal{T})$ is discrete if and only if $\mathcal{T}$
is well-founded. Note that if $\mathcal{T}$ is well-founded, so is
$\Phi(\mathcal{T})$. In any well-founded tree the maximal filters are finite,
and are therefore isolated by the unique maximal string in the filter.
Therefore, any well-founded tree gives rise to a discrete space. If
$\mathcal{T}$ is not well-founded let $A$ be a path in $T$. It is
straightforward to confirm that $A$ is a limit point of
$(A\operatorname{\upharpoonright}n)^{\frown}*$, so $\Phi(\mathcal{T})$ is not
discrete. ∎

The above calculation is made exact by the fact that $MaxFilt(X)$ can be
expressed as an arithmetic formula. It does not yield a similar result with
ordinary MF spaces as the given definition of discreteness would be
$\Pi_{2}^{1}$ in $P$. This is a good example of how moving to the hybrid
formalism can allow for greater expressive power in a way that facilitates
calculations above the level of ACA0. The same comments apply to the example
below.

######  Proposition 27.

The set of covers of a regular hybrid MF spaces are $\mathbf{\Pi}_{1}^{1}$
complete.

###### Proof.

First we note that there is a $\mathbf{\Pi}_{1}^{1}$ definition. To say that a
set of opens $\\{p_{i}\\}_{i\in\omega}$ covers a space is to say every maximal
filter contains one of these points. This can be expressed as

$\forall
X~{}MaxFilt(X)\to\mathop{\mathchoice{\bigvee\mkern-15.0mu\bigvee}{\bigvee\mkern-12.5mu\bigvee}{\bigvee\mkern-12.5mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}p_{i}\in
X.$

By Lemma 14 , $MaxFilt(X)$ can be expressed as an arithmetic formula, so the
above expression is $\Pi_{1}^{1}$ in $\\{p_{i}\\}_{i\in\omega}$ as desired.

We now note that $\\{\sigma^{\frown}*|\sigma\in\mathcal{T}\\}$ covers
$\Phi(\mathcal{T})$ if and only if $\mathcal{T}$ is well-founded. If
$\mathcal{T}$ is well-founded the maximal filters in $\Phi(\mathcal{T})$ are
all maximal finite segments. By construction, these all end in $*$; i.e. there
is a point in the filter among $\\{\sigma^{\frown}*|\sigma\in\mathcal{T}\\}$.
Therefore, $\\{\sigma^{\frown}*|\sigma\in\mathcal{T}\\}$ covers
$\Phi(\mathcal{T})$. If $\mathcal{T}$ is If $\mathcal{T}$ is not well-founded
let $A$ be a path in $T$. It is straightforward to confirm that $A$ is a point
in $\Phi(\mathcal{T})$ that is not within
$\\{\sigma^{\frown}*|\sigma\in\mathcal{T}\\}$. ∎

This proposition begins to aim at the theory of compactness in which covers
play a central role. The following remains an open and motivating question for
further development of this area.

######  Question 1.

What is the reverse mathematical strength of the one point compactification
theorem?

## References

  * [1] Douglas K. Brown.  Notions of closed subsets of a complete separable metric space in weak subsystems of second-order arithmetic.  In Logic and computation (Pittsburgh, PA, 1987), volume 106 of Contemp. Math., pages 39–50. Amer. Math. Soc., Providence, RI, 1990\.
  * [2] Damir D. Dzhafarov and Carl Mummert.  Reverse mathematics—problems, reductions, and proofs.  Theory and Applications of Computability. Springer, Cham, [2022] ©2022.
  * [3] François G. Dorais.  Reverse mathematics of compact countable second-countable spaces.  https://arxiv.org/abs/1110.6555, 2011.
  * [4] Alexander S. Kechris.  Classical descriptive set theory, volume 156 of Graduate Texts in Mathematics.  Springer-Verlag, New York, 1995.
  * [5] Steffen Lempp and Carl Mummert.  Filters on computable posets.  Notre Dame J. Formal Logic, 47(4):479–485, 2006.
  * [6] Antonio Montalbán.  Open questions in reverse mathematics.  Bull. Symbolic Logic, 17(3):431–454, 2011.
  * [7] Carl Mummert and Stephen G. Simpson.  Reverse mathematics and $\Pi_{2}^{1}$ comprehension.  Bull. Symbolic Logic, 11(4):526–533, 2005.
  * [8] Carl Mummert and Frank Stephan.  Topological aspects of poset spaces.  Michigan Math. J., 59(1):3–24, 2010.
  * [9] Carl Mummert.  On the reverse mathematics of general topology.  ProQuest LLC, Ann Arbor, MI, 2005.  Thesis (Ph.D.)–The Pennsylvania State University.
  * [10] Paul Shafer.  The strength of compactness for countable complete linear orders.  Computability, 9(1):25–36, 2020.
  * [11] Stephen G. Simpson.  Subsystems of second order arithmetic.  Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009.