# Biomedical Entity Linking for Dutch: Fine-tuning a Self-alignment BERT Model
on an Automatically Generated Wikipedia Corpus

###### Abstract

Biomedical entity linking, a main component in automatic information
extraction from health-related texts, plays a pivotal role in connecting
textual entities (such as diseases, drugs and body parts mentioned by
patients) to their corresponding concepts in a structured biomedical knowledge
base. The task remains challenging despite recent developments in natural
language processing. This paper presents the first evaluated biomedical entity
linking model for the Dutch language. We use MedRoBERTa.nl as base model and
perform second-phase pretraining through self-alignment on a Dutch biomedical
ontology extracted from the UMLS and Dutch SNOMED. We derive a corpus from
Wikipedia of ontology-linked Dutch biomedical entities in context and fine-
tune our model on this dataset. We evaluate our model on the Dutch portion of
the Mantra GSC-corpus and achieve $54.7\%$ classification accuracy and
$69.8\%$ 1-distance accuracy. We then perform a case study on a collection of
unlabeled, patient-support forum data and show that our model is hampered by
the limited quality of the preceding entity recognition step. Manual
evaluation of small sample indicates that of the correctly extracted entities,
around 65% is linked to the correct concept in the ontology. Our results
indicate that biomedical entity linking in a language other than English
remains challenging, but our Dutch model can be used to for high-level
analysis of patient-generated text.

Keywords: Biomedical Entity Linking, Dutch, Data and evaluation

Biomedical Entity Linking for Dutch: Fine-tuning a Self-alignment BERT Model
on an Automatically Generated Wikipedia Corpus

Fons Hartendorp1, Tom Seinen2, Erik van Mulligen2, Suzan Verberne1
---
1Leiden Institute of Advanced Computer Science, Leiden University, the
Netherlands
2Dept of Medical Informatics, Erasmus University Medical Center, Rotterdam,
the Netherlands
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>

Abstract content

## 1\. Introduction

Biomedical entity linking (BEL) is the task of linking mentions of biomedical
entities in free text to their corresponding canonical form in a knowledge
base Garda et al. (2023) (Figure 1). Entity linking is a commonly used step
after entity extraction to enable normalization and aggregation of entity
mentions. Applications include automatically categorizing and improving search
in medical scientific literature and information extraction from clinical
notes and patient forums Lee et al. (2016). In the analysis of patient
experiences and patient–doctor communication, BEL can identify common concepts
and aggregate free-text mentions from different authors and contexts. For
example, a patient on an online support forum might mention that they have
trouble with sleeping after taking medication. A BEL model would be able to
link the mention “trouble with sleeping” to the medical concept insomnia in a
medical ontology and thereby aggregate all the mentions of insomnia from all
patients.

Initial text pattern-based attempts to entity linking date back to the early
2000s, while modern models incorporate machine-learning algorithms French and
McInnes (2022). The task remains challenging for four reasons: 1) The high
diversity in surface form of identical biomedical terms. For example, MI and
hartaanval (heart attack) both belong to the same canonical concept form
myocard infarct (myocardial infarction). 2) The similarity in surface form of
different biomedical terms: candida and cardia refer to a yeast and the heart
respectively, while their Levenshtein distance is only two. 3) Free text
generated by patients and medical professionals is often noisy, including
spelling errors and (personal) abbreviations. 4) The number of entities in the
biomedical domain is very large. The Unified Medical Language System (UMLS),
the largest biomedical ontology and composed of various medical vocabularies,
contains more than 3.3 million unique concepts Bodenreider (2004); Vashishth
et al. (2021).

Labeled biomedical entity linking datasets are limited, particularly in
languages other than
English.111https://paperswithcode.com/datasets?mod=texts&task=entity-linking
In this paper, we present WALVIS, a weakly labeled Dutch biomedical entity
linking dataset that was automatically generated using Wikidata and Wikipedia.
We evaluate the quality of the WALVIS dataset and its effectiveness for
training BEL models. Specifically, we train a BEL model for Dutch using self-
alignment pretraining of BERT (sapBERT) Liu et al. (2021) on a cleaned Dutch
sample of the UMLS. We further fine-tune this model in a supervised setting on
WALVIS and evaluate it on the Dutch subset of the Mantra GSC corpus Kors et
al. (2015). Additionally, we perform a case study on a collection of
unlabeled, patient-support forum data to give an indication of the
effectiveness of our Dutch SapBERT on patient-written texts.

Figure 1: The task of biomedical entity linking. An entity recognition model
identifies entities in free text that are then passed to the biomedical entity
linking (BEL) model. The BEL model associates the new, unseen mention with its
corresponding concept from an ontology.

The contributions of this paper are as follows: 1) introduction of a method
for automatically generating a weakly labeled BEL-dataset in any preferred
target language, by combining the UMLS, Wikidata and Wikipedia and thereby
obviating the need for manual labelling by a domain expert. 2) introduction of
the first evaluated BEL model trained on the Dutch language. 3) Evaluation of
the model’s performance and generalizability on the Dutch portion of the
Mantra GSC dataset. 4) An analysis of the model’s performance on patient-
generated text through a case study on an online patient-support forum. We
release our code and data on
github.222https://github.com/fonshartendorp/dutch_biomedical_entity_linking

## 2\. Related Work

The goal of BEL is to associate an entity mention in a text with its
corresponding concept in a medical ontology, usually the UMLS. BEL models are
commonly part of pipelines including biomedical named entity recognition
(NER), followed by BEL and finally relation extraction French and McInnes
(2022). Some dedicated entity-linking corpora such as ShARe/CLEF and the NCBI
dataset have been published Pradhan et al. (2013), encouraging the development
and evaluation of pure BEL-models without possible propagation of errors from
the entity recognition module. A BEL-model typically involves a candidate
generation step followed by candidate ranking McInnes et al. (2009); D’Souza
and Ng (2015). In machine learning approaches to BEL, it is considered a
mapping problem. However, learning the mapping function is complicated by the
lack of large, labeled datasets for training and the huge amount of classes
Loureiro and Jorge (2020).

With representation learning, the need for a labeled dataset can be obviated
by leveraging the incorporated knowledge of a medical ontology. Since 2019,
several BERT models Devlin et al. (2019) for the biomedical domain have been
released for English Lee et al. (2020); Gu et al. (2021). For BEL, the entity
embeddings are then further improved in a second-phase pretraining step by
using information from the ontology Sung et al. (2020); Liu et al. (2021). At
inference, a similarity search is performed between the embedding of the new,
unseen mention and the precomputed embeddings of all the terms from the
ontology. The mention is then linked to the most similar term from the
ontology. Self-alignment pretraining BERT (SapBERT) is a current state-of-the-
art model that achieves $81.1\%$ accuracy on the COMETA corpus and $52.2\%$ on
the MedMentions corpus Liu et al. (2021); Basaldella et al. (2020); Loureiro
and Jorge (2020). Improvements have been attempted by incorporating context in
the second-phase pretraining step or by using cluster-based inference Zhang et
al. (2022); Ujiie et al. (2021); Angell et al. (2021). In the past years,
generative language models have also been explored for the task of BEL Yuan et
al. (2022).

There is limited prior work on BEL for Dutch. There are two public medical
annotation tools that includes Dutch and BEL: the rule-based Dutch
implementation of MedSpaCy’s QuickUMLS Seinen et al. (2023), and the Dutch
model pack for the MedCat library Kraljevic et al. (2021). MedCat’s linking
module consists of two steps. First, dictionary matching is used for linking
unambiguous terms (e.g. unique terms in the ontology, linked to one concept).
Second, ambiguous terms are linked based on context embedding similarity. The
context embeddings are trained on unambiguous terms and their context, in this
case from the Dutch medical Wikipedia articles. Although MedCat uses
similarity search with Word2Vec or BERT embeddings, the embeddings are not
refined by leveraging knowledge incorporated in the ontology.

## 3\. Preliminaries

BEL is the task of mapping entity mentions in text documents to canonical
concepts in a given ontology. A mention is a string that describes an entity
in natural language. A concept is semantic unit that is clearly defined in the
ontology and has a unique identifier. Mentions (words/phrases from text) can
refer to either real world entities or abstract concepts from the ontology. We
formally define the task of BEL as follows:

Problem definition Given a biomedical ontology $O$ consisting of $n$ concepts
$O=\\{c_{1},c_{2},...,c_{n}\\}$, a document D that contains a set $M$ of $p$
biomedical mentions $M=\\{m_{1},m_{2},...,m_{p}\\}$, the task of BEL is to
learn a mapping $M\rightarrow O$ that maps the mention $m_{j}\in M$ to the
corresponding concept $c_{i}\in O$ that it refers to.

### 3.1. Unified Medical Language System

The Unified Medical Language System (UMLS) is a large and comprehensive
biomedical ontology created and maintained by the US National Library of
Medicine. It is a collection of over 160 vocabularies, containing more than 15
million entries in 27 different languages. It maps entries from different
databases and terminologies to around $3.3$ million unique concepts, that are
identified by their Concept Unique Identifier (CUI). The Dutch portion
contains around $290{,}000$ terms. The UMLS also contains data on $54$ types
of semantic relations between concepts, both hierarchical (e.g. ‘is a’) and
non-hierarchical (e.g. ‘is conceptually related
to’).333https://www.nlm.nih.gov/research/umls/knowledge_sources/metathesaurus/release/statistics.html

### 3.2. Self-alignment pretraining BERT

The main challenge of BEL in a representation learning setting is the quality
of the entity embeddings Basaldella et al. (2020). Self-supervised learning
with masked language modelling on medical data has improved BEL, but does not
lead to a well separated representation space Liu et al. (2021).

Self-alignment pretraining (sap) Liu et al. (2021) improves the embeddings of
a pretrained BERT model, by self-aligning synonymous entries from a biomedical
ontology. Formally, the goal of self-alignment is to learn a function
$f(.;\theta):O\rightarrow E$ that is parameterized by $\theta$ and where $O$
represents the set of terms in an ontology and $E$ the corresponding embedding
representations with $\forall e\in E,\ e\in\mathbb{R}^{d}$. In sapBERT, $f$ is
modelled by a BERT model with the output [CLS] token as embedding
representation of the input term $c$. The similarity between two terms,
$<f(c_{i}),f(c_{j})>$ can be estimated by taking the cosine similarity. During
the training procedure, online hard triplet mining is used for generating
informative pairs that are used for contrastive learning. From each mini-
batch, a random anchor term $c_{a}$ is drawn. Together with a positive match –
or synonym – $c_{p}$ and a negative match $c_{n}$, the triplet
$(c_{a},c_{p},c_{n})$ is formed. Informative triplets are generated by
selecting positive matches (synonyms in the ontology) that get very dissimilar
embeddings and, conversely, negative matches with embeddings that are nearly
similar. Formally, triplets are selected that violate the following condition:

$||f(c_{a})-f(c_{p})||_{2}<||f(c_{a})-f(c_{n})||_{2}+\lambda$ (1)

where $\lambda$ is a pre-set margin. That is, we only select those triplets
where the distance between the anchor and the positive term is larger than the
distance between the anchor and the negative term plus margin $\lambda$. The
mining of informative triplets only is useful for improving the embeddings,
since otherwise non-informative triplets would dominate the training process
due to the enormous size of the ontology Liu et al. (2021). The Multi-
Similarity loss function is used for pulling the embeddings of positive pairs
closer and pushing the embeddings of negative pairs further apart Wang et al.
(2019). This process leads to a better separated representation space by
leveraging the semantic biases of synonymy relations in the ontology.

## 4\. Methods

Due to the need for expensive, manually labelling by domain experts, BEL
datasets are not broadly available, especially in languages other than
English. We introduce a method for automatically generating a weakly labeled
BEL dataset in any given target language, by combining the structured
knowledge source Wikidata, the UMLS and inter-article hyperlinks on Wikipedia.
We implement the pipeline for Dutch. We first clean and enhance the Dutch
subset of the UMLS and generate a Dutch biomedical ontology specifically
tailored for BEL tasks.

### 4.1. Enhancing the UMLS

Roughly $1.7\%$ of the UMLS 2022AB release, comprising $290{,}056$ terms, is
in
Dutch.444https://www.nlm.nih.gov/research/umls/knowledge_sources/metathesaurus/release/index.html
However, there is variability in the quality of the records. By following the
same steps as the Dutch medical concepts
project555https://github.com/umcu/dutch-medical-concepts, we created a
cleaned, UMLS-based Dutch biomedical ontology in several filtering and
expansion steps.666Note that we cannot re-use their data because the UMLS is
licensed and cannot be re-shared. An overview is provided in Figure 2. We
exported, using the MetaMorphosys-tool, the terms of all seven Dutch
vocabularies that are included in the release. From the $290{,}056$ terms, we
removed the vocabularies LNC-NL-NL and ICPC2ICD10DUT that contain composed
terms that are non-informative for the task of BEL such as
report:finding:date:polyclinical:document: endocrinology.777Translated from
Dutch for the readers’ convenience From the vocabularies ICD10DUT and MDRDUT
we removed descriptive subterms, such as non-specified, as they are usually
not found in free text. Also, duplicate entries were dropped, irrespective of
capitalization. We added the Dutch SNOMED vocabulary, as this is not included
in the UMLS. Since the US SNOMED is included in the UMLS, we matched Dutch to
English terms on their SNOMED ID, and subsequently assign them their
corresponding UMLS IDs (CUIs), dropping ambiguous terms. Entries linked to one
of 26 semantic types that we considered non-relevant for BEL, such as Birds
and Geographic areas were also removed. Finally, we added English drug names
from the ATC, DRUGBANK and RXNORM vocabularies, since they are occasionally
used in Dutch Miller and Britt (1995); Wishart et al. (2018); Nelson et al.
(2011).

Figure 2: Flow diagram of ontology enhancement. The remaining number of
entries are denoted in italic.

The newly generated Dutch biomedical ontology contains $752{,}536$ terms
sourced from 11 vocabularies, all linked to one of the $366{,}071$ distinct
concepts. On average, each term is associated with one synonym, but the
distribution is heavily right skewed (25% percentile is 0 synonyms per term /
75% percentile is 2 synonyms per term). Table 1 shows the semantic group
distribution of the ontology. The semantic groups are not classes in our
entity linking problem, but rather a categorization of the classes. The four
largest groups – disorders (DISO), chemicals & drugs (CHEM), procedures (PROC)
and anatomy (ANAT) – make up for $97\%$ of the terms in the ontology.

Since the UMLS and SNOMED are licensed, we cannot distribute the ontology.
However, comprehensive details of all steps are provided in a Python Notebook
in the project’s Github repository. The ontology can be reproduced after
requesting a UMLS and SNOMED license.

Table 1: Semantic group distributions of the ontology, train- and validation
set of the no-duplicates, ontology-filtered subsets (*) from the WALVIS corpus
(WALVIS*) and Mantra GSC (Mantra*). DISO: disorders, CHEM: chemicals & drugs,
PROC: procedures, ANAT: anatomy, LIVG: living beings, PHEN: phenomena, DEVI:
devices, PHYS: physiology and ACTI: activities & behaviors, OBJC: Objects,
GENE: genes & molecular sequences, OCCU: occupations, CONC: concepts & ideas.
1559 terms in the ontology are not assigned a semantic group (other).
|  | Ontology | WALVIS* tra. | WALVIS* val. | Mantra*
---|---|---|---|---|---
Group | Example | count | perc. | count | perc. | count | perc | count | perc.
DISO |  MS (multiple sclerosis) | 310057 | 41.3 | 957 | 49.8 | 224 | 46.7 | 149 | 39.3
CHEM | Neupro | 185096 | 24.6 | 402 | 20.9 | 108 | 22.5 | 66 | 17.4
PROC |  Dialyse (dialysis) | 124345 | 16.6 | 90 | 4.7 | 20 | 4.2 | 68 | 17.9
ANAT |  Heup (hip) | 108622 | 14.5 | 391 | 20.4 | 105 | 21.9 | 33 | 17.4
LIVB |  Patiënt (patient) | 7586 | 1.0 | 14 | 0.7 | 6 | 1.2 | 29 | 7.7
PHEN |  Licht (light) | 5997 | 0.8 | 4 | 0.2 | 1 | 0.2 | 7 | 1.8
DEVI | IUD’s | 3153 | 0.4 | 3 | 0.2 | 0 | 0.0 | 5 | 1.3
PHYS |  Groei (growth) | 3125 | 0.4 | 33 | 1.7 | 11 | 2.3 | 19 | 5.0
ACTI |  Macht (power) | 1053 | 0.1 | 0 | 0.0 | 0 | 0.0 | 1 | 0.3
OBJC |  Stof (fabric) | 678 | 0.1 | 13 | 0.7 | 3 | 0.6 | 2 | 0.5
GENE | Codon | 497 | 0.1 | 3 | 0.2 | 2 | 0.4 | 0 | 0.0
OCCU | Genomics | 464 | 0.1 | 10 | 0.5 | 0 | 0.0 | 0 | 0.0
CONC |  Retentie (retention) | 304 | 0.0 | 0 | 0.0 | 0 | 0.0 | 0 | 0.0
Oth. |  | 1559 | 0.2 | 0 | 0.0 | 0 | 0.0 | 0 | 0.0
Total |  | 752536 |  | 1920 |  | 480 |  | 379 |

Figure 3: WALVIS corpus compilation. All Wikidata entries with a linked Dutch
Wikipedia page and a UMLS CUI that are in the ontology are retrieved using
SPARQL. Then, all sentences from the Wikipedia dump are parsed and selected if
they contain a hyperlink to one of the collected Wikipedia pages.

### 4.2. Corpus compilation

For the automatic generation of our weakly labeled dataset WALVIS, we combine
our enhanced ontology with textual data from Wikipedia and structured data
from Wikidata. An overview is provided in Figure 3. Wikidata is a
collaboratively edited multilingual knowledge graph that acts as central
storage for structured data of its Wikimedia sister projects including
Wikipedia Vrandečić and Krötzsch (2014). Relevant data can be obtained from
Wikidata through SPARQL queries. We retrieve all $4,519$ Wikidata entities
that have been assigned a UMLS CUI and are linked to a Wikipedia page that is
part of the Dutch Wikipedia collection. The SPARQL query is provided in
Listing 1.

⬇

SELECT ?concept ?conceptLabel ?cui ?article WHERE {

?concept wdt:P2892 ?cui .

?article schema:about ?concept .

?article schema:isPartOf

<https://nl.wikipedia.org/>.

SERVICE wikibase:label {

bd:serviceParam wikibase:language "nl"

}

}

Listing 1: SPARQL query for retrieving all Wikidata entities that contain a
UMLS CUI and where there exists an article about the entity that is part of
the Dutch Wikipedia

We process all pages from the Dutch Wikipedia dump of March
2023888https://dumps.wikimedia.org using the SpaCy sentence splitter with the
Dutch nl_core_news_sm pipeline. We then collect all $51{,}693$ sentences that
contain a hyperlink to one of the $4{,}519$ Dutch Wikipedia articles that on
their turn are linked to a Wikidata entity with a UMLS CUI property. The
anchor texts of the hyperlinks are considered biomedical entity mentions. On
average, a sentence contains $18$ $(\pm 9)$ tokens and $53{,}960$ $(0.06\%)$
of the tokens in the collection are biomedical entity mentions that are linked
to a UMLS CUI (Table 2).

For the WALVIS* subset, we kept each first unique mention and dropped their
duplicates. Also, only mentions that link to a CUI that is present in the
ontology are included. The WALVIS* corpus contains $2{,}400$ unique mentions
from $2{,}307$ sentences. $1{,}751$ mentions are unseen by our model in the
sapBERT training phase as they are not present in the ontology. The mentions
map to $1{,}086$ unique CUI’s that are all included in the ontology.

In Table 1, we see that the distribution of mentions over the semantic groups
in the train- and validation set of WALVIS* is relatively similar to the
distribution of terms in the ontology over the semantic groups, except for
procedures (PROC). Procedures are possibly terms more commonly used by medical
experts only, compared to disorders, chemicals & drugs and anatomical terms,
which could explain their lower prevalence on Wikipedia.

The code for parsing the Wikipedia dump and creating the corpus is available
on Github, and the the WALVIS corpus and WALVIS* subset are available for
download in XML format.

Table 2: Corpora statistics. The WALVIS corpus contains many duplicate
mentions that occur in different contexts. The WALVIS* subset (Wal.*) contains
no duplicate mentions and only links to CUI’s that have an entry in the
ontology. We created a similar subset of the Mantra GSC corpus (Man.*).
| WALVIS | WAL.* | Man.*
---|---|---|---
Sentences | 51515 | 2307 | 166
Avg. #tok/sent | 18 | 20 | 17
Mentions | 53781 | 2400 | 379
Unique mentions | 3201 | 2400 | 379
Unseen mentions | 49497 | 1751 | 214
CUI’s | 56141 | 2758 | 402
Unique CUI’s | 1334 | 1086 | 359
Unlinkable CUI’s | 47548 | 0 | 0

### 4.3. Self-alignment pre-training

We use the RoBERTa-derived language model MedRoBERTa.nl as base model.
MedRoBERTa.nl was pretrained on nearly 10 million anonymized hospital notes
obtained from the Amsterdam University Medical Centres Verkijk and Vossen
(2021). The model is distributed with uninitialized head layers, allowing for
fine-tuning on specific tasks.

We generate the training data for the self alignment pretraining from the
cleaned Dutch medical ontology (Section 4.1). We generate a text file with
positive pairs in the form of: CUI||term 1||term 2, where term 1 and term 2
are synonyms, so associated to the same CUI in the ontology. If more than 2
terms are associated to the same CUI, all pairwise combinations are traversed
and added. We sample from the pool of positive pairs during the contrastive
learning step for improving the pretrained BERT embeddings. Negative pairs are
sampled online by randomly drawing a term from the ontology that is not linked
to the same CUI. Both the negative and positive pairs must violate the minimum
margin condition in Equation 1.

We use Multi-Similarity loss for re-aligning of the embeddings with parameters
set to the same values as in Liu et al. (2021). We use a learning rate of
0.0001 with a weight decay of 0.01 for $\\{0,1,3,10\\}$ epoch(s) with a batch
size of 512. The similarity margin $\lambda$ is set to $0.2$. The [CLS] token
is used as representation of the input term. The model is built in Pytorch
2.1.0, mostly based on code from Liu et al.
(2021).999https://github.com/cambridgeltl/sapbert

### 4.4. Fine-tuning

Fine-tuning on the WALVIS corpus is performed in a similar manner. Now, the
positive pairs are generated by combining mentions, linked terms and their
corresponding CUI from the labeled dataset: CUI||mention||linked term. The
hyperparameters are set to the same values as in Section 4.3.We fine-tune for
$\\{0,1,3,10\\}$ epoch(s), building on the pretrained models from the previous
step.

### 4.5. Inference

All terms from the ontology are fed to the trained model, generating a set of
precomputed embeddings. At inference, a new, unseen mention is also fed to the
trained model and a nearest neighbour search can be performed with the
precomputed embeddings. The new mention is assigned the CUI of the most
similar embedding from the ontology. Since a nearest neighbour search on
$752{,}536$ items is computationally expensive, we built a FAISS index from
the precomputed embeddings. FAISS is a library for approximate nearest
neighbour search of dense
vectors.101010https://github.com/facebookresearch/faiss/wiki For memory
purposes, the precomputed embeddings are first compressed by using only their
first $256$ principal components.

### 4.6. Evaluation data and metrics

We evaluated our method on the Dutch subset of the Mantra GSC corpus. The
Mantra GSC corpus is a hand-labeled corpus annotated by domain-experts that
was originally created for biomedical concept recognition in languages other
than English Kors et al. (2015). The texts are sourced from MEDLINE titles and
drug labels. The biomedical entities are also annotated with a UMLS CUI, that
we use as gold labels for our linking model. Since the ontology does not
contain all UMLS CUIs, we use the WALVIS* and Mantra* subsets that contain
only mentions that link to a CUI that is included in the ontology. In both
corpora, duplicate mentions were also removed since our model is not context-
aware. Table 2 shows the corpora statistics of WALVIS* and Mantra*. The
Mantra* subset contains 379 mentions from 166 sentences. The sentences are
slightly shorter than the WALVIS* sentences, on average 17 tokens per
sentence, and have more entity mentions per sentence.

For finding the optimal number of sapBERT- and fine-tune epochs, we performed
a hyperparameter optimization on the train set of WALVIS* and validated on its
validation set. In the evaluation phase, we fine-tuned our optimal model on
the full WALVIS* subset and evaluated on the Mantra* corpus.

In addition to our primary metric classification accuracy, we also look at the
1-distance accuracy. For this metric, predictions are scored correct if they
are any kind of 1-distance UMLS relation away from the gold label. For
example, the prediction cystopyelonephritis for a term with gold label
pyelonephritis would be correct since the UMLS contains a ‘classified
as’-relation between the two.

### 4.7. Case study on patient-support forum

The Dutch online patient-support forum https://www.kanker.nl/ donated
anonymized textual data from between 2013 and 2016 in the form of blog posts,
discussions and question-answering threads. The data does not have any manual
annotations. We split the data in sentences using pySBD’s sentence splitter,
finding $123{,}338$ sentences and $2{,}191{,}424$ tokens. Before being able to
apply BEL, we need entity extraction. To that end, we finetune MedRoBERTa.nl
for NER on the machine translated MedMentions dataset in Dutch Seinen et al.
(2024).111111https://github.com/mi-erasmusmc/DutchClinicalCorpora This gives
us $368{,}840$ medical named entities. We run both the base model and our
finetuned BEL model on these entities to link them to the Dutch UMLS and
analyze the results.

## 5\. Results and analysis

We first assess the quality of our automatically generated WALVIS-corpus. We
then turn to an evaluation of the optimal model on Mantra* and perform a brief
error analysis. Finally, we explore its performance on entities sourced from
the patient-support forum.

### 5.1. Quality of WALVIS-corpus

We randomly sample 100 mentions from the WALVIS-corpus and manually evaluate
the correctness of their label (Wikidata–UMLS link). The grading was performed
by the first author using a tool that was developed for this purpose, for easy
comparison of UMLS
entries.121212https://anonymous.4open.science/r/biomedical_entity_linking-
FCB4/ontology-browser/ 28 mentions were found to be linked to a concept that
is related but not the same. For example, the mention kerndelingen (divisions
of the nucleus) on the Dutch Wikipedia page about asexual reproduction, is
linked to cell nucleus, which is related but not the same. The remaining 72
mentions seem to be labeled correctly. The label quality score indicates that
the quality of the automatically generated corpus is suboptimal and that the
data is not suited for evaluation purposes. The 100 samples and their grading
can be found in our Github repository.

### 5.2. Main results

In hyperparameter tuning, the model with 3 sapBERT epochs and 10 fine-tune
epochs performed optimal with a classification accuracy of $30.5\%$ and a
1-distance accuracy of $49.8\%$ on the validation set of WALVIS. Table 3 shows
the results on the Mantra* corpus. All results are averaged over 5 runs with
different random seeds. The model (3S10FT) achieves a classification accuracy
of $54.7\%$ and a 1-distance accuracy of $69.8\%$. That is a $10.1\%$ point
and $13.1\%$ point improvement respectively, compared to the base model (BM).

In Table 3, the results grouped by semantic group are separately shown. We do
not see a clear relation between the size of the semantic groups in the
training data (the ontology and WALVIS), and their evaluation performance on
Mantra*. On all four largest groups in the training data, an average
improvement of around $10\%$ point in classification accuracy is observed,
even though the largest group – disorders (DISO) – is with 149 samples four
and a half times larger than the fourth-largest group ANAT (anatomy). We note
that the numbers of mentions per semantic group in Mantra* are too small to
derive clear conclusions.

Table 3: Evaluation results on the Mantra* corpus for the base model (BM) and
our optimal model (trained for 3 self-alignment epochs + 10 fine-tune epochs).
The semantic groups are not classes themselves, but rather a categorization of
the classes. DISO: disorders, PROC: procedures, CHEM: chemicals & drugs, ANAT:
anatomy, LIVG: living beings, PHYS: physiology, PHEN: phenomena, DEVI:
devices, OBJC: Objects, ACTI: activities & behaviors. The total micro-average
is shown for all 379 mentions averaged over 5 experiment runs with different
random seeds.
|  | Accuracy | 1-dist acc.
---|---|---|---
Group | # | BM | 3S10FT | BM | 3S10FT
DISO | 149 | 49.3 | 59.6 | 63.0 | 77.0
PROC | 68 | 29.7 | 39.5 | 41.5 | 56.1
CHEM | 66 | 48.2 | 57.6 | 58.5 | 67.3
ANAT | 33 | 57.6 | 66.7 | 66.7 | 78.2
LIVB | 29 | 33.8 | 48.3 | 48.3 | 61.4
PHYS | 19 | 56.8 | 58.9 | 66.3 | 71.6
PHEN | 7 | 57.1 | 76.2 | 71.2 | 82.4
DEVI | 5 | 20.0 | 20.0 | 20.0 | 28.0
OBJC | 2 | 0.0 | 0.0 | 50.0 | 70.0
ACTI | 1 | 0.0 | 20.0 | 0.0 | 100.0
Total | 379 | 44.6 | 54.7 | 56.7 | 69.8

### 5.3. Error analysis

We manually reviewed the mispredictions made by our optimal model. Due to the
sometimes noisy and at some points extremely branched structure of the UMLS,
seemingly small differences between prediction and gold label are scored
incorrect. For example, the mention advies (advice) is linked to voorlichting
en advies (counseling-C0010210) by our optimal model. However, in Mantra GSC,
its gold label is given as adviseren (advice-C0150600). The prediction is
called correct by the 1-distance metric, since a RN (‘Relation Narrow’) exists
between the two concepts in the UMLS.

Sometimes, a mention is linked to an on surface form-level similar but
semantically slightly different concept from the ontology. For example,
mention cannabis is linked to the plant genus cannabis (C0936079), while its
gold label in Mantra GSC is the drug cannabis (C0678449). Also, the mention
pijnlijke rug (sore back) is linked to pijnlijke rug (sore back-C0863105), but
labeled as rugpijn (back pain-C0004604). This indicates that our accuracies
are perhaps an under-estimation of the actual effectiveness of the entity
linking – a finding that was also observed in previous work Dirkson et al.
(2023).

We further observe a high focus on surface form by our model. For example,
mention oren (ears) is linked to ren (running-C0022646) instead of gold label
oor (ear-C0013443). Moreover, mentions in all capitals, are often linked to a
concept in all capitals,sometimes to a concept that is on surface form and
semantical meaning very different. For example, mention SOMATOTYPE is linked
to DOPAMINERGIC AGENTS (C0013036), while the surface form of its gold label is
exactly similar to the mention but lower cased: somatotype (C0037669). Lower
casing all terms in the ontology and newly seen mentions could help, but by
doing so some information is lost, for example in abbreviations (‘pos’ is
commonly used for ‘positive’, whereas ‘POS’ could mean ‘Polycystic Ovary
Syndrome’). While a context-aware model like KRISSBERT could reduce reliance
on surface form, we did not implement such a model due to the lack of large,
publicly available Dutch medical literature that is required for training
Zhang et al. (2022).

Table 4: Top 5 most found named entities and corresponding linked concepts
from the patient-support forum data from kanker.nl. Translated from Dutch for
the reader’s convenience.
# | Named entity | Linked concept
---|---|---
4356 | cancer | primary malignant
|  | neoplasm
4240 | chemo | chemo-immunotherapy
3043 | surgery | operative surgical
|  | procedures
3034 | therapy | milieu therapy
2287 | tumor | neoplasms

### 5.4. Case study

On the unlabeled data from https://www.kanker.nl, our finetuned BEL-model
disagreed with the base model in the linking of $77.7\%$ ($286{,}654$) of the
found named entities. This indicates that self-alignment pre-training and
finetuning has a substantial effect on the model behaviour. To get an
impression of the model quality, we manually graded 100 randomly sampled
mentions. We found that 42 mentions were errors in the named entity
recognition step. Of the 58 correct entity mentions, 20 entities (34%) are
linked to a wrong concept, another 20 mentions (34%) are linked to a related
concept and the remaining 18 (31%) are linked correctly. The grading can be
found on Github.

The most commonly found named entities, such as kanker (cancer), chemo
(chemo), and operatie (surgery), seem likely to appear frequently on a support
forum for cancer patients (Table 4). While the named entities are simpler
terms compared to their linked concepts, for the majority they seem to be
words that are also practiced by medical professionals. The main difference
between layman talk and medical jargon is probably to be found in the context
the words are used in. If we look at the semantic groups of the linked
entities, we see that Disorders – the largest group in the ontology – is also
the most used semantic group on the forum, but with $34\%$ much less
proportionally than on Wikipedia ($50\%$ in WALVIS) and medical literature
($39\%$ in Mantra). Procedures on the other hand, are much more prevalent on
the forum ($23\%$) than on Wikipedia ($5\%$) according to our model.

## 6\. Conclusion

To the best of our knowledge, our work is the first to introduce an evaluated
biomedical entity linking model in the Dutch language. We also present a
method for automatically generating a weakly labeled biomedical entity linking
dataset in any preferred target language, by combining the data from a
biomedical ontology, Wikidata and Wikipedia pages. Using this method, we
introduce the first – weakly labeled – Dutch biomedical entity linking corpus:
WALVIS. We trained a BEL model by self alignment pretraining on the
MedRoBERTa.nl, followed by fine-tuning on WALVIS*. With around 70% 1-distance
accuracy on the external evaluation set Mantra*, we achieve a substantial
improvement over the base model. This was achieved with a relatively small
fine-tuning corpus. A case study on a collection of patient-written texts
showed that the main source of error remains to be the named entity
recognition step. Manual evaluation of small sample indicates that of the
correctly extracted entities, our model links around 65% to a correct or
closely related concept in the ontology. In our evaluation on Mantra, we
observe that our model relies heavily on surface form, which is for example
observed by the erroneous linking of upper case mentions to upper case
concepts that are otherwise very dissimilar. A context-aware model could
further improve performance.

In conclusion, our biomedical entity linking model can be used for higher-
level analysis of patient-oriented text data in Dutch. In future work, a
larger corpus for fine-tuning could further improve the model’s performance. A
larger corpus could be created by automatically translating the English
Wikipedia pages, which are not only larger in number, but also contain more
words per article.

## Bibliographical References

##

  * Angell et al. (2021) Rico Angell, Nicholas Monath, Sunil Mohan, Nishant Yadav, and Andrew McCallum. 2021\.  Clustering-based Inference for Biomedical Entity Linking.  In _Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies_ , pages 2598–2608, Online. Association for Computational Linguistics.
  * Basaldella et al. (2020) Marco Basaldella, Fangyu Liu, Ehsan Shareghi, and Nigel Collier. 2020.  COMETA: A Corpus for Medical Entity Linking in the Social Media.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 3122–3137, Online. Association for Computational Linguistics.
  * Bodenreider (2004) Olivier Bodenreider. 2004.  The unified medical language system (UMLS): integrating biomedical terminology.  _Nucleic acids research_ , 32(suppl_1):D267–D270.
  * Devlin et al. (2019) Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2019.  BERT Pre-training of Deep Bidirectional Transformers for Language Understanding.  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 4171–4186, Minneapolis, Minnesota. Association for Computational Linguistics.
  * Dirkson et al. (2023) Anne Dirkson, Suzan Verberne, Gerard Van Oortmerssen, Hans Gelderblom, and Wessel Kraaij. 2023.  How do others cope? Extracting coping strategies for adverse drug events from social media.  _Journal of Biomedical Informatics_ , 139:104228.
  * D’Souza and Ng (2015) Jennifer D’Souza and Vincent Ng. 2015.  Sieve-based entity linking for the biomedical domain.  In _Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 2: Short Papers)_ , pages 297–302.
  * French and McInnes (2022) Evan French and Bridget T McInnes. 2022.  An overview of biomedical entity linking throughout the years.  _Journal of Biomedical Informatics_ , page 104252.
  * Garda et al. (2023) Samuele Garda, Leon Weber-Genzel, Robert Martin, and Ulf Leser. 2023.  BELB: a biomedical entity linking benchmark.  _Bioinformatics_ , 39(11):btad698.
  * Gu et al. (2021) Yu Gu, Robert Tinn, Hao Cheng, Michael Lucas, Naoto Usuyama, Xiaodong Liu, Tristan Naumann, Jianfeng Gao, and Hoifung Poon. 2021.  Domain-specific language model pretraining for biomedical natural language processing.  _ACM Transactions on Computing for Healthcare (HEALTH)_ , 3(1):1–23.
  * Kors et al. (2015) Jan A Kors, Simon Clematide, Saber A Akhondi, Erik M Van Mulligen, and Dietrich Rebholz-Schuhmann. 2015.  A multilingual gold-standard corpus for biomedical concept recognition: the Mantra GSC.  _Journal of the American Medical Informatics Association_ , 22(5):948–956.
  * Kraljevic et al. (2021) Zeljko Kraljevic, Thomas Searle, Anthony Shek, Lukasz Roguski, Kawsar Noor, Daniel Bean, Aurelie Mascio, Leilei Zhu, Amos A Folarin, Angus Roberts, et al. 2021.  Multi-domain clinical natural language processing with MedCAT: the medical concept annotation toolkit.  _Artificial intelligence in medicine_ , 117:102083.
  * Lee et al. (2020) Jinhyuk Lee, Wonjin Yoon, Sungdong Kim, Donghyeon Kim, Sunkyu Kim, Chan Ho So, and Jaewoo Kang. 2020.  BioBERT: a pre-trained biomedical language representation model for biomedical text mining.  _Bioinformatics_ , 36(4):1234–1240.
  * Lee et al. (2016) Sunwon Lee, Donghyeon Kim, Kyubum Lee, Jaehoon Choi, Seongsoon Kim, Minji Jeon, Sangrak Lim, Donghee Choi, Sunkyu Kim, Aik-Choon Tan, et al. 2016.  BEST: next-generation biomedical entity search tool for knowledge discovery from biomedical literature.  _PloS one_ , 11(10):e0164680.
  * Liu et al. (2021) Fangyu Liu, Ehsan Shareghi, Zaiqiao Meng, Marco Basaldella, and Nigel Collier. 2021\.  Self-Alignment Pretraining for Biomedical Entity Representations.  In _Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies_ , pages 4228–4238, Online. Association for Computational Linguistics.
  * Loureiro and Jorge (2020) Daniel Loureiro and Alípio Mário Jorge. 2020.  Medlinker: Medical entity linking with neural representations and dictionary matching.  In _European Conference on Information Retrieval_ , pages 230–237. Springer.
  * McInnes et al. (2009) Bridget T McInnes, Ted Pedersen, and Serguei VS Pakhomov. 2009.  UMLS-Interface and UMLS-Similarity: open source software for measuring paths and semantic similarity.  In _AMIA annual symposium proceedings_ , volume 2009, page 431. American Medical Informatics Association.
  * Miller and Britt (1995) GC Miller and H Britt. 1995.  A new drug classification for computer systems: the ATC extension code.  _International journal of bio-medical computing_ , 40(2):121–124.
  * Nelson et al. (2011) Stuart J Nelson, Kelly Zeng, John Kilbourne, Tammy Powell, and Robin Moore. 2011\.  Normalized names for clinical drugs: RxNorm at 6 years.  _Journal of the American Medical Informatics Association_ , 18(4):441–448.
  * Pradhan et al. (2013) Sameer Pradhan, Noemie Elhadad, Brett R South, David Martinez, Lee M Christensen, Amy Vogel, Hanna Suominen, Wendy W Chapman, and Guergana K Savova. 2013.  Task 1: ShARe/CLEF eHealth Evaluation Lab 2013.  _CLEF (working notes)_ , 1179.
  * Seinen et al. (2023) Tom M Seinen, Jan A Kors, Erik M van Mulligen, Egill Fridgeirsson, and Peter R Rijnbeek. 2023.  The added value of text from Dutch general practitioner notes in predictive modeling.  _Journal of the American Medical Informatics Association_ , 30(12):1973–1984.
  * Seinen et al. (2024) Tom M Seinen, Jan A Kors, Erik M van Mulligen, and Peter R Rijnbeek. 2024.  Annotation-preserving machine translation of English corpora to validate Dutch clinical concept extraction tools.  _medRxiv_ , pages 2024–03.
  * Sung et al. (2020) Mujeen Sung, Hwisang Jeon, Jinhyuk Lee, and Jaewoo Kang. 2020.  Biomedical Entity Representations with Synonym Marginalization.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 3641–3650, Online. Association for Computational Linguistics.
  * Ujiie et al. (2021) Shogo Ujiie, Hayate Iso, and Eiji Aramaki. 2021.  Biomedical Entity Linking with Contrastive Context Matching.  _arXiv preprint arXiv:2106.07583_.
  * Vashishth et al. (2021) Shikhar Vashishth, Denis Newman-Griffis, Rishabh Joshi, Ritam Dutt, and Carolyn P Rosé. 2021.  Improving broad-coverage medical entity linking with semantic type prediction and large-scale datasets.  _Journal of biomedical informatics_ , 121:103880.
  * Verkijk and Vossen (2021) Stella Verkijk and Piek Vossen. 2021.  Medroberta.nl: a language model for Dutch electronic health records.  _Computational Linguistics in the Netherlands Journal_ , 11:141–159.
  * Vrandečić and Krötzsch (2014) Denny Vrandečić and Markus Krötzsch. 2014.  Wikidata: a free collaborative knowledge base.  _Communications of the ACM_ , 57(10):78–85.
  * Wang et al. (2019) Xun Wang, Xintong Han, Weilin Huang, Dengke Dong, and Matthew R Scott. 2019.  Multi-similarity loss with general pair weighting for deep metric learning.  In _Proceedings of the IEEE/CVF conference on computer vision and pattern recognition_ , pages 5022–5030.
  * Wishart et al. (2018) David S Wishart, Yannick D Feunang, An C Guo, Elvis J Lo, Ana Marcu, Jason R Grant, Tanvir Sajed, Daniel Johnson, Carin Li, Zinat Sayeeda, et al. 2018.  DrugBank 5.0: a major update to the DrugBank database for 2018.  _Nucleic acids research_ , 46(D1):D1074–D1082.
  * Yuan et al. (2022) Hongyi Yuan, Zheng Yuan, and Sheng Yu. 2022.  Generative biomedical entity linking via knowledge base-guided pre-training and synonyms-aware fine-tuning.  _arXiv preprint arXiv:2204.05164_.
  * Zhang et al. (2022) Sheng Zhang, Hao Cheng, Shikhar Vashishth, Cliff Wong, Jinfeng Xiao, Xiaodong Liu, Tristan Naumann, Jianfeng Gao, and Hoifung Poon. 2022.  Knowledge-Rich Self-Supervision for Biomedical Entity Linking.  In _Findings of the Association for Computational Linguistics: EMNLP 2022_ , pages 868–880, Abu Dhabi, United Arab Emirates. Association for Computational Linguistics.


# The Strategic Balance of Games in Logic11endnote: 1This paper is written in
response to a question by Samson Abramsky, about where in my book [19] are the
promised translations between strategies of the various games that I present.
To my surprise I had not given the translations explicitly in the book,
perhaps because in the book I move freely from games to inductive definitions
and back. In this paper the translations are given explicitly and I thank
Samson for pointing out the omission in my book.

Jouko Väänänen
University of Helsinki, Finland
and
University of Amsterdam, The Netherlands This project has received funding
from the Academy of Finland (grant No 322795) and from the European Research
Council (ERC) under the European Union’s Horizon 2020 research and innovation
programme (grant agreement No 101020762).

###### Abstract

Truth, consistency and elementary equivalence can all be characterised in
terms of games, namely the so-called evaluation game, the model-existence
game, and the Ehrenfeucht-Fraïssé game. We point out the great affinity of
these games to each other and call this phenomenon the _strategic balance in
logic_. In particular, we give explicit translations of strategies from one
game to another.

##  1 The three games of logic

The Game Theoretical Semantics of first order logic, and many other logics
too, is a combination of three games: The Evaluation Game, the Model Existence
Game and the EF game (short for Ehrenfeucht-Fraïssé Game). These games are
closely related to each other and cover the main semantic concepts of logic.
We use the term “Game Theoretical Semantics” for the general approach that
emphasises and utilizes these games in semantics, rather than some other
approach, e.g. set-theoretical semantics in the Tarskian sense.

In the Evaluation Game we have a structure $A$ and a sentence $\phi$. The game
gives meaning to the proposition that $\phi$ is true in $A$. The meaning is
equivalent to the one given by Tarski’s Turth Definition. In the Model
Existence Game the structure $A$ is missing and we have just the sentence
$\phi$. The game gives meaning to the proposition that $\phi$ is consistent,
or alternatively, that there is a structure in which $\phi$ is true. This game
appears in different incarnations throughout logic, all the way from Gentzen’s
Natural Deduction, to Beth Tableaux, to Dialogical Games, to Hintikka’s model
sets, to semantic trees, to Smullyan’s consistency properties. Finally, in the
EF game the sentence $\phi$ is missing and we just have two models $A$ and
$B$. The game gives meaning to the proposition that some sentence is true in
$A$ but false in $B$. Alternatively we can say that the EF game gives meaning
to, or equivalently a definition of the elementary equivalence of $A$ and $B$.

Figure 1: The translations of strategies.

The meanings that these games give to truth, consistency, and elementary
equivalence are intertranslatable in the sense that a strategy in one can be
converted to a strategy in the other (see Figure 1). If the former is a
winning strategy, so is the latter. We need not traverse via Tarski’s Truth
Definition. In this sense Game Theoretical Semantics stands autonomously on
its own feet. This is important for those who find Tarski’s approach too set-
theoretical. However, the set-theoretical treatment is arguably the best
representation of even the Game Theoretical Semantics, despite the intuitive
appeal of the latter, when one goes into the gritty details of complicated
proofs.

The three games, Evaluation Game, Model Existence Game, and EF game, penetrate
into the heart of logic where we find the concepts of truth, consistency,
provability, definability and isomorphism. Their mathematical interpretations
and elaborations lead us into the deepest questions of mathematical logic,
especially model theory and set theory. They provide tools for understanding
central questions of philosophical logic such as intuitionistic, modal and
other non-classical logic. They have become indispensable in theoretical
computer science modelling interaction and complexity.

For more details and for references to the original sources we refer to [19].
Everything in this paper was essentially known already in the fifties and
sixties. What is perhaps new is the emphasis on the mutual relationships
between the three games, taking the form of a collection of translations
between strategies. This aspect has been forcefully emphasised in [20]. The
author feels that despite the ripe age of the main results, this topic has
more to offer than has been discovered so far. An interesting recent
development is [1].

Notation:  If $X$ is a set, an $X$-assignment is a mapping with a set of
variables as its domain and values in $X$. If $s$ is an $X$-assignment and
$a\in X$, then $s(a/x)$ is the $X$-assignment which agrees with $s$ except
that it gives $x$ the value $a$. If $X$ is clear from the context, we drop it
and talk about assignments only.

##  2 Given both a sentence and a model: the Evaluation Game

We describe a game which gives meaning to the _truth_ of a given sentence in a
given model. In its simplest form this game, the Evaluation Game, is the
following: Suppose $M$ is a structure for a vocabulary $L$, $\phi$ is a first
order (or, more generally, infinitary) $L$-sentence and $s$ is an assignment.
We allow identity. Let $\Gamma(s)$ denote the set of all literals i.e. atomic
and negated atomic formulas that $s$ satisfies in $M$. As the logical
operations allowed in $\phi$ we include $\neg,\wedge,\vee,\forall$ and
$\exists$. To make the situation as clear as possible, we assume that $\phi$
is in Negation Normal Form, meaning that negation occurs only in front of
atomic formulas. The game $G(M,\phi)$ has two players Abelard and Eloise.
Intuitively, Eloise defends the proposition that $\phi$ is (informally) true
in $M$ and Abelard doubts it. All through the game the players are inspecting
an $L$-sentence and an assignment $s$. We call the pair $(\psi,s)$ a
_position_ of the game. In the beginning of the game the position is
$(\phi,\emptyset)$. The rules are as follows: Suppose the position is
$(\psi,s)$.

  1. (1)

If $\psi$ is a literal, the game ends and Eloise wins if $\psi\in\Gamma(s)$.
Otherwise Abelard wins.

  2. (2)

If $\psi$ is $\psi_{0}\wedge\psi_{1}$, then Abelard chooses whether the next
position is $(\psi_{0},s)$ or $(\psi_{1},s)$.

  3. (3)

If $\psi$ is $\psi_{0}\vee\psi_{1}$, then Eloise chooses whether the next
position is $(\psi_{0},s)$ or $(\psi_{1},s)$.

  4. (4)

If $\psi$ is $\forall x\theta$, then Abelard chooses $a\in M$ and the next
position is $(\theta,s(a/x))$.

  5. (5)

If $\psi$ is $\exists x\theta$, then Eloise chooses $a\in M$ and the next
position is $(\theta,s(a/x))$.

A _strategy_ for a player is a set of rules (functions) that describe exactly
how that player should choose, depending on how the two players have played at
earlier moves. It is a _winning strategy_ if the player wins whichever way the
opponent plays. The game $G(M,\phi)$ is clearly a determined game i.e. always
one of the players has a winning strategy.

We say that $\phi$ is _true in_ $M$ if Eloise has a winning strategy in
$G(M,\phi)$. This is the game-theoretical meaning of truth in a model. We can
go further and say that the _game_ $G(M,\phi)$ is the _meaning_ of $\phi$ in
$M$. Here meaning would be a broader concept than the mere truth or falsity of
$\phi$.

The first to formulate the Evaluation Game explicitly was probably J. Hintikka
[11] who later advocated the importance and usefulness of the game forcefully.
Hintikka mentions L. Wittgenstein [21] as an inspiration. Earlier L. Henkin
[8] formulated a game theoretic approach to quantifiers pointing out
generalizations to very general infinitary and partially ordered quantifiers.
Nowadays the Evaluation Game is a standard tool in mathematical, philosophical
and computer science logic.

The game $G(M,\phi)$ reflects the entire syntactical structure of $\phi$ in
the sense that the game $G(M,\phi\wedge\psi)$ is intimately related to the two
games $G(M,\phi)$ and $G(M,\psi)$, the same with $G(M,\phi\vee\psi)$,
$G(M,\exists x\phi)$ and $G(M,\forall x\phi)$. This phenomenon is a
manifestation of the broader concept of _compositionality_.

If $\phi$ is propositional i.e. has only zero-place relation symbols and no
constant or function symbols, and no quantifiers, then only moves (1)-(3)
occur in $G(M,\phi)$, and the assignments can be forgotten. If $\phi$ is
universal, the game $G(M,\phi)$ has no moves of type (5). If it is
existential, the game has no moves of type (4). If universal-existential, then
all type (5) moves come before type (4) moves. Furthermore, if we add new
logical operations to our logic, such as infinite conjunctions and
disjunctions, generalized quantifiers or higher order quantifiers, it is clear
how to modify the game $G(M,\phi)$ to accommodate the new logical operations.
For example, for $\phi$ in $L_{\infty\omega}$, we modify above (2) and (3) as
follows:

  1. (2’)

If $\psi$ is $\bigwedge_{i\in I}\psi_{i}$, then Abelard chooses $i\in I$ and
the next position is $(\psi_{i},s)$.

  2. (3’)

If $\psi$ is $\bigvee_{i\in I}\psi_{i}$, then Eloise chooses $i\in I$ and the
next position is $(\psi_{i},s)$.

This extends also to so-called team semantics [18], in which case a position
in the game $G(M,\phi)$ is a pair $(\psi,X)$, where $\psi$ is a subformula of
$\phi$ and $X$ is a team. Finally, if $M$ is a Kripke-model and $\phi$ a
sentence of modal logic, the game $G(M,\phi)$ is entirely similar. The
assignments have a singleton domain $\\{x_{0}\\}$ and values in the frame of
$M$. The moves corresponding to $\Diamond$ and $\Box$ are like (4) and (5):

  1. (4’)

If $\psi$ is $\Box\theta$, then Abelard chooses a node $b$ accessible from
$s(x_{0})$ and the next position is $(\theta,s(b/x_{0}))$.

  2. (5’)

If $\psi$ is $\Diamond\theta$, then Eloise chooses a node $b$ accessible from
$s(x_{0})$ and the next position is $(\theta,s(b/x_{0}))$.

The game $G(M,\phi)$ can also reflect the structure of $M$. In fact, the games
$G(M\times N,\phi)$, $G(M+N,\phi)$, and $G(\Pi_{i}M_{i}/F,\phi)$ are
intimately related to the games $G(M,\phi)$, $G(N,\phi)$ and $G(M_{i},\phi)$
[4]. The game $G(M,\phi)$ is also helpful in finding a countable submodel $N$
of $M$ with desired properties. For any strategy $\tau$ of Eloise in
$G(M,\phi)$ let $T(M,\tau)$ be the set of countable submodels $N$ of $M$ such
that $N$ is closed under the functions of $M$ and under $\tau$ i.e. if Abelard
plays in (4) always $a\in N$, then also Eloise plays in (5) always $b\in N$.
Note that if $N\in T(M,\tau)$, then $\tau$ is necessarily a strategy of Eloise
in $G(N,\phi)$. Moreover, if $\tau$ is a winning strategy in $G(M,\phi)$, then
it is also a winning strategy in $G(N,\phi)$. The Löwenheim-Skolem Theorem of
$L_{\omega_{1}\omega}$ is essentially the statement that
$T(M,\phi)\neq\emptyset$, when $\phi\in L_{\omega_{1}\omega}$. In the _Cub
Game_ due to D. Kueker [14] there are two players Abelard and Eloise, a set
$X$ and a set $T$ of countable subsets of $X$. During the game, which we
denote $G_{T}$, the players choose alternatingly elements $a_{n}\in X$,
Abelard being the first to move. After $\omega$ moves a set
$\\{a_{0},a_{1},\ldots\\}$ has been produced. We say that Eloise is the winner
if this set is in $T$, otherwise Abelard is the winner. This game need not be
determined. If Eloise has a winning strategy in $G_{T}$, then $T$ contains a
so-called cub (closed unbounded) set of countable subsets of $X$.

Below is a strong form of a Löwenheim-Skolem Theorem for
$L_{\omega_{1}\omega}$, based on the Evaluation Game. It shows that the
countable submodels for which the given strategy works for Eloise are
“everywhere” (i.e. cub) inside $M$. The theorem is due to [14].

######  Theorem 1.

Suppose $M$ is a model in a countable vocabulary and $\phi$ is a sentence of
$L_{\omega_{1}\omega}$. There is a mapping $\Upsilon$ such that if $\tau$ is a
strategy of Eloise in $G(M,\phi)$, then $\Upsilon(\tau)$ is a strategy of
Eloise in $G_{T(M,\phi)}$. If $\tau$ is a winning strategy, then so is
$\Upsilon(\tau)$.

###### Proof.

(Sketch) Using bookkeeping Eloise makes sure during the game $G_{T(M,\phi)}$
that her moves $a_{2n+1}\in M$ render the final set $\\{a_{0},a_{1},\ldots\\}$
such that it is both the domain of a submodel of $M$ and if Abelard plays his
moves of type (4) in $\\{a_{0},a_{1},\ldots\\}$ then so does Eloise, using
$\tau$, in her moves of type (5). ∎

In conclusion, the game $G(M,\phi)$ is a versatile tool for understanding the
meaning of a logical sentence $\phi$ in a mathematical structure $M$.
Alternative tools, yielding equivalent results, are inductive methods such as
the so-called Tarski’s Truth Definition and the theory of inductive
definitions.

##  3 The model is missing: the Model Existence Game

Here we have a sentence and we ask whether the sentence has a model. Thus this
is about _consistency_ and its opposite, _contradiction_. In particular, the
issue is whether there is some model $M$ such that Eloise can win $G(M,\phi)$?
This question is governed by the Model Existence Game $\mbox{MEG}(\phi)$.

Suppose $\phi$ is a first order sentence. As the logical operations allowed in
$\phi$ we include $\neg,\wedge,\vee,\forall$ and $\exists$. To make this as
simple as possible, we assume again that $\phi$ is in Negation Normal Form.
The game $\mbox{MEG}(\phi)$ has two players Abelard and Eloise. Intuitively,
Eloise defends the proposition that $\phi$ has a model and Abelard doubts it.
Abelard expresses his doubt by asking questions. It may be the case that
Eloise has a model at her disposal but she does not want to reveal it, apart
from using it to give answers to Abelard’s questions, but she may also just
pretend that she does. For all we know there may not be any model. Conceivably
$\phi$ is a contradiction, but the game should settle this. We let
$C=\\{c_{0},c_{1},\ldots,c_{n},\ldots\\}$ be a set of new distinct constant
symbols. Intuitively these are names of elements of the supposed model. A
position of the game is a finite collection $S$ of pairs $(\psi,s)$, where
$\psi$ is a subformula of $\phi$ and $s$ is a $C$-assignment. In infinitary
logic we may consider also infinite $S$. In the beginning of the game the
position is $\\{(\phi,\emptyset)\\}$. The rules are as follows: Suppose the
position is $S$.

  1. 1.

If $(\psi_{0}\wedge\psi_{1},s)\in S$, then Abelard may decide that the next
position is $S\cup\\{(\psi_{0},s)\\}$ or $S\cup\\{(\psi_{1},s)\\}$.

  2. 2.

If $(\psi_{0}\vee\psi_{1},s)\in S$, then Abelard may decide that Eloise has to
choose whether the next position is $S\cup\\{(\psi_{0},s)\\}$ or
$S\cup\\{(\psi_{1},s)\\}$.

  3. 3.

If $(\forall x\theta,s)\in S$, then Abelard may choose $n\in{\mathbb{N}}$ and
decide that the next position is $S\cup\\{(\theta,s(c_{n}/x))\\}$.

  4. 4.

If $(\exists x\theta,s)\in S$, then Abelard may decide that Eloise has to
choose $c_{n}$ and the next position is $S\cup\\{(\theta,s(c_{n}/x))\\}$.

Abelard wins if at some point the position $S$ contains both $(\psi,s)$ and
$(\neg\psi,s^{\prime})$, where $\psi$ is an atomic formula and
$s(x)=s^{\prime}(x)$ for all variables $x$ in $\psi$. If Abelard does not win,
then the game may continue for infinitely many moves and then Eloise is
declared the winner. Note that Abelard has a lot of control on how the game
proceeds as he may focus attention on any formula in the finite set $s$. This
is clearly a determined game.

The Model Existence Game is a game-theoretic rendering of the method of Beth
Tableaux, with background in Gentzen’s natural deduction. It was presented
roughly as above, but without explicit mention of a game, for first order
logic at about the same time by E. Beth [2] and J. Hintikka [10], later in a
more abstract form by R. Smullyan [17], and for infinitary logic by M. Makkai
[15].

The following theorem, essentially due to [2], demonstrates how the Model
Existence Game and the Evaluation Game can be combined in the somewhat trivial
case that a model is not missing but actually known (see Figure 2).

$\begin{array}[]{ccccccc}&C&-\\!\\!\\!-\\!\\!\\!-&N&\subseteq&M&\\\
\Phi(\tau)&\bigg{|}&&&&\bigg{|}&\tau\\\ &\phi&&&&\phi\end{array}$
Figure 2: From model to model existence.

######  Theorem 2.

Suppose the vocabulary of $M$ is countable. There is a mapping $\Phi$ so that
if $\tau$ is a strategy of Eloise in $G(M,\phi)$, then $\Phi(\tau)$ is a
strategy of Eloise in $\mbox{MEG}(\phi)$. If $\tau$ is a winning strategy,
then so is $\Phi(\tau)$.

###### Proof.

By Theorem 1 there is a countable submodel $N$ of $M$ such that $\tau$ is a
strategy of Eloise in $G(N,\phi)$ and if $\tau$ is a winning strategy in
$G(M,\phi)$, then it is also a winning strategy in $G(N,\phi)$. Let $\pi:C\to
N$ be an onto map. Let us say that a pair $(\psi,s)$ is a $\tau$-position if
there is there is some sequence of positions in $G(N,\phi)$, following the
rules of $G(N,\phi)$ starting with $(\phi,\emptyset)$, Eloise using $\tau$,
which ends at $(\psi,s)$. A _$C$ -translation_ of the $\tau$-position
$(\psi,s)$ is a pair $(\psi,s^{\prime})$ where $s^{\prime}$ is a
$C$-assignment with $\pi(s^{\prime}(x))=s(x)$. The strategy $\Phi(\tau)$ of
Eloise in $\mbox{MEG}(\phi)$ is to make sure that at all times the position
$S$ consists only of $C$-translations of $\tau$-positions. Let us now check
that Eloise can actually follow this strategy: Suppose the position is $S$.

  1. 1.

If $(\psi_{0}\wedge\psi_{1},s^{\prime})\in S$, then Abelard may decide that
the next position is $S\cup\\{\psi_{0},s^{\prime}\\}$ or
$S\cup\\{\psi_{1},s^{\prime}\\}$. Let us assume he chooses
$S\cup\\{\psi_{0},s^{\prime})\\}$ as the next position. There is a sequence
$\alpha$ of moves in $G(N,\phi)$ in which Eloise uses $\tau$, which ends at
$(\psi_{0}\wedge\psi_{1},s)$, a $C$-translation of which is
$(\psi_{0}\wedge\psi_{1},s^{\prime})$. We continue $\alpha$ by letting Abelard
move $\psi_{0}$. Now $S\cup\\{(\psi_{0},s^{\prime})\\}$ consists of
$C$-translations of $\tau$-positions.

  2. 2.

If $(\psi_{0}\vee\psi_{1},s^{\prime})\in S$, then Eloise can decide that the
next position is $S\cup\\{(\psi_{0},s^{\prime})\\}$ or
$S\cup\\{(\psi_{1},s^{\prime})\\}$. There is a sequence $\alpha$ of moves in
$G(N,\phi)$ in which Eloise uses $\tau$, which ends at
$(\psi_{0}\vee\psi_{1},s)$, a $C$-translation of which is
$(\psi_{0}\vee\psi_{1},s^{\prime})$. We continue $\alpha$ by letting Eloise
move whatever $\tau$ tells her to move, say $\psi_{0}$. Now
$S\cup\\{(\psi_{0},s^{\prime})\\}$ consists of $C$-translations of
$\tau$-moves. So we let Eloise choose $S\cup\\{(\psi_{0},s^{\prime})\\}$ as
the next position.

  3. 3.

If $(\forall x\theta,s^{\prime})\in S$, then Abelard may choose $c\in C$ and
the next position is $S\cup\\{(\theta,s^{\prime}(c/x))\\}$. There is a
sequence $\alpha$ of moves in $G(N,\phi)$ in which Eloise uses $\tau$, which
ends at $(\forall x\theta,s)$, a $C$-translation of which is $(\forall
x\theta,s^{\prime})$. We continue $\alpha$ by letting Abelard move
$(\theta,s(\pi(c)/x))$. Now $S\cup\\{(\theta,s^{\prime}(c/x))\\}$ consists of
$C$-translations of $\tau$-moves.

  4. 4.

If $(\exists x\theta,s)\in S$, then Eloise may choose $a\in M$ and the next
position is $S\cup\\{\theta\langle s(a/x)\rangle\\}$. There is a sequence
$\alpha$ of moves in $G(N,\phi)$ in which Eloise uses $\tau$, which ends at
$(\exists x\theta,s)$, a $C$-translation of which is $(\exists
x\theta,s^{\prime})$. We continue $\alpha$ by letting Eloise use $\tau$ to
move $(\theta,s(a/x))$. Let $a=\pi(c)$. Now $S\cup\\{\theta\langle
s^{\prime}(c/x)\rangle\\}$ consists of $C$-translations of $\tau$-moves. We
let Eloise choose $S\cup\\{\theta\langle s^{\prime}(c/x)\rangle\\}$ as the
next position.

If Eloise follows this strategy and $\tau$ happens to be a winning strategy,
then she wins because if at some point there are $(\psi,s^{\prime})$ and
$(\neg\psi,t^{\prime})$ in the set $S$, such that $\psi$ is atomic and
$s^{\prime}(x)=t^{\prime}(x)$ for variables $x$ in $\psi$, then these would be
$C$-translations of $(\psi,s)$ and $(\neg\psi,t)$, where $s(x)=t(x)$ for $x$
in $\psi$, respectively, and $s$ (and $t$) would satisfy both $\psi$ and
$\neg\psi$ in $N$ because $\tau$ is a winning strategy, a contradiction. ∎

The following theorem is more interesting because here we do not have a model
to start with but we have to construct a model. In this sense this is
reminiscent of Gödel’s Completeness Theorem. The theorem demonstrates how the
Model Existence Game can yield a model which then has a good fit with the
Evaluation Game (see Figure 3). The theorem goes back to [2].

$\begin{array}[]{rcccl}&C&-\\!\\!\\!-\\!\\!\\!-&M(\tau)&\\\
\tau&\bigg{|}&&\bigg{|}&\Psi(\tau)\\\ &\phi&&\phi\end{array}$ Figure 3: From
model existence to a model.

######  Theorem 3.

There are a mapping $\Psi$ and an “enumeration strategy” $\sigma_{0}$ of
Abelard in $\mbox{MEG}(\phi)$ such that if $\tau$ is any strategy of Eloise in
$\mbox{MEG}(\phi)$, playing $\tau$ against $\sigma_{0}$ determines a unique
model $M(\tau)$ and a strategy $\Psi(\tau)$ of Eloise in $G(M(\tau),\phi)$. If
$\tau$ is winning, then so is $\Psi(\tau)$.

###### Proof.

To make the presentation a little easier, we assume $\phi$ has a relational
vocabulary and does not contain the identity symbol. Let $\sigma_{0}$ be the
following “enumeration strategy” of Abelard in $\mbox{MEG}(\phi)$: During the
game Abelard makes sure by means of careful bookkeeping that if $S$ is the
position, then:

  1. 1.

If $(\psi_{0}\wedge\psi_{1},s)\in S$, then during the game he will at some
position $S^{\prime}\supseteq S$ decide that the next position is
$S^{\prime}\cup\\{(\psi_{0},s)\\}$ and at some further position
$S^{\prime\prime}\supseteq S^{\prime}$ he will decide that the next position
is $S^{\prime\prime}\cup\\{(\psi_{1},s)\\}$.

  2. 2.

If $(\psi_{0}\vee\psi_{1},s)\in S$, then at some position $S^{\prime}\supseteq
S$ Abelard asks Eloise to choose whether the next position is
$S^{\prime}\cup\\{(\psi_{0},s)\\}$ or $S^{\prime}\cup\\{(\psi_{1},s)\\}$.

  3. 3.

If $(\forall x\theta,s)\in S$, then for all $n$ during the game he will at
some position $S^{\prime}\supseteq S$ decide that the next position is
$S^{\prime}\cup\\{(\theta,s(c_{n}/x)\\}$.

  4. 4.

If $(\exists x\theta,s)\in S$, then at some position $S^{\prime}\supseteq S$
Abelard will ask Eloise to choose $n$ after which the next position is
$S^{\prime}\cup\\{(\theta,s(c_{n}/x))\\}$.

Let us play $\mbox{MEG}(\phi)$ while Abelard uses this strategy and Eloise
plays $\tau$. Let

$\mathcal{S}=\langle S_{n}:n<\omega\rangle$

be the infinite sequence of positions during this play. Since the strategies
of the players have been fixed, the sequence $\mathcal{S}$ is uniquely
determined. Note that $S_{n}\subseteq S_{n+1}$ for all $n$. Let $\Gamma$ be
the union of all the positions in $\mathcal{S}$. We build a model $M=M(\tau)$
as follows: The domain of the model is $\\{c_{n}:n\in{\mathbb{N}}\\}$. If $R$
is a relation symbol, then we let $R(c_{n_{0}},\ldots,c_{n_{k}})$ hold in $M$
if $(R(x_{n_{0}},\ldots,x_{n_{k}}),s)\in\Gamma$ for some $s$ such that
$s(x_{i})=c_{i}$ for $i=n_{0},\ldots,n_{k}$. The strategy $\Psi(\tau)$ of
Eloise in $G(M,\phi)$ is the following: She makes sure that if the position in
$G(M,\phi)$ is $(\psi,s)$, then $(\psi,s)\in\Gamma$. Let us see that she can
follow the strategy throughout the game:

  1. 1.

If $\psi$ is $\psi_{0}\wedge\psi_{1}$, then Abelard chooses whether the next
position is $(\psi_{0},s)$ or $(\psi_{1},s)$. Suppose he chooses
$(\psi_{1},s)$. Now, $(\psi_{0}\wedge\psi_{1},s)$ occurs in a position $S$
during the game, because $(\psi_{0}\wedge\psi_{1},s)\in\Gamma$. According to
how $\sigma_{0}$ is defined, Abelard has at some later position
$S^{\prime}\supseteq S$ of the game decided that the next position is
$S^{\prime}\cup\\{(\psi_{1},s)\\}$. Hence $(\psi_{1},s)\in\Gamma$.

  2. 2.

If $\psi$ is $\psi_{0}\vee\psi_{1}$, then Eloise should choose whether the
next position is $(\psi_{0},s)$ or $(\psi_{1},s)$. We know
$(\psi_{0}\vee\psi_{1},s)\in S$ for some position $S$ during the game, because
$(\psi_{0}\vee\psi_{1},s)\in\Gamma$. By how $\sigma_{0}$ was defined, Abelard
has at some later position $S^{\prime}\supseteq S$ asked Eloise to choose
between $(\psi_{0},s)$ and $(\psi_{1},s)$. The strategy $\tau$ has directed
Eloise to choose, say $(\psi_{0},s)$. Thus $(\psi_{0},s)\in\Gamma$ and she can
safely play $(\psi_{0},s)$ in $G(M,\phi)$.

  3. 3.

If $\psi$ is $\forall x\theta$, then Abelard chooses $a\in M$ and the next
position is $(\theta,s(a/x))$. Suppose he chooses $a=c_{n}$. Now, $(\forall
x\theta,s)$ occurs in a position $S$ during the game, because $(\forall
x\theta,s)\in\Gamma$. According to how $\sigma_{0}$ is defined, Abelard has at
some later position $S^{\prime}\supseteq S$ of the game decided that the next
position is $S^{\prime}\cup\\{(\theta,s(c_{n}/x))\\}$. Hence
$(\theta,s(a/x))\in\Gamma$.

  4. 4.

If $\psi$ is $\exists x\theta$, then Eloise should choose for which $n$ the
next position is $(\theta,s(c_{n}/x))$. We know $(\exists x\theta,s)\in S$ for
some position $S$ during the game, because $(\exists x\theta,s)\in\Gamma$. By
how $\sigma_{0}$ was defined, Abelard has at some later position
$S^{\prime}\supseteq S$ asked Eloise to choose $n$ for which the next position
would be $S^{\prime}\cup\\{(\theta,s(c_{n}/x))\\}$. The strategy $\tau$ has
directed Eloise to indeed choose an $n$ leading to the new position
$S^{\prime}\cup\\{(\theta,s(c_{n}/x))\\}$. Thus $(\theta,s(c_{n}/x))\in\Gamma$
and she can safely play $(\theta,s(c_{n}/x))$ in $G(M,\phi)$.

Suppose now that $\tau$ is a winning strategy of Eloise. We show that then
$\Psi(\tau)$ is a winning strategy as well. Suppose the game $G(M,\phi)$ ends
at a position $(\psi,s)$ where $\psi$ is atomic. Then $(\psi,s)$ is in
$\Gamma$ whence $s$ satisfies $\psi$ in $M$. Suppose, on the other hand, the
game $G(M,\phi)$ ends at a position $(\neg\psi,s)$ where $\psi$ is atomic.
Then $(\neg\psi,s)$ is in $S_{n}$ for some $n$. It suffices to show that $s$
does not satisfy $\psi$ in $M$. Suppose it does. Then there is
$(\psi,s^{\prime})\in S_{m}$ for some $m$ and some $s^{\prime}$ such that
$s(x)=s^{\prime}(x)$ for variables $x$ in $\psi$. Then $S_{n+m}$ has both
$(\neg\psi,s)$ and $(\psi,s^{\prime})$, contrary to the assumption that $\tau$
is a winning strategy of Eloise. ∎

Let us suppose we investigate $\phi$ using the Model Existence Game and find
out that Abelard has a winning strategy in $\mbox{MEG}(\phi)$. We can form a
tree, a Beth Tableaux, of all the positions when Abelard plays his winning
strategy and we stop playing as soon as Abelard has won. Every branch of the
tree is finite and ends in a position which includes a contradiction. We can
make the tree finite by looking at the game more carefully. We can then view
this tree as a kind of proof of $\neg\phi$. In this sense the Model Existence
Game builds a bridge between proof theory and model theory. Strategies of
Abelard direct us to proof theory, while strategies of Eloise direct us to
model theory.

A winning strategy of Eloise in $\mbox{MEG}(\phi)$ can be conveniently given
in the form of a so-called _consistency property_ , which is just a set of
finite sets of sentences satisfying conditions which essentially code a
winning strategy for Eloise in $\mbox{MEG}(\phi)$. Sometimes it is more
convenient to use a consistency property than Model Existence Game. But as far
as strategies of Eloise are concerned, the two are one and the same thing.
Consistency properties have been successfully used to prove interpolation and
preservations results in model theory, especially infinitary model theory
[15].

Apart from first order and infinitary logic, the Model Existence Game can be
used in the proof theory and model theory of logic with generalized
quantifiers and higher order logic. In the infinitary logic
$L_{\kappa\lambda}$, $\lambda>\omega$, the Model Existence Game yields so-
called _chain models_ , rather than real models. In the case of generalized
quantifiers, such as the quantifier “there exists uncountably many”, the Model
Existence Game yields so-called weak models, which have to be transformed to
real models by a model theoretic argument [12]. In the case of higher order
logics the Model Existence Game yields so-called _general models_ , where the
higher order variables range over a set of subsets and relations rather than
over all subsets and relations [7]. The Model Existence Game can be used also
in propositional and modal logic.

##  4 The sentence is missing: The EF game

In the EF game we have a model but no sentence. To indicate what kind of
sentence we are looking for we have two models. The sentence is supposed to be
true in one but false in the other. It may be that no such sentence can be
found. Then the models are _elementarily equivalent_. We describe a game in
which strategies of one player track possibilities for elementary equivalence
and the strategies of the other player track possibilities for a separating
sentence. In its simplest form this game, the EF-game (a.k.a. Ehrenfeucht-
Fraïssé game, the back-and-forth game or the model comparison game),
introduced by A. Ehrenfeucht [3], is the following: Suppose $M$ and $N$ are
two structures for the same vocabulary $L$.

The game $\mbox{EF}_{m}(M,N)$ has two players Abelard and Eloise and $m$
moves. A position of the game is a set

$s=\\{(a_{0},b_{0}),\ldots,(a_{n-1},b_{n-1})\\}$ (1)

of pairs of elements such that the $a_{i}$ are from $A$ and the $b_{i}$ are
from $B$, and $n\leq m$. In the beginning of the game the position is
$\emptyset$. The rules are as follows: Suppose the position is $s$.

  1. 1.

Abelard may choose some $a_{n}\in A$. Then Eloise chooses $b_{n}\in B$ and the
next position is $s\cup\\{(a_{n},b_{n})\\}$.

  2. 2.

Abelard may choose some $b_{n}\in B$. Then Eloise chooses $a_{n}\in A$ and the
next position is $s\cup\\{(a_{n},b_{n})\\}$.

Abelard wins if during the game the position (1) is such that
$(a_{0},\ldots,a_{n-1})$ satisfies some literal in $M$ but
$(b_{0},\ldots,b_{n-1})$ does not satisfy the corresponding literal in $N$. If
Abelard does not win, then Eloise is declared the winner.

Intuitively, Eloise defends the proposition that $M$ and $N$ are very similar
in the sense that isomorphic structures are similar (but $M$ and $N$ need not
be actually isomorphic). Abelard doubts this similarity. Abelard expresses his
doubt by asking where would the purported isomorphism map this or that
element.

An extremely simple example is two models of size $\geq m$ in the empty
vocabulary. Then Eloise’s winning strategy is based on her playing different
elements when Abelard does the same. A slightly less trivial example is two
finite linear orders of size $\geq 2^{m}$.

Note that this game is determined. Moreover, if Eloise knows an isomorphism
$f:M\to N$ she can respond by playing always so that $b_{n}=f(a_{n})$.

$\begin{array}[]{ccccc}&&\tau&&\\\ &M&-\\!\\!\\!-\\!\\!\\!-&N&\\\
\sigma&\bigg{|}&&\bigg{|}&\Theta(\sigma,\tau)\\\ &\phi&&\phi\end{array}$
Figure 4: Interaction of Evaluation Game and EF game.

The following theorem demonstrates how the EF game and the Evaluation Game
interact when we actually do have a sentence (see Figure 4). The theorem is
due to [3].

######  Theorem 4.

There is a function $\Theta$ such that if $\tau$ is a strategy of Eloise in
$\mbox{EF}_{m}(M,N)$, $\phi$ is an $L_{\infty\omega}$-sentence of quantifier
rank $\leq m$, and $\sigma$ is a strategy of Eloise in $G(M,\phi)$, then
$\Theta(\sigma,\tau)$ is a strategy of Eloise in $G(N,\phi)$. If $\tau$ and
$\sigma$ are winning strategies, then so is $\Theta(\sigma,\tau)$.

###### Proof.

We call a position of the game $\mbox{EF}_{m}(M,N)$ a $\tau$-position if it
arises while Eloise is playing $\tau$. Suppose $\phi$ is a sentence of
quantifier rank $\leq m$ and Eloise has a strategy $\sigma$ in $G(M,\phi)$. We
call a position of the game $G(M,\phi)$ a $\sigma$-position, if it arises
while Eloise is playing $\sigma$. We use $\tau$ and $\sigma$ to construct a
strategy of Eloise in $G(N,\phi)$. If the position of the game $G(N,\phi)$ is
$(\psi,s)$, the strategy $\eta=\Theta(\sigma,\tau)$ of Eloise is to play
simultaneously with $G(N,\phi)$ the game $\mbox{EF}_{m}(M,N)$ and the game
$G(M,\phi)$ and make sure that if

$\pi=\\{(a_{0},b_{0}),\ldots,(a_{n-1},b_{n-1})\\}$

is the current $\tau$-position in $\mbox{EF}_{m}(M,N)$ and
$s(x)=\pi(s^{\prime}(x))$ for all $x$ in the domain of $s$, then
$(\psi,s^{\prime})$ is the current $\sigma$-position in $G(M,\phi)$ (see
Figure 5).

Let us check that it is possible for Eloise to play this strategy:

  1. 1.

If the position is $(\psi,s)$ where $\psi$ is a literal, the game ends.

  2. 2.

If the position is $(\psi,s)$ where is $\psi$ is $\bigwedge_{i}\phi_{i}$, then
Abelard chooses $i$ and the next position is $(\psi_{i},s)$. Whichever he
chooses, we let Abelard make the respective move $(\psi_{i},s^{\prime})$ in
$G(M,\phi)$.

  3. 3.

If the position is $(\psi,s)$ where is $\psi$ is $\bigvee_{i}\phi_{i}$, then
Eloise chooses $i$ as follows. Since $(\psi,s^{\prime})$ is a
$\sigma$-position, the strategy $\sigma$ tells Eloise which of
$(\psi_{i},s^{\prime})$ to play in $G(M,\phi)$. Then Eloise plays the
respective $(\psi_{i},s)$ in $G(N,\phi)$.

$\begin{array}[]{ccccc}&&\pi&&\\\ &M&-\\!\\!\\!-\\!\\!\\!-&N&\\\
s^{\prime}&\bigg{|}&&\bigg{|}&s\\\ &\phi&&\phi\end{array}$ Figure 5: The
strategy $\Theta(\sigma,\tau)$,

  4. 4.

If the position $(\psi,s)$ is $(\forall x\theta,s)$, then Abelard chooses
$b_{n}\in N$ and the next position is $(\theta,t)$, $t=s(b_{n}/x)$. We
continue the game $\mbox{EF}_{m}(M,N)$ from the $\tau$-position
$\\{(a_{0},b_{0}),\ldots,(a_{n-1},b_{n-1})\\}$ letting Abelard play $b_{n}$.
The strategy $\tau$ tells Eloise to choose $a_{n}\in M$ so that

$\pi^{\prime}=\\{(a_{0},b_{0}),\ldots,(a_{n},b_{n})\\}$ (2)

is again a $\tau$-position. Now we continue the game $G(M,\phi)$ from position
$(\forall x\theta,s^{\prime})$ by letting Abelard play $a_{n}$. We reach the
position $(\theta,t^{\prime})$, $t^{\prime}=s^{\prime}(a_{n}/x)$, which is
still a $\sigma$-position, and we have $\pi^{\prime}(t^{\prime}(y))=t(y)$ for
all $y$ in the domain of $t^{\prime}$.

  5. 5.

The position $(\psi,s)$ is $(\exists x\theta,s)$. Now we continue the game
$G(M,\phi)$ from position $(\exists x\theta,s^{\prime})$ by letting Eloise
play, according to $\sigma$, an element $a_{n}$ and we reach a new
$\sigma$-position $(\theta,t^{\prime})$, $t^{\prime}=s^{\prime}(a_{n}/x)$. We
continue the game $\mbox{EF}_{m}(M,N)$ from the $\tau$-position
$\\{(a_{0},b_{0}),\ldots,(a_{n-1},b_{n-1})\\}$ letting Abelard play $a_{n}$.
The strategy $\tau$ tells Eloise to choose $b_{n}\in N$ so that (2) is again a
$\tau$-position. We reach the position $(\theta,t)$, $t=s(b_{n}/x)$, and we
have $t(y)=\pi(t^{\prime}(y))$ for all $y$ in the domain of $t$.

If $\sigma$ is a winning strategy and the game $G(N,\phi)$ ends in the
position $(\psi,s)$, where $\psi$ is a literal, then Eloise wins because then
$(\psi,s^{\prime})$ is a $\sigma$-position meaning that $s^{\prime}$ satisfies
the literal $\psi$ in $M$, and $\tau$ being a winning strategy this means that
$s$ satisfies the literal $\psi$ in $N$. ∎

Just as the Model Existence Game can yield a model, the EF game can produce a
sentence. The next theorem shows how this arises from co-operation of the EF
game and the Evaluation Game (see Figure 6). The theorem is due to [3]. The
emphasis on this kind of translations between strategies occurs already in
[20].

$\begin{array}[]{ccccc}&&\tau&&\\\ &M&-\\!\\!\\!-\\!\\!\\!-&N&\\\
\Xi_{E}(\tau)&\bigg{|}&&\bigg{|}&\Xi_{A}(\tau)\\\ &\phi&&\neg\phi\end{array}$
Figure 6:

######  Theorem 5.

There is a sentence $\phi\in L_{\infty\omega}$ of quantifier rank $\leq m$ and
mappings $\Xi_{E}$ and $\Xi_{A}$ such that if $\tau$ is a strategy of Abelard
in $\mbox{EF}_{m}(M,N)$, then $\Xi_{E}(\tau)$ is a strategy of Eloise in
$G(M,\phi)$, and $\Xi_{A}(\tau)$ is a strategy of Abelard in $G(N,\phi)$. If
$\tau$ is a winning strategy, then $\Xi_{E}(\tau)$ and $\Xi_{A}(\tau)$ are
winning strategies. If $L$ is finite and relational, the sentence $\phi$ is
logically equivalent to a first order sentence of quantifier rank $\leq m$.

###### Proof.

Suppose $s$ is an assignment into $M$ with domain
$\\{x_{0},\ldots,x_{n-1}\\}$. Let

$\begin{array}[]{lcl}\psi^{0,n}_{M,s}&=&\displaystyle{\bigwedge_{i}\psi_{i}}\\\
\psi^{m+1,n}_{M,s}&=&(\forall x_{n}\displaystyle{\bigvee_{a\in
M}}\psi^{m,n+1}_{M,s(a/x_{n})})\wedge(\displaystyle{\bigwedge_{a\in M}}\exists
x_{n}\psi^{m,n+1}_{M,s(a/x_{n})}),\end{array}$

where $\psi_{i}$ lists all the literals in the variables
$x_{0},\ldots,x_{n-1}$ satisfied by $s$ in $M$.

The sentence $\phi$ we need to prove the theorem is
$\psi^{m,0}_{M,\emptyset}$. Note that this only depends on $M$. Clearly Eloise
has a trivial strategy $\Xi_{E}(\tau)$ in $G(M,\phi)$ (independently of
$\tau$), and this strategy is always a winning strategy: after Abelard has
chosen a value for $x_{n}$, she uses that value as her choice of $a\in M$, and
after Abelard has chosen $a\in M$, she uses that element as her value for
$x_{n}$. Note that the quantifier-rank of $\psi^{m,n}_{M,s}$ is always $m$.

We now describe the strategy $\Xi_{A}(\tau)$ of Abelard in $G(N,\phi)$. We
call a position of the EF-game a _$\tau$ -position _if it arises while Abelard
is playing $\tau$. Suppose $s$ is an assignment into $M$ and $s^{\prime}$ an
assignment into $N$, both with domain $\\{x_{0},\ldots,x_{n-1}\\}$. We use
$s\cdot s^{\prime}$ to denote the set of pairs $(s(x_{i}),s^{\prime}(x_{i}))$,
$i=0,\ldots,n-1$. The strategy of Abelard is to play $G(N,\phi)$ in such a way
that if the position at any point is $(\psi^{i,m-i}_{M,s},s^{\prime})$, then
$s\cdot s^{\prime}$ is a $\tau$-position. In the beginning the position is
$(\phi,\emptyset)$.

  1. 1.

Suppose the position in $G(N,\phi)$ is $(\psi^{i,m-i}_{M,s},s^{\prime})$,
$i>0$, and the next move for Abelard in $\mbox{EF}_{m}(M,N)$ according to
$\tau$ is $a\in M$. The strategy of Abelard is to choose the latter conjunct
of $\psi^{i,m-i}_{M,s}$. Then Abelard chooses the element $a\in M$ in the big
conjunction move. Now it is the turn of Eloise to choose some $b\in N$ as the
value of $x_{m-i}$ and that will be the next move of Eloise in
$\mbox{EF}_{m}(M,N)$. The new position $s(a/x_{m-i})\cdot
s^{\prime}(b/x_{m-i})$ is still a $\tau$-position in $\mbox{EF}_{m}(M,N)$. The
next position in $G(N,\phi)$ is

$(\psi^{i-1,m-i+1}_{M,s(a/x_{m-i})},s^{\prime}(b/x_{m-i})).$ (3)

  2. 2.

Suppose the position in $G(N,\phi)$ is $(\psi^{i,m-i}_{M,s},s^{\prime})$,
$i>0$, and the next move for Abelard in $\mbox{EF}_{m}(M,N)$ according to
$\tau$ is $b\in N$. The strategy of Abelard is to choose the former conjunct
where he plays $b$ as $x_{m-i}$. Now it is the turn of Eloise to choose some
$a\in M$ in $G(N,\phi)$. The new position $s(a/x_{m-i})\cdot
s^{\prime}(b/x_{m-i})$ is still a $\tau$-position in $\mbox{EF}_{m}(M,N)$. The
next position in $G(N,\phi)$ is (3).

  3. 3.

Finally the position is $(\psi^{0,m}_{M,s},s^{\prime})$. Note that $s\cdot
s^{\prime}$ is still a $\tau$-position in $\mbox{EF}_{m}(M,N)$. The game
$\mbox{EF}_{m}(M,N)$ has now ended. Abelard now chooses the first (in some
fixed enumeration) literal conjunct of the formula $\psi^{0,m}_{M,s}$ that is
not satisfied by $s^{\prime}$ in $N$, if any exist, otherwise he simply
chooses the first conjunct.

Suppose now $\tau$ was a winning strategy of Abelard. Then at the end of the
game $s\cdot s^{\prime}$ is a winning position for Abelard and therefore he is
indeed able to choose a conjunct of the formula $\psi^{0,m}_{M,s}$ that is not
satisfied by $s^{\prime}$ in $N$. He has won $G(N,\phi)$.

If $L$ is finite and relational, all the conjunctions and disjunctions are
essentially finite because there are only finitely many non-equivalent
formulas of a fixed quantifier rank. Thus, although $\phi$ is, a priori, a
formula of the infinitary logic $L_{\infty\omega}$, it is logically equivalent
to a first order formula. ∎

There is a tight connection between $\sigma$, $\tau$ and $\Xi(\sigma,\tau)$.
This is reflected in a connection between $\phi$ and $\mbox{EF}_{m}(M,N)$
which goes deeper into the structure of $\phi$ than the mere condition that
its quantifier rank is at most $m$. If the non-logical symbols of $\phi$ are
in $L^{\prime}\subset L$, then it suffices that $\tau$ is a strategy of Eloise
in the game $\mbox{EF}_{m}(M\restriction L^{\prime},N\restriction L^{\prime})$
between the reducts $M\restriction L^{\prime}$ and $N\restriction L^{\prime}$.
If we know more about the syntax of $\phi$, for example that it is
existential, universal or positive, we can modify $\mbox{EF}_{m}(M,N)$
accordingly by stipulating that Abelard only moves in $M$, only moves in $N$,
or that he has to win by finding an atomic (rather than literal) relation
which holds in $M$ but not in $N$.

Likewise, many useful observations can be made about the sentence $\phi$ and
the strategy $\tau$. Here are some. We already observed that the quantifier
rank of the separating sentence $\phi$ is the same as the length of the EF
game for which Abelard has a winning strategy. If $\tau$ is a winning strategy
of Abelard even in the game $\mbox{EF}_{m}(M\restriction
L^{\prime},N\restriction L^{\prime})$ for some $L^{\prime}\subset L$, then the
separating sentence $\phi$ can be chosen so that its non-logical symbols are
all in $L^{\prime}$. If $\tau$ is such that Abelard plays only in $M$, we can
make $\phi$ existential. If $\tau$ is such that Abelard plays only in $N$, we
can make $\phi$ universal. If Abelard wins with $\tau$ even the harder game in
which he has to win by finding an atomic (rather than literal) relation which
holds in $M$ but not in $N$, then we can take $\phi$ to be a positive
sentence.

Strategies in $\mbox{EF}_{m}(M,N)$ reflect structural properties of $M$ and
$N$. If we know a strategy of Eloise in $\mbox{EF}_{m}(M_{i},N_{i})$ for $i\in
I$, we can construct strategies of Eloise for EF games between products and
sums of the models $M_{i}$ and the respective products and sums of the models
$N_{i}$. This can be extended to so-called $\kappa$-local functors [4]. For an
example of the use of tree-decompositions, see e.g. [5].

Just as in the Evaluation Game, the EF game permits modifications which extend
the above two theorems to other logics. Accordingly, EF games are known for
infinitary logics, generalized quantifiers, and higher order logics. In modal
logic the corresponding game is called a bisimulation game. Even propositional
logic has an EF game although there are no quantifiers [6]. In the EF game for
team semantics the players moves teams, not elements [18].

The sentences arising from Theorem 5 are behind the Distributive Normal Forms
of J. Hintikka [9] and are known in infinitary logic as building blocks of
Scott Sentences [16].

In an important variant called the Pebble Game, the players can pick only a
fixed finite number of elements from the models but they can give up some
elements in order to make room for new ones. This game is closely related to
first order (or infinitary) logic with a fixed finite number of variables
(free or bound). It was introduced independently by N. Immerman and B. Poizat
in 1982. A good reference is [13].

##  5 Further work

The Evaluation Game, the Model Existence Game and the EF game go so deep into
the essential concepts of logic such as truth, consistency, and separating
models by sentences, that a lot of research in logic can be represented in
terms of these games. This may not be very interesting in itself. However, the
translations of the strategies between the games suggest a coherent uniform
approach to syntax and semantics and at the same time to model theory and
proof theory. Moreover, both the Evaluation Game and the EF game are oblivious
to whether the models are finite or infinite, which gives them a useful role
in computer science logic. Despite the vast literature on each of the three
games separately, there seems to be a lot of potential for the study of their
interaction as a manifestation of the Strategic Balance of Logic.

## References

  * [1] Samson Abramsky, Anuj Dawar, and Pengming Wang.  The pebbling comonad in finite model theory.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017.
  * [2] E. W. Beth.  Semantic entailment and formal derivability.  Mededelingen der koninklijke Nederlandse Akademie van Wetenschappen, afd. Letterkunde. Nieuwe Reeks, Deel 18, No. 13. N. V. Noord-Hollandsche Uitgevers Maatschappij, Amsterdam, 1955.
  * [3] Andrzej Ehrenfeucht.  An application of games to the completeness problem for formalized theories.  Fund. Math., 49:129–141, 1960/1961.
  * [4] Solomon Feferman.  Infinitary properties, local functors, and systems of ordinal functions.  In Conference in Mathematical Logic—London ’70 (Proc. Conf., Bedford Coll., London, 1970), pages 63–97. Lecture Notes in Math., Vol. 255\. Springer, Berlin, 1972.
  * [5] Martin Grohe.  The complexity of homomorphism and constraint satisfaction problems seen from the other side.  J. ACM, 54(1):Art. 1, 24, 2007.
  * [6] Lauri Hella and Jouko Väänänen.  The size of a formula as a measure of complexity.  In Åsa Hirvonen, Juha Kontinen, Roman Kossak, and Andrés Villaveces, editors, Logic Without Borders - Essays on Set Theory, Model Theory, Philosophical Logic and Philosophy of Mathematics, volume 5 of Ontos Mathematical Logic, pages 193–214. De Gruyter, 2015.
  * [7] Leon Henkin.  Completeness in the theory of types.  J. Symbolic Logic, 15:81–91, 1950.
  * [8] Leon Henkin.  Some remarks on infinitely long formulas.  In Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw, 1959), pages 167–183. Pergamon, Oxford, 1961.
  * [9] Jaakko Hintikka.  Distributive normal forms in the calculus of predicates.  Acta Philos. Fenn., 6:71, 1953.
  * [10] Jaakko Hintikka.  Form and content in quantification theory.  Acta Philos. Fenn., 8:7–55, 1955.
  * [11] Jaakko Hintikka.  Language-games for quantifiers.  In Nicholas Rescher, editor, Studies in Logical Theory, pages 46–72. Blackwell, 1968.
  * [12] H. Jerome Keisler.  Logic with the quantifier “there exist uncountably many”.  Ann. Math. Logic, 1:1–93, 1970.
  * [13] Phokion G. Kolaitis and Moshe Y. Vardi.  Infinitary logics and $0$-$1$ laws.  volume 98, pages 258–294. 1992.  Selections from the 1990 IEEE Symposium on Logic in Computer Science.
  * [14] David W. Kueker.  Countable approximations and Löwenheim-Skolem theorems.  Ann. Math. Logic, 11(1):57–103, 1977.
  * [15] Michael Makkai.  On the model theory of denumerably long formulas with finite strings of quantifiers.  J. Symbolic Logic, 34:437–459, 1969.
  * [16] Dana Scott.  Logic with denumerably long formulas and finite strings of quantifiers.  In Theory of Models (Proc. 1963 Internat. Sympos. Berkeley), pages 329–341. North-Holland, Amsterdam, 1965.
  * [17] Raymond M. Smullyan.  A unifying principal in quantification theory.  Proc. Nat. Acad. Sci. U.S.A., 49:828–832, 1963.
  * [18] Jouko Väänänen.  Dependence logic, volume 70 of London Mathematical Society Student Texts.  Cambridge University Press, Cambridge, 2007.  A new approach to independence friendly logic.
  * [19] Jouko Väänänen.  Models and games, volume 132 of Cambridge Studies in Advanced Mathematics.  Cambridge University Press, Cambridge, 2011.
  * [20] Johan van Benthem.  Logic in games.  MIT Press, Cambridge, MA, 2014.
  * [21] Ludwig Wittgenstein.  Philosophical investigations.  The Macmillan Co., New York, 1953.  Translated by G. E. M. Anscombe.