# Conclusion-based Counter-Argument Generation

Milad Alshomary $\dagger$ Henning Wachsmuth $\dagger$
$\dagger$Leibniz University Hannover, Institute of Artificial Intelligence
<EMAIL_ADDRESS>

###### Abstract

In real-world debates, the most common way to counter an argument is to reason
against its main point, that is, its conclusion. Existing work on the
automatic generation of natural language counter-arguments does not address
the relation to the conclusion, possibly because many arguments leave their
conclusion implicit. In this paper, we hypothesize that the key to effective
counter-argument generation is to explicitly model the argument’s conclusion
and to ensure that the stance of the generated counter is opposite to that
conclusion. In particular, we propose a multitask approach that jointly learns
to generate both the conclusion and the counter of an input argument. The
approach employs a stance-based ranking component that selects the counter
from a diverse set of generated candidates whose stance best opposes the
generated conclusion. In both automatic and manual evaluation, we provide
evidence that our approach generates more relevant and stance-adhering
counters than strong baselines.

##  1 Introduction

Given an argument, a valid counter-argument should be relevant to the topic
discussed by the argument while opposing to its conclusion’s stance.
Countering the opponent’s arguments in a debate effectively is key to winning
the debate Zhang et al. (2016). While some counter-arguments attack an
argument’s premises or their connection to the conclusion, the most common way
is to directly rebut the argument’s conclusion Walton (2009).

The automatic countering of natural language arguments is one of the most
challenging tasks in the area of computational argumentation. Previous work
has addressed the task through retrieval Wachsmuth et al. (2018); Orbach et
al. (2020) or generation-based approaches Hua and Wang (2018); Hidey and
McKeown (2019). By concept, the former requires the presence of suitable
counter-arguments in a predefined collection, limiting its flexibility.
Existing generation-based approaches, on the other hand, either consider a
single claim as input or do not model the relation between premise and
conclusion in the input argument. In daily-life debates, however, people often
do not explicitly state their argument’s main point (i.e., its conclusion),
since it is often clear from the context Habernal and Gurevych (2015). This
makes it challenging for computational models to generate a proper counter.
Table 1 shows an example of an argument with the conclusion “Purchasing meat
is encouraging animal abuse”. The author states that meat production would
often lead to animal abuse. However, this statement is never linked explicitly
to the conclusion. Such a link may be easy to infer for humans, but it is
challenging for machines.

Conclusion (title): Purchasing meat encourages animal abuse.
---
Premises (post): All meat, to my knowledge, is obtained by raising animals in
cramped quarters and slaughtering them as soon as they are fully grown. The
only exception i can think of is perhaps when you go into the woods and hunt
food for yourself in which case the animal has lived an undisturbed life and
is put down by humane means compared to how it happens in nature. However,
this is, of course, time intensive, requires skill, expensive, and thus is of
course not how the vast majority of meat is obtained.
Table 1: An example argument (conclusion + premises) taken from Reddit
ChangeMyView, showing how the conclusion is mentioned implicitly only in the
body.

State-of-the-art transformer-based language models excel in many downstream
text generation tasks, such as summarization and machine translation Vaswani
et al. (2017). While they have been applied successfully for reconstructing
implicit argument components such as conclusions Gurcke et al. (2021); Syed et
al. (2021), even they still fall short on more complex tasks, such as counter-
argument generation Hua and Wang (2019).

In this paper, we study how to enable transformer-based language models to
generate an effective counter-argument to a given argument. We observe that
the performance of these models in generating relevant counters with correct
stance deteriorates particularly when the input argument does not mention its
conclusion. Hence, we hypothesize that explicitly modeling the argument’s
conclusion and its stance will lead to more adequate counter-arguments. For
this purpose, we propose a multitask generation approach with a stance-based
ranking component. Our approach jointly models the two tasks of conclusion
generation and counter-argument generation, and it ensures stance correctness
through a stance-based ranking component.

Given a training dataset, where we have access to both the premises of
arguments and their corresponding conclusions and counters, we explore two
variations of the approach: The first shares the transformer’s encoder and
decoder between the two tasks, and we learn to generate both the conclusion
and the counter as one sequence (separated with a special token). By contrast,
the second variation is composed of one shared encoder along with two
decoders, one to generate the conclusion and the other to generate the
counter-argument. Although we expect the trained models to often capture the
stance relation between the argument and its counter, we reinforce opposite
stance through a stance-based ranking component at inference time. This
component samples different counter-arguments and ranks them based on their
stance score towards the corresponding generated conclusion.

To evaluate both approach variations, we use the ChangeMyView dataset of Jo et
al. (2020) that consists of discussions where someone posts a view and others
write comments opposing to this view. In line with related work Alshomary et
al. (2021b), we use a post’s title as the conclusion, its body text as the
premises, and each comment as a counter. To classify stance as part of our
ranking component, we fine-tune RoBERTa Liu et al. (2019) on a dataset of
pairs of claim and counter-claim collected from the Kialo.org debate platform.
We compare the approach variations against two baselines; one that learns to
generate the conclusion and the counter-argument independently in a pipeline
model and one that employs a sequence-to-sequence model but does not learn
actively to represent the conclusion. The results demonstrate the deficiency
of standard transformer-based models, particularly when the conclusion is not
mentioned explicitly, highlighting the importance of conclusions in counter-
argument generation. In most cases, our variation with shared encoder and
decoder produces the best counter-arguments in terms of relevance and stance
correctness.

We summarize our contributions as follows:111Code is attached in the
materials, and will be made publicly available upon acceptance.

  * •

We study how to generate effective counter-arguments even if the attacked
argument’s conclusion is implicit.

  * •

We present two multitask transformer-based counter-argument approaches, tuned
to opposing to the argument’s conclusion.

  * •

We reveal the impact of modeling an argument’s conclusion and counter-argument
jointly in the given task.

##  2 Related Work

Argument generation is one of the main branches of computational
argumentation, studying the synthesis of arguments in natural language texts.
This field includes a host of tasks like the generation of argument
conclusions Alshomary et al. (2020); Syed et al. (2021), implicit premises
Chakrabarty et al. (2021), controlled claims Schiller et al. (2021); Alshomary
et al. (2021a), as well as the generation of counter-arguments Hua and Wang
(2018); Alshomary et al. (2021b). Our work studies the task of counter-
argument synthesis.

The task of counter-argument synthesis has been addressed through either
retrieval or generation-based approaches. An example of the former is the work
of Orbach et al. (2020) whose approach tries to retrieve relevant counters for
a given argument from a collection of documents. Wachsmuth et al. (2018)
utilized topic knowledge to retrieve the best counter for a given argument.

On the other hand, generation-based approaches aim to construct counter-
arguments from scratch. For example, both Bilu et al. (2015) and Hidey and
McKeown (2019) worked on the task of counter-claim generation. The former
developed a set of rules and classifiers to negate claims, while the latter
used neural methods to learn from data. Alshomary et al. (2021b) proposed an
approach to generate counter-arguments by automatically identifying weak
points in the input argument given the conclusion and attacking them.
Moreover, Hua and Wang (2018, 2019) proposed an approach for generating long
texts and applied it to the counter-argument generation task. Their approach
relies on a retrieval component that acquires relevant key phrases for an
input argument to be used to guide the generation of counter-arguments. While
the size of the given argument collection limits retrieval-based approaches,
the generation-based approaches either rely on the conclusion being given in
the input or don’t distinguish the different components in the input
argumentative text. Our proposed approach is generation-based, where we study
the conclusion’s role in the counter-argument generation task.

Argument conclusion is the main point an argument argues towards/against,
which is important for understanding the argument. In daily life
argumentation, conclusions often are left implicit Alshomary et al. (2020).
While it is easy for humans to infer the main point of an argument, it remains
a challenging task for machines. Hence, several works have addressed the task
of conclusion inference. Alshomary et al. (2020) reconstructed implicit claim
targets from argument premises using triplet neural networks. Syed et al.
(2021) studied the effectiveness of several transformer-based models on the
conclusion generation and evaluated the informativeness criteria of
conclusions. Gurcke et al. (2021) utilized conclusion generation to study
argument quality. Our proposed approach also generates conclusions for a given
argument as the first step in order to generate reliable counters.

##  3 Approach

Figure 1: Proposed approach to counter-argument generation. In the _training
phase_ , we learn to jointly generate the conclusion and counter either as one
sequence (Joint-based One-seq) or as two separated sequences (Joint-based Two-
decoders). In the _inference phase_ , we classify and rank a diverse set of
counters with respect to their stance towards the corresponding conclusion.

As discussed above, the conclusions of arguments are important for
understanding them properly. However, they are often left implicit, making
understanding hard for machines. Our goal is to study how the absence of
conclusions affects the performance of transformer-based counter-argument
generation models. To alleviate this problem, we propose an approach that
jointly learns to generate both the conclusion and the counter of an argument.
At inference time, it utilizes a stance-based ranking component to select the
most contrastive candidate counter in each case. We detail the generation and
ranking in the following.

###  3.1 Joint Generation of Conclusions and Counters

Text generation is usually modeled as a sequence-to-sequence generation task
and is widely addressed through transformer-based encoder-decoder models
Vaswani et al. (2017). Since we aim to learn two generation tasks (conclusion
and counter), one could think of either sharing the full model between the two
tasks or only the encoder part. Hence, as illustrated in Figure 1, we
experiment with both options to realize our approach:

#### Fully-shared Encoder and Decoder

In the first model, we maintain the same transformer-based encoder-decoder
architecture and train it to generate output sequences containing both the
conclusion and the counter. Hence, the model learns to perform the two tasks
simultaneously. Particularly, the input to the model is one sequence
representing an argument’s premises, and the output is a single sequence
composed of the ground-truth conclusion and counter-argument separated by
special tokens, <conclusion> and <counter>. The model encodes premises and
decodes first the conclusion and then the counter in one sequence. We train
the model to optimize the following loss function:

$L(\theta)=-\sum_{1}^{n}\log p(y_{i}|X,y_{<i};\theta)$

Where $X$ is the input sequence representing premises, $y$ is the sequence
composing the conclusion and counter, and $\theta$ is the model’s parameters.
We call this model Joint One-seq later in our experiments.

At inference time, we utilize a mechanism to generate a diverse set of $n$
candidate conclusions and their counter-arguments, which are later passed to
our stance-based ranking component to select the best counter. The diverse
generation is as follows. We first extract a set of $m$ Wikipedia concepts
from the input premises using the approach of Dor et al. (2018). Then, during
decoding, we use these concepts to prompt our trained model by masking all
logits except the ones matching the prompt tokens, resulting in conclusions
addressing different aspects of the premises followed by their corresponding
counters. Moreover, to ensure candidate diversity, we enable nucleus sampling
Holtzman et al. (2019), where at each step, we randomly select one of the top
$k$ tokens with an accumulated probability of more than $p$.

#### Shared Encoder with two Decoders

Similarly, the second model starts with an argument’s premises as input.
However, it then decodes two independent sequences representing the conclusion
and the counter-argument as output. First, the input premises are passed
through a shared encoder, and then two decoders are used to learn to generate
the counter and the conclusion. During training, we optimize the following
multi-task loss function, which is a weighted average of the two language
modeling losses of the two decoders:222The best weights, $\alpha_{a}$ and
$\alpha_{b}$ are determined experimentally during validation.

$\displaystyle L(\theta_{e},\theta_{a},\theta_{b})\;=\;$
$\displaystyle\alpha_{a}\cdot\sum_{1}^{n}\log
p(y^{a}_{i}|X,y^{a}_{<i};\theta_{e};\theta_{a})$ (1)
$\displaystyle+\;\alpha_{b}\cdot\sum_{1}^{m}\log
p(y^{b}_{i}|X,y^{b}_{<i};\theta_{e};\theta_{b})$ (2)

Here, $y^{a}$ and $y^{b}$ are the conclusion and counter sequences.
$\theta_{e}$ and $\theta_{a}$, and $\theta_{b}$ are the weight parameters of
the encoder, the conclusion, and counter decoders, respectively.

The distinction between this model and the previous one is the shared layers
between the two tasks. In the previous model, both the encoder and decoder
layers are shared between the two tasks, while, here, only the encoder’s
layers are shared, keeping a dedicated decoder for each of the two tasks. We
refer to this model as Joint Two-seq below.

We aim to generate a diverse set of candidate counters similar to the above
model. However, we noticed that counters rarely start by referring to entities
or similar concepts, and prompting the model with concepts might lead to
generating irrelevant texts. Hence, we generate one conclusion for this model,
but a set of candidate counters by only enabling the nucleus sampling during
decoding.333We tested the performance of the model empirically and noticed
that these prompted counters of low quality.

###  3.2 Ranking Component

Give a set of $n$ generated candidate counters, we rank them based on their
stance contrastiveness towards the corresponding generated conclusion and
select the top-ranked as our final output. In particular, we trained a
transformer-based stance classifier on pairs of claim and counter-claim
acquired from the kialo.com platform to be used to predict whether the pair
have a pro or con stance. Experimental details are provided in the next
section. To guarantee stance coherence of the selected counter, we compute the
stance-based scores on the sentence level to ensure all sentences have some
degree of contrastiveness towards the conclusion. In particular, given a pair
of a conclusion and the corresponding counter, we first split the counter into
a set of sentences. For each sentence $s_{i}$, we apply our trained classifier
to compute the stance $label$ towards the conclusion $c$ and its probability
$pr_{label}$. We then translate this into a stance contrastiveness score as
follows:

$cont(s_{i},c)=\begin{cases}\text{$pr_{con}$},&\text{if $label=con$}\\\
\text{$-pr_{pro}$},&\text{if $label=pro$}\end{cases}$

The final score of a counter is averaged across its sentences, ranging from -1
to 1. The counters are then ranked accordingly, selecting the top one.

##  4 Experiments

This section describes the experiments carried out to investigate the
conclusion’s importance in counter-argument generation.

###  4.1 Data

We evaluate our approach on the ChangeMyView (CMV) dataset of Jo et al.
(2020). On the CMV platform, users publish their opinions on controversial
topics as posts consisting of a title summarizing the main point and a body
representing the reasoning behind it. In turn, others comment on these posts
trying to convince the authors to change their mind. We follow Alshomary et
al. (2021b) by assuming the following mapping: The title of a post represents
an argument’s conclusion and its body is the premises, while each comment is a
counter-argument. To ensure our models are trained on high quality counters,
we select for each post the comment with highest argumentative quality score
predicted by the model proposed by Gretz et al. (2020).

To study counter-argument generation for settings where the conclusion is not
mentioned explicitly, we use only the post’s body as input, and the title as
training output to learn to generate the conclusion. Since users might also
restate their post’s main point (the conclusion) inside their post, this
allows us to study and evaluate the correlation between a model’s
effectiveness in generating good counter-arguments and the level of
implicitness of the conclusion in the input.

The stance-based ranking component relies on a classifier that assesses the
stance polarity between two statements. To train such a classifier, we use
dataset of Syed et al. (2021), which is based on the Kialo.org platform, where
claims on controversial topics contributed by humans are organized in a
hierarchical structure with supporting and opposing relations. We transformed
the data into pairs of claims labeled as _pro_ or _con_ , and we split it by
debates into 95.6k instances for training, 7.7k for validation, and 22.4k for
testing.

###  4.2 Models

#### Approach

For generation, we used BART as our base model Lewis et al. (2020), and fine-
tuned it starting from the _BART-large_ checkpoint. We trained for three
epochs using a learning rate of $5^{e}-5$ and a batch size of $8$. We then
selected the checkpoint with the lowest error on the validation set. To find
the best parameters $\alpha_{a}$ and $\alpha_{b}$ for the Joint Two-seq model,
we explored pairs of values between 0.1 and 1.0 on a sample of the training
set, and took the pair that led to the lowest validation loss:
$\alpha_{a}=0.7$ and $\alpha_{b}=0.3$.

To obtain a diverse set of candidate counters for ranking, we used nucleus
sampling Holtzman et al. (2019) with $p=0.95$ and $top\\_k=50$. For the Joint
One-seq model, we obtained relevant Wikipedia concepts from the input premises
using Project Debater’s API444https://github.com/IBM/debater-eap-tutorial that
we used to prompt the output sequence (conclusion and counter-argument) to
encourage diversity. As for the stance classifier, we fine-tuned roberta-large
on the Kialo pairs for three epochs with learning rate $2e^{-5}$ and batch
size $64$. The trained classifier achieved an F1-score of 0.81 on the test
split. To test its performance on the ChangeMyView data, we took a sample of
2k instances with pro pairs (an argument and its conclusion) and con pairs
(conclusion and counter). The trained classifier resulted in an F1-score of
0.70.

#### Baselines

To study the effectiveness of transformer-based models when the conclusion is
not explicitly stated, we compare against four BART-based models, all trained
on the conclusion and premises as input and the counter-argument as output,
but treated differently in the inference time.

In particular, the first baseline (BART-based w/o Conclusion) relies only on
the premises at inference time. To account for the missing conclusion, the
second (Pipeline-based) generates a conclusion using another BART-based
conclusion generation model trained independently on the training split of the
CMV dataset. This can be seen a pipeline alternative to our approach, since
conclusions and counters are learned independently. We also evaluate a
variation of this pipeline approach that chooses the best counter among a
diverse set of candidates using our ranking component (Pipeline-based w/
Stance). Finally, the fourth model is an oracle that knows the ground-truth
conclusion in addition to the premises (BART-based w/ Conclusion).

Additionally, we compare our approach with the argument undermining approach
of Alshomary et al. (2021b) in which the argument’s weak points are first
identified subject to its conclusion. Then a counter is generated to attack
the weakest point(s). We obtained the trained model from the authors and used
it to generate counter-arguments corresponding to the top three weak points
(similar to their experiments).

###  4.3 Automatic Evaluation

In the following we introduce the automatic evaluation measures used in our
experiments. We then present the evaluation results of our approaches, as well
as a detailed analysis of their effectiveness with respect to argument length
(measured by number of tokens) and conclusion implicitness.

Approach | BLEU | Be.F1 | Stance | Contr.
---|---|---|---|---
BART-based w/o Conclusion | 0.149 | 0.138 | 0.814 | 0.447
Pipeline-based | 0.148 | 0.142 | 0.816 | 0.437
Pipeline-based w/ Stance | 0.141 | 0.142 | 0.852 | 0.615
Joint One-seq | 0.143 | *0.159 | 0.850 | *0.480
Joint One-seq w/ Stance | 0.140 | *0.147 | 0.889 | *0.661
Joint Two-decoders | *0.154 | *0.148 | 0.798 | 0.423
Joint Two-decoders w/ Stance | *0.164 | *0.153 | 0.825 | *0.652
BART-based w/ Conclusion | 0.175 | 0.160 | 0.773 | 0.584
Argument Undermining | 0.072 | 0.090 | 0.805 | 0.664
Table 2: Automatic evaluation of our two models, with and without _stance_
ranking, compared to baselines, in terms of the similarity of the generated
and the ground-truth counters (BLEU and BERT F1-score) and of the counter’s
correct (opposing) stance. Stance is computed once using Project Debater’s API
(_Stance_) and once with our stance classifier (_Contrastiveness_). Results
highlighted with * are significantly better than the BART-based w/o Conclusion
with confidence level of 95%. Figure 2: Contrastiveness and BERT F$1$-scores
of our approach against the baseline subject to different levels of argument
complexity (measure by number of tokens) and conclusion implicitness (measures
by maximum similarity of the ground-truth conclusion to the premises).

#### Evaluation Measures

To approximate the similarity of generated and ground-truth counters, we
compute BLEU and BERT F1-score555For each instance, we compare against all
ground-truth counters and take the maximum score achieved. In addition, we
measure the stance correctness of the generated counter with respect to the
ground-truth conclusion in two ways: First, a contrastiveness score is
computed using the stance classifier trained for our ranking component. It
represents the average likelihood of classifying the counter and the
corresponding ground-truth conclusion as _con_ across the evaluation dataset.
Second, a target-based stance score measures the stance of both the conclusion
and the counter towards the conclusion target. Given the valdiation set, we
extract the target of each conclusion for this purpose as proposed by
Alshomary et al. (2020) and then use Project Debater’s API666https://early-
access-program.debater.res.ibm.com/ to classify the conclusion’s stance and
the generated counter’s stance towards the extracted target. The final measure
is the absolute difference between the counter and conclusion scores, averaged
across the evaluation dataset.

#### Results

Table 1 shows the evaluation results. All approaches are close in BLEU and
BERT F$1$-score, with small but significant advantages for our models. We
observe that the absence of explicit mention of the conclusion in the input
(Bart-based w/o Conclusion) worsens the results across all measures but the
Stance score, and vice versa when introducing the conclusion (Bart-based w/
Conclusion). This clearly indicates the importance of the conclusion in the
process of counter-argument generation.

When the conclusion is not mentioned explicitly but has to be inferred, we can
see that both our generation models which jointly generate conclusions and
counters, outperform the baselines in terms of correct stance. As expected,
adding the ranking component to our approaches and the pipeline baseline
consistently boosts the correctness, the best being _Joint One-seq w/ Stance_
with stance score 0.889 and contrastiveness score 0.661.

Although the Argument Undermining approach of Alshomary et al. (2021b)
requires an explicit mention of the conclusion to rank premises according to
their attackability, its effectiveness lacks behind. This could be because
their model is trained on only a subset of the training data where the
comments are countering specific points in the post.

#### Analysis

As mentioned, conclusions may appear in arguments implicitly, which we expect
to correlate with the quality of the generated counters: the more explicit the
conclusion, the better the generated counters. Moreover, we hypothesize that,
the longer an argument is, the more important the conclusion inference is in
counter-argument generation. We empirically investigate these two hypotheses
by comparing the performance of the counter-argument generation models subject
to _argument length_ (in terms of the number of tokens) and to the degree of
_conclusion implicitness_ (in terms of the maximum similarity between the
ground-truth conclusion and premises). In particular, for both dimensions, we
sorted the a sample of 2k instances from the test set accordingly and split it
into five subsets of equal size. We then compare the BERT F$1$-score and
contrastiveness score of Joint One-seq against BART-based w/o Conclusion and
BART-based w/ Conclusion on the respective subset.

Figure 2 shows the scores for all three models at different levels of argument
length and conclusion implicitness. In Figure 2a, we see that the baseline’s
contrastiveness drops from 0.53 to 0.43 the longer the argument gets, while
the scores for _BART-based w/ Conclusion_ fluctuate relatively around 0.57. In
contrast, our approach achieves scores between 0.64 and 0.73, indicating the
benefit of the explicit modeling of conclusions. Figure 2c suggests that the
more direct the conclusion is formulated in the premises, the better _BART-
based w/o Conclusion_ ’s contrastiveness score gets, and vice versa for _BART-
based w/ Conclusion_ model. We observe an unexpected drop in scores for
arguments where conclusions have an average similarity of 0.7 to the premises.
Upon inspection, we found that the baselines tend to copy parts of the
premises with slight rephrasing. Our approach, however, maintains high scores
and also benefits from the clear formulation of the conclusion in premises
since it helps to generate better conclusions.

Lastly, looking at BERT F$1$-scores in Figures 2b and 2d, we notice a drop
across all approaches when arguments get longer. Similarly, the more apparent
the conclusion in the premises, the better the scores get.

###  4.4 Manual Evaluation

To gain more reliable insights into the performance of our approaches, we
designed a human evaluation study to measure the quality of the generated
counters in terms of relevance to the input argument and the correctness of
their stance. In a second study, we also let humans assess the validity of the
generated conclusions.

#### Counter-Arguments

We selected 100 test set arguments randomly along with the counters generated
by the two variations of our approach, _Joint One-seq w/ Stance_ and _Joint
Two-decoders w/ Stance_ , as well as by two baselines, _BART-based w/o
Conclusion_ and _Pipeline-based_. Using the UpWork platform, we recruited
three human annotators who are proficient in English with a job success of
more than 90%. We presented them the 100 arguments together with the texts of
the four given counters, shuffled pseudo-randomly for each argument. For each
argument, we then asked them to rank the texts based on their adequacy of
being a counter-argument to the input argument, where we defined adequacy as
follows:

> An adequate counter is a text that (1) carries an argumentative and coherent
> language and (2) clearly represents an opposing stance to one of the main
> points in the input argument.

Additionally, the annotators should provide comments describing their decision
regarding the counters ranked first (the best) and fourth (the worst).
Computing the inter-annotator agreement using Kendall’s $\tau$ results in an
average of 0.32 (ranging from 0.32 to 0.43), while we observed majority
agreement on full ranks between the annotators in 78% of the evaluated cases.

Counter Generation Approach | Average $\downarrow$ | Majority $\downarrow$
---|---|---
BART-based w/o Conclusion | 2.56 | 2.54
Pipeline-based w/ Stance | 2.38 | 2.31
Joint-based One-seq w/ Stance | 2.39 | 2.26
Joint-based Two-decoders w/ Stance | 2.65 | 2.72
Table 3: Manual evaluation: The _average_ and _majority_ rank of the counters
generated by our approaches and baselines.

Table 3 reports the mean of the average and majority ranks achieved by each
approach. When considering cases with majority agreement, our model Joint One-
seq w/ Stance performs best (mean rank 2.26). This also can be seen in Figure
3, where we plot the rank distribution for all approaches. In 55% of the
cases, the approach generated counters that were ranked either first or
second. However, the variation with two decoders falls short compared to all
others (mean rank 2.72). This suggests that sharing only the encoder between
the two tasks is not enough to generate relevant counters. Also, as indicated
before, not being able to prompt the generated conclusions limits the
diversity of candidates in the stance-based ranking component. Finally, we see
that the _pipeline-based_ baseline equipped with our ranking component is
almost on par with our approaches, indicating the importance of promoting
stance correctness.

Figure 3: A histogram of Ranking scores that each of the manually evaluated approaches achieved. Conclusion Generation Approach | Validity $\uparrow$
---|---
Pipeline-based w/ Stance | 1.42
Joint-based One-seq w/ Stance | 1.91
Joint-based Two-decoders w/ Stance | 2.03
Ground-truth Conclusions | 2.39
Table 4: Manual evaluation: Average _validity_ score from 1 (non-valid) to 3
(valid) of the conclusions generated by our approaches and the baseline
compared to the ground truth.

#### Conclusions

To investigate whether the joint learning of conclusion and counter-argument
generation leads to more valid conclusions, we designed another human
evaluation study, for which we defined validity in a simple way:

> A conclusion is valid if humans can infer it from the input argument.

For 50 random arguments, we selected their ground-truth conclusion as well as
two conclusions generated by the two variations of our approach and the best
baseline (_Pipeline-based w/ Stance_), summing up to seven conclusions per
argument. We hired two annotators through UpWork again. We asked them to read
each argumentsand to evaluate the validity of each conclusion on a 3-point
Likert scale, where $3$ means that they strongly agree that the conclusion can
be inferred and $1$ means they strongly disagree. The agreement of the two
annotators was 0.46 in terms of Cohen’s $\kappa$.

Table 4 shows the average scores achieved by each evaluated model. With 1.42,
the pipeline-based approach is notably worse than the others, indicating the
advantage of multitask learning for conclusion and counter generation. The
best score is achieved by Joint Two-decoders w/ Stance (2.03), being only 0.36
points below the ground-truth conclusion’s score. Given the low effectiveness
of this model on the counter-argument generation task, we assume that the
training process optimized more towards generating conclusions, especially
since the task may be easier than generating counters. A better weighting
scheme for the two tasks may alleviate this in future work.

##  5 Conclusion

In this paper, we studied the task of counter-argument generation, considering
the role of the argument’s conclusion. We argued that automatically generating
counter-arguments becomes more challenging when the argument’s conclusion is
implicit, mandating explicit modeling. To validate our claims, we propose an
approach that jointly learns to generate the conclusion and a counter for a
given argument and compare it to baselines with no explicit conclusion
modeling. We then realize our approach in two ways, both using transformer-
based models. Moreover, our approach explicitly ensures that the generated
counters have a correct stance through a stance-based ranking component. Our
results show that, although far from perfect, the joint learning of the two
tasks leads to better counters and more valid conclusions of the input
argument when compared to baselines.

##  6 Limitation

In our experiments, we only experiment with the BART as the underlining
transformer-based model. However, a stronger experiment setting could
demonstrate the gain of modeling the conclusion across several transformer-
based models, like GPT and T5. We didn’t explore all possible weighting
schemes for the two jointly learned tasks in our multitask setting. A
potential direction could consider a more systematic evaluation of different
schemes. Our models are limited by the quality of the data we use. To this
end, we build on the assumption that CMV commentators rebut the original
post’s conclusion. However, this might not always be a valid assumption.

##  7 Ethics

Although our experiments demonstrate the role of conclusion in counter-
argument generation, we believe this task is far from resolved. We are aware
that issues such as faithful text generation must be considered when working
with language models to avoid misinformation. We believe that a fact-checking
component should accommodate any text generation model. The sole goal of our
experiments is to highlight the potential of conclusion inference as part of
the counter-argument generation pipeline.

## References

  * Alshomary et al. (2021a) Milad Alshomary, Wei-Fan Chen, Timon Gurcke, and Henning Wachsmuth. 2021a.  Belief-based generation of argumentative claims.  In _Proceedings of the 16th Conference of the European Chapter of the Association for Computational Linguistics: Main Volume_ , pages 224–233.
  * Alshomary et al. (2021b) Milad Alshomary, Shahbaz Syed, Arkajit Dhar, Martin Potthast, and Henning Wachsmuth. 2021b.  Counter-argument generation by attacking weak premises.  In _Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021_ , pages 1816–1827.
  * Alshomary et al. (2020) Milad Alshomary, Shahbaz Syed, Martin Potthast, and Henning Wachsmuth. 2020.  Target inference in argument conclusion generation.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 4334–4345, Online. Association for Computational Linguistics.
  * Bilu et al. (2015) Yonatan Bilu, Daniel Hershcovich, and Noam Slonim. 2015.  Automatic claim negation: Why, how and when.  In _Proceedings of the 2nd Workshop on Argumentation Mining_ , pages 84–93, Denver, CO. Association for Computational Linguistics.
  * Chakrabarty et al. (2021) Tuhin Chakrabarty, Aadit Trivedi, and Smaranda Muresan. 2021.  Implicit premise generation with discourse-aware commonsense knowledge models.  In _Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing_ , pages 6247–6252.
  * Dor et al. (2018) Liat Ein Dor, Alon Halfon, Yoav Kantor, Ran Levy, Yosi Mass, Ruty Rinott, Eyal Shnarch, and Noam Slonim. 2018.  Semantic relatedness of wikipedia concepts–benchmark data and a working solution.  In _Proceedings of the Eleventh International Conference on Language Resources and Evaluation (LREC 2018)_.
  * Gretz et al. (2020) Shai Gretz, Roni Friedman, Edo Cohen-Karlik, Assaf Toledo, Dan Lahav, Ranit Aharonov, and Noam Slonim. 2020.  A large-scale dataset for argument quality ranking: Construction and analysis.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 34, pages 7805–7813.
  * Gurcke et al. (2021) Timon Gurcke, Milad Alshomary, and Henning Wachsmuth. 2021.  Assessing the sufficiency of arguments through conclusion generation.  In _Proceedings of the 8th Workshop on Argument Mining_ , pages 67–77, Punta Cana, Dominican Republic. Association for Computational Linguistics.
  * Habernal and Gurevych (2015) Ivan Habernal and Iryna Gurevych. 2015.  Exploiting debate portals for semi-supervised argumentation mining in user-generated web discourse.  In _Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing_ , pages 2127–2137. Association for Computational Linguistics.
  * Hidey and McKeown (2019) Christopher Hidey and Kathleen McKeown. 2019.  Fixed that for you: Generating contrastive claims with semantic edits.  In _Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers)_ , pages 1756–1767.
  * Holtzman et al. (2019) Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. 2019.  The curious case of neural text degeneration.  _arXiv preprint arXiv:1904.09751_.
  * Hua and Wang (2018) Xinyu Hua and Lu Wang. 2018.  Neural argument generation augmented with externally retrieved evidence.  In _Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 219–230, Melbourne, Australia. Association for Computational Linguistics.
  * Hua and Wang (2019) Xinyu Hua and Lu Wang. 2019.  Sentence-level content planning and style specification for neural text generation.  In _Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP)_ , pages 591–602.
  * Jo et al. (2020) Yohan Jo, Seojin Bang, Emaad Manzoor, Eduard Hovy, and Chris Reed. 2020.  Detecting attackable sentences in arguments.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 1–23, Online. Association for Computational Linguistics.
  * Lewis et al. (2020) Mike Lewis, Yinhan Liu, Naman Goyal, Marjan Ghazvininejad, Abdelrahman Mohamed, Omer Levy, Veselin Stoyanov, and Luke Zettlemoyer. 2020.  Bart: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 7871–7880.
  * Liu et al. (2019) Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. 2019.  Roberta: A robustly optimized bert pretraining approach.  _arXiv preprint arXiv:1907.11692_.
  * Orbach et al. (2020) Matan Orbach, Yonatan Bilu, Assaf Toledo, Dan Lahav, Michal Jacovi, Ranit Aharonov, and Noam Slonim. 2020.  Out of the echo chamber: Detecting countering debate speeches.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 7073–7086, Online. Association for Computational Linguistics.
  * Schiller et al. (2021) Benjamin Schiller, Johannes Daxenberger, and Iryna Gurevych. 2021.  Aspect-controlled neural argument generation.  In _Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies_ , pages 380–396, Online. Association for Computational Linguistics.
  * Syed et al. (2021) Shahbaz Syed, Khalid Al Khatib, Milad Alshomary, Henning Wachsmuth, and Martin Potthast. 2021.  Generating informative conclusions for argumentative texts.  In _Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021_ , pages 3482–3493.
  * Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. 2017.  Attention is all you need.  _Advances in neural information processing systems_ , 30.
  * Wachsmuth et al. (2018) Henning Wachsmuth, Shahbaz Syed, and Benno Stein. 2018.  Retrieval of the best counterargument without prior topic knowledge.  In _Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 241–251. Association for Computational Linguistics.
  * Walton (2009) Douglas Walton. 2009.  Objections, rebuttals and refutations.
  * Zhang et al. (2016) Justine Zhang, Ravi Kumar, Sujith Ravi, and Cristian Danescu-Niculescu-Mizil. 2016\.  Conversational flow in Oxford-style debates.  In _Proceedings of the 2016 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies_ , pages 136–141, San Diego, California. Association for Computational Linguistics.

##  Appendix A Example Analysis

Conclusion (title): Artificial General Intelligence does not need to be
conscious to be more intelligent or effective than humans
---
Premises (post): In my opinion AGI needs the algorithms that make us
intelligent and by having these missing pieces they will be a generally
intelligent entity. I hear arguments that an AGI needs to have a subjective
experience like a human being in order to be generally intelligent and I find
this theory to be lackluster if the laws of physics can be computed than so
can the algorithms that make general intelligence. After all we are
information processing systems however, i am trying to explore all avenues of
thought, even play devil’s advocate and not get caught in some sort of echo
chamber or even worse a spirit of the age.
BART-based w/o Conclusion:
Counter: I don’t think that AGI needs to have a subjective experience like a
human being in order to be generally intelligent. I think it’s more accurate
to say that an AGI doesn’t need to have subjective experience, but that
doesn’t mean that it can’t have an objective experience.
Pipeline-based w/ Stance:
Conclusion: i need to be more intelligent in order to be an AGI.
Counter: intelligence is not determined by a subjective experience like a
human being. it is determined by the laws of physics. an agi does not need to
have an objective experience to be intelligent, but it does need to be able to
understand the world around it.
Joint-based One-seq w/ Stance:
Conclusion: Scientific law is the only thing that can make AGI generally
intelligent.
Counter: The problem with AGI is that we don’t really know what it is that
makes us intelligent. we have no idea how it works, what it’s like to be an
AGI, how it’s different from a human being, or how it will work in the real
world.
Table 5: An example argument (conclusion + premises) taken from CMV showing
how the conclusion is implicitly mentioned in the body

#### Qualitative Analysis

Table 5 shows an example argument discussing Artificial Intelligence along
with counters generated by the two baselines as well as by our approach Joint-
based One-seq w/ Stance. BART-based w/o Conclusion rephrases sentences from
the input argument without generating a proper counter, possibly due to the
ignorance of the conclusion. While the pipeline-based baseline equipped with
our ranking component generates a somehow relevant conclusion, its counter
still vague and doesn’t clearly oppose the argument’s stance. Finally, Joint-
based One-seq infers a conclusion that addresses the main point of the input
argument (Scientific law), and counter it by pointing out the difficulty of
defining intelligent , making it hard to be measured.

Upon exploring annotators’ comments that justified their decisions of what is
the best/worse counter, we identified some patterns. For example, Joint-based
One-seq was most appreciated, because it generated argumentative and coherent
counters that sometimes offered new perspectives. In contrast, the cases in
which the model’s output was ranked worst happen mainly due to being vague,
incoherent, or diverging from the main topic. The counters of BART-based w/o
Conclusion were ranked worse due to coherences sometimes, but often due to not
opposing to the input argument.

##  Appendix B Computing Infrastructure

All our experiments are run inside an ubuntu20.04 system using Python 3.8.10.
The CUDA version is 11.2. We used one A100-SXM4-40GB GPU to train our models.
The following libraries are required to run our experiments:

  * •

torch==1.11.0+cu113

  * •

transformers==4.18.0

  * •

flair==0.11

  * •

spacy==3.3.1

  * •

debater-python-api==3.5.8


16312 LABEL:LastPageMay 01, 2019Aug. 20, 2020

# The Sierpinski Object in the Scott Realizability Topos

Tom de Jong  School of Computer Science, University of Birmingham
<EMAIL_ADDRESS>and  Jaap van Oosten  Department of Mathematics,
Utrecht University<EMAIL_ADDRESS>
###### Abstract.

We study the Sierpinski object $\Sigma$ in the realizability topos based on
Scott’s graph model of the $\lambda$-calculus. Our starting observation is
that the object of realizers in this topos is the exponential $\Sigma^{N}$,
where $N$ is the natural numbers object. We define order-discrete objects by
orthogonality to $\Sigma$. We show that the order-discrete objects form a
reflective subcategory of the topos, and that many fundamental objects in
higher-type arithmetic are order-discrete. Building on work by Lietz, we give
some new results regarding the internal logic of the topos. Then we consider
$\Sigma$ as a dominance; we explicitly construct the lift functor and
characterize $\Sigma$-subobjects. Contrary to our expectations the dominance
$\Sigma$ is not closed under unions. In the last section we build a model for
homotopy theory, where the order-discrete objects are exactly those objects
which only have constant paths.

###### Key words and phrases:

realizability topos, Scott model of $\lambda$-calculus, order-discrete
objects, homotopy

Corresponding author: Jaap van Oosten

##  1\. Introduction

In this paper, we aim to revive interest in what we call the Sierpinski object
in the Scott realizability topos. We show that it is of fundamental importance
in studying the subcategory of order-discrete objects (section 3), arithmetic
in the topos (section 4), the Sierpinski object as a dominance (section 5) and
a notion of homotopy based on it (section 6). Section 2 deals with
preliminaries and establishes notation.

##  2\. Preliminaries

Independently observed by G. Plotkin and D.S. Scott ([11, 12, 10]), there is a
combinatory algebra structure (in fact, a $\lambda$-model structure) on the
power set ${\mathcal{P}}(\mathbb{N})$ of the natural numbers.

Identifying ${\mathcal{P}}(\mathbb{N})$ with $\prod_{n\in\mathbb{N}}\\{0,1\\}$
and giving $\\{0,1\\}$ the Sierpinski topology (with $\\{1\\}$ the only
nontrivial open set), we endow ${\mathcal{P}}(\mathbb{N})$ with the product
topology. Concretely, basic opens of ${\mathcal{P}}(\mathbb{N})$ are of the
form

${\mathcal{U}}_{p}\;=\;\\{U\subseteq\mathbb{N}\,|\,p\subseteq U\\}$

for $p$ a finite subset of $\mathbb{N}$. A function
$F:{\mathcal{P}}(\mathbb{N})\to{\mathcal{P}}(\mathbb{N})$ is continuous for
this topology if and only if it has the property that

$n\in F(U)\text{ if and only if for some finite $p\subseteq U$, }n\in F(p).$

Note, that every continuous function automatically preserves the inclusion
$\subseteq$.

Such continuous maps are encoded by elements of ${\mathcal{P}}(\mathbb{N})$ in
the following way. Consider the following coding of finite subsets of
$\mathbb{N}$:

$e_{n}=\\{k_{1},\ldots,k_{m}\\}\text{ if and only if
}n=2^{k_{1}}+\cdots+2^{k_{m}}.$

By convention, $e_{0}=\emptyset$. So: $e_{1}=\\{0\\}$, $e_{2}=\\{1\\}$,
$e_{3}=\\{0,1\\}$, $e_{2^{n}}=\\{n\\}$, etc.

Consider also a bijection
$\langle{\cdot},{\cdot}\rangle:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$, which
we don’t specify.

Now we define a binary operation (written as juxtaposition) on
${\mathcal{P}}(\mathbb{N})$:

$UV=\\{n\,|\,\text{ for some }m,e_{m}\subseteq V\text{ and }\langle
m,n\rangle\in U\\}$

For every function $F:{\mathcal{P}}(\mathbb{N})\to{\mathcal{P}}(\mathbb{N})$
we have

${\sf graph}(F)\;=\;\\{\langle m,n\rangle\,|\,n\in F(e_{m})\\}$

so that, when $F$ is continuous, ${\sf graph}(F)V=F(V)$ for all
$V\in{\mathcal{P}}(\mathbb{N})$. Note that the operation $U,V\mapsto UV$ is a
continuous map of two variables.

We think of the operation $U,V\mapsto UV$ as an application operation: apply
the continuous function coded by $U$ to the argument $V$.

The structure ${\mathcal{P}}(\mathbb{N})$ together with this application
function is denoted $\mathcal{S}$. The fact that $\mathcal{S}$ is a
$\lambda$-model is worked out in detail in [12]. We shall use $\lambda$-terms
to denote elements of $\mathcal{S}$ according to this interpretation. We use
repeated juxtaposition and associate to the left when discussing iterated
application: $VU_{1}\cdots U_{n}$ means $(\cdots((VU_{1})U_{2})\cdots)U_{n}$.
For continuous functions of several variables
$F:{\mathcal{P}}(\mathbb{N})^{n}\to{\mathcal{P}}(\mathbb{N})$ we let

${\sf graph}(F)\,=\,\\{\langle m_{1},\langle m_{2},\langle\cdots
m_{n},k\rangle\cdots\rangle\rangle\,|\,k\in F(e_{m_{1}},\ldots,,e_{m_{n}})\\}$

So with these conventions, ${\sf graph}(F)U_{1}\cdots
U_{n}=F(U_{1},\ldots,U_{n})$.

In $\mathcal{S}$, special combinators for important operations are available:

Pairing and unpairing combinators:

${\sf p},{\sf p}_{0},{\sf p}_{1}\in{\mathcal{S}}$ satisfying ${\sf p}_{0}({\sf
p}UV)=U$, ${\sf p}_{1}({\sf p}UV)=V$. In fact we can take

$\\{\langle 2^{n},\langle
0,2n\rangle\rangle\,|\,n\in\mathbb{N}\\}\cup\\{\langle 0,\langle
2^{n},2n+1\rangle\rangle\,|\,n\in\mathbb{N}\\}$

for $\sf p$, so that

${\sf p}U\;=\;\\{\langle 0,2n\rangle\,|\,n\in U\\}\cup\\{\langle
2^{n},2n+1\rangle\,|\,n\in\mathbb{N}\\}$

and

${\sf p}UV\;=\;\\{2n\,|\,n\in U\\}\cup\\{2n+1\,|\,n\in V\\}.$

Booleans:

${\sf t}=\\{1\\}$, ${\sf f}=\\{0\\}$. We have an “if … then …, else…” operator
$\sf q$, satisfying ${\sf qt}UV=U$ and ${\sf qf}UV=V$.

Natural numbers:

we write $\overline{n}$ for the element $\\{n\\}$.

Coding of tuples:

we write $[U_{0},\ldots,U_{n}]$ for a standard coding of $n+1$-tuples in
$\mathcal{S}$. This coding has the usual properties as given in [15]: there
are elements of $\mathcal{S}$ which give the length of a coded tuple, the
$i$’th element (for appropriate $i$), and the code of the concatenation of two
tuples.

As usual we have a category of assemblies over $\mathcal{S}$, denoted ${\sf
Ass}({\mathcal{S}})$ and the realizability topos ${\sf RT}({\mathcal{S}})$,
which we call the Scott realizability topos (unfortunately, the term “Scott
topos” is already in use). We briefly introduce these categories.

An assembly over $\mathcal{S}$ is a pair $X=(|X|,E_{X})$ where $|X|$ is a set
and $E_{X}$ gives, for each $x\in|X|$, a nonempty subset $E_{X}(x)$ of
$\mathcal{S}$. A morphism of assemblies $(|X|,E_{X})\to(|Y|,E_{Y})$ is a
function $f:|X|\to|Y|$ for which there is some element $U$ of $\mathcal{S}$
which tracks $f$, meaning that for all $x\in|X|$ and all $V\in E_{X}(x)$ we
have $UV\in E_{Y}(f(x))$.

The category ${\sf Ass}({\mathcal{S}})$ is a quasitopos. By way of example,
let us construct exponentials explicitly: the exponent $(Y,E_{Y})^{(X,E_{X})}$
can be given as $(Z,E_{Z})$ where $Z$ is the set of morphisms from $(X,E_{X})$
to $(Y,E_{Y})$ and $E_{Z}(f)$ is the set of those elements of $\mathcal{S}$
which track the morphism $f$.

Actually, ${\sf Ass}({\mathcal{S}})$ has countable products: given a countable
family $((X_{n}),E_{n})_{n\in\mathbb{N}}$ of assemblies over $\mathcal{S}$,
one has the assembly $(\prod_{n}X_{n},E)$ where

$E((x_{n})_{n})\;=\;\\{U\,|\,U\overline{n}\in E_{n}(x_{n})\text{ for all
}n\\}.$

The category ${\sf Ass}({\mathcal{S}})$ has several subcategories of interest.
First we recall that there is an adjunction

${\rm Set}\stackrel{{\scriptstyle\nabla}}{{\to}}{\sf
Ass}({\mathcal{S}});\;\;\;{\sf
Ass}({\mathcal{S}})\stackrel{{\scriptstyle\Gamma}}{{\to}}{\rm
Set};\;\;\;\Gamma\dashv\nabla$

where $\Gamma(|X|,E_{X})=|X|$, $\nabla(Y)=(Y,E)$ with $E(y)={\mathcal{S}}$ for
all $y$.

An assembly $X$ is partitioned if $E_{X}(x)$ is always a singleton. It is not
hard to see that the object $\nabla(Y)$ is isomorphic to $(Y,E)$ where
$E(y)=\\{\emptyset\\}$ for all $y$, so all objects $\nabla(Y)$ are isomorphic
to partitioned assemblies. Up to isomorphism, the partitioned assemblies are
exactly the regular projective objects (the objects for which the
representable functor into Sets preserves regular epimorphisms), which, in the
topos ${\sf RT}({\mathcal{S}})$, coincide with the internally projective
objects (the objects $X$ for which the endofuctor $(-)^{X}$ preserves
epimorphisms); see 2 below.

An assembly $X$ is modest if $E_{X}(x)\cap E_{X}(y)=\emptyset$ whenever $x\neq
y$. The modest assemblies are, up to isomorphism, the ones for which the
diagonal map $X\to X^{\nabla(2)}$ is an isomorphism (here, 2 denotes any two-
element set); such objects are called discrete in [4].

A special object of ${\sf Ass}({\mathcal{S}})$ is the object of realizers
$S=({\mathcal{S}},E)$ where $E(U)=\\{U\\}$; one sees that $S$ is both
partitioned and modest. Every object which is both partitioned and modest is a
regular subobject of $S$: that is, isomorphic to an object $({\mathcal{A}},E)$
where ${\mathcal{A}}\subseteq{\mathcal{S}}$ and $E$ is the restriction to
$\mathcal{A}$ of the map defining $S$.

Another partitioned and modest object is the natural numbers object
$N=(\mathbb{N},E_{N})$, where $E_{N}(n)=\\{\overline{n}\\}$.

As Andrej Bauer observed in his thesis ([1]), one can embed the category
$T_{0}^{\rm cb}$ of countably based $T_{0}$-spaces into the subcategory of
partitioned and modest assemblies over $\mathcal{S}$. To be precise, by
“countably based $T_{0}$-space” we mean a $T_{0}$-space together with a chosen
enumeration of a subbasis. If $(X,\\{S_{n}\,|\,n\in\mathbb{N}\\})$ is such,
then the map $e:X\to{\mathcal{S}}$ given by

$e(x)=\\{n\,|\,x\in S_{n}\\}$

defines an embedding of $X$ into $\mathcal{S}$. Moreover, given countably
based spaces $X$ and $Y$ with associated embeddings
$e:X\to{\mathcal{S}},d:Y\to{\mathcal{S}}$, there is for every continuous map
$f:X\to Y$ a continuous extension $F_{f}:{\mathcal{S}}\to{\mathcal{S}}$
satisfying $F_{f}{\circ}e=d{\circ}f$. This means that if we see the space $X$
with embedding $e:X\to{\mathcal{S}}$ as assembly $(X,E_{X})$ where
$E_{X}(x)=\\{e(x)\\}$, then every continuous map $f:X\to Y$ is tracked (as a
morphism of assemblies $(X,E_{X})\to(Y,E_{Y})$) by ${\sf graph}(F_{f})$.

Finally, we have the Scott realizability topos, the realizability topos over
$\mathcal{S}$, denoted ${\sf RT}({\mathcal{S}})$. Its objects are pairs
$(X,\sim)$ where $X$ is a set and for $x,y\in X$, $[x\sim y]$ is a subset of
$\mathcal{S}$ (so $\sim$ is a ${\mathcal{P}}({\mathcal{S}})$-valued relation
on $X$), which satisfies certain conditions (we refer to [15] for details).
Every assembly $(X,E)$ is an object of ${\sf RT}({\mathcal{S}})$ if we define

$[x\sim y]\;=\;\left\\{\begin{array}[]{cl}E(x)&\text{if }x=y\\\
\emptyset&\text{otherwise}\end{array}\right.$

As subcategory of ${\sf RT}({\mathcal{S}})$, the category ${\sf
Ass}({\mathcal{S}})$ is equivalent to the category of $\neg\neg$-stable
objects of ${\sf RT}({\mathcal{S}})$, that is: the objects $(X,\sim)$
satisfying $\forall x,x^{\prime}:X.\neg\neg(x\sim x^{\prime})\to x\sim
x^{\prime}$. We shall not rehearse the structure of ${\sf RT}({\mathcal{S}})$
or its internal logic, based on realizability over $\mathcal{S}$, any further,
as for this theory now standard texts are available. We only recall the
following facts from [15], pp.135–7 (the proofs generalize to arbitrary pcas):

######  Lemma 1.

If $P$ is a partitioned assembly and $X$ is any object, then the exponential
$X^{P}$ is isomorphic to the object $(|X|^{|P|},\approx)$ where

$f\approx g=[\forall p(E_{P}(p)\to f(p)\sim_{X}g(p))].$

######  Lemma 2.

An object is internally projective in ${\sf RT}({\mathcal{S}})$ if and only if
it is isomorphic to a partitioned assembly.

The following small proposition will be of use later on. Given an assembly
$(X,E)$ let ${\int}(X,E)$ be $(X^{\prime},E^{\prime})$ where
$X^{\prime}=\\{(x,U)\,|\,U\in E(x)\\}$ and $E^{\prime}(x,U)=\\{U\\}$. Consider
also ${\int\\!\\!\\!\int}(X,E)=(X^{\prime\prime},E^{\prime\prime})$ where
$X^{\prime\prime}=\\{(x,U,V)\,|\,U,V\in E(x)\\}$ and
$E^{\prime\prime}(x,U,V)=\\{{\sf p}UV\\}$. Clearly, we have a projection
${\int}(X,E)\to(X,E)$ and two projections
${\int\\!\\!\\!\int}(X,E)\to{\int}(X,E)$, and these maps form a coequalizer
diagram in ${\sf Ass}({\mathcal{S}})$.

######  Proposition 3.

Let $(Y,\sim)$ be an arbitrary object of ${\sf RT}({\mathcal{S}})$ and let
$(X,E)$ be an assembly over $\mathcal{S}$. The exponential $(Y,\sim)^{(X,E)}$
can be presented as follows: its underlying set is the set of functions from
$\\{(x,U)\,|\,U\in E(x)\\}$ to $Y$. Given two such functions $f,g$, the set
$[f\approx g]$ consists of those coded triples $[P,Q,R]$ (coded in the sense
of $\mathcal{S}$) of elements of $\mathcal{S}$, which satisfy the following
three conditions:

  1. (1)

for $U\in E(x)$, $PU\in[f(x,U)\sim f(x,U)]$;

  2. (2)

for $U,U^{\prime}\in E(x)$, $QUU^{\prime}\in[f(x,U)\sim f(x,U^{\prime})]$;

  3. (3)

for $U\in E(x)$, $RU\in[f(x,U)\sim g(x,U)]$.

######  Proof 2.1.

Observe that the objects ${\int}(X,E)$ and ${\int\\!\\!\\!\int}(X,E)$ are
partitioned assemblies, hence projective objects in ${\sf RT}({\mathcal{S}})$.
Also note that the contravariant functor $(Y,\sim)^{(-)}$ sends coequalizers
to equalizers. Finally, use Lemma 1.

##  3\. The Sierpiński object and order-discrete objects

The _Sierpiński object_ $\Sigma$ is the image of Sierpiński space under the
embedding $T_{0}^{\text{cb}}\to\mathsf{RT}(\mathcal{S})$. Concretely, $\Sigma$
is the modest set $(\\{0,1\\},E_{\Sigma})$ with

$E_{\Sigma}(0)=\\{\emptyset\\}\text{ and }E(1)=\\{\\{1\\}\\}.$

The _object of realizers_ $S$ is the modest set $(\mathcal{S},\\{-\\})$.

The two objects above are related, as follows.

######  Proposition 4.

The object of realizers is isomorphic to the exponential $\Sigma^{N}$, where
$N$ is the natural numbers object of $\mathsf{RT}(\mathcal{S})$.

######  Proof 3.1.

We prove that the underlying set of $\Sigma^{N}$ is $\\{0,1\\}^{\mathbb{N}}$.
Since any morphism from $N$ to $\Sigma$ is in particular a function from
$\mathbb{N}$ to $\\{0,1\\}$, one inclusion is clear. Conversely, if
$f\colon\mathbb{N}\to\\{0,1\\}$, then $f$ is tracked by $\textup{graph}(F)$,
where $F\colon\mathcal{S}\to\mathcal{S}$ is the continuous function defined
by:

$\overline{n}\mapsto\begin{cases}\overline{1}&\text{if }f(n)=1;\\\
\emptyset&\text{if }f(n)=0.\end{cases}$

Thus, $\Sigma^{N}$ is the assembly $(\\{0,1\\}^{\mathbb{N}},E)$ where
$E(f)\subseteq\mathcal{S}$ is the set of trackers of the function $f$ (note,
that this set is always nonempty).

We have a canonical bijection

$\chi\colon\mathcal{S}\to\\{0,1\\}^{\mathbb{N}},\quad U\mapsto\chi_{U}$

(where $\chi_{U}$ is the characteristic function of $U$) with inverse

$\chi^{-1}\colon\\{0,1\\}^{\mathbb{N}}\to\mathcal{S},\quad f\mapsto
f^{-1}(\\{1\\}).$

It remains to prove that these functions are tracked. For $\chi$, consider the
continuous function $F\colon\mathcal{S}\to\mathcal{S}$ given by
$U\mapsto\\{\langle 2^{n},1\rangle\mid n\in U\\}.$ Then $\chi$ is tracked by
graph($F$). Indeed, if $U\in\mathcal{S}$ and $n\in\mathbb{N}$, then
$\textup{graph}(F)U\overline{n}=F(U)\overline{n}$ and this is $\overline{1}$
if $n\in U$ and $\emptyset$ otherwise.

For the inverse of $\chi$, we define $G\colon\mathcal{S}\to\mathcal{S}$
continuous by $U\mapsto\\{n\in\mathbb{N}\mid U\overline{n}=\overline{1}\\}$.
(This is continuous, because the application of $\mathcal{S}$ is continuous.)
We claim that $\chi^{-1}$ is tracked by $\textup{graph}(G)$. Indeed, for
$f\in\\{0,1\\}^{\mathbb{N}}$ and $U\in E(f)$, we have $n\in G(U)$ if and only
if $f(n)=1$, since $U$ tracks $f$.

###  3.1. Order-discrete objects

An object $X$ of $\mathsf{RT}(\mathcal{S})$ is _order-discrete_ if it is
orthogonal to $\Sigma$, viz. the diagonal
$X\xrightarrow{\delta_{X}}X^{\Sigma}$ is an isomorphism.

We wish to characterize the order-discrete objects in terms of their
realizers. To this end, we first present some useful lemmas.

######  Lemma 5.

An object $X$ is order-discrete if and only if the diagonal $\delta_{X}$ is an
epimorphism.

######  Proof 3.2.

Of course, $\delta_{X}$ is epic if $X$ is order-discrete. Conversely, suppose
$\delta_{X}$ is an epi. Clearly, the unique morphism
$!_{\Sigma}\colon\Sigma\to 1$ is an epimorphism. Hence, the diagonal
$\delta_{X}=X^{!_{\Sigma}}$ is monic. Thus, $\delta_{X}$ is an iso, as
desired.

######  Proposition 6.

An object $X$ is order-discrete if and only if there is $A\in\mathcal{S}$ such
that for any $x,x^{\prime}\in|X|$: if $U\in[x\sim_{X}x]$ and
$V\in[x^{\prime}\sim_{X}x^{\prime}]$ with $U\subseteq V$, then
$AUV\in[x\sim_{X}x^{\prime}]$.

######  Proof 3.3.

Suppose first that $X$ is order-discrete. We construct the desired element
$A\in\mathcal{S}$. Assume we have $x,x^{\prime}\in|X|$ and
$U\in[x\sim_{X}x],V\in[x^{\prime}\sim_{X}x^{\prime}]$ with $U\subseteq V$. By
Lemma 1 we have $X^{\Sigma}\cong(|X|^{\\{0,1\\}},\approx)$. Define
$f\colon\\{0,1\\}\to|X|$ by $f(0)=x$ and $f(1)=x^{\prime}$. The map
$H\colon\mathcal{S}^{2}\to\mathcal{S}$ defined as

$(W,W^{\prime})\mapsto\\{\langle 0,n\rangle\mid n\in W\\}\cup\\{\langle
2,n\rangle\mid n\in W^{\prime}\\}$

is easily seen to be continuous. Write $G=\textup{graph}(H)$. We claim that
$GUV\in[f\approx f]$. Indeed, $GUV=\\{\langle 0,n\rangle\mid n\in
U\\}\cup\\{\langle 2,n\rangle\mid n\in V\\}$, so that
$GUV\emptyset=U\in[f(0)\sim_{X}f(0)]$. Moreover, $GUV\overline{1}=U\cup
V=V\in[f(1)\sim_{X}f(1)]$, since $e_{0}=\emptyset$ and $e_{2}=\overline{1}$
and $U\subseteq V$. Thus, $GUV\in[f\approx f]$. Now let $R\in\mathcal{S}$ be a
realizer of the fact that $\delta$ is epic. Then $R(GUV)$ is an element of
$[\forall p(E_{\Sigma}(p)\to x_{0}\sim_{X}f(p))]$ for some $x_{0}\in|X|$.
Thus, $R(GUV)\emptyset\in[x_{0}\sim_{X}x]$ and
$R(GUV)\overline{1}\in[x_{0}\sim_{X}x^{\prime}]$. Finally, let
$t,s\in\mathcal{S}$ respectively realize transitivity and symmetry of
$\sim_{X}$. Then, we see that

$\lambda{uv}.t(\mathsf{p}(s(R(Guv)\emptyset))(R(Guv)\overline{1}))$

is the desired element $A$.

Conversely, suppose we have an $A\in\mathcal{S}$ as in the proposition. Let
$f\colon\\{0,1\\}\to|X|$ be arbitrary. By Lemma 5, it suffices to show that
from an element of $[f\approx f]$, we can continuously find an $x\in|X|$ and
an element of $[\forall p(E_{\Sigma}(p)\to x\sim_{X}f(p))]$. Let
$F\in[f\approx f]$. Then $F\emptyset\in[f(0)\sim_{X}f(0)]$,
$F\overline{1}\in[f(1)\sim_{X}f(1)]$ and $F\emptyset\subseteq F\overline{1}$,
so $A(F\emptyset)(F\overline{1})\in[f(0)\sim_{X}f(1)]$ and
$A(F\emptyset)(F\emptyset)\in[f(0)\sim_{X}f(0)]$. Hence, if we set $x=f(0)$,
then the graph of the continuous function

$\emptyset\mapsto A(F\emptyset)(F\emptyset),\quad W\neq\emptyset\mapsto
A(F\emptyset)(F\overline{1})$

is the desired element.

######  Corollary 7.

An assembly $X$ is order-discrete if and only if the existence of realizers
$U\in E_{X}(x)$ and $V\in E_{X}(y)$ with $U\subseteq V$ implies that $x$ and
$y$ are equal.

######  Proof 3.4.

Immediate.

The natural numbers object $N$ (c.f. the proof of 4) is easily seen to be
order-discrete using the corollary above.

Recall from the section on preliminaries that an object is called _discrete_
if it is orthogonal to $\nabla(2)$. For an assembly $X$, this means that the
realizing sets are disjoint. Thus, Corollary 7 shows that any order-discrete
assembly is also discrete (alternatively, one might observe that the map from
$\Sigma$ to $\nabla(2)$ is an epi in ${\sf Ass}({\mathcal{S}})$, and therefore
the map $X^{\nabla(2)}\to X^{\Sigma}$ is monic. From this one also easily
deduces that order-discrete implies discrete, for assemblies). In fact, this
holds for all objects, not just assemblies.

######  Proposition 8.

Any order-discrete object is discrete.

######  Proof 3.5.

This follows from Proposition 6 and [15], Corollary 3.2.20. The statement
there carries over to arbitrary realizability toposes.

######  Remark 9.

One might expect the availability of a simpler proof of the proposition above,
i.e. a proof that does not rely on the characterization of the
(order-)discrete objects. However, note that although we have a morphism
$\Sigma\to\nabla(2)$, it is not a regular epimorphism, so one cannot apply
[4], Lemma 2.2.

In [4], it it shown that the class of objects orthogonal to an object $A$
satisfies some nice properties if $A$ is well-supported and internally
projective. By Lemma 2, the object $\Sigma$ is internally projective. It is
clearly well-supported, which gives us the following proposition:

######  Proposition 10.

The order-discrete objects are closed under all existing limits, subobjects
and quotients in $\mathsf{RT}(\mathcal{S})$. Moreover, they form an
exponential ideal. Finally, they form a reflective subcategory of
$\mathsf{RT}(\mathcal{S})$.

######  Proof 3.6.

The first statement is true, because any collection of orthogonal objects is
closed under all existing limits (see [4], p. 1). Similarly, any collection of
orthogonal objects forms an exponential ideal. The other closure properties
follow from Lemmas 2.3 and 2.8 of [4], and Lemma 2 above. The final claim is
proven as a corollary right after Lemma 2.3 of [4].

######  Remark 11.

For comparison with the notion of homotopy to be defined below, we give a
concrete representation of the order-discrete reflection of an arbitrary
object $(X,\sim)$. It has the same underlying set $X$, and we let $[x\approx
y]$ consist of those coded (in the sense of $\mathcal{S}$) $(3n+1)$-tuples
$[U_{0},V_{0},W_{0},\ldots,U_{n-1},V_{n-1},W_{n-1},U_{n}]$ for which there is
a sequence $(x_{0},y_{0},\ldots,x_{n},y_{n})$ of elements of $X$, such that
the following conditions hold:

  1. (1)

$x_{0}=x$ and $y_{n}=y$;

  2. (2)

$U_{k}\in[x_{k}\sim y_{k}]$ for $0\leq k\leq n$;

  3. (3)

$V_{k}\in[y_{k}\sim y_{k}]$ and $W_{k}\in[x_{k+1}\sim x_{k+1}]$ for $0\leq
k<n$;

  4. (4)

$V_{k}\subseteq W_{k}$ or $W_{k}\subseteq V_{k}$ must hold.

##  4\. Arithmetic in ${\sf RT}({\mathcal{S}})$

The order-discrete modest sets already make a disguised appearance in [5].
Herein, Lietz singles out a class of so-called well-behaved modest sets. It is
not hard to show that a modest set is well-behaved if and only if it is order-
discrete and moreover, it has the join-property, which we define now. An
assembly has the _join-property_ if it is isomorphic to an assembly $X$ whose
realizing sets are closed under binary joins, viz. if $U\in E_{X}(x)$ and
$V\in E_{X}(x)$, then $U\cup V\in E_{X}(x)$ for all $x\in|X|$. The natural
numbers object $N$ has the join-property. The following proposition is a very
slight generalization of [5], Theorem 2.3.

######  Proposition 12.

Let $X$ and $Y$ be modest sets. If $X$ has the join-property and $Y$ is order-
discrete, then the following form of the Axiom of Choice holds in
$\mathsf{RT}(\mathcal{S})$:

$\forall x{:}X\exists y{:}Y\phi(x,y)\to\exists f{:}Y^{X}\forall
x{:}X\phi(x,f(x)).$

######  Proof 4.1.

See the proof of [5], Theorem 2.3.

We have already seen that the order-discrete objects form an exponential ideal
and are closed under binary products. In [5], Theorem 2.2, it is shown that
this also holds for the modest objects that have the join-property. Since $N$
is order-discrete and has the join-property, it follows that the Axiom of
Choice holds for all finite types. Consequently, the following two principles

$\displaystyle\forall f{:}N^{N}\exists x{:}N\phi(f,x)\to\forall
f{:}N^{N}\exists xy{:}N\forall
g{:}N^{N}(\overline{f}y=\overline{g}y\to\phi(g,x)),$ where
$\overline{f}y=\overline{g}y$ is short for $\forall z{:}N(z<y\to f(z)=g(z))$
(Weak Continuity for Numbers) $\displaystyle\forall F{:}N^{(N^{N})}\forall
f{:}N^{N}\exists x{:}N\forall g{:}N^{N}(\overline{f}x=\overline{g}x\to
F(f)=F(g))$ (Brouwer’s Principle)

are equivalent (and false) in $\mathsf{RT}(\mathcal{S})$; c.f. [5], Section
2.3.

###  4.1. Second-order arithmetic in ${\sf RT}({\mathcal{S}})$

We close this section by some brief considerations on second-order arithmetic
in realizability toposes and $\mathsf{RT}(\mathcal{S})$ in particular.

######  Lemma 13.

Let $A$ be any partial combinatory algebra. Write $\overline{n}$ for the
$n$-th Curry numeral in $A$ and let ${\mathsf{p}}$ be a pairing combinator in
$A$ with projections ${\mathsf{p}}_{0}$ and ${\mathsf{p}}_{1}$.

The power object ${\mathcal{P}}(N)$ of the natural numbers object $N$ in ${\sf
RT}(A)$ can be given as the object $(P,\approx)$ where $P$ is the set

$P=\\{\phi\colon\mathbb{N}\to\mathcal{P}(A)\mid\text{for all $n\in\mathbb{N}$,
if $a\in\phi(n)$, then ${\mathsf{p}}_{1}a=\overline{n}$}\\}$

and

$\psi\approx\psi=[\forall n(\phi(n)\leftrightarrow\psi(n))].$

######  Proof 4.2.

Straightforward.

We now turn our attention to $\lnot\lnot$-stable subsets of $N$, viz. subsets
$X$ such that

$\forall x(\lnot\lnot(x\in X)\to x\in X)$

is true in $\mathsf{RT}(A)$. We will abbreviate this formula by
$\textup{Stab}(X)$.

We formulate the following triviality as a proposition for comparison with 15
below, in the case of $A={\mathcal{S}}$.

######  Proposition 14.

If $A$ is nontrivial, then not every subset is $\lnot\lnot$-stable, i.e. the
sentence $\forall X\textup{Stab}(X)$ is not valid in ${\sf RT}(A)$.

######  Proof 4.3.

Note that $\forall X\textup{Stab}(X)$ implies $\forall p.\neg\neg p\to p$
(where $p$ is a variable of type $\Omega$), which fails in ${\sf RT}(A)$ as
soon as $A$ has two disjoint nonempty subsets. If $A$ is trivial then ${\sf
RT}(A)={\rm Set}$, and $\forall X\textup{Stab}(X)$ obviously holds.

By contrast, in ${\sf RT}({\mathcal{S}})$ we have the following result
(substituting $\mathcal{S}$ for $A$ in the definition of $P$ in Lemma 13):

######  Proposition 15.

For any $\alpha\in P$, we have a realizer of $\textup{Stab}(\alpha)$. Hence,
the sentence $\forall X\lnot\lnot\textup{Stab}(X)$ is true in
$\mathsf{RT}(\mathcal{S})$.

######  Proof 4.4.

Let $\alpha\in P$. Note that there is a function
$f_{\alpha}\colon\mathbb{N}\to\mathcal{S}$ such that

$f_{\alpha}(n)\in\begin{cases}[n\in\alpha]&\text{if
}[n\in\alpha]\neq\emptyset;\\\ \\{\emptyset\\}&\text{else}.\end{cases}$

Moreover, there is an element $F_{\alpha}\in\mathcal{S}$ such that
$F_{\alpha}\overline{n}=f_{\alpha}(n)$. Now note that
$\lambda{xy}.F_{\alpha}x$ realizes $\textup{Stab}(\alpha)$.

######  Corollary 16.

First-order arithmetic in ${\sf RT}({\mathcal{S}})$ is the same as first-order
arithmetic in Set.

######  Proof 4.5.

Given a true first-order arithmetical sentence $\phi$, we have, by Proposition
15, a realizer for $\forall x(\psi(x)\vee\neg\psi(x))$, for every subformula
$\psi$ of $\phi$. From this one constructs a realizer for $\phi$.

Just as for ordinary natural numbers, we write $\langle-,\\!-\rangle$ for a
definable coding of $N^{2}$ to $N$ in ${\sf RT}(A)$. The sentence $\forall
X\exists Y(\textup{Stab}(Y)\land\forall x(x\in X\leftrightarrow\exists
y\langle{y,x}\rangle\in Y))$ is known as _Shanin’s Principle_. It holds in the
Effective Topos ([15], p. 127). Internally, it says that every subset of $N$
is covered by a stable subset of $N$.

######  Proposition 17.

If $|A|>|\mathbb{N}|$, then Shanin’s Principle does not hold in ${\sf RT}(A)$.

######  Proof 4.6.

Assume for the sake of contradiction that it does. Then we have a realizer

$R\in\bigcap_{\alpha\in P}\bigcup_{\beta\in
P}\llbracket\textup{Stab}(\beta)\land\forall
x(x\in\alpha\leftrightarrow\exists y\langle y,x\rangle\in\beta)\rrbracket.$

Let us write $R_{0}=\mathsf{p_{0}}R$ and $R_{1}=\mathsf{p_{1}}R$. For each
$a\in A$, define the element $\alpha_{a}\in P$ by:

$\alpha_{a}(0)=\\{\mathsf{p}a\overline{0}\\}\quad\text{and}\quad\alpha_{a}(n+1)=\emptyset\quad\text{for
any }n\in\mathbb{N}.$

For each $a\in A$, pick some $\beta_{a}\in P$ such that
$R\in\llbracket\textup{Stab}(\beta_{a})\land\forall
x(x\in\alpha_{a}\leftrightarrow\exists y\langle
y,x\rangle\in\beta_{a})\rrbracket$.

From $R_{1}$, we effectively obtain $R^{\prime}\in A$ such that for every
$a\in A$, we have:

$R^{\prime}(\mathsf{p}a\overline{0})\in[\langle m,0\rangle\in\beta_{a}]$

for some $m\in\mathbb{N}$. As $|A|>|\mathbb{N}|$, there must be two different
$a,a^{\prime}\in A$ such that

$R^{\prime}(\mathsf{p}a\overline{0})\in[\langle m,0\rangle\in\beta_{a}]\text{
and }R^{\prime}(\mathsf{p}a^{\prime}\overline{0})\in[\langle
m,0\rangle\in\beta_{a^{\prime}}]$ ($\ast$)

for the same $m\in\mathbb{N}$.

From $R_{0}$, we effectively obtain $s\in A$ witnessing the stability of
$\beta_{a}$ and $\beta_{a^{\prime}}$. Thus, by $(\ast)$, we can use $s$ to get
a common realizer:

$s\overline{\langle m,0\rangle}\mathsf{i}\in[\langle
m,0\rangle\in\beta_{a}]\cap[\langle m,0\rangle\in\beta_{a^{\prime}}].$

Finally, using $s\overline{\langle m,0\rangle}\mathsf{i}$ and $R_{1}$, we find
a realizer in the intersection
$[0\in\alpha_{a}]\cap[0\in\alpha_{a^{\prime}}]=\alpha_{a}\cap\alpha_{a^{\prime}}$.
But this is impossible, because $a$ and $a^{\prime}$ are different, so that
$\alpha_{a}$ and $\alpha_{a^{\prime}}$ are disjoint.

######  Corollary 18.

Shanin’s Principle does not hold in $\mathsf{RT}(\mathcal{S})$ and
$\mathsf{RT}({\mathcal{K}}_{2})$ (where ${\mathcal{K}}_{2}$ is Kleene’s second
model).

##  5\. The Sierpiński object as a dominance

One can also study the Sierpiński object from a synthetic domain theoretic
standpoint. This was done by Wesley Phoa ([8], Chapter 12 and [9], Proposition
3.1), who worked in the category of modest sets over the r.e. graph model,
John Longley ([6], 5.3.7) and Alex Simpson ([7]). Our treatment is based on
Proposition 4. Define a relation $\in$ between $N$ and $S$ (the object of
realizers) by taking the following pullback

${\in}$${1}$${N\times S\cong
N\times\Sigma^{N}}$${\Sigma}$${\Omega}$${\lrcorner}$$\scriptstyle{t}$ev

where $\Sigma\to\Omega$ is the morphism induced by the function
$0\mapsto\emptyset$ and $1\mapsto\mathcal{S}$.

######  Remark 19.

Observe that $\in$ is given by

$[n\in U]=\begin{cases}\mathsf{p}\overline{n}U&\text{if $n$ is an element of
$U$};\\\ \emptyset&\text{else}.\end{cases}$

In particular, $\in$ is $\lnot\lnot$-stable.

######  Lemma 20.

Let $\mathcal{A}$ be a arbitrary _total_ pca and let
$\mathsf{RT}(\mathcal{A})$ be its realizability topos. Let
$A=(\mathcal{A},\\{-\\})$ be the object of realizers in the topos. The scheme

$(\textup{IP}_{A})\quad(\lnot\phi\to\exists x{:}A\psi)\to\exists
x{:}A(\lnot\phi\to\psi)$

with $x$ not free in $\phi$ is valid in $\mathsf{RT}(\mathcal{A})$.

######  Proof 5.1.

It is not hard to verify that $\lambda u.{\mathsf{p}}({\mathsf{p}}_{0}(u{\sf
k}))(\lambda v.{\mathsf{p}}_{1}(u{\sf k}))$ realizes the scheme.

######  Proposition 21.

The subobject $\Omega^{\prime}$ of $\Omega$ given by

$\Omega^{\prime}=\llbracket\exists X{:}S(p\leftrightarrow 1\in X)\rrbracket$

with $p$ ranging over $\Omega$, is a dominance in $\mathsf{RT}(\mathcal{S})$.
Moreover, it is $\lnot\lnot$-separated, i.e. $\forall
p{:}\Omega^{\prime}(\lnot\lnot p\to p)$. Furthermore,
$\bot\in\Omega^{\prime}$.

######  Proof 5.2.

Double negation separation is immediate by Remark 19. Further, it is clear
that $\top\in\Omega^{\prime}$ (take $X=\overline{1}$).

Suppose $p\in\Omega^{\prime}$ and $p\to(q\in\Omega^{\prime})$. Take
$U\in\mathcal{S}$ such that $p\leftrightarrow 1\in U$. Then, $1\in U\to\exists
X{:}S(q\leftrightarrow 1\in X)$, so by Lemma 20 and Remark 19, we get that
$\exists X{:}S(1\in U\to(q\leftrightarrow 1\in X))$. Take such
$V\in\mathcal{S}$. Then, $p\land q\leftrightarrow 1\in U\cap V$. Hence,
$p\land q\in\Omega^{\prime}$ and $\Omega^{\prime}$ is a dominance.

We have already remarked that the object $\Omega^{\prime}$ from 21 is
$\lnot\lnot$-separated. Indeed, it is isomorphic to an assembly.

######  Proposition 22.

The object $\Omega^{\prime}$ is isomorphic to $\Sigma$.

######  Proof 5.3.

First of all, observe that $\Omega^{\prime}$ is isomorphic to the object
$(\mathcal{P}(\mathcal{S}),\sim)$ where

$\displaystyle\mathcal{U}\sim\mathcal{V}$
$\displaystyle=\mathcal{U}\leftrightarrow\mathcal{V}\land
E(\mathcal{U}),\text{with}$ $\displaystyle E(\mathcal{U})$
$\displaystyle=\\{[W,U]\in\mathcal{S}\mid\text{if $1\in W$, then
$U\in\mathcal{U}$ and if $\mathcal{U}\neq\emptyset$, then $1\in W$}\\}.$

Define a continuous function $F\colon\mathcal{S}\to\mathcal{S}$ by

$F(\emptyset)=\emptyset\text{ and }F(V)=\overline{1}\text{ for any non-empty
$V$}.$

Next, define
$\Phi\colon\mathcal{P}(\mathcal{S})\times\\{0,1\\}\to\mathcal{P}(\mathcal{S})$
by

$(\mathcal{U},i)\mapsto\\{[W,U,C]\mid[W,U]\in E(\mathcal{U}),C\in
E_{\Sigma}(i)\text{ and }i=1\Leftrightarrow 1\in W\\}.$

We show that $\Phi$ is a functional relation from
$(\mathcal{P}(\mathcal{S}),\sim)$ to $\Sigma$. Strictness is immediate. For
single-valuedness, suppose we have $[W,U,C]\in\Phi(\mathcal{U},i)$ and
$[W^{\prime},U^{\prime},C^{\prime}]\in\Phi(\mathcal{U},j)$. We show that
$i=j$. By definition, we have

$i=1\Leftrightarrow 1\in W\Leftrightarrow U\in\mathcal{U}\Rightarrow 1\in
W^{\prime}\Leftrightarrow j=1$

and similarly, $i=0\Rightarrow j=0$. Thus, $i=j$, as desired. Suppose
$[W,U,C]\in\Phi(\mathcal{U},i)$ and
$B\in[\mathcal{U}\leftrightarrow\mathcal{V}]$. We must effectively obtain an
element of $\Phi(\mathcal{V},i)$. But if $B_{0}$ realizes
$\mathcal{U}\to\mathcal{V}$, then one easily sees that $[W,B_{0}U,C]$ is an
element of $\Phi(\mathcal{V},i)$. So, $\Phi$ is relational. For totality,
suppose $[W,U]\in E(\mathcal{U})$, then $[W,U,F(W)]\in\Phi(\mathcal{U},i)$ for
some $i\in\\{0,1\\}$, by construction of $E$ and $F$. We conclude that $\Phi$
is a functional relation.

Moreover, (the arrow represented by) $\Phi$ is easily seen to be epic. For, if
$C\in E_{\Sigma}(i)$, then $[F(C),F(C),C]\in\Phi(\mathcal{U}_{i},i)$ with
$\mathcal{U}_{1}=\\{\overline{1}\\}$ and $\mathcal{U}_{0}=\emptyset$ by
construction of $F$ and definition of $E_{\Sigma}$.

Finally, we prove that $\Phi$ is monic and hence that $\Phi$ represents an
isomorphism, as desired. Suppose we have $[W,U,C]\in\Phi(\mathcal{U},i)$ and
$[W^{\prime},U^{\prime},C]\in\Phi(\mathcal{V},i)$. It suffices to effectively
provide an element of $\mathcal{U}\leftrightarrow\mathcal{V}$, since $[W,U]$
is an element of $E(\mathcal{U})$ already. But $[\lambda x.U^{\prime},\lambda
x.U]$ is easily seen to do the job.

Proposition 22 implies that we have a notion of $\Sigma$-subobjects of any
object in $\mathsf{RT}(\mathcal{S})$: a mono $Y\to X$ represents a
$\Sigma$-subobject of $X$ if and only if its classifying map factors through
$\Sigma$. We write $U\subseteq_{\Sigma}X$ to indicate that $U$ is a
$\Sigma$-subobject of $X$.

The following proposition characterizes these $\Sigma$-subobjects for
assemblies $X$.

######  Proposition 23.

Let $X$ be an assembly. There is a bijective correspondence between morphisms
$X\to\Sigma$ and subsets $X^{\prime}\subseteq|X|$ for which there is an open
$\mathcal{U}\subseteq\mathcal{S}$ with the following properties:

$\displaystyle x\in X^{\prime}$ $\displaystyle\Rightarrow
E_{X}(x)\subseteq\mathcal{U};$ $\displaystyle x\not\in X^{\prime}$
$\displaystyle\Rightarrow E_{X}(x)\cap\mathcal{U}=\emptyset.$

Moreover, an assembly $Y$ is a $\Sigma$-subobject of $X$ if and only if $Y$ is
isomorphic to some assembly $(X^{\prime},E)$ where $X^{\prime}\subseteq|X|$ is
as above and $E$ is the restriction of $E_{X}$ to $X^{\prime}$.

######  Proof 5.4.

Let $f$ be a morphism from $X$ to $\Sigma$ that is tracked by
$U\in\mathcal{S}$. Set

$X^{\prime}=\\{x\in X\mid
f(x)=1\\}\quad\text{and}\quad\mathcal{U}=\\{V\in\mathcal{S}\mid
UV=\overline{1}\\}.$

We show that $\mathcal{U}$ is open. Let
$\mathcal{Q}\coloneqq\\{p\subseteq\mathcal{S}\mid p\text{ is finite and
}Up=\overline{1}\\}$. Recall the notation $\uparrow\\!p=\\{V\in\mathcal{S}\mid
p\subseteq V\\}$. By continuity of the application, one can show that
$\mathcal{U}=\bigcup_{p\in\mathcal{Q}}\uparrow\\!p$. Thus, $\mathcal{U}$ is an
open of $\mathcal{S}$.

From the definition of $\mathcal{U}$ and the fact that $U$ tracks $f$, it is
immediate that $\mathcal{U}$ has the desired properties.

For the converse, assume we are given an open
$\mathcal{U}\subseteq\mathcal{S}$ and a subset $X^{\prime}\subseteq|X|$ with
the properties stated. Define $f\colon X\to\Sigma$ by $f(x)=1$ if $x\in
X^{\prime}$ and $f(x)=0$ if $x\not\in X^{\prime}$. We claim that it is tracked
by $\textup{graph}(F)$ where $F(U)=\\{1\mid U\in\mathcal{U}\\}$. That this $F$
is continuous follows from the assumption that $\mathcal{U}$ is open. Now if
$x\in X$ and $U\in E_{X}(x)$, then either $f(x)=1$, in which case
$E_{X}(x)\subseteq\mathcal{U}$, so that $F(U)=\overline{1}\in
E_{\Sigma}(f(x))$; or $f(x)=0$, in which case $E(x)\cap\mathcal{U}=\emptyset$,
so that $F(U)=\emptyset\in E_{\Sigma}(f(x))$. So $f$ is tracked, as desired.

That the operations above are each other’s inverses is readily verified. The
final claim follows immediately from the construction above and the
description of pullbacks in the category of assemblies.

The referee has suggested that Proposition 23 gives a notion of synthetic
topology on $\mathsf{RT}(\mathcal{S})$ in the sense of [2]. However, observe
the caveat after Proposition 27.

For any dominance $\Sigma\subset\Omega$ in a topos, one has for every object
$X$ the partial map classifier for $\Sigma$-subobjects: that is, a
$\Sigma$-subobject $\eta_{X}:X\to L(X)$ which classifies partial maps into $X$
defined on a $\Sigma$-subobject. It follows that $L$ is a functor (generally
dubbed the “lift functor”) and $\eta$ is a natural transformation from the
identity functor to $L$. Now Propositions 21 and 22 together imply that the
functor $L$ restricts to an endofunctor on the category of assemblies. The
following proposition describes this restriction explicitly.

######  Proposition 24.

The lift functor $L$ on ${\sf Ass}({\mathcal{S}})$ is given by on objects by:

$L(X)=\left(|X|\cup\\{\bot_{X}\\},E_{L(X)}\right),$

where $\bot_{X}$ is some element not in $|X|$ and

$E_{L(X)}(\bot_{X})=\\{\emptyset\\}\quad\text{and}\quad
E_{L(X)}(x)=\\{[U,\overline{1}]\mid U\in E_{X}(x)\\}\text{ for $x\in|X|$}.$

Given an arrow $f\colon X\to Y$, we define $L(f)$ as the unique extension of
$f$ satisfying $\bot_{X}\mapsto\bot_{Y}$. The natural transformation
$\eta\colon\operatorname{\textup{id}}_{\mathsf{Ass}(\mathcal{S})}\to L$ is
defined as $\eta_{X}(x)=x$.

######  Proof 5.5.

Given a morphism $f\colon X\to Y$ of $\mathsf{Asm}(\mathcal{S})$ tracked by
$U_{f}\in\mathcal{S}$, note that $L(f)$ is tracked, as

$[V_{0},V_{1}]\mapsto\begin{cases}[U_{f}V_{0},\overline{1}]&\text{if }1\in
V_{1};\\\ \emptyset&\text{else};\end{cases}$

is a continuous map $\mathcal{S}\to\mathcal{S}$. Verifying that $L$ is indeed
a functor is routine. Also, note that $\eta_{X}$ is tracked by
$\lambda{u}.[u,\overline{1}]$. That $\eta$ is natural is easily checked.

Finally, suppose we have a morphism $f\colon U\to Y$ and
$U\subseteq_{\Sigma}X$. By Proposition 23, we may assume that we have
$|U|\subseteq|X|$ and an open $\mathcal{U}$ such that for $x\in|X|$:

$\text{if }x\in|U|,\text{then
}E_{X}(x)\subseteq\mathcal{U}\quad\text{and}\quad\text{if
}x\not\in|U|,\text{then }E_{X}(x)\cap\mathcal{U}=\emptyset.$

Define $\tilde{f}\colon X\to L(Y)$ by

$\tilde{f}(x)=\begin{cases}f(x)&\text{if }x\in|U|;\\\
\bot_{Y}&\text{else}.\end{cases}$

Note that $\tilde{f}$ is tracked, for if $f$ is tracked by $U_{f}$, then

$U\mapsto\begin{cases}U_{f}U&\text{if }U\in\mathcal{U};\\\
\emptyset&\text{else}\end{cases}$

is a continuous map $\mathcal{S}\to\mathcal{S}$, because $\mathcal{U}$ is
open.

If we have morphisms $g\colon Z\to X$ and $h\colon Z\to Y$ such that
$\tilde{f}g=\eta_{Y}h$, then we must have that $g(z)\in|U|$ for any $z\in|Z|$.
Hence, $g$ factors uniquely through $(U,E_{U})$. This proves that $\tilde{f}$
makes the square

$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq_{\Sigma}}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tilde{f}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{Y}}$$\textstyle{L(Y)}$

into a pullback.

It remains to show that it is unique with this property. To this end, suppose
we have $f^{\prime}\colon X\to L(Y)$, such that the square

$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq_{\Sigma}}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f^{\prime}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{Y}}$$\textstyle{L(Y)}$

is a pullback. From the commutativity of the square, it follows that for
$x\in|U|$ we must have $f^{\prime}(x)=f(x)=\tilde{f}(x)$. Now suppose for a
contradiction that we have $x_{0}\in|X|\setminus|U|$ and
$f^{\prime}(x_{0})\in|Y|$. The universal property of the pullback then yields
a map $U\cup\\{x_{0}\\}\to U$ such that the inclusion
$|U|\cup\\{x_{0}\\}\to|X|$ factors through $|U|$, but this is impossible, as
$x_{0}\not\in|U|$. Hence, no such $x_{0}$ exists and therefore, $f^{\prime}$
and $\tilde{f}$ coincide.

######  Remark 25.

Observe that $L(1)\cong\Sigma$ and that $\eta_{1}=1\xrightarrow{t}\Sigma$.

######  Lemma 26.

For any $X$, we have $X\subseteq_{\Sigma}L(X)$ via $\eta_{X}$.

######  Proof 5.6.

It is straightforward to verify that

${X}$${1}$${L(X)}$${\Sigma}$$\scriptstyle{\eta_{X}}$$\scriptstyle{t}$$\scriptstyle{\chi_{X}}$

with $\chi_{X}(x)=1$ and $\chi_{X}(\bot_{X})=0$ is a pullback. (Note the map
$F(V)=\overline{1}$ if $1\in\mathsf{p_{1}}V$ and $\emptyset$ otherwise is
continuous and its graph tracks $\chi_{X}$.)

As always, the lift functor $L$ is a monad on ${\sf Ass}({\mathcal{S}})$. The
multiplication $\mu\colon L^{2}(X)\to L(X)$ is given by the map $x\mapsto
x,\bot_{X}\mapsto\bot_{X},\bot_{L(X)}\mapsto\bot_{X}$.

##  6\. A notion of homotopy for the order-discrete objects

In [14], a notion of homotopy for the Effective Topos is given. This notion is
tied up with the subcategory of discrete objects, in the following way:
internally, for each object $X$, the “discrete reflection” of $X$ is the set
of path components of $X$. It is just natural to wonder whether this would
also work for the order-discrete objects in ${\sf RT}({\mathcal{S}})$.

Another interpretation of homotopy for the Effective Topos is in the paper [3]
by Dan Frumin and Benno van den Berg. They build a very elegant framework on
purely category-theoretic notions. The basic ingredients are: an interval
object $\mathbb{I}$ with two distinct points
$\partial_{0},\partial_{1}:1\to\mathbb{I}$ , binary maps $\wedge,\vee:I\times
I\to I$ satisfying some axioms, and a dominance $\Sigma$ which is closed under
finite unions and satisfies the condition that the inclusion
$[\partial_{0},\partial_{1}]:1+1\to\mathbb{I}$ is a $\Sigma$-subobject. From
these notions, a subcategory of “fibrant objects” is defined, and there is a
Quillen model structure on this subcategory. When applying to the Effective
Topos they take the trivial dominance: $\Omega$ itself.

In ${\sf RT}({\mathcal{S}})$ we have an interesting dominance: the Sierpiński
object. However, the Frumin-van den Berg framework is not applicable for this
dominance, as the following proposition shows.

######  Proposition 27.

The Sierpiński object, as subobject of $\Omega$, is not closed under finite
unions.

######  Proof 6.1.

We apply the characterization 22. Let the variables $X,Y,Z$ range over the
object of realizers $S$ (which in turn is seen as subobject of
${\mathcal{P}}(N)$). We prove that the statement

$\forall XY\exists Z(1\in Z\leftrightarrow 1\in X\vee 1\in Y)$ ($\ast$)

is not valid in ${\sf RT}({\mathcal{S}})$. Indeed, working out the
realizability of $(\ast)$, we see that we need continuous functions $F$ and
$G$ on $\mathcal{S}$ such that for all $U,V\in{\mathcal{S}}$ we have:

  * •

If $1\in U$ or $1\in V$ then $1\in F(U,V)$.

  * •

If $1\in F(U,V)$ then either $G(F(U,V))=\overline{0}$ and $1\in U$, or
$G(F(U,V))=\overline{1}$ and $1\in V$.

However, this is impossible: consider $G(F(\\{1\\},\\{1\\}))$. If this is
equal to $\overline{0}$ then by continuity we cannot have
$G(F(\emptyset,\\{1\\}))=\overline{1}$; the other case is similar.

Caveat: note that if we interpret Escardó’s “synthetic topology” in ${\sf
RT}({\mathcal{S}})$, we see from Proposition 27 that this topology will not be
standard, but “substandard” in the terminology of [2].

In view of Proposition 27, we revert to the more ‘hands-on’ approach of [14].
The main extra complication is the essential asymmetry of the object $\Sigma$.
In the effective topos case, we had for every natural number $n$ a ‘generic
interval’ $I_{n}$ (which essentially is an iterated pushout of copies of
$\nabla(2)$). Here, we have more generic intervals, indexed by 01-sequences.
For each natural number $n\geq 1$ and each 01-sequence
$\sigma=(\sigma_{0},\ldots,\sigma_{n-1})$ we define the assembly
$I_{n,\sigma}=(\\{0,\ldots,n\\},E_{n,\sigma})$ where:

$\begin{array}[]{lcl}E_{n,\sigma}(0)&=&\left\\{\begin{array}[]{cl}\\{{\sf
p}\overline{0}\,\overline{1},{\sf p}\overline{1}\emptyset\\}&\text{if
}\sigma_{0}=0;\\\ \\{{\sf p}\overline{0}\,\overline{1},{\sf
p}\overline{1}\,\overline{1}\\}&\text{if }\sigma_{0}=1;\end{array}\right.\\\
E_{n,\sigma}(k+1)\text{ (for $k+1<n$)}&=&\left\\{\begin{array}[]{cl}\\{{\sf
p}\overline{k}\,\overline{1},{\sf p}\overline{k+1}\emptyset\\}&\text{if
}\sigma_{k}=0,\sigma_{k+1}=0;\\\ \\{{\sf p}\overline{k}\,\overline{1},{\sf
p}\overline{k+1}\,\overline{1}\\}&\text{if }\sigma_{k}=0,\sigma_{k+1}=1;\\\
\\{{\sf p}\overline{k}\emptyset,{\sf p}\overline{k+1}\emptyset\\}&\text{if
}\sigma_{k}=1,\sigma_{k+1}=0;\\\ \\{{\sf p}\overline{k}\emptyset,{\sf
p}\overline{k+1}\,\overline{1}\\}&\text{if
}\sigma_{k}=1,\sigma_{k+1}=1;\end{array}\right.\\\
E_{n,\sigma}(n)&=&\left\\{\begin{array}[]{cl}\\{{\sf
p}\overline{n}\,\overline{1},{\sf p}\overline{n+1}\emptyset\\}&\text{if
}\sigma_{n-1}=0;\\\ \\{{\sf p}\overline{n}\emptyset,{\sf
p}\overline{n+1}\emptyset\\}&\text{if
}\sigma_{n-1}=1.\end{array}\right.\end{array}$

So, each set $E_{n,\sigma}(k)$ consists of two elements $\alpha_{k}$,
$\beta_{k}$ which satisfy the following conditions:

  * •

${\sf p}_{0}\alpha_{k}=\overline{k}$, ${\sf p}_{0}\beta_{k}=\overline{k+1}$;

  * •

$\beta_{k}\subset\alpha_{k+1}$ if $\sigma_{k}=0$;

  * •

$\beta_{k}\supset\alpha_{k+1}$ if $\sigma_{k}=1$.

The object $I_{n,\sigma}$ is called a generic interval of length $n$.

######  Proposition 28.

Let $(X,\sim)$ be an arbitrary object of ${\sf RT}({\mathcal{S}})$ and let
$I_{n,\sigma}$ be a generic interval of length $n$. The exponent
$(X,\sim)^{I_{n,\sigma}}$ can be described as follows: its underlying set is
the set of $2n+2$-tuples $(\vec{x},\vec{y})=(x_{0},y_{0},\ldots,x_{n},y_{n})$
of elements of $X$. Given such a tuple, we define $E(\vec{x},\vec{y})$ as the
set of coded $3n-2$-tuples (coded in the sense of $\mathcal{S}$)

$[U_{0},V_{0},W_{0},\ldots,U_{n-1},V_{n-1},W_{n-1},U_{n}]$

of elements of $\mathcal{S}$ such that we have:

  * •

$U_{k}\in[x_{k}\sim y_{k}]$ for $0\leq k\leq n$;

  * •

$V_{k}\in[y_{k}\sim y_{k}]$, $W_{k}\in[x_{k+1}\sim x_{k+1}]$ for $0\leq k<n$;

  * •

$V_{k}\subseteq W_{k}$ if $\sigma_{k}=0$, and $V_{k}\supseteq W_{k}$ if
$\sigma_{k}=1$.

For two such tuples $(\vec{x},\vec{y}),(\vec{x^{\prime}},\vec{y^{\prime}})$,
the set $[(\vec{x},\vec{y})\approx(\vec{x^{\prime}},\vec{y^{\prime}})]$ is the
set of coded triples (in the sense of $\mathcal{S}$) $[\alpha,\beta,\gamma]$
of elements of $\mathcal{S}$, which satisfy:

  * •

$\alpha\in E(\vec{x},\vec{y})$;

  * •

$\beta\in E(\vec{x^{\prime}},\vec{y^{\prime}})$;

  * •

$\beta\overline{k}\in[x_{k}\sim x^{\prime}_{k}]$ for $0\leq k\leq n$.

######  Proof 6.2.

This is left to the reader, who may find it useful to review Proposition 3. It
should be noted that realizers of elements of $(X,\sim)^{I_{n,\sigma}}$ don’t
contain information about $\sigma$. This is not necessary, since for any
$V,W\in{\mathcal{S}}$ we have a continuous endomap on $\mathcal{S}$ which
sends ${\sf p}\overline{k}\emptyset$ to $V\cap W$ and ${\sf
p}\overline{k}\,\overline{1}$ to $V\cup W$, so it is enough to know that some
inclusion between $U_{k},V_{k}$ exists. Note also that the number $n$ can be
retrieved from any element of $E(\vec{x},\vec{y})$.

As in [14], we say that an arrow $I_{n,\sigma}\to I_{m,\tau}$ is order and
end-point preserving if its underlying function:
$\\{0,\ldots,n\\}\to\\{0,\ldots,m\\}$ is so (with respect to the usual order).
Let $(X,\sim)$ be an object of ${\sf RT}({\mathcal{S}})$. Its path object
${\sf P}(X,\sim)$ defined as follows. Its underlying set is the set of all
tuples $(x_{0},y_{0},\ldots,x_{n},y_{n})$, which we write as $(\phi,n)$. For
two such tuples $(\phi,n)$ and $(\psi,m)$ we let $[(\phi,n)\sim(\psi,m)]$ be
the set of coded triples (in the sense of $\mathcal{S}$) $[\alpha,s,\beta]$ of
elements of $\mathcal{S}$ such that for suitable 01-sequences $\sigma,\tau$ we
have:

  1. (1)

$\alpha\in E(\phi,n)$ as element of $(X,\sim)^{I_{n,\sigma}}$;

  2. (2)

$\beta\in E(\psi,m)$ as element of $(X,\sim)^{I_{m,\tau}}$;

  3. (3)

There are order and endpoint preserving maps
$I_{p,\rho}\stackrel{{\scriptstyle f}}{{\to}}I_{n,\sigma}$,
$I_{p,\rho}\stackrel{{\scriptstyle g}}{{\to}}I_{m,\tau}$ such that $s\in[\phi
f\approx\psi g]$ in the sense of $(X,\sim)^{I_{p,\rho}}$.

######  Remark 29.

The third clause corrects an inaccuracy in Definition 2.5 of [14], which was
noted in [3].

With this definition of path object we can now mimick [14] and prove the
following theorem:

######  Theorem 30.

  1. (1)

The construction of ${\sf P}(X,\sim)$ extends to an endofunctor on ${\sf
RT}({\mathcal{S}})$, which preserves finite limits.

  2. (2)

The object ${\sf P}(X,\sim)$ comes equipped with well-defined maps:

     * ${\sf s}$ (source), $\sf t$ (target): ${\sf P}(X,\sim)\to(X,\sim)$;

     * $\sf c$ (constant path): $(X,\sim)\to{\sf P}(X,\sim)$;

     * $\ast$ (composition of paths): ${\sf P}(X,\sim)\times_{(X,\sim)}{\sf P}(X,\sim)\to{\sf P}(X,\sim)$ where the domain is the pullback $\\{(x,y)\,|\,{\sf t}(x)={\sf s}(y)\\}$;

     * $\widetilde{(-)}$ (converse path): ${\sf P}(X,\sim)\to{\sf P}(X,\sim)$.

Moreover, with these data the object ${\sf P}(X,\sim)$ has the structure of an
internal category in ${\sf RT}({\mathcal{S}})$ with a contravariant involution
which is the identity on objects.

######  Proposition 31.

The set of path components of $(X,\sim)$, i.e. the quotient of $(X,\sim)$ by
the equivalence relation “there is a path from $x$ to $y$”, is exactly the
order-discrete reflection of $(X,\sim)$.

######  Proof 6.3.

Inspection of Remark 11 and Definition 6.

Just as in [14], we see that we have a “path object category” in the sense of
Van den Berg and Garner ([13]). For a countably based $T_{0}$-space, its image
under the embedding in ${\sf RT}({\mathcal{S}})$ is always discrete (that is
the $T_{0}$-property); it is order-discrete if and only if the space is
$T_{1}$. For any $T_{0}$-space $X$, the specialization order on $X$ is the
partial order defined by: $x\leq y$ if and only if every open set which
contains $x$, also contains $y$ (in the notation of the introduction:
$e(x)\subseteq e(y)$, if the embedding of X is $(X,E_{X})$ with
$E_{X}(x)=\\{e(x)\\}$). We can see this order relation as an undirected graph
on $X$. A path from $x$ to $y$ is just a path in this graph.

## References

  * [1] A. Bauer.  The Realizability Approach to Computable Analysis and Topology.  PhD thesis, Carnegie Mellon University, Pittsburgh, 2000.
  * [2] M. Escardó.  Topology via higher-order intuitionistic logic.  Notes of talk at MFPS, Pittsburgh 2004. Available at https://www.cs.bham.ac.uk/$\sim$mhe/papers/
  * [3] D. Fumin and B. van den Berg.  A homotopy-theoretic model of function extensionality in the effective topos.  Mathematical Structures in Computer Science, 29:588–614, 2019\.
  * [4] J.M.E. Hyland, E.P. Robinson, and G. Rosolini.  The discrete objects in the effective topos.  Proceedings of the London Mathematical Society, 60:1–60, 1990.
  * [5] Peter Lietz.  Comparing realizability over ${\mathcal{P}}\omega$ and ${K}_{2}$.  Note, TU Darmstadt, October 28, 1999. Available at `http://www.staff.science.uu.nl/~ooste110/realizability.html`, 1999.
  * [6] J. Longley.  Realizability Toposes and Language Semantics.  PhD thesis, Edinburgh University, 1995.
  * [7] J.R. Longley and A.K. Simpson.  A uniform approach to domain theory in realizability models.  Mathematical Structures in Computer Science, 7:469–505, 1997.
  * [8] W. Phoa.  Domain Theory in Realizability Toposes.  PhD thesis, Cambridge University, 1990.
  * [9] W. Phoa.  Building domains from graph models.  Mathematical Structures in Computer Science, 2:277–299, 1992.
  * [10] G. Plotkin.  A set-theoretical definition of application, 1972.  Memorandum MIP-R-95, School of Artificial Intelligence, University of Edinburgh.
  * [11] D.S. Scott.  The language lambda.  Journal of Symbolic Logic, 39(2):425–427, 1974.
  * [12] D.S. Scott.  Data types as lattices.  SIAM Journal of Computing, 5(3):522–587, 1976.
  * [13] B. van den Berg and R. Garner.  Topological and simplicial models of identity types.  ACM Transactions on Computational Logic, 13(1):1–44, 2012.
  * [14] J. van Oosten.  A notion of homotopy for the effective topos.  Mathematical Structures in Computer Science, 25:1132–1146, 2015.
  * [15] J. van Oosten.  Realizability: an Introduction to its Categorical Side, volume 152 of Studies in Logic.  North-Holland, 2008.