# Paraphrase Generation as Unsupervised Machine Translation

Chun Fan♠, Yufei Tian${}^{\text{\char 170}}$, Yuxian Meng♣, Nanyun
Peng${}^{\text{\char 170}}$
Xiaofei Sun♣, Fei Wu◆ and Jiwei Li◆♣
◆Zhejiang University, ♠Computer Center of Peking University
${}^{\text{\char 170}}$University of California, Los Angeles
♣Shannon.AI
{yuxian_meng, xiaofei_sun<EMAIL_ADDRESS>
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

In this paper, we propose a new paradigm for paraphrase generation by treating
the task as unsupervised machine translation (UMT) based on the assumption
that there must be pairs of sentences expressing the same meaning in a large-
scale unlabeled monolingual corpus. The proposed paradigm first splits a large
unlabeled corpus into multiple clusters, and trains multiple UMT models using
pairs of these clusters. Then based on the paraphrase pairs produced by these
UMT models, a unified surrogate model can be trained to serve as the final
Seq2Seq model to generate paraphrases, which can be directly used for test in
the unsupervised setup, or be finetuned on labeled datasets in the supervised
setup. The proposed method offers merits over machine-translation-based
paraphrase generation methods, as it avoids reliance on bilingual sentence
pairs. It also allows human intervene with the model so that more diverse
paraphrases can be generated using different filtering criteria. Extensive
experiments on existing paraphrase dataset for both the supervised and
unsupervised setups demonstrate the effectiveness the proposed paradigm.

##  1 Introduction

The goal of paraphrase generation Prakash et al. (2016a); Cao et al. (2016);
Ma et al. (2018); Wang et al. (2018) is to generate a sentence semantically
identical to a given input sentence but with variations in lexicon or syntax.
It has been applied to various downstream NLP tasks such as parsing (Berant
and Liang, 2014), question answering (Dong et al., 2017), summarization
(Barzilay, 2004) and machine translation (Callison-Burch et al., 2006).

Building a strong paraphrase generation system usually requires massive
amounts of high-quality annotated paraphrase pairs, but existing labeled
datasets (Lin et al., 2014; Fader et al., 2013; Lan et al., 2017) are either
of small sizes or restricted in narrow domains. To avoid such a heavy reliance
on labeled datasets, recent works have explored unsupervised methods (Li et
al., 2018b; Fu et al., 2019; Siddique et al., 2020) to generate paraphrase
without annotated training data, among which the back-translation based model
is an archetype (Mallinson et al., 2017; Sokolov and Filimonov, 2020). It
borrows the idea of back-translation (BT) in machine translation (Sennrich et
al., 2016) where the model first translates a sentence $s_{1}$ into another
sentence $s_{2}$ in a different language (e.g., En$\rightarrow$Fr), and then
translates $s_{2}$ back to $s_{1}$. In this way, the model is able to generate
paraphrases by harnessing bilingual datasets, removing the need for label
paraphrase data.

However, BT-based models for paraphrase generation have the following severe
issues: Firstly, BT-based systems rely on external resources, i.e., bilingual
datasets, making them hard to be applied to languages whose bilingual datasets
are hard to obtain. Secondly, translation errors, such as duplicate words
(Holtzman et al., 2020), missing words (Luong et al., 2015) and polysemous
words (Rios Gonzales et al., 2017), will accumulate during the forward and
backward translations, resulting in inferior performances. Thirdly, machine
translation models work like a blackbox, making it hard for humans to
intervene with the model and control the generation process.

In this work, we propose to address these problems based on the assumption
that there must be pairs of sentences expressing the same meaning in a large-
scale unlabeled corpus. Inspired by unsupervised machine translation (UMT)
models, which align semantic spaces of two languages using monolingual data,
we propose a pipeline system to generate paraphrases following two stages: (1)
splitting a large-scale monolingual corpus into multiple clusters/sub-
datasets, on which UMT models are trained based on pairs of these sub-
datasets; and (2) training a unified surrogate model based on the paraphrase
pairs produced by the trained multiple UMT models, where we can design
filtering functions to remove the pairs with undesired properties. The unified
surrogate model can be then directly used for paraphrase generation in the
unsupervised setup, or be finetuned on labeled datasets in the supervised
setup.

The proposed framework provides the following merits over existing BT-based
methods: (1) it is purely based on a large-scale monolingual corpus, which
removes the reliance on bilingual datasets; (2) the trained unified model is
able to generate paraphrases end-to-end, which avoids the issue of error
accumulation that exists in vanilla BT-based models; and (3) human
interventions can take place in the filtering step, which gives finer-grained
controls over the generated paraphrases.

We conduct extensive experiments on a wide range of paraphrase datasets to
evaluate the effectiveness of the proposed framework, and we are able to
observe performance boosts against strong baselines under both supervised and
unsupervised setups.

##  2 Related Work

##### Paraphrase Generation

Methods for paraphrase generation usually fall into two categories: supervised
and unsupervised approaches. Supervised methods for paraphrase generation rely
on annotated paraphrase pairs. Xu et al. (2018); Qian et al. (2019) employed
distinct semantic style embeddings to generate diverse paraphrases, and Iyyer
et al. (2018); Li et al. (2019); Chen et al. (2019); Goyal and Durrett (2020)
proposed to use different syntactic structure templates. A line of work
(Mallinson et al., 2017; Sokolov and Filimonov, 2020) formalized paraphrase
generation as machine translation. Unsupervised paraphrase generation is
primarily based on reinforcement learning (RL) generative models Ranzato et
al. (2015); Li et al. (2016b). RL optimizes certain criteria, e.g. BLEU, to
reward paraphrases with higher quality (Li et al., 2018b; Siddique et al.,
2020). Bowman et al. (2016); Yang et al. (2019) trained a variational auto-
encoder (VAE) (Kingma and Welling, 2013) to generate paraphrases. Other
unsupervised methods for paraphrase generation include VAE (VQ-VAE) (Roy and
Grangier, 2019), latent bag-of-words alignment (Fu et al., 2019) and simulated
annealing (Liu et al., 2019a). Adapting large-scale pretraining Devlin et al.
(2018); Radford et al. (2018); Liu et al. (2019b); Clark et al. (2020); Sun et
al. (2021b) to paraphrase generation has been recently investigated (Witteveen
and Andrews, 2019; Hegde and Patil, 2020; Niu et al., 2020; Meng et al., 2021)
and has shown promising potentials to improve generation quality. Our work is
distantly related to unsupervised text style transfer (Hu et al., 2017;
Mueller et al., 2017; Shen et al., 2017; Li et al., 2018a; Fu et al., 2018),
where the model alters a specific text attribute of an input sentence (such as
sentiment) while preserving other text attributes.

Regarding soliciting large-scale paraphrase datasets, Bannard and Callison-
Burch (2005) used statistical machine translation methods obtain paraphrases
in parallel text, the technique of which is scaled up by Ganitkevitch et al.
(2013) to produce the Paraphrase Database (PPDB). Wieting et al. (2017)
translate the non-English side of parallel text to obtain paraphrase pairs.
Wieting and Gimpel (2017) collected paraphrase dataset with million of pairs
via machine translation. Hu et al. (2019a, b) produced paraphrases from a
bilingual corpus based on the techniques of negative constraints and inference
sampling.

##### Unsupervised Machine Translation

(UMT) has been an active research direction in NLP (Ravi and Knight, 2011).
Pioneering work for unsupervised neural machine translation used denoising
auto-encoders and back-translation (Sennrich et al., 2016) to iteratively
refine the generated translation. Artetxe et al. (2017) proposed to use a
shared encoder to encode source input sentences from different languages.
Lample et al. (2017) additionally used adversarial and cross-domain training
objectives to better identify different language domains. Yang et al. (2018)
relaxed the strategy of sharing the entire encoder in Artetxe et al. (2017) by
building independent encoders to maintain unique characteristics of each
language. Another line of work for UMT is to combine statistical machine
translation (SMT) and NMT. Artetxe et al. (2018); Lample et al. (2018) built a
phrase-level mapping table from the source language to the target language.
Following works improved UMT by combining SMT and NMT in different ways, such
as warming up an NMT model with a trained SMT model (Marie and Fujita, 2018;
Artetxe et al., 2019) and using SMT as posterior regularization (Ren et al.,
2019). Other works involve initializing the model using retrieved semantically
similar sentence pairs (Wu et al., 2019; Ren et al., 2020; Sun et al., 2021a),
using auxiliary parallel data (Li et al., 2020; Garcia et al., 2020) and
pretraining on large-scale multi-lingual data (Lample and Conneau, 2019; Song
et al., 2019; Liu et al., 2020; Zhu et al., 2020).

##  3 Background for Unsupervised Machine Translation

We use the unsupervised machine translation (UMT) framework proposed by Lample
et al. (2017) as the backbone. We briefly go though the model structure in
this section. Let $C_{src}$ and $C_{tgt}$ respectively denote the monolingual
dataset for the source and target language, on which a translation model $M$
is trained to to generate target sequences $y$ based on source sequences $x$,
$y=M(x)$. The model is first initialized by training in a word-by-word
translation manner using a parallel dictionary. The initial parallel
dictionary is thus a word being translated to itself. Next, the model is
iteratively trained based on a denoising auto-encoding (DAE), back-training
(BT) and adversarial learning (AL). DAE allows the model to reconstruct the
translation from a noisy input sentence by dropping and swapping words in the
original sentence. The training objective of DAE is given by:

$\displaystyle\mathcal{L}^{l}_{\text{DAE}}=\mathbb{E}_{x\sim C_{l},\hat{x}\sim
d(e(N(x),l),l)}[\Delta(\hat{x},x)]$ (1)

where $l=src$ or $l=tgt$ specifies the language, $N(x)$ is a noisy version of
$x$, $e$ and $d$ respectively means encoding and decoding, and $\Delta$
measures the difference between the two sequences, which is the cross-entropy
loss in this case. BT encourages the model to reconstruct the input sentence
$x$ from $N(y)$, a corrupted version of the model’s translation $y=M(x)$. The
training objective is given by:

$\displaystyle\mathcal{L}^{l_{1}\to l_{2}}_{\text{BT}}=\mathbb{E}_{x\sim
C_{l_{1}},\hat{x}\sim d(e(N(M(x)),l_{2}),l_{1})}[\Delta(\hat{x},x)]$ (2)

AL uses a discriminator to distinguish the language from the encoded latent
representations, and by doing so, the model is able to better map two
languages into the same latent space. The discriminative training objective is
given by:

$\displaystyle\mathcal{L}^{l}_{\text{Dis}}=-\mathbb{E}_{(x,l)}[\log
p(l|e(x,l))]$ (3)

The encoder is trained to fool the discriminator so that the encoder and the
discriminator perform together in an adversarial style (Goodfellow et al.,
2014):

$\displaystyle\mathcal{L}^{l_{1}\to
l_{2}}_{\text{Adv}}=-\mathbb{E}_{(x_{1},l_{1})}[\log p(l_{2}|e(x_{1},l_{1}))]$
(4)

The final training objective is given by:

$\displaystyle\mathcal{L}=\lambda_{1}[\mathcal{L}^{l_{1}}_{\text{DAE}}+\mathcal{L}^{l_{2}}_{\text{DAE}}]+\lambda_{2}[\mathcal{L}^{l_{1}\to
l_{2}}_{\text{BT}}+\mathcal{L}^{l_{2}\to l_{1}}_{\text{BT}}]$ (5)
$\displaystyle+\lambda_{3}[\mathcal{L}^{l_{1}\to
l_{2}}_{\text{Adv}}+\mathcal{L}^{l_{2}\to l_{1}}_{\text{Adv}}]$

The discriminative loss $\mathcal{L}^{l}_{\text{Dis}}$ is alternatively
optimized with $\mathcal{L}$ to train the discriminator. We follow Lample et
al. (2017) to implement each of the UMT models. We used the transformer-large
Vaswani et al. (2017) as the backbone instead of LSTMs in Bahdanau et al.
(2014).

##  4 Model

The core idea of the proposed the strategy is to use two subdatasets from a
large monolingual corpus $C$ and train unsupervised NMT models based on the
two subdatasets. The path towards this goal naturally constitutes two modules:
(1) constructing two subdatasets $C_{src}$ and $C_{tgt}$ from $C$; and (2)
training the UMT model based on $C_{src}$ and $C_{tgt}$.

###  4.1 Dataset Split

The crucial part in the framework is how to build the two subdatasets, on
which the unsupervised NMT model is trained. To this end, we propose to (1)
first construct candidates $\\{c_{1},c_{2},...,c_{K}\\}$ for $C_{src}$ and
$C_{tgt}$ from $C$ based on the clustering models; and (2) selecting $C_{src}$
and $C_{tgt}$. Based on $C_{src}$ and $C_{tgt}$, UMT models will be trained.
We use two criteria for clustering, LDA (Blei et al., 2003) and K-means
clustering. The number of clusters/topics $K$ is set to 80.111Here we use
“topic” and “cluster” interchangeably.

##### LDA Clustering

For LDA, we use Gibbs sampling and iterate over the entire corpus 5 times in
total. In the last round, a sentence is assigned to the topic/cluster which
has the largest probability of generating it. In LDA, each cluster is
characterized as a distribution over the vocabulary. The distance between two
subset $c_{m}$, $c_{n}$ is the Jensen–Shannon (JS) divergence between the two
distributions over the vocabulary:

$\displaystyle\text{Dis}(c_{m},c_{n})$
$\displaystyle=\text{KL}(c_{m}||c_{n})+\text{KL}(c_{n}||c_{m})$ (6)
$\displaystyle\text{KL}(c_{m}||c_{n})$ $\displaystyle=-\sum_{v\in
V}p(v|c_{m})\log\frac{p(v|c_{m})}{p(v|c_{n})}$
$\displaystyle\text{KL}(c_{n}||c_{m})$ $\displaystyle=-\sum_{v\in
V}p(v|c_{n})\log\frac{p(v|c_{n})}{p(v|c_{m})}$

Since topics clustered by LDA can be incoherent (e.g., the clustering of stop
words), we ask humans to examine the top words of the topics, and discard
meaningless clusters.

##### K-means Clustering

For K-means, we use the average of the top layer embeddings from BERT (Devlin
et al., 2018) to represent the sentence. Let $h_{s}$ denote the sentence
representation for the sentence $s$. We run the hard K-means model on the
corpus, where the distance between a sentence and the cluster center is the
$L_{2}$ distance between the two vector representations.

The LDA and K-means methods described above focus more on the situation that
centers of two clusters are far away, but not individual sentences belonging
to different clusters are different. These two focuses are correlated, but not
exactly the same. The JS divergence for LDA clusters and $L_{2}$ distance for
K-means clusters will be updated after the post-processing stage. LDA and
K-means algorithms are performed on part of the the CommonCrawl corpus
containing 10 billion English tokens.

###  4.2 UMT Training on $C_{src}$ and $C_{tgt}$

####  4.2.1 Multiple UMT Models

We can randomly pick one pair of subsets from $\\{c_{1},...,c_{K}\\}$ as
$C_{src}$ and $C_{tgt}$, on which a single UMT model will be trained. The
problem with single UMT model is obvious: each subset in
$\\{c_{1},c_{2},...,c_{K}\\}$ potentially represents a specific domain. The
UMT model trained on the single $C_{src}$ can thus only be able to properly
paraphrase sentences from the $C_{src}$ domain. To cover the full domain, we
propose to train $K$ UMT models, denoted by $\\{M_{1},M_{2},...,M_{K}\\}$,
where $K$ is the number of clusters. Each of the trained UMT models uses a
different $c\in\\{c_{1},c_{2},...,c_{K}\\}$ as $C_{src}$, paired with a
randomly selected $C_{tgt}$.

Figure 1: An overview of deriving the UMT-Multi model. Step 1: First, for each
cluster $c_{i}$, we treat it as $C_{src}$ and find its corresponding cluster
$C_{tgt}$, and then train a UMT model on ($C_{src}$, $C_{tgt}$). The number of
total UMT models is $K$ (in this figure, $K=4$). Step 2: For a given input
sentence $s$, we first select the $C_{src}$ that $s$ belongs to, and use the
model trained on $C_{src}$ to generate the paraphrase of $s$. This process
goes on over the entire corpus, leading to a pseudo labeled dataset of
paraphrase pairs. Step 3: Human intervenes by removing paraphrase pairs whose
inputs and output are the same, and outputs are two times longer than sources.
Step 4: Training the single UMT-Multi model using the dataset after filtering.
Step 5 (optional): fine-tuning the UMT-Multi model on the supervised
paraphrase dataset in the supervised setup.

To paraphrase sentence $s$, we need to find its corresponding paraphrase
generation model $M\in\\{M_{1},M_{2},...,M_{K}\\}$, which takes $s$ as the
input and outputs its paraphrase. We first select the
$C_{src}\in\\{c_{1},c_{2},...,c_{K}\\}$ that $s$ belongs to. Next, we pick
that model $M$ trained using $C_{src}$ as sources, and use $M$ to generate the
output.

For LDA, $C_{src}$ is the topic that generates $s$ with the largest
probability:

$C_{src}=\operatorname*{arg\,max}_{c\in\\{c_{1},c_{2},...,c_{K}\\}}p(s|c)$ (7)

For the K-means model, $C_{src}$ is the cluster whose center is closest to
$s$:

$C_{src}=\operatorname*{arg\,min}_{c\in\\{c_{1},c_{2},...,c_{K}\\}}||h_{s}-\mu_{c}||^{2}$
(8)

where $\mu_{c}$ denotes the center of the cluster $c$.

We follow Lample et al. (2017) to implement each of the UMT models. We used
the transformer Vaswani et al. (2017) as the backbone instead of LSTMs in
Bahdanau et al. (2014), where the number of encoder blocks, decoder blocks,
the number of heads, $d_{model}$ and $d_{ff}$ are respectively set to 6, 6, 8,
512 and 2,048. For UMT models based on specific $C_{src}$ and $C_{tgt}$, both
the encoder and the decoder are trained using Adam (Kingma and Ba, 2014), with
the learning rate set to 0.00025, $\beta_{1}$ set to 0.5. We evenly alternate
between the encoder-decoder and the discriminator.

##### Unifying $M$s into a Surrogate Model

We need to maintain $K$ different domain-specific UMT models, which is both
memory costly and computationally intensive, especially for online services.
We thus propose to unify different $M$s into a single surrogate one. For each
sentence $s$ in a selected corpus, we first find the cluster $C_{src}$ it
belongs to using LDA or K-means described above, and then we use the model $M$
trained on $C_{src}$ to generate the paraphrase of $s$. In this way, we are
able to collect massive amounts of pseudo-labeled paraphrase pairs by treating
the original sentence $s$ as the source and the produced paraphrase as the
target. We collected a total number of 25 million pairs. Human interventions
can happen in this stage, where we can design filtering functions to remove
pairs with undesired properties. Here, human interventions involve (1)
removing pairs with identical source and target; (2) removing targets two
times longer than sources. 16 million pairs remain after filtering.

We train a Seq2Seq model Sutskever et al. (2014); Vaswani et al. (2017)
(referred to as UMT-Multi) on the remaining pseudo-labeled data, which is used
as the ultimate paraphrase generation model. We use the Transformer-base
(Vaswani et al., 2017) as the model backbone, where the number of encoder
blocks, decoder blocks, the number of heads, $d_{model}$ and $d_{ff}$ are
respectively set to 6, 6, 8, 512 and 2,048. We use Adam (Kingma and Ba, 2014)
with learning rate of 1e-4, $\beta_{1}$ = 0.9, $\beta_{2}$ = 0.999, and a
warmup step of 4K. Batch size is set to 256 pairs. This model can be directly
used in the unsupervised learning setup. An overview of deriving the UMT-Multi
model is shown in Figure 1. Up to now, UMT-Multi is purely based on unlabeled
commoncrawl corpus.

###  4.3 Supervised Setup

For the supervised setup, where we have pairs of paraphrases containing
sources from a source domain and paraphrases of sources from a target domain,
we can fine-tune the pretrained UMT-Multi model on the supervised paraphrase
pairs, where we initialize the model using the UMT-Multi model, and run
additional iterations on the supervised dataset. The fine-tuned model thus
shares the structure with UMT-Multi. Again, we use adam (Kingma and Ba, 2014)
for fine-tuning, with $\beta_{1}=0.9$, $\beta_{2}=0.98$. Batch size, learning
rate and the number of iterations are treated as hyper-parameters, to be tuned
on the dev set. At test time, beam search Sutskever et al. (2014); Li et al.
(2016a) is used for decoding.

An additional use of the gold labeled paraphrase datasets is to help to select
$C_{tgt}\in\\{c_{1},c_{2},...,c_{K}\\}$ that best aligns with $C_{src}$, while
in the unsupervised setup, we can only randomly pair $C_{src}$ and $C_{tgt}$
due to the lack of training signals for pairing. In the most straightforward
setup, for each $C_{src}\in\\{c_{1},c_{2},...,c_{K}\\}$, we can construct
$K-1$ pairs $(C_{src},c)$ by treating all
$c\in\\{c_{1},c_{2},...,c_{K}\\},c\neq C_{src}$ as $C_{tgt}$. Next, we train
$K-1$ UMT models based on the pairs, and select the model that achieves the
highest evaluation score on the labeled dataset. This strategy leads to a
total number of $K\times(K-1)$ models to be trained, which is computationally
prohibitive. We propose a simplified learning model that maps the distance
between $C_{src}$ and $C_{tgt}$ as inputs to output the evaluation score (here
we use iBLEU) on the labeled dataset. Specifically, we randomly select $L$
pairs, where $L\ll K\times(K-1)$. We train $L$ UMT models on the selected
dataset pairs. Using the trained UMT models, we generate paraphrases for the
labeled datasets, and obtain corresponding evaluation scores. Based on the
distance between $C_{src}$ and $C_{tgt}$, and the evaluation score
$S(M_{(src,tgt)})$, we train a simple polynomial function $F$ to learn to map
the distance to the evaluation score:

$S(M_{(src,tgt)})=F(\text{Dis}(C_{src},C_{tgt}))$ (9)

The function $F$ can be then used to select $C_{tgt}$ with highest predicted
evaluation score for $C_{src}$.

##  5 Experiments

###  5.1 Experiment Setups

We consider both the unsupervised and unsupervised setups. There are two
differences between the unsupervised and unsupervised setups: for the
supervised setup, (1) the training data provides guidance on pairing $C_{src}$
and $C_{tgt}$; and (2) the pretrained model will be used as initialization and
later finetuned on the labeled dataset. Datasets that we use for evaluation
include Quora, WikiAnswers (Fader et al., 2013), MSCOCO (Lin et al., 2014) and
Twitter Liu et al. (2019a).

For the supervised setup, we compare our proposed model to the follow
baselines: ResidualLSTM (Prakash et al., 2016b), VAE-SVG-eq (Gupta et al.,
2018), Pointer (See et al., 2017), Transformer (Vaswani et al., 2017), DNPG
(Li et al., 2019). For the unsupervised setup, we use the following models for
comparison: VAE (Bowman et al., 2016), Lag VAE (He et al., 2019), CGMH (Miao
et al., 2019), UPSA (Liu et al., 2019a). Results for VAE, Lag VAE, CGMH and
UPSA on different datasets are copied from Miao et al. (2019) and Liu et al.
(2019a). Results for ResidualLSTM, VAE-SVG-eq, Pointer, Transformer on various
datasets are copied from Li et al. (2019). We leave the details of these
datasets, baselines and training to the supplementary material due to the
space limit.

We are particularly interested in comparing the proposed model with bilingual
MT based models. BT is trained end-to-end on WMT’14
En$\leftrightarrow$Fr.222Wieting et al. (2017); Wieting and Gimpel (2017)
suggested little difference among Czech, German, and French as source
languages for backtranslation. We use En$\leftrightarrow$Fr since it contains
more parallel data than other language pairs.  A paraphrase pair is obtained
by pairing the English sentence in the original dataset and the translation of
the French sentence. Next we train a Transformer-large model on paraphrase
pairs. The model is used as initialization to be further finetuned on the
labeled dataset. We also use WMT-14 En-Zh for reference purposes. We use BLEU
(Papineni et al., 2002), iBLEU (Sun and Zhou, 2012) and ROUGE scores (Lin,
2004) for evaluation.

###  5.2 Results

##### In-domain Results

We first show the in-domain results in Table 5.2. We can observe that across
all datasets and under both the supervised and unsupervised setups, the
proposed UMT model significantly outperforms baselines. As expected, multiple
UMT models performs better than a single UMT model as the former is more
flexible at selecting the correct domain $C_{src}$ for an input sentence. We
can also observe that the BT model is able to achieve competitive results,
which shows that back-translation serves as a strong and simple baseline for
paraphrase generation. The BT model trained on En-Fr consistently outperforms
the one trained on En-Zh, and this is because that En-Zh translation is a
harder task than En-Fr due to the greater difference in grammars between the
two languages.

| Model | iBLEU | BLEU | R1 | R2
---|---|---|---|---|---
Supervised |  Quora
ResidualLSTM | 12.67 | 17.57 | 59.22 | 32.40
VAE-SVG-eq | 15.17 | 20.04 | 59.98 | 33.30
Pointer | 16.79 | 22.65 | 61.96 | 36.07
Transformer | 16.25 | 21.73 | 60.25 | 33.45
DNPG | 18.01 | 25.03 | 63.73 | 37.75
BT(En-Fr) | 18.04 | 25.34 | 63.82 | 37.92
BT(En-Zh) | 17.67 | 24.90 | 63.32 | 37.38
UMT-Single | 17.70 | 24.97 | 63.65 | 37.77
UMT-Multi | 18.78 | 26.49 | 64.12 | 38.31
2-6 |  Wikianswers
| ResidualLSTM | 22.94 | 27.36 | 48.52 | 18.71
| VAE-SVG-eq | 26.35 | 32.98 | 50.93 | 19.11
| Pointer | 31.98 | 39.36 | 57.19 | 25.38
| Transformer | 27.70 | 33.01 | 51.85 | 20.70
| DNPG | 34.15 | 41.64 | 57.32 | 25.88
|  BT(En-Fr) | 34.55 | 41.90 | 57.84 | 26.44
|  BT(En-Zh) | 33.98 | 41.04 | 56.37 | 25.60
| UMT-Single | 34.50 | 41.72 | 57.58 | 26.31
| UMT-Multi | 36.04 | 42.94 | 58.71 | 27.35
Unsupervised |  Quora
VAE | 8.16 | 13.96 | 44.55 | 22.64
Lag VAE | 8.73 | 15.52 | 49.20 | 26.07
CGMH | 9.94 | 15.73 | 48.73 | 26.12
UPSA | 12.03 | 18.21 | 59.51 | 32.63
BT(En-Fr) | 11.98 | 17.84 | 59.03 | 32.11
BT(En-Zh) | 11.33 | 17.02 | 56.19 | 31.08
UMT-Single | 11.47 | 17.21 | 56.35 | 31.27
UMT-Multi | 13.10 | 18.98 | 59.90 | 33.04
2-6 |  Wikianswers
| VAE | 17.92 | 24.13 | 31.87 | 12.08
| Lag VAE | 18.38 | 25.08 | 35.65 | 13.21
| CGMH | 20.05 | 26.45 | 43.31 | 16.53
| UPSA | 24.84 | 32.39 | 54.12 | 21.45
|  BT(En-Fr) | 23.55 | 31.10 | 52.03 | 20.86
|  BT(En-Zh) | 22.60 | 30.12 | 51.29 | 20.11
| UMT-Single | 23.01 | 30.62 | 51.79 | 20.35
| UMT-Multi | 25.90 | 33.80 | 54.52 | 23.48
2-6 |  MSCOCO
| VAE | 7.48 | 11.09 | 31.78 | 8.66
| Lag VAE | 7.69 | 11.63 | 32.20 | 8.71
| CGMH | 7.84 | 11.45 | 32.19 | 8.67
| UPSA | 9.26 | 14.16 | 37.18 | 11.21
|  BT(En-Fr) | 8.15 | 13.78 | 36.30 | 10.48
|  BT(En-Zh) | 7.80 | 11.97 | 32.40 | 9.21
| UMT-Single | 8.21 | 13.99 | 36.52 | 10.75
| UMT-Multi | 9.70 | 15.42 | 38.51 | 12.39
2-6 |  Twitter
| VAE | 2.92 | 3.46 | 15.13 | 3.40
| Lag VAE | 3.15 | 3.74 | 17.20 | 3.79
| CGMH | 4.18 | 5.32 | 19.96 | 5.44
| UPSA | 4.93 | 6.87 | 28.34 | 8.53
|  BT(En-Fr) | 4.32 | 5.97 | 26.37 | 7.59
|  BT(En-Zh) | 4.15 | 5.40 | 25.83 | 7.32
| UMT-Single | 4.40 | 6.11 | 26.89 | 7.78
| UMT-Multi | 5.35 | 7.80 | 29.74 | 9.88

Table 1: In-domain performances of different models for both supervised and
unsupervised setups.

Model | iBLEU | BLEU | R1 | R2
---|---|---|---|---
Wikianswers$\rightarrow$Quora
Pointer | 5.04 | 6.96 | 41.89 | 12.77
Transformer+Copy | 6.17 | 8.15 | 44.89 | 14.79
DNPG | 10.39 | 16.98 | 56.01 | 28.61
BT(En-Fr) | 12.14 | 17.98 | 59.42 | 32.44
BT(En-Zh) | 11.43 | 17.21 | 56.65 | 31.45
UMT-Single | 11.86 | 17.49 | 57.01 | 32.44
UMT-Multi | 13.62 | 19.48 | 61.04 | 33.85
1-5 Quora$\rightarrow$Wikianswers
Pointer | 21.87 | 27.94 | 53.99 | 20.85
Transformer+Copy | 23.25 | 29.22 | 53.33 | 21.02
DNPG | 25.60 | 35.12 | 56.17 | 23.65
BT(En-Fr) | 25.77 | 35.30 | 56.41 | 23.78
BT(En-Zh) | 24.84 | 34.19 | 55.71 | 22.60
UMT-Single | 25.43 | 34.70 | 56.10 | 23.31
UMT-Multi | 26.85 | 36.64 | 57.45 | 24.60

Table 2: Domain-adapted performances of different models. “R1” stands for
ROUGE-1 and “R2” stands for ROUGE-2.

Input |  BT |  UMT
---|---|---
Time is the most accurate test of how puberty is going to progress. |  Time is the most accurate test of how puberty is going to progress. (En-Fr) |  How adolescence develops is most accurately test by time.
GM told truck owners about the defect in the first half of October. |  GM owners told truck about the defect in the first half of October . (En-Fr) |  GM informed truck owners of the defect in the first half of October .
To keep him alive , well , there ’s no reason to keep him alive . |  To keep him alive , well , there ’s no reason to keep him alive . (En-Fr) |  To let him live , well , there ’s no reason to let him live .
Washington did not have the formal education his elder brothers received at Appleby Grammar School in England, but he did learn mathematics, trigonometry, and land surveying . |  Washington did not pursue the same formal education as his older brothers at England’s Appleby Grammar School, but he did study geometry, trigonometry, and land surveying . |  Unlike his older brothers, who studied at England’s Appleby Grammar School, Washington did not receive formal education but studied mathematics, trigonometry, and land surveying .

Table 3: Sampled paraphrases from the BT and UMT models.

##### Domain-adapted Results

We test the model’s domain adaptation ability on Quora and Wikianswers. Table
5.2 shows the results. We can see that UMT-multi performs significantly better
than baselines, including UMT-single, showing the better ability of UMT-multi
for domain adaptation.

###  5.3 Human Evaluation

To further validate the performance of the proposed model, we randomly sample
500 sentences from the Quora test set for human evaluation. The input sentence
and its two paraphrases respectively generated by the UMT model and the BT
model (En-Fr) are assigned to two human annotators at Amazon Mechanical Turk
(AMT), with “¿ 95$\%$ HIT approval rate”. Annotators are asked to judge which
output is better in terms of three aspects: (1) semantics: whether the two
sentences are of the same semantic meaning; (2) diversity: whether the two
sentences are diverse in expressions; and (3) fluency: whether the generated
paraphrase is fluent. Ties are allowed. If the two annotators’ evaluations do
not agree with each other, the job will be assigned to one more annotator, and
we take the majority as the final result.333 If the three annotators all
disagree, we discard the instance. Comparing with BT, the proportions of win,
tie and lose for the proposed UMT-model are respectively $41\%$, $36\%$, and
$22\%$, demonstrating its superiority over BT models.

###  5.4 Examples

Table 3 presents sampled paraphrases from the BT and UMT models. From these
examples, we can identify several intrinsic drawbacks of the BT model that the
UMT model can circumvent: (1) For the first example, the tense from the BT
paraphrase model based on En-Zh translation is incorrect. This is because the
Chinese language expresses tense in a more implicit way. This leads the model
to make mistake in tense when Chinese is translated back to English. The UMT
model does not have this issue; (2) For the second example, the BT model
directly copies the input, this is because the En-Fr can perfectly map the
meaning in two languages with no expression variations. Due to the blackbox
nature of MT models, it is hard to intervene with the process to avoid
producing the same copy. Instead, for the proposed UMT framework, developers
can intervene with the model in both clustering stage and data filtering
stage. (3) For the third example, the BT model changes the meaning of the
original sentence, which is due to the mistake made by the translation model.
These mistakes are sometimes inevitable due to the limitation of current MT
models, but can be fixed in the proposed system.

##  6 Ablation Study

In this section, we perform comprehensive ablation studies on the Wikianswers
dataset to understand behaviors of the proposed model. The iBLEU score is
reported for comparison.

##### Size of $C$ for UMT Training

First, we explore how the size of $C$, the CommonCrawl corpus used for dataset
split and UMT training, affects downstream performances. Table 4 shows the
results, where the size is respectively 10M, 100M, 1B and 10B. We can observe
that with more training data, the performance significantly improves. This is
because the trained model can better learn to align sentences between
different clusters.

Size | 10M | 100M | 1B | 10B
---|---|---|---|---
Unsupervised. UMT-Multi | 15.5 | 21.1 | 24.2 | 25.9

Table 4: The effect of data size of $C$ for training UMT.

##### The Number of LDA Topics

Table 5 presents the influence of the number of LDA clusters. The trend is
clear: more topics lead to better performances. This is because the model with
more topics has a stronger ability of disentangling very similar sentences in
the original corpus $C$, and thus avoids copying. It is worth noting that more
topics means training more UMT models before unifying them, leading to greater
computational intensity.

# LDA Topic | 5 | 20 | 50 | 80
---|---|---|---|---
Unsupervised. UMT-Multi | 14.9 | 22.4 | 24.9 | 25.9

Table 5: The effect of number of LDA topics.

##### Pairing $C_{src}$ and $C_{tgt}$

In our main experiments, we randomly select $C_{tgt}$ given $C_{src}$. It
would be interesting to see the effects of different cluster selection
strategies. We consider four strategies: Largest (select $C_{tgt}$ with the
largest distance to $C_{src}$), Medium (select $C_{tgt}$ with the medium
distance to $C_{src}$), Smallest (select $C_{tgt}$ with the smallest distance
to $C_{src}$) and for referring purposes, Supervised (select $C_{tgt}$ using
the supervised strategy proposed). In the real unsupervised setup, the
supervised strategy cannot be readily applied since we have no access to
supervised labels. We list performance for supervised here for referring
purpose.

Table 6 shows the results. For both supervised and unsupervised setups,
Supervised performs the best against the other strategies, especially under
the unsupervised setup. The difference in performances between these
strategies is greater for the unsupervised setup than the supervised setup.
This is because supervised training serves to compensate the performance gap
due to the presence of labeled training data. We find that the random strategy
outperforms both Largest and Smallest. For Largest , this is because Largest
leads to very different paired clusters, having the risk that some sentences
in $C_{src}$ might not have correspondences in $C_{tgt}$. For Smallest, since
paired clusters are pretty close, sentences in $C_{src}$ are more likely to
have copies in $C_{tgt}$. Largest and Smallest leads to inferior performances.
random performs comparable to medium.

Strategy | Unsuper. UMT-Multi | Super. UMT-Multi
---|---|---
Random | 25.9 | 35.4
Largest | 24.7 | 35.1
Medium | 25.8 | 35.7
Smallest | 25.3 | 35.5
Supervised | 26.3 | 36.0

Table 6: The effect of different strategies to pair $C_{src}$ and $C_{tgt}$.

##### Clustering Methods

We study the effect of different clustering methods, i.e., LDA and K-means.
Table 7 shows the results. As can be seen, for both supervised and
unsupervised setups, the model trained with LDA consistently performs better
than the model trained with K-means. We think there are potentially two
reasons: (1) the BERT representations, on which clustering relies, cannot well
represent sentence semantics for clustering (Reimers and Gurevych, 2019); and
(2) the K-means model for sentence clustering operates at a relatively low
level of semantics (i.e., sentence level), while LDA takes into the more
global document level information. Due to the entanglement of sentence
semantics in $C$, it is hard for K-means to separate sentences apart, or if it
can, it takes long until convergence.

| LDA | K-means
---|---|---
Clustering | Single | Multi | Single | Multi
Uns. | 23.0 | 25.9 | 21.9 | 24.2
Su. | 34.5 | 36.0 | 32.1 | 34.2

Table 7: The effect of different clustering methods for $C$. “Uns.” means we
use the unsupervised setup and “Su.” represents the supervised setup.

##  7 Conclusion

Here, we propose a new framework for paraphrase generation by treating the
task as unsupervised machine translation (UMT). The proposed framework first
splits a large unlabeled corpus into multiple sub-datasets and then trains one
or multiple UMT models based on one or more pairs of these sub-datasets.
Experiments and ablation studies under supervised and unsupervised setups
demonstrate the effectiveness of the proposed framework.

## References

  * Artetxe et al. (2018) Mikel Artetxe, Gorka Labaka, and Eneko Agirre. 2018.  Unsupervised statistical machine translation.  _arXiv preprint arXiv:1809.01272_.
  * Artetxe et al. (2019) Mikel Artetxe, Gorka Labaka, and Eneko Agirre. 2019.  An effective approach to unsupervised machine translation.  _arXiv preprint arXiv:1902.01313_.
  * Artetxe et al. (2017) Mikel Artetxe, Gorka Labaka, Eneko Agirre, and Kyunghyun Cho. 2017.  Unsupervised neural machine translation.  _arXiv preprint arXiv:1710.11041_.
  * Bahdanau et al. (2014) Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. 2014.  Neural machine translation by jointly learning to align and translate.
  * Bannard and Callison-Burch (2005) Colin Bannard and Chris Callison-Burch. 2005.  Paraphrasing with bilingual parallel corpora.  In _Proceedings of the 43rd Annual Meeting of the Association for Computational Linguistics (ACL’05)_ , pages 597–604.
  * Barzilay (2004) Regina Barzilay. 2004.  Information fusion for multidocument summarization: Paraphrasing and generation.
  * Berant and Liang (2014) Jonathan Berant and Percy Liang. 2014.  Semantic parsing via paraphrasing.  In _Proceedings of the 52nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 1415–1425.
  * Blei et al. (2003) David M Blei, Andrew Y Ng, and Michael I Jordan. 2003.  Latent dirichlet allocation.  _the Journal of machine Learning research_ , 3:993–1022.
  * Bowman et al. (2016) Samuel R. Bowman, Luke Vilnis, Oriol Vinyals, Andrew Dai, Rafal Jozefowicz, and Samy Bengio. 2016.  Generating sentences from a continuous space.  In _Proceedings of The 20th SIGNLL Conference on Computational Natural Language Learning_ , pages 10–21, Berlin, Germany. Association for Computational Linguistics.
  * Callison-Burch et al. (2006) Chris Callison-Burch, Philipp Koehn, and Miles Osborne. 2006.  Improved statistical machine translation using paraphrases.  In _Proceedings of the Human Language Technology Conference of the NAACL, Main Conference_ , pages 17–24.
  * Cao et al. (2016) Ziqiang Cao, Chuwei Luo, Wenjie Li, and Sujian Li. 2016.  Joint copying and restricted generation for paraphrase.
  * Chen et al. (2019) Mingda Chen, Qingming Tang, Sam Wiseman, and Kevin Gimpel. 2019.  Controllable paraphrase generation with a syntactic exemplar.  _arXiv preprint arXiv:1906.00565_.
  * Clark et al. (2020) Kevin Clark, Minh-Thang Luong, Quoc V Le, and Christopher D Manning. 2020.  Electra: Pre-training text encoders as discriminators rather than generators.  _arXiv preprint arXiv:2003.10555_.
  * Devlin et al. (2018) Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2018.  Bert: Pre-training of deep bidirectional transformers for language understanding.  _arXiv preprint arXiv:1810.04805_.
  * Dong et al. (2017) Li Dong, Jonathan Mallinson, Siva Reddy, and Mirella Lapata. 2017.  Learning to paraphrase for question answering.  _arXiv preprint arXiv:1708.06022_.
  * Fader et al. (2013) Anthony Fader, Luke Zettlemoyer, and Oren Etzioni. 2013.  Paraphrase-driven learning for open question answering.  In _Proceedings of the 51st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 1608–1618, Sofia, Bulgaria. Association for Computational Linguistics.
  * Fu et al. (2019) Yao Fu, Yansong Feng, and John P Cunningham. 2019.  Paraphrase generation with latent bag of words.  In _Advances in Neural Information Processing Systems_ , pages 13645–13656.
  * Fu et al. (2018) Zhenxin Fu, Xiaoye Tan, Nanyun Peng, Dongyan Zhao, and Rui Yan. 2018.  Style transfer in text: Exploration and evaluation.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 32.
  * Ganitkevitch et al. (2013) Juri Ganitkevitch, Benjamin Van Durme, and Chris Callison-Burch. 2013.  Ppdb: The paraphrase database.  In _Proceedings of the 2013 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies_ , pages 758–764.
  * Garcia et al. (2020) Xavier Garcia, Pierre Foret, Thibault Sellam, and Ankur P Parikh. 2020.  A multilingual view of unsupervised machine translation.  _arXiv preprint arXiv:2002.02955_.
  * Goodfellow et al. (2014) Ian J Goodfellow, Jean Pouget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sherjil Ozair, Aaron Courville, and Yoshua Bengio. 2014.  Generative adversarial networks.  _arXiv preprint arXiv:1406.2661_.
  * Goyal and Durrett (2020) Tanya Goyal and Greg Durrett. 2020.  Neural syntactic preordering for controlled paraphrase generation.  _arXiv preprint arXiv:2005.02013_.
  * Gupta et al. (2018) Ankush Gupta, Arvind Agarwal, Prawaan Singh, and Piyush Rai. 2018.  A deep generative framework for paraphrase generation.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 32.
  * He et al. (2019) Junxian He, Daniel Spokoyny, Graham Neubig, and Taylor Berg-Kirkpatrick. 2019.  Lagging inference networks and posterior collapse in variational autoencoders.  _arXiv preprint arXiv:1901.05534_.
  * Hegde and Patil (2020) Chaitra Hegde and Shrikumar Patil. 2020.  Unsupervised paraphrase generation using pre-trained language models.  _arXiv preprint arXiv:2006.05477_.
  * Holtzman et al. (2020) Ari Holtzman, Jan Buys, M. Forbes, and Yejin Choi. 2020.  The curious case of neural text degeneration.  _ArXiv_ , abs/1904.09751.
  * Hu et al. (2019a) J Edward Hu, Huda Khayrallah, Ryan Culkin, Patrick Xia, Tongfei Chen, Matt Post, and Benjamin Van Durme. 2019a.  Improved lexically constrained decoding for translation and monolingual rewriting.  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 839–850.
  * Hu et al. (2019b) J Edward Hu, Rachel Rudinger, Matt Post, and Benjamin Van Durme. 2019b.  Parabank: Monolingual bitext generation and sentential paraphrasing via lexically-constrained neural machine translation.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 33, pages 6521–6528.
  * Hu et al. (2017) Zhiting Hu, Zichao Yang, Xiaodan Liang, Ruslan Salakhutdinov, and Eric P Xing. 2017\.  Toward controlled generation of text.  In _International Conference on Machine Learning_ , pages 1587–1596. PMLR.
  * Iyyer et al. (2018) Mohit Iyyer, John Wieting, Kevin Gimpel, and Luke Zettlemoyer. 2018.  Adversarial example generation with syntactically controlled paraphrase networks.  _arXiv preprint arXiv:1804.06059_.
  * Kingma and Ba (2014) Diederik P Kingma and Jimmy Ba. 2014.  Adam: A method for stochastic optimization.  _arXiv preprint arXiv:1412.6980_.
  * Kingma and Welling (2013) Diederik P Kingma and Max Welling. 2013.  Auto-encoding variational bayes.  _arXiv preprint arXiv:1312.6114_.
  * Lample and Conneau (2019) Guillaume Lample and Alexis Conneau. 2019.  Cross-lingual language model pretraining.  _arXiv preprint arXiv:1901.07291_.
  * Lample et al. (2017) Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. 2017\.  Unsupervised machine translation using monolingual corpora only.  _arXiv preprint arXiv:1711.00043_.
  * Lample et al. (2018) Guillaume Lample, Myle Ott, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. 2018.  Phrase-based & neural unsupervised machine translation.  _arXiv preprint arXiv:1804.07755_.
  * Lan et al. (2017) Wuwei Lan, Siyu Qiu, Hua He, and Wei Xu. 2017.  A continuously growing dataset of sentential paraphrases.  In _Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing_ , pages 1224–1234, Copenhagen, Denmark. Association for Computational Linguistics.
  * Li et al. (2016a) Jiwei Li, Will Monroe, and Dan Jurafsky. 2016a.  A simple, fast diverse decoding algorithm for neural generation.  _arXiv preprint arXiv:1611.08562_.
  * Li et al. (2016b) Jiwei Li, Will Monroe, Alan Ritter, Michel Galley, Jianfeng Gao, and Dan Jurafsky. 2016b.  Deep reinforcement learning for dialogue generation.  _arXiv preprint arXiv:1606.01541_.
  * Li et al. (2018a) Juncen Li, Robin Jia, He He, and Percy Liang. 2018a.  Delete, retrieve, generate: A simple approach to sentiment and style transfer.  _arXiv preprint arXiv:1804.06437_.
  * Li et al. (2018b) Zichao Li, Xin Jiang, Lifeng Shang, and Hang Li. 2018b.  Paraphrase generation with deep reinforcement learning.  In _Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing_ , pages 3865–3878, Brussels, Belgium. Association for Computational Linguistics.
  * Li et al. (2019) Zichao Li, Xin Jiang, Lifeng Shang, and Qun Liu. 2019.  Decomposable neural paraphrase generation.  In _Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics_ , pages 3403–3414, Florence, Italy. Association for Computational Linguistics.
  * Li et al. (2020) Zuchao Li, Hai Zhao, Rui Wang, Masao Utiyama, and Eiichiro Sumita. 2020.  Reference language based unsupervised neural machine translation.  _arXiv preprint arXiv:2004.02127_.
  * Lin (2004) Chin-Yew Lin. 2004.  ROUGE: A package for automatic evaluation of summaries.  In _Text Summarization Branches Out_ , pages 74–81, Barcelona, Spain. Association for Computational Linguistics.
  * Lin et al. (2014) Tsung-Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick. 2014.  Microsoft coco: Common objects in context.  In _European conference on computer vision_ , pages 740–755. Springer.
  * Liu et al. (2019a) Xianggen Liu, Lili Mou, Fandong Meng, Hao Zhou, Jie Zhou, and Sen Song. 2019a.  Unsupervised paraphrasing by simulated annealing.  _arXiv preprint arXiv:1909.03588_.
  * Liu et al. (2020) Yinhan Liu, Jiatao Gu, Naman Goyal, Xian Li, Sergey Edunov, Marjan Ghazvininejad, Mike Lewis, and Luke Zettlemoyer. 2020.  Multilingual denoising pre-training for neural machine translation.  _arXiv preprint arXiv:2001.08210_.
  * Liu et al. (2019b) Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. 2019b.  Roberta: A robustly optimized bert pretraining approach.  _arXiv preprint arXiv:1907.11692_.
  * Luong et al. (2015) Minh-Thang Luong, Ilya Sutskever, Quoc V. Le, Oriol Vinyals, and Wojciech Zaremba. 2015.  Addressing the rare word problem in neural machine translation.
  * Ma et al. (2018) Shuming Ma, Xu Sun, Wei Li, Sujian Li, Wenjie Li, and Xuancheng Ren. 2018.  Query and output: Generating words by querying distributed word representations for paraphrase generation.  In _Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers)_ , pages 196–206, New Orleans, Louisiana. Association for Computational Linguistics.
  * Mallinson et al. (2017) Jonathan Mallinson, Rico Sennrich, and Mirella Lapata. 2017.  Paraphrasing revisited with neural machine translation.  In _Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers_ , pages 881–893.
  * Marie and Fujita (2018) Benjamin Marie and Atsushi Fujita. 2018.  Unsupervised neural machine translation initialized by unsupervised statistical machine translation.  _arXiv preprint arXiv:1810.12703_.
  * Meng et al. (2021) Yuxian Meng, Xiang Ao, Qing He, Xiaofei Sun, Qinghong Han, Fei Wu, Jiwei Li, et al. 2021.  Conrpg: Paraphrase generation using contexts as regularizer.  _arXiv preprint arXiv:2109.00363_.
  * Miao et al. (2019) Ning Miao, Hao Zhou, Lili Mou, Rui Yan, and Lei Li. 2019.  Cgmh: Constrained sentence generation by metropolis-hastings sampling.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 33, pages 6834–6842.
  * Mueller et al. (2017) Jonas Mueller, David Gifford, and Tommi Jaakkola. 2017.  Sequence to better sequence: continuous revision of combinatorial structures.  In _International Conference on Machine Learning_ , pages 2536–2544. PMLR.
  * Niu et al. (2020) Tong Niu, Semih Yavuz, Yingbo Zhou, Huan Wang, Nitish Shirish Keskar, and Caiming Xiong. 2020.  Unsupervised paraphrase generation via dynamic blocking.  _arXiv preprint arXiv:2010.12885_.
  * Papineni et al. (2002) Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. 2002.  Bleu: a method for automatic evaluation of machine translation.  In _Proceedings of the 40th annual meeting on association for computational linguistics_ , pages 311–318. Association for Computational Linguistics.
  * Prakash et al. (2016a) Aaditya Prakash, Sadid A Hasan, Kathy Lee, Vivek Datla, Ashequl Qadir, Joey Liu, and Oladimeji Farri. 2016a.  Neural paraphrase generation with stacked residual lstm networks.  _arXiv preprint arXiv:1610.03098_.
  * Prakash et al. (2016b) Aaditya Prakash, Sadid A. Hasan, Kathy Lee, Vivek Datla, Ashequl Qadir, Joey Liu, and Oladimeji Farri. 2016b.  Neural paraphrase generation with stacked residual LSTM networks.  In _Proceedings of COLING 2016, the 26th International Conference on Computational Linguistics: Technical Papers_ , pages 2923–2934, Osaka, Japan. The COLING 2016 Organizing Committee.
  * Qian et al. (2019) Lihua Qian, Lin Qiu, Weinan Zhang, Xin Jiang, and Yong Yu. 2019.  Exploring diverse expressions for paraphrase 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 3164–3173.
  * Radford et al. (2018) Alec Radford, Karthik Narasimhan, Tim Salimans, and Ilya Sutskever. 2018.  Improving language understanding by generative pre-training.
  * Ranzato et al. (2015) Marc’Aurelio Ranzato, Sumit Chopra, Michael Auli, and Wojciech Zaremba. 2015.  Sequence level training with recurrent neural networks.  _arXiv preprint arXiv:1511.06732_.
  * Ravi and Knight (2011) Sujith Ravi and Kevin Knight. 2011.  Deciphering foreign language.  In _Proceedings of the 49th Annual Meeting of the Association for Computational Linguistics: Human Language Technologies_ , pages 12–21, Portland, Oregon, USA. Association for Computational Linguistics.
  * Reimers and Gurevych (2019) Nils Reimers and Iryna Gurevych. 2019.  Sentence-bert: Sentence embeddings using siamese bert-networks.  _arXiv preprint arXiv:1908.10084_.
  * Ren et al. (2020) Shuo Ren, Yu Wu, Shujie Liu, Ming Zhou, and Shuai Ma. 2020.  A retrieve-and-rewrite initialization method for unsupervised machine translation.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 3498–3504, Online. Association for Computational Linguistics.
  * Ren et al. (2019) Shuo Ren, Zhirui Zhang, Shujie Liu, Ming Zhou, and Shuai Ma. 2019.  Unsupervised neural machine translation with smt as posterior regularization.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 33, pages 241–248.
  * Rios Gonzales et al. (2017) Annette Rios Gonzales, Laura Mascarell, and Rico Sennrich. 2017.  Improving word sense disambiguation in neural machine translation with sense embeddings.  In _Proceedings of the Second Conference on Machine Translation_ , pages 11–19, Copenhagen, Denmark. Association for Computational Linguistics.
  * Roy and Grangier (2019) Aurko Roy and David Grangier. 2019.  Unsupervised paraphrasing without translation.  _arXiv preprint arXiv:1905.12752_.
  * See et al. (2017) Abigail See, Peter J. Liu, and Christopher D. Manning. 2017.  Get to the point: Summarization with pointer-generator networks.  In _Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 1073–1083, Vancouver, Canada. Association for Computational Linguistics.
  * Sennrich et al. (2016) Rico Sennrich, Barry Haddow, and Alexandra Birch. 2016.  Improving neural machine translation models with monolingual data.  In _Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 86–96, Berlin, Germany. Association for Computational Linguistics.
  * Shen et al. (2017) Tianxiao Shen, Tao Lei, Regina Barzilay, and Tommi Jaakkola. 2017.  Style transfer from non-parallel text by cross-alignment.
  * Siddique et al. (2020) A. B. Siddique, Samet Oymak, and Vagelis Hristidis. 2020.  Unsupervised paraphrasing via deep reinforcement learning.  _Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining_.
  * Sokolov and Filimonov (2020) Alex Sokolov and Denis Filimonov. 2020.  Neural machine translation for paraphrase generation.  _arXiv preprint arXiv:2006.14223_.
  * Song et al. (2019) Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu. 2019.  Mass: Masked sequence to sequence pre-training for language generation.  _arXiv preprint arXiv:1905.02450_.
  * Sun and Zhou (2012) Hong Sun and Ming Zhou. 2012.  Joint learning of a dual smt system for paraphrase generation.  In _Proceedings of the 50th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers)_ , pages 38–42.
  * Sun et al. (2021a) Xiaofei Sun, Yuxian Meng, Xiang Ao, Fei Wu, Tianwei Zhang, Jiwei Li, and Chun Fan. 2021a.  Sentence similarity based on contexts.  _arXiv preprint arXiv:2105.07623_.
  * Sun et al. (2021b) Zijun Sun, Xiaoya Li, Xiaofei Sun, Yuxian Meng, Xiang Ao, Qing He, Fei Wu, and Jiwei Li. 2021b.  Chinesebert: Chinese pretraining enhanced by glyph and pinyin information.  _arXiv preprint arXiv:2106.16038_.
  * Sutskever et al. (2014) Ilya Sutskever, Oriol Vinyals, and Quoc V Le. 2014.  Sequence to sequence learning with neural networks.  In _Advances in neural information processing systems_ , pages 3104–3112.
  * 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.  In _Advances in neural information processing systems_ , pages 5998–6008.
  * Wang et al. (2018) Su Wang, Rahul Gupta, Nancy Chang, and Jason Baldridge. 2018.  A task in a suit and a tie: paraphrase generation with semantic augmentation.
  * Wieting and Gimpel (2017) John Wieting and Kevin Gimpel. 2017.  Paranmt-50m: Pushing the limits of paraphrastic sentence embeddings with millions of machine translations.  _arXiv preprint arXiv:1711.05732_.
  * Wieting et al. (2017) John Wieting, Jonathan Mallinson, and Kevin Gimpel. 2017.  Learning paraphrastic sentence embeddings from back-translated bitext.  _arXiv preprint arXiv:1706.01847_.
  * Witteveen and Andrews (2019) Sam Witteveen and Martin Andrews. 2019.  Paraphrasing with large language models.  _arXiv preprint arXiv:1911.09661_.
  * Wu et al. (2019) Jiawei Wu, Xin Wang, and William Yang Wang. 2019.  Extract and edit: An alternative to back-translation for unsupervised neural machine translation.  _arXiv preprint arXiv:1904.02331_.
  * Xu et al. (2018) Qiongkai Xu, Juyan Zhang, Lizhen Qu, Lexing Xie, and Richard Nock. 2018.  D-page: Diverse paraphrase generation.  _arXiv preprint arXiv:1808.04364_.
  * Yang et al. (2019) Qian Yang, Dinghan Shen, Yong Cheng, Wenlin Wang, Guoyin Wang, Lawrence Carin, et al. 2019.  An end-to-end generative architecture for paraphrase 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 3123–3133.
  * Yang et al. (2018) Zhen Yang, Wei Chen, Feng Wang, and Bo Xu. 2018.  Unsupervised neural machine translation with weight sharing.  In _Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 46–55, Melbourne, Australia. Association for Computational Linguistics.
  * Zhu et al. (2020) Jinhua Zhu, Yingce Xia, Lijun Wu, Di He, Tao Qin, Wengang Zhou, Houqiang Li, and Tie-Yan Liu. 2020.  Incorporating bert into neural machine translation.  _arXiv preprint arXiv:2002.06823_.

##  Appendix A Datasets

(1) Quora444https://www.kaggle.com/c/quora-question-pairs: The Quora dataset
contains 140K parallel paraphrases of questions and 260K non-parallel
sentences collected from the question answering website
Quora555https://www.quora.com/. We follow the standard setup in Miao et al.
(2019) and use 3K/30K paraphrase pairs respectively for validation and test.

(2) Wikianswers: The WikiAnswers corpus (Fader et al., 2013) contains clusters
of questions tagged by WikiAnswers users as paraphrases. It contains a total
number of 2.3M paraphrase pairs. We follow Liu et al. (2019a) to randomly pick
5K pairs for validation and 20K for test.666Note that the selected data is
different from Liu et al. (2019a) but is comparable in the statistical sense.
(3) MSCOCO: The MSCOCO dataset (Lin et al., 2014) contains over 500K
paraphrase pairs for 120K image captions, with each image caption annotated by
five annotators. We follow the dataset split and the evaluation protocol in
Prakash et al. (2016b), where only image captions with fewer than 15 words are
considered. (4) Twitter: The Twitter dataset is collected via linked tweets
through shared URLs (Lan et al., 2017), which originally contains 50K
paraphrase pairs. We follow the data split in Liu et al. (2019a), where 10% of
the training data is used as validation and the test set only contains
sentence pairs that are labeled as “paraphrases”.

##  Appendix B Baselines

For the supervised setup, we compare our proposed model to the follow
baselines:

(1) ResidualLSTM: Prakash et al. (2016b) deepened the LSTM network by stacking
multiple layers with residual connection. This deep Seq2Seq model is trained
on labeled paraphrase datasets. (2) VAE-SVG-eq: Gupta et al. (2018) combined
VAEs with LSTMs to generate paraphrases in a Seq2Seq generative style. (3)
Pointer: See et al. (2017) augmented the standard Seq2Seq model by using a
pointer, i.e., the copy mechanism. Word in the input sentence can be directly
copied as the current decoded word. (4) Transformer: Vaswani et al. (2017)
proposed the Transformer architecture which is based on the self-attention
mechanism. (5) DNPG: Li et al. (2019) proposed a Transformer-based model that
learns and generates paraphrases at different levels of granularity, i.e.,
from the lexical to phrasal and then to sentential levels.

For the unsupervised setup, we use the following models for comparison:

(1) VAE: Bowman et al. (2016) proposed variational auto-encoders (VAEs) to
generate sentences from a continuous space. By minimizing the reconstruction
loss between the input sentence and the output sentence, VAEs are able to
sample paraphrases from the continuous space. (2) Lag VAE: To overcome the
posterior collapse issue of VAEs, He et al. (2019) proposed to aggressively
optimize the inference network by performing multiple updates before reverting
back to basic VAE training. (3) CGMH: Miao et al. (2019) used
Metropolis–Hastings sampling to generate paraphrases, where a word can be
deleted, replaced or inserted into the current sentence based on the sampling
distribution. (4) UPSA: Liu et al. (2019a) proposed to use simulated annealing
to optimize the paraphrase generation model. The training objective is
composed of three parts: semantic similarity, expression diversity and
language fluency.


# Incompleteness Ex Machina

Sebastian Oberhoff
<EMAIL_ADDRESS>
###### Abstract

In this essay we’ll prove Gödel’s incompleteness theorems twice. First, we’ll
prove them the good old-fashioned way. Then we’ll repeat the feat in the
setting of computation. In the process we’ll discover that Gödel’s work,
rightly viewed, needs to be split into two parts: the transport of computation
into the arena of arithmetic on the one hand and the actual incompleteness
theorems on the other. After we’re done there will be cake.

> It is a profoundly erroneous truism, repeated by all copy-books and by
> eminent people when they are making speeches, that we should cultivate the
> habit of thinking of what we are doing. The precise opposite is the case.
> Civilization advances by extending the number of important operations which
> we can perform without thinking about them. Operations of thought are like
> cavalry charges in a battle—they are strictly limited in number, they
> require fresh horses, and must only be made at decisive moments.
>
> Alfred North Whitehead

All possible stringsAxiomsProvableTrue but undecidable$G$DisprovableFalse but
undecidable$\neg G$

##  1 The Incompleteness Theorems On Fast-Forward

Kurt Gödel’s incompleteness theorems are clearly the most significant results
in the history of mathematics (fight me). The first establishes that no single
“proper” formal system can fully settle all mathematical questions; that truth
and provability are distinct concepts.111Note to the veteran reader: this
entire presentation is focused on the standard interpretation of arithmetic.
No funky transfinite numbers. The second shows that such a formal system also
can’t prove itself free of contradiction. If it tries, its wings will melt and
it will crash to the ground.

Gödel accomplished these triumphs as follows. Suppose we’re given a formal
system222For the purpose of this discussion every formal system is effectively
axiomatized by definition. This basically just boils down to the fact that
proofs are computer checkable. $\mathcal{F}$ that is capable of reasoning
about elementary arithmetic. Then, as Gödel showed through a lot of toil [1],
it is possible to construct a sentence $G$ which essentially says “I am not
provable in $\mathcal{F}$”. Once he had built this sentence he then simply
asked: can $G$ be proven or disproven—that is decided—in $\mathcal{F}$?

Suppose $G$ is provable:

Either $\neg G$ is also provable:

  *   * $\Rightarrow$

Both $G$ and $\neg G$ are provable in $\mathcal{F}$. Any system in which such
a situation arises is also called inconsistent.

Or $\neg G$ isn’t provable:

  *   * $\Rightarrow$

Since $G$ is provable there exists some concrete proof of $G$ which we can
write out inside $\mathcal{F}$. This is done using a device called Gödel
numbering which allows numbers to talk about proofs. It’s complicated.

  * $\Rightarrow$

Because this proof leads to $G$ this allows us to construct a new proof of
<<$G$ is provable>> = $\neg G$.333Whereas regular quotes (“ ”) perform their
usual function, guillemets (¡¡ ¿¿) surround formal sentences denoted by their
English description. Also “=” doesn’t always have to mean exact equality. I
also use it to relate sentences which are merely logically equivalent,
provided this is obvious. But we’re assuming $\neg G$ isn’t provable. We have
arrived at a genuine contradiction, not just an inconsistency. So this can’t
happen. We’ll use the shorthand “↯” for this in the future.

Suppose $\neg G$ is provable:

This is what it means to disprove $G$. But beware: $\neg G$ isn’t a self-
referential sentence. In particular, it’s not equal to <<$\neg G$ isn’t
provable>>. Instead, it’s <<$G$ is provable>>. These are very different
sentences. $\neg G$ is really more like an evil twin that’s telling lies about
its sibling (assuming the system $\mathcal{F}$ as a whole is honest).
Furthermore, mind the fact that this case and the previous aren’t logical
opposites. That’s where I use either/or.

Either $G$ is also provable:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent.

Or $G$ isn’t provable:

  *   * $\Rightarrow$

Since $\neg G$ is provable there exists some concrete proof of $\neg G$ which
we can write out inside $\mathcal{F}$.

  * $\Rightarrow$

But in order to force a contradiction we’ll have to find a proof of $G$ =
<<$G$ isn’t provable>>, not <<$\neg G$ is provable>> (uh-oh).

  * $\Rightarrow$

We can’t find a proof of $G$ despite the fact that its existence is exactly
what $\neg G$ = <<$G$ is provable>> asserts.

  * $\Rightarrow$

We haven’t convicted $\mathcal{F}$ of an outright inconsistency. But something
is still very, very wrong with it.

These deductions, as well as the ones in the proofs to follow, are
deliberately written in such a painstaking style in order to make the
similarities between the first and second set of proofs as plain as possible.
These are the decisive moments of our battle.

Now, it would be nice to say that we’ve proven that, if our formal system
$\mathcal{F}$ is consistent, then $G$ is undecidable. Unfortunately our second
case wasn’t strong enough. So, just as Gödel did in 1931, we’ll have to settle
for a weaker formulation:

[First Incompleteness Theorem—Original Version] Let $\mathcal{F}$ be an
honest444The traditional term is “sound”. But when explaining this concept to
my mother I had to admit that “honesty” is much more fitting. Also, I’ve been
burned by overloaded usage of the term “soundness” in the past. formal system
capable of reasoning about elementary arithmetic. Then $\mathcal{F}$ is
incomplete; it contains a sentence that can neither be proven nor disproven in
$\mathcal{F}$.

###### Proof.

We just did that. ∎

Okay, I pulled a fast one there. Crucially, I skipped over a rather important
concept: honesty. What exactly do I mean by that?

As the name suggests, an honest formal system is a formal system that speaks
the truth. We can believe the claims it makes. In particular, if our
$\mathcal{F}$ is honest and proves $\neg G$ = <<$G$ is provable>>, then, just
as $\neg G$ says, it really is the case that $G$ is provable. This is how we
can force a contradiction out of the second case.

But honesty is a stronger assumption than consistency. An honest formal system
is always consistent. After all, an inconsistent formal system contains a
sentence $S$ such that both $S$ and $\neg S$ is provable. One of these must be
a lie. However, a consistent formal system isn’t necessarily honest. Here’s a
completely hypothetical example to illustrate:

Imagine I’m the leader of an idyllic communist utopia. Everything is going
according to current five-year plan. Except one day a nuclear reactor of mine
suddenly catches fire. If I then go on to tell the world community that
there’s nothing to worry about, this will merely be a lie, not a
contradiction. Even once Swedish scientists begin smelling the fire my
excuses, while fabricated, can still retain their internal consistency. It’s
only when I finally confess to my mishap that I contradict myself. At that
point I have given two directly contradictory accounts. Now even those without
a Geiger counter can tell that I’ve been dishonest.

Disorienting as it may be, this dishonest-yet-consistent state can also occur
in formal systems. Most important for our purposes, it is conceivable that
$\mathcal{F}$ can prove $\neg G=$ <<$G$ is provable>> while $G$ in fact isn’t
provable. This would lead to a curious situation I’ll call sub-
inconsistency555Also known under the name “$\omega$-inconsistency”. Let’s
spare our horses. where for all $n\in\mathbb{N}$ the sentence

<<$G$ doesn’t have a proof shorter than $n$>>

can be proven in $\mathcal{F}$ by just going through all possible proofs up to
length $n$ and pointing out that none of them do the trick. Yet the sentence
with the “for all” on the inside,

<<$G$ doesn’t have a proof shorter than $n$ for all $n\in\mathbb{N}$>> = $G$,

is not only unprovable but flat out contradicted by $\neg G$. This is why
Gödel had to assume honesty (or at least super-consistency) in his original
proof. Basically, he had to press $\mathcal{F}$ up against the wall and shout:
“No games, dammit!”

Okay, but isn’t there a less violent way to prevent this kind of sub-terfuge?
Indeed there is. In 1936 J. Barkley Rosser found a way [2] to demonstrate the
improved

[First Incompleteness Theorem—Rosser’s Version] Let $\mathcal{F}$ be a
consistent formal system capable of reasoning about elementary arithmetic.
Then $\mathcal{F}$ is incomplete.

###### Proof.

In hindsight Rosser’s trick is quite simple. Instead of formalizing “I am not
provable” he formalized the sentence “For every proof of me there exists a
shorter disproof”. Let’s refer to this sentence as $R$ and see how $R$ can
help us.

Suppose $R$ is provable:

$\Rightarrow$ There exists some shortest proof $p$ of $R$.

Either there is a proof of $\neg R$ that’s shorter than $p$:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯666Inconsistencies can be promoted to genuine
contradictions if they collide with the assumption of consistency.

Or there isn’t:

  *   * $\Rightarrow$

We can go through all strings shorter than $p$ and determine that none of them
are a proof of $\neg R$.

  * $\Rightarrow$

We can write out this list inside $\mathcal{F}$ and point out that all longer
strings are at least as long as $p$.

  * $\Rightarrow$

This allows us to construct a new (longer) proof of <<There exists a proof of
$R$ with no shorter disproof (namely $p$)>> = $\neg R$.

  * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Suppose $\neg R$ is provable:

$\Rightarrow$ There exists some shortest proof $p$ of $\neg R$.

Either there is a proof of $R$ that’s shorter than $p$:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Or there isn’t:

  *   * $\Rightarrow$

We can go through all strings shorter than $p$ and determine that none of them
are a proof of $R$.

  * $\Rightarrow$

We can write out this list inside $\mathcal{F}$ and point out that all longer
strings are at least as long as $p$.

  * $\Rightarrow$

This allows us to construct a new (longer) proof of <<For every proof of $R$
there exists a shorter disproof (namely $p$)>> = $R$.

  * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯∎

Whereas Gödel’s original proof was limping on one leg, Rosser’s version is
perfectly balanced, as all things should be, yielding the stronger result.

Finally, there’s one more summit to conquer in this mathematical Himalaya.
That’s the Second Incompleteness Theorem.

[Second Incompleteness Theorem] Again, let $\mathcal{F}$ be a consistent
formal system capable of reasoning about elementary arithmetic. Then
$\mathcal{F}$ can’t prove its own consistency.

Perhaps the fact that this theorem speaks of consistency, not honesty, makes
you a little suspicious. Is this another one of Rosser’s upgrades? No. For the
Second Incompleteness Theorem Gödel only needed half of his First
Incompleteness Theorem. And, as luck would have it, this was exactly the half
that spoke of consistency.

###### Proof.

Let’s assume for the purpose of contradiction that $\mathcal{F}$ can prove its
own consistency

  * $\Rightarrow$

The first half of the proof for the First Incompleteness Theorem can be read
as a proof by contradiction that if $\mathcal{F}$ is consistent, then $G$
isn’t provable.

  * $\Rightarrow$

Using the fact that <<$G$ isn’t provable>> = $G$ this can be stated more
concisely as “$\mathcal{F}$ is consistent $\implies G$”.

  * $\Rightarrow$

As Gödel himself pointed out with some hand-waving, there wasn’t actually
anything in the reasoning we used to prove this that we couldn’t carry out
just as well in $\mathcal{F}$. So <<$\mathcal{F}$ is consistent $\implies G$>>
is actually a theorem in $\mathcal{F}$.

  * $\Rightarrow$

We’re assuming that $\mathcal{F}$ can prove <<$\mathcal{F}$ is consistent>>.
So by modus ponens777Modus ponens is the inference rule that from $A$ and
¡¡$A\implies B$¿¿ follows $B$. $\mathcal{F}$ can also prove $G$.

  * $\Rightarrow$

But $G$ can’t be proven. ↯∎

Moral of the story: if you declare yourself a very stable genius, you’re not
[3].

##  2 The Rise Of The Machines

We now come to the dramatic turn in our story. Namely, we’re about to demand
that our formal system $\mathcal{F}$ can reason about algorithms, not just
elementary arithmetic. And then we’ll reprove all three of the previous
results on top of that.

What could possibly provoke such heresy? Well, you may recall that in the
prequel we relied quite heavily on the fact that both $G$ and $R$ could
somehow be constructed in $\mathcal{F}$. But we never actually performed these
constructions. We also liberally made assertions of the form: “we can list out
all proofs up to length $n$ inside $\mathcal{F}$”. But $\mathcal{F}$ is about
numbers, not formal sentences. How is all of this ultimately accomplished?

The reality is that I hand-waved these details for a reason. They are non-
trivial in the extreme (ideal exercises for the reader!). That’s because, from
a modern perspective, Gödel basically had to teach programming to formal
systems that were about arithmetic. And he had to do it half a decade before
the first models of computation were even devised. This is where all the tough
technical work had to be done. The incompleteness theorems themselves were
mere victory laps at the end.

This delimitation between the different parts of Gödel’s work is frequently
passed over without comment but will become even more apparent as we move on.
In fact, setting the record straight on this matter is really the main point
of this essay. By placing computation—for example in the form of Turing
machines—directly into the bedrock of our formal system our task will become
orders of magnitude simpler. Gödel had to scale a vertical cliff to convince
his peers that “$p$ is a proof of $S$” could be expressed within the confines
of arithmetic. We, on the other hand, aided by the ski lift built by Turing
and his apostles, can see at a glance that the same could be checked by a
computer. Let’s exploit that.

Anybody who still harbors a nostalgic longing for “elementary arithmetic” can
then take on the separate task of showing how to ponder computation in the
realm of the natural numbers. Perhaps one can also study computation starting
from a different base camp such as knot theory. Who knows? (I’m completely
clueless regarding knot theory.) Meanwhile, we will have the incompleteness
theorems above the clouds all to ourselves.

##  3 To Halt Or Not To Halt

Alright, here we go. The only ingredient we need to prepare is the
unsolvability of the Halting Problem due to Alan Turing in 1936 [4].

[Unsolvability Of The Halting Problem] There’s no algorithm that implements
the function

$A\mapsto\begin{cases}\text{accept}&\text{if $A(A)$ halts}\\\
\text{reject}&\text{if $A(A)$ doesn't halt.}\end{cases}$

(“$A(A)$” denotes an algorithm $A$ running on its own source code.)

###### Proof.

Suppose $H$ solves the Halting Problem. Then one could create the following
algorithm:

$\overline{H}(A)$

if $H(A)$ rejects

halt

if $H(A)$ accepts

loop

“halt” just… halts. We don’t even need to bother accepting or rejecting. It
doesn’t matter. And “loop” is a simple infinite loop without exits. Now,
question: does $\overline{H}(\overline{H})$ halt?
Either $\overline{H}(\overline{H})$ halts: $\Rightarrow$ $H(\overline{H})$
accepts. $\Rightarrow$ $\overline{H}(\overline{H})$ doesn’t halt. ↯ Or
$\overline{H}(\overline{H})$ doesn’t halt: $\Rightarrow$ $H(\overline{H})$
rejects. $\Rightarrow$ $\overline{H}(\overline{H})$ halts. ↯
Either way we get a contradiction. ∎

Easy peasy. As you’d expect of a mere lemma. We’re now ready for the First
Incompleteness Theorem.

[First Incompleteness Theorem—Original Version By Computation] Let
$\mathcal{F}$ be an honest Turing complete formal system. Then $\mathcal{F}$
is incomplete.

For a formal system to be Turing complete simply means that it can reason
about algorithms. And our arguments won’t be overly technical anyway. So let
me just leave it there.

###### Proof.

Suppose $\mathcal{F}$ was complete. Then we could solve the Halting Problem
using the following algorithm:

$H(A)$

for $x\in$ all possible strings888In case it wasn’t clear: we’re iterating in
lexicographical order. This procedure is sometimes also jokingly referred to
as the British Museum algorithm because it’s akin to using chimps in front of
typewriters in an attempt to reproduce all the books in the British Museum.

if $x$ proves <<$A(A)$ doesn’t halt>>

reject

if $x$ proves <<$A(A)$ halts>>

accept

Because $\mathcal{F}$ is complete this search will eventually hit upon a proof
of either <<$A(A)$ halts>> or <<$A(A)$ doesn’t halt>>. And because
$\mathcal{F}$ is honest we’ll be able to trust its judgment. That determines
whether or not $A(A)$ halts. But, as we saw only a moment ago, it’s impossible
to solve the Halting Problem. So $\mathcal{F}$ couldn’t have been complete. ↯∎

That certainly went by a lot faster than my last reading of Gödel, Escher,
Bach [5]. Though, if you’ve ever had the incompleteness theorems explained to
you by a computer scientist, then you probably saw this proof coming a mile
away. And for good reason. It’s a very elegant little proof; deserving of its
popularity.

##  4 Welcome To The World Of Mirrors

Nevertheless, this isn’t the proof I want to use going forward. The reasons
are threefold:

  * $\bullet$

The jump from honesty to consistency is rather tricky.

  * $\bullet$

The Second Incompleteness Theorem doesn’t follow naturally at all.

  * $\bullet$

The parallels to Gödel’s and Rosser’s original proofs are lost. (This one’s
the biggie.)

We can do better. Watch this:

###### Second Proof Of Theorem 3.

Consider the following algorithm:

$P(A)$

for $x\in$ all possible strings

if $x$ proves <<$A(A)$ doesn’t halt>>

halt

I now claim that <<$P(P)$ doesn’t halt>> is undecidable in $\mathcal{F}$.
Let’s call this sentence $\accentset{\scalebox{0.35}{$\infty$}}{G}$ because
it’s the perfect analogue of Gödel’s $G$. The critical new feature of
$\accentset{\scalebox{0.35}{$\infty$}}{G}$ is that its construction has become
just a small matter of programming. If we go through the alternatives, we
find:

Suppose $\accentset{\scalebox{0.35}{$\infty$}}{G}$ is provable:

Either $\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ is also provable:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Or $\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ isn’t provable:

  *   * $\Rightarrow$

Since $\accentset{\scalebox{0.35}{$\infty$}}{G}$ is provable $P(P)$ will
eventually find such a proof after some sequence of steps which we can write
out inside $\mathcal{F}$.

  * $\Rightarrow$

Because this sequence leads to a terminal state this allows us to construct a
new proof of <<$P(P)$ halts>> =
$\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$. ↯

Suppose $\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ is provable:

Either $\accentset{\scalebox{0.35}{$\infty$}}{G}$ is also provable:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Or $\accentset{\scalebox{0.35}{$\infty$}}{G}$ isn’t provable:

  *   * $\Rightarrow$

Since $\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ is provable $P(P)$ will
eventually find such a proof after some sequence of steps which we can write
out inside $\mathcal{F}$.

  * $\Rightarrow$

But in order to halt $P(P)$ will have to find a proof of
$\accentset{\scalebox{0.35}{$\infty$}}{G}$ = <<$P(P)$ doesn’t halt>>, not
$\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ (uh-oh).

  * $\Rightarrow$

$P(P)$ doesn’t halt despite the fact that this is exactly what
$\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ = <<$P(P)$ halts>> asserts.

  * $\Rightarrow$

$\mathcal{F}$ is dishonest. ↯∎

Is anybody else experiencing déjà vu? Note that, whereas in the previous proof
we only established the existence of undecidable sentences in $\mathcal{F}$,
here we actually have a concrete undecidable sentence on our hands. And we
didn’t even need the Halting Problem!

Moreover, almost miraculously, the two cases for
$\accentset{\scalebox{0.35}{$\infty$}}{G}$’s provability run into the exact
same problems as $G$. In the first case $\mathcal{F}$ plants its
$\mathcal{F}$ace squarely in inconsistency. In the second one the precise
correlation between the information $\mathcal{F}$ communicated and the facts
insofar as they can be determined and demonstrated is such as to cause
epistemological problems of sufficient magnitude as to lay upon the logical
and semantic resources of the English language a heavier burden than they can
reasonably be expected to bear. It told a lie [6].

Upon closer inspection we notice that we’re even dealing with the same kind of
lie:

$\mathord{\mathchoice{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}}$
sub-inconsistency $\mathord{\mathchoice{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}}$

After all, if $\accentset{\scalebox{0.35}{$\infty$}}{G}$ isn’t provable, then
one can still prove that $P(P)$ hasn’t halted after $n$ steps for all
$n\in\mathbb{N}$ by just writing out $n$ steps of the computation in
$\mathcal{F}$ and noting that it’s still running. But the summarizing sentence
<<$P(P)$ hasn’t halted after $n$ steps for all $n\in\mathbb{N}$>> =
$\accentset{\scalebox{0.35}{$\infty$}}{G}$ is mysteriously unprovable. If
$\mathcal{F}$ then goes on to prove
$\neg\accentset{\scalebox{0.35}{$\infty$}}{G}$ = <<$P(P)$ halts>>, this will
be a false promise. Yet we’re unable to catch it red-handed.

And if you thought that was neat, just wait until you see Rosser’s trick. As
you may recall, this one worked by patching the asymmetry between the two
cases in Gödel’s original argument. Let’s see what happens if we try the same
here.

[First Incompleteness Theorem—Rosser’s Version By Computation] Let
$\mathcal{F}$ be a consistent Turing complete formal system. Then
$\mathcal{F}$ is incomplete.

###### Proof.

Consider the following algorithm:

$B(A)$999I picked the names $P$ and $B$ because there’s a slight visual
resemblance between the letters and the programs they denote. (Also this is
why I placed the “doesn’t halt” case first.)

for $x\in$ all possible strings

if $x$ proves <<$A(A)$ doesn’t halt>>

halt

if $x$ proves <<$A(A)$ halts>>

loop

In a sense we’ve seen this algorithm before. Just take $H$ as it’s defined in
the first proof of Theorem 3, substitute it into $\overline{H}$, and simplify.
It’s $\mathcal{F}$’s most valiant attempt to implement $\overline{H}$. This
time our undecidable sentence is (you guessed it)
$\accentset{\scalebox{0.35}{$\infty$}}{R}$ = <<$B(B)$ doesn’t halt>>.

Suppose $\accentset{\scalebox{0.35}{$\infty$}}{R}$ is provable:

$\Rightarrow$ There exists some shortest proof $p$ of
$\accentset{\scalebox{0.35}{$\infty$}}{R}$.

Either there is a proof of $\neg\accentset{\scalebox{0.35}{$\infty$}}{R}$
that’s shorter than $p$:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯101010I might add that in this case $B(B)$
never reaches $p$ but finds the shorter proof first. We could dwell on this.
But we already have an inconsistency which is all we need.

Or there isn’t:

  *   * $\Rightarrow$

$B(B)$ will go through all strings shorter than $p$ and determine that none of
them are a proof of $\neg\accentset{\scalebox{0.35}{$\infty$}}{R}$.

  * $\Rightarrow$

We can write out this computation inside $\mathcal{F}$ and point out that
$B(B)$ will then find $p$ and enter a terminal state.

  * $\Rightarrow$

This allows us to construct a new (longer) proof of <<$B(B)$ halts>> =
$\neg\accentset{\scalebox{0.35}{$\infty$}}{R}$.

  * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Suppose $\neg\accentset{\scalebox{0.35}{$\infty$}}{R}$ is provable:

$\Rightarrow$ There exists some shortest proof $p$ of
$\neg\accentset{\scalebox{0.35}{$\infty$}}{R}$.

Either there is a proof of $\accentset{\scalebox{0.35}{$\infty$}}{R}$ that’s
shorter than $p$:

  *   * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯

Or there isn’t:

  *   * $\Rightarrow$

$B(B)$ will go through all strings shorter than $p$ and determine that none of
them are a proof of $\accentset{\scalebox{0.35}{$\infty$}}{R}$.

  * $\Rightarrow$

We can write out this computation inside $\mathcal{F}$ and point out that
$B(B)$ will then find $p$ and enter an infinite loop.111111Proving that a
program runs forever raises the specter ($\mathord{\mathchoice{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}}$)
of sub-inconsistency. But rest assured. Any formal system capable of reasoning
about algorithms can prove that “while true do nothing” runs forever.
Otherwise it ought to be ashamed of itself.

  * $\Rightarrow$

This allows us to construct a new (longer) proof of <<$B(B)$ doesn’t halt>> =
$\accentset{\scalebox{0.35}{$\infty$}}{R}$.

  * $\Rightarrow$

$\mathcal{F}$ is inconsistent. ↯∎

I feel like I’m watching a reboot (in more than one sense). We can even
recognize the phenomenon of finding either shorter or longer disproofs and
proofs; pure satisfaction.

Alright, time for the grand finale.

[Second Incompleteness Theorem—By Computation] One last time, let
$\mathcal{F}$ be a consistent Turing complete formal system. Then
$\mathcal{F}$ can’t prove its own consistency.

We could continue using $B$ for the Second Incompleteness Theorem. But that
would be ugly. Gödel didn’t need Rosser’s help for his proof. Neither shall
we.

###### Proof.

Let’s assume for the purpose of contradiction that $\mathcal{F}$ can prove its
own consistency

  * $\Rightarrow$

The first half of our new proof for the First Incompleteness Theorem can be
read as a proof by contradiction that if $\mathcal{F}$ is consistent, then
$P(P)$ doesn’t halt.

  * $\Rightarrow$

Using the fact that <<$P(P)$ doesn’t halt>> =
$\accentset{\scalebox{0.35}{$\infty$}}{G}$ this can be stated more concisely
as “$\mathcal{F}$ is consistent $\implies$
$\accentset{\scalebox{0.35}{$\infty$}}{G}$”.

  * $\Rightarrow$

Now we simply observe (with some faith) that there wasn’t actually anything in
the reasoning we used to prove this that we couldn’t carry out just as well in
$\mathcal{F}$. So <<$\mathcal{F}$ is consistent $\implies$
$\accentset{\scalebox{0.35}{$\infty$}}{G}$>> is actually a theorem in
$\mathcal{F}$.

  * $\Rightarrow$

We’re assuming that $\mathcal{F}$ can prove <<$\mathcal{F}$ is consistent>>.
So by modus ponens $\mathcal{F}$ can also prove
$\accentset{\scalebox{0.35}{$\infty$}}{G}$.

  * $\Rightarrow$

But then $P(P)$ will eventually find such a proof and halt. ↯∎

##  5 Taking Off The Glasses

At this point I can’t even tell the difference between the classical approach
and the algorithmic retelling anymore. Can you? All these proofs are exactly
the same as before! In fact, the relation is so strong that I was able to
write the latter ones by copy-pasting wholesale and then tinkering a little.
Just line them up and see for yourself. Every single line matches. Clearly,
this can’t be coincidence. There must be a deeper reason for this
overabundance of similarities. And there is. Perhaps you’ve already caught on
long ago. Or perhaps Clark Kent’s glasses fooled you too. Drum whirl please.

Recall once more what $\accentset{\scalebox{0.35}{$\infty$}}{G}$ says. It says
“$P(P)$ doesn’t halt”. But $P(P)$ isn’t just executing some simple infinite
loop. It’s looking for something. It’s scouring the proofs in $\mathcal{F}$
for a proof of <<$P(P)$ doesn’t halt>> =
$\accentset{\scalebox{0.35}{$\infty$}}{G}$.
$\accentset{\scalebox{0.35}{$\infty$}}{G}$’s claim that $P(P)$ will never find
a proof of $\accentset{\scalebox{0.35}{$\infty$}}{G}$ is echoing $G$’s claim
that the original computers, you and me, will never find a proof of $G$. In
other words, $\accentset{\scalebox{0.35}{$\infty$}}{G}$ is also proclaiming to
the world:

“I am not provable!”

Exercise: Take off $\accentset{\scalebox{0.35}{$\infty$}}{R}$’s glasses as
well.

This means I could’ve organized this presentation very differently. I could’ve
just made these observations right away and then said: “Now reread the first
section.  $\square$ ”. I’ve been wasting your time!

##  6 Refactoring The Incompleteness Theorems

Gödel was programming the integers. That is that. And he didn’t even know it
at the time; truly impressive. I think this feat deserves to be encapsulated
with its own theorem. Perhaps we can come together and save posterity from the
grim fate of also only realizing this much later in their lives. It’s for the
kids—and for the horses.

Elementary arithmetic is a Turing complete domain.

I’ll have to leave the exact formulation of this theorem to smarter people.
After all, I did recently score in the bottom 7% of the GRE’s analytical
writing section (come on!). The upshot is that this allows us to easily
recover the incompleteness theorems for elementary arithmetic from a more
general insight:

[Turing Incompleteness Theorem] Any consistent formal system $\mathcal{F}$
capable of reasoning about a Turing complete domain can reason about
algorithms. That makes $\mathcal{F}$ a consistent Turing complete formal
system. Thereby, the incompleteness theorems apply to it. In slogan form:

If it’s complete, then it’s incomplete.

###### Proof.

I think the idea is best conveyed with an example. Take the famously Turing
complete Game of Life. For any algorithm one can create a configuration in the
Game of Life which mimics that algorithm. Now suppose somebody came up with a
formal system $\mathcal{F}$ to reason about the Game of Life. This formal
system might be able to prove assertions such as: <<Starting with a
configuration of the form […] square $(0,0)$ will never be occupied>>.

The incompleteness theorems are now immediate. All we have to do is to encode
the algorithms $P$ and $B$ into a Game of Life configuration and reiterate the
previous arguments. Conclusion: $\mathcal{F}$ will never be able to decide
whether the encoding of $B$ “halts”. And it won’t be able to prove its own
consistency. ∎

As a consequence computational undecidability and logical undecidability go
hand in hand. And elementary arithmetic is just one further entry in the long
list containing the Game of Life,  Fractran ,  Post Tag Systems ,  Magic the
Gathering ,  the human brain ,  Rule 110 ,  the Lambda Calculus ,  musical
notation ,  …
(Thank you so much for your attention! The cake I promised in the abstract is
on its way. Please stand by.) $\mathord{\mathchoice{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}{\vrule
width=0.0pt,height=0.0pt,depth=0.0pt\@HwM@right@or@left{}{}\picture(3.2,2.6)(-1.6,-1.0)\ignorespaces\qbezier(-0.3,-1.5)(0.0,-1.2)(0.3,-1.5)\ignorespaces\put(-0.4,0.7){\circle*{0.4}}\put(0.4,0.7){\circle*{0.4}}\endpicture}}$

## References

  * [1] Kurt Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, Issue 38, Dec. 1931 pp. 173–198
  * [2] John Barkley Rosser, Extensions of Some Theorems of Gödel and Church, Journal of Symbolic Logic, Volume 1, No. 3, Sep. 1936, pp. 87–91
  * [3] Donald Trump, Twitter, 6. Jan. 2018 (I just want to be able to say that Donald Trump has been cited when discussing the fundamentals of mathematics.)
  * [4] Alan Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Volume s2–42, Issue 1, 1937, pp. 230–265
  * [5] Douglas Hofstadter, Gödel, Escher, Bach, 1979
  * [6] Yes, Prime Minister, The Tangled Web (it’s a British television sitcom from the 80s)
  * [7] Algorithm $B$ also appears in Scott Aaronson’s Quantum Computing since Democritus where he uses it to give a pseudo proof of the Second Incompleteness Theorem. It was in plugging the holes in Aaronson’s argument that these ideas took their origin.

## Closing Credits

I’d like to thank Scott Aaronson for his feedback as well as for being
gracious enough to post this essay on his blog. Additionally, Cristopher Moore
has provided many helpful comments. Finally, I strongly urge you to read
Cristopher Moore and Stephan Mertens’ book The Nature of Computation. It’s
what made me fall in love with computer science.