Reinforcement learning for EV charging demand coordination
Lahariya M et al.

$\Delta t^\textit{slot}$
$\Delta t^\textit{depart}$
$\Delta t^\textit{charge}$
$\Delta t^\textit{flex}$

mode = title]
Computationally efficient joint coordination of multiple electric vehicle charging points using reinforcement learning

1]Manu Lahariya

2]Nasrin Sadeghianpourhamami

1]Chris Develder

[1]IDLab, Ghent University – imec, Technologiepark Zwijnaarde 126, 9052 Gent
[2]62 Steacie Drive, Suite 102, Ottawa, Ontario, Canada, K2K 2A9

A major challenge in today's power grid is to manage the increasing load from electric vehicle (EV) charging.
Demand response (DR) solutions aim to exploit flexibility therein, the ability to shift EV charging in time and thus avoid excessive peaks or achieve better balancing.

Whereas the majority of existing research works either focus on control strategies for a single EV charger, or use a multi-step approach (a first high level aggregate control decision step, followed by individual  control decisions), we rather propose a single-step solution that jointly coordinates multiple charging points at once.

In this paper, we further refine an initial proposal using reinforcement learning (RL), specifically addressing  computational challenges that would limit its deployment in practice.

More precisely, we design a new Markov decision process (MDP) formulation of the EV charging coordination process, exhibiting only linear space and time complexity (as opposed to the earlier quadratic space complexity).
We thus improve upon earlier state-of-the-art, demonstrating 30% reduction of training time in our case study using real-world EV charging session data. Yet, we do not sacrifice the resulting performance in meeting the DR objectives: our new RL solutions still

improve the performance of charging demand coordination by 40-50% compared to a business-as-usual policy (that charges EV fully upon arrival) and 20-30% compared to a heuristic policy (that uniformly spreads individual  charging over time).

Reinforcement learning (RL),
Markov decision process (MDP),
Fitted Q-iteration (FQI),
Demand response (DR),
Electric vehicle (EV)

$s'$The next state from $s$
Time left until departure
Time needed for charging completion
Flexibility (time charging can be delayed)
Duration of a decision slot
Maximum number of decision slots
Maximum connection time
Number of jointly coordinated charging stations
$N_s$Number of connected EVs in state $s$
$N_d$Number of EVs with flexibility $= d$
Representation of state $s$
Aggregate demand in state $s$ (matrix state)
Aggregate flexibility in state $s$ (vector state)
Action taken in state $s$
Locally scaled action taken in state $s$
${U}_{s,l}$Set of possible locally scaled actions from state $s$
Globally scaled action taken in state $s$
${U}_{s,g}$Set of possible globally scaled actions from state $s$
Quadratic cost function
Linear cost function based on the average of preceding $E$ episodes
Linear cost function based on the median of preceding $E$ episodes
$L_{\pi}^{e}$Load in episode $e$ by policy $\pi$
$\tilde{L}_{\pi}^{e}$Normalized load in episode $e$ by policy $\pi$
$\mathcal{B}_{a}^{b}$EV session data from episode $a$ to episode $b$
$\mathcal{V}_{t}$Set of EVs in the system at time $t$

§ INTRODUCTION

Reliable operation of smart grids requires efficient load management, which can be achieved by demand response (DR) algorithms. A DR algorithm coordinates the demand-supply of energy to meet an objective, load balancing, maximizing profit, Traditional DR is based on model predictive control (MPC) <cit.>, where an optimization problem is solved using a predefined model. However, deployment of such model-based DR algorithms is limited due to uncertainties associated with the assumed models and lack of scalability and generalizability <cit.>.

Model-free approaches circumvent the aforementioned challenges by formulating the problem using a Markov decision process (MDP) where the optimum policy is learned by interacting with the environment <cit.>.

In recent years, data-driven reinforcement learning (RL) algorithms have been proposed based on an MDP for exploiting the user flexibility to coordinate the demand <cit.>.
In reinforcement learning, a coordinating agent learns by iteratively interacting with the environment and taking control actions.
The agent receives a reward/cost in each interaction and is thus trained to maximize/minimize the long term reward/cost.

The underlying MDP framework, which will be used in RL to find a (close to) optimal DR policy, is defined in terms of

* a $state$ representation,

* an $action$ representation, and

* a reward/cost signal, a $cost$ function
The specific DR objective (peak shaving <cit.>, load balancing <cit.>, valley filling <cit.>) is realized by appropriately designing the cost function, reflecting the utility of a certain action.
Yet, designing a meaningful but manageable MDP is challenging in practice. First of all, the complexity of the $state$-$action$ representation affects the space and computational complexity of the RL based control policy, thus potentially limiting its scalability (computational requirements that depend on the number of EVs we aim to control jointly). Furthermore, an incorrect or uninformative cost function can degrade or annihilate the performance of the RL based control policy (known as the credit-assignment problem <cit.>). Thus, the MDP design can greatly impact the performance and optimization of an RL based control policy <cit.>.

This paper defines and evaluates novel MDP formulations for  fleet charging coordination, which can be used to implement state-of-the-art RL-based DR.
The proposed formulations represent a joint  coordination scenario, where we control  multiple  chargers jointly at once. This is more complicated than the common setting of controlling a single  charging point <cit.>.
The proposed MDPs are defined using

* $state$-$action$ representations to facilitate scalability, and

* computationally linear cost functions to expedite learning
We will experimentally demonstrate the superiority of the newly engineered MDP in
terms of training time and space requirements
compared to the original MDP representation used in an
initial proof-of-concept paper <cit.>.

In summary, the main contributions of this paper on jointly coordinating EV charging demand to reduce the resulting peak load include:

* the definition of novel $state$-$action$ representations based on aggregate demand and compact aggregate flexibility characterization (subsec:mdp),

* the definition of novel linear cost functions that provide information on a posteriori established optimal  charging coordination over the recent past (sec:costfun), and

*  the quantitative analysis of the impact of the MDP formulation on the learning speed of the RL based control policy (sec:results).

For <ref>, we provide experimental results using real-world EV charging data and the fitted $Q$-iteration (FQI) algorithm <cit.> (with a neural network based function approximation, sec:batchRL).
Additionally, we compare our RL policies with both a business-as-usual policy (that charges EV fully upon arrival), and a heuristic policy (that uniformly spreads individual EV charging over time). In particular, we define experiments (sec:ExpDetails) to answer the following questions:

*  What features (connection time, required energy, etc.) should be used to define $state$-$action$ representations?

What is the impact of the cost function definition on the learning speed and performance of the learned policy?

*  What is the impact of our MDP formulation on

* the performance of the RL policy, and

* the space and computation time complexity of learning such optimum RL policy?

*  What is the impact of varying parameter settings during training on the performance of the RL policy?[The parameters of interest are

* the number of preceding days used in cost function,

* the time span of the training data, and

* the number of iterations in FQI algorithm.

For details see sec:Experiments and sec:results_crd.]

Conclusions and open issues for future work are presented in sec:conclusions.

§ RELATED WORK

In recent years, RL has attracted attention to facilitate data-driven DR to coordinate  charging. Researchers have exploited RL for charging coordination of individual s to achieve objectives such as cost reduction, providing customized services, For example, <cit.> achieve 10%-50% reduction in long term cost compared to business-as-usual using a RL control policy with a MDP framework where

* the states are based on charging prices, price fluctuations, and timing variables, and

* the actions are based on daily energy consumption
Controlling the charging/discharging of an individual EV under price uncertainty for providing vehicle-to-grid (V2G) services is studied by <cit.>. Their MDP has

* a state based on the hourly electricity price, state-of-charge, and time left till departure, and

* an action based on the decision of charging, delaying the charging, and discharging
Cost-saving by scheduling charging/discharging of a single  for a user is studied by <cit.>, where the MDP is based on

* a state defined using electricity price and current state of charge of  and,

* a binary action of either charging or discharging
As opposed to the previously stated cases <cit.>, where the authors study controlled charging of a single , we study the joint coordination of a group of s. Additionally, the objective of our control policy is load flattening in contrast to the objective of cost-minimization.

For the collective charging of a group of s, previous studies have proposed stepwise approaches. <cit.> propose a three-step DR algorithm for a group of s, based on which <cit.> learn a collective charging plan for s using batch RL. Both their three-step DR approaches comprise an aggregation step, an optimization step, and a real-time control step. A heuristic algorithm is used in the control step to dispatch the energy corresponding to the charging actions determined in the optimization step. Batch RL is employed to generate these actions in the optimization step and trained using the aggregated constraints for each .
A two-step time-of-day pricing demand response is proposed in <cit.>, where an aggregator agent sells energy to clusters of EVs. Interactions in these aggregator agents is formulated as a two-step optimization problem, where,

* at the top level the aggregator maximizes its benefits, and,

* at the lower level the rational of EV driver is optimized

Contrary to these stepwise DR approaches based on separate aggregation and optimization steps, our DR jointly controls all s directly based on an efficient aggregated state representation.

The current paper more specifically addresses real-world implementation and scalability challenges of RL-based control, by defining and exploring state-of-the-art MDP formulations. In our previous work <cit.>, we provided a proof-of-concept for RL-based DR for joint  coordination (with MDP formulation that has quadratic cost function and $state$-$action$ representation). In the current work we further focus on the MDP formulation (which we refine) and the learning speed of said RL-based DR.
More specifically, in this paper, we,

* define new compact $state$-$action$ representations that scale linearly with system capacity and coordination horizon in contrast to exponential scaling in <cit.>,

* propose computationally linear cost functions compared to the quadratic cost function in <cit.>, and

* we study the impact of our cost functions on RL based control policy optimization (by evaluating the computation time per iteration in FQI algorithm), in contrast, no such analysis is done in <cit.>.

In the next section, we define the different components of the MDP.

§ MARKOV DECISION PROCESS (MDP)

Our main focus is flattening the load stemming from charging a group of s, we aim to minimize the peak-to-average ratio of the aggregate charging load of the group of EVs. This objective is achieved by minimizing the long term cost or T-step return in a Markov decision process (MDP). We use the MDP framework for model-free coordination for aggregated electric vehicle charging, by formulating the charging coordination as a discrete sequential decision making process. The learning objective is to find an optimum coordinated charging policy such that the long term expected cost is minimized.

We use RL to learn an optimum policy that achieves the said load flattening objective by jointly coordinating the charging demand of s connected to  charging stations. We assume that state transition probabilities are a priori unknown, thus, the policy is learned from interacting with the environment, by taking actions and observing the rewards/costs and next state. In the following subsections, we define two $state$ representations, two $action$ representations, and different cost functions that can be used to define the MDP formulation.

§.§ State Representations

An individual EV charging session is characterized by the

* EV arrival time,

* EV departure time (),

* required energy, and

* charging power
. We implicitly assume the same charging power for all EVs and compute the time needed to complete the charging () by dividing the required energy with the charging power. A state representation is defined using the information from these features.
At timesetp $t$, the number of s in the system is , and the available information can be summarized as:

\begin{equation}
\mathcal{V}_t = \{(\Delta t ^{depart} _ {1}, \Delta t ^{charge} _ {1}), \dots, (\Delta t ^{depart} _ {N_{s}}, \Delta t ^{charge} _ {N_{s}})\}
\label{eqn:matrixsetinfo}
\end{equation}

The underlying idea of charging demand coordination is to exploit the available flexibility in the system. Thus, this flexibility can be used to define the state representation. The flexibility, how much charging can be delayed, offered by each EV is represented by  =  $-$ . We thus redefine the avaliable information as:

\begin{equation}
\mathcal{V}'_t = \{(\Delta t ^{flex} _ {1}), \dots, (\Delta t ^{flex} _ {N_{s}})\}
\label{eqn:vectorsetinfo}
\end{equation}

The state representation is of the form $s=(t,$ ), where $t$ is the timeslot ($\ie t \in \{1, \dots, $ $\}$)
and  provides the aggregate information of all EVs in the system. A binning algorithm inspired by <cit.> is used to aggregate the EVs connected to the charging stations while retaining the required information to facilitate learning.

We previously <cit.> defined a matrix state representation  using set $\mathcal{V}_t$. We now propose a new compact and improved vector state representation  using set $\mathcal{V}'_t$.

* Matrix State Representation (): The aggregate demand represented in a 2D grid, with one axis representing , and other . The element of  at position $(i, j)$ counts the number of s in the corresponding (, ) bin, for which $i$ =  and $j$ = .

* Vector State Representation (): The aggregate flexibility represented using a vector. The element of  at position $i$ counts the number of s in the corresponding () bin, for which $i$ = .

The maximum number of decision slots is  = / ( is the maximum connection time). For an exemplary scenario with  = 4 and  = 3, fig:matrix_rep provides the matrix state representation () and fig:vector_rep provides the vector state representation (). At time $t$ = 1, assume that we have $N_s$ = 3 cars: $c_1$ = (, ) = (3,2), $c_2$ = (, ) = (2,1) and $c_2$ = (, ) = (2,2) with no other arrivals during the control horizon.
The resulting states are divided by  = 4 to maintain generalizability in our state representations. We have shown previously that the policy learned from the  representation can be generalized to a different number of charging stations if the state representation is normalized by system capacity . To maintain this generalizability in our new state representations, we perform the same normalization.

Fully observable matrix state representation () that provides aggregate demand.

Partially observable vector state representation () that provides aggregate flexibility.

Aggregate representations of state $s$ with system capacity  = 4, and decision slots  = 3. Each state is characterized by timeslot $t$ and an aggreate state representation, for example, $s$ = ($t$,). (Yellow: =0; Blue: =1; Green: =2)

In the matrix state representation, s binned into cells on the main diagonal of  (i.e., $i$ = $j$) have zero flexibility while
the ones binned into cells on the upper diagonals of  are
flexible charging requests. In a vector state representation EVs binned into the first cell of  (i.e., $i$ = 0) have zero flexibility while
the ones binned into cells after the first cell of  are
flexible charging requests. Negative , corresponding to the lower diagonals of , would indicate s for which the requested charging demand cannot be fulfilled (> ).

The matrix state representation summarizes all the information available from the environment and results in a fully observable setting. The information about the flexibility ( = $-$) can also be identified from the matrix state representation. The vector state representation only summarizes the information about flexibility, and results in a partially observable setting. Yet it still is highly relevant for making charging decisions. We use the matrix and vector state representations to answer q:stateactionfeatures (What features should be used to define $state$-$action$ representations?), where these representations are based on different features and provide different levels of detail, observability, to learn the control policy. Note that the vector state representation results in a smaller number of states in the state space of the problem compared to the matrix state representation.

§.§ Action Representations

The action our agent needs to decide on is
which EVs to charge and which ones' charging to delay in state $s$ = (t, ). We will make the decisions based on flexibility (): s that offer similar flexibility will be charged/delayed together. Thus, actions are represented by a vector  where the element at position $d$, given by , provides the number of s to charge in flexibility bin  = $d$ ($d \in \{0, \dots,$ $-$ 1}). The total number of s in flexibility bin  = $d$ is . Thus, the element  of the action vector will be a number in {0, …, }. For example,  = 3 means that 3 cars offer the same flexibility, and  is the number of cars that will be charged, and thus lies in {0, 1, 2, 3}.

We scale the elements of action  to be numbers in [0,1], representing the fraction of cars that we will charge, we divide  by  or .
We previously <cit.> divided action  by  to estimate a locally scaled action , which is difficult to interpret as  depends on $d$ and changes after each interaction with the system. To improve interpretability, we now divide action  by  to estimate a globally scaled action , and keeping the scaling factor fixed.

We thus have the following two action representations:

* Locally Scaled Action Representation (): Each element of the action vector is divided by the total number of cars in its flexibility bin,  = /.

* Globally Scaled Action Representation ():  Each element of the action vector is divided by the system capacity (),  = /.

For the exemplary scenario stated before with  = 4 and $N_s$ = 3,

fig:action_spaces illustrates how  and  are constructed from both state representations ( and ) and the counts . We will ensure that  charging demands are never violated, the s for which  = 0 will always be charged. Thus, there are 3 possible actions to take in this state. For the other two s the possible actions are: charge none, charge one or charge both. State representations are used to estimate an intermediate vector in which the value at position $d$ represents , the total number of s with flexibility $d$. This intermediate vector can be used to define action space $U_{s,l}$ for locally scaled actions and action space $U_{s,g}$ for globally scaled actions.

Action spaces for different state representations ($U_{s,l}$: Action space with locally scaled actions, $U_{s,g}$: Action space with globally scaled actions). Derived from the matrix () or vector () state representations for a system with  = 4  charging points. (Yellow: =0; Blue: =1; Green: =2)

§.§ Cost Function

Our objective is to flatten the aggregate  charging load, while fulfilling the charging demand for each EV before its departure. This will be achieved through defining a cost function denoted as $C(s,$$,s')$ quantifying the utility of a transition from state $s$ to $s$' by taking action . Each state $s$ is given by ($t$, ), where $t$ is the timeslot and  is the state (matrix or vector state representation).

The cost function will clearly be related to charging load, power consumption. Power consumed from all s by taking action  in state  will be represented by $P (\textbf{x}_s,\textbf{u}_{s})$:

\begin{equation}
P (\textbf{x}_s,\textbf{u}_{s}) = \sum\limits^{S_{max}-1}_{d=0} N_d \textbf{u}_{s}^d
\label{eqn:policypowerconsumption}
\end{equation}

§.§.§ Quadratic Cost Function ()

In our previous work <cit.>, we defined a cost function based on the squared power consumption. This quadratic cost function is defined in eq:RL_quadcost where the cost for taking action  in state $s$ =$(t,$$)$ amounts to the squared charging power consumption.

\begin{align}
\textit{C}_q(s, \textbf{u}_{s}, s') &= \textit{C}_q(\underbrace{(t,\textbf{x}_s)}_{s},\textbf{u}_{s},\underbrace{(t+1,\textbf{x}_{s'})}_{s'}) \nonumber \\
\label{eq:RL_quadcost}
\end{align}

Minimizing the long term cost based on this function translates to load-flattening across all  charging stations.

§.§.§ Linear Cost Functions ( and )

We define cost functions that utilize the information from optimum policies of the preceding days (where we have information for all  sessions). This is based on the assumption that days with similar  session characteristics (arrivals, departures and required energy) will have similar optimal solutions.
The optimal solution, power consumption for each timeslot, for a prior day can be calculated using an all-knowing optimum policy (by formulating the problem as a quadratic optimization problem). The power consumed from all s under optimal policy coordination is represented by $P^{opt} (t,e)$, where $t$ is timeslot and $e$ represents the corresponding episodic `day'.[
We will assume that  charging stations empty at the end of a day. Thus, an episodic `day' constitutes the period during which s are present, and ends with an empty car park at the end of the day.
For details see sec:training]
For the set of preceding $E$ episodic `days', the consumed powers from episode $e-1$ to $e-E$ can be summarized in the set defined in eqn:setpastEopt, where $e$ is the current episodic `day'.

\begin{equation}
\mathcal{P}^{opt}_{t,e,E} = \{P^{opt} (t,e-1),\dots,P^{opt} (t,e-E) \}
\label{eqn:setpastEopt}
\end{equation}

By utilizing the information about the optimal policy available in this set, we define two cost functions. These cost functions are based on the absolute difference between power consumed, $P^{\pi}(\textbf{x}_s,\textbf{u}_{s})$, and either the average (eq:RL_linavgcost) or the median (eq:RL_linmedcost) of set $\mathcal{P}^{opt}_{t,e,E}$.

\begin{equation}
\textit{C}_{l,a}^E(s, \textbf{u}_{s}, s') \triangleq \left| P^{\pi}(\textbf{x}_s,\textbf{u}_{s}) - \text{avg}(\mathcal{P}^{opt}_{t,e,E}) \right|
%\sum \mathcal{P}^{opt}_{t,e,E}}{E}
\label{eq:RL_linavgcost}
\end{equation}

\begin{equation}
\textit{C}_{l,m}^E(s, \textbf{u}_{s}, s') \triangleq \left| P^{\pi}(\textbf{x}_s,\textbf{u}_{s}) - \text{median}(\mathcal{P}^{opt}_{t,e,E}) \right|
\label{eq:RL_linmedcost}
\end{equation}

The second term of these cost functions is the average/median of power consumption by optimum policy coordination for the preceding $E$ episodic `days'. Minimizing the long term cost calculated from these cost functions translates to reducing the deviation of the current charging policy ($\pi$) from the optimum policies of preceding episodes. Hence, the current charging policy ($\pi$) learns to mimic the behavior, and subsequently the objective, of these optimum policies. These cost functions will be effective for any coordination objective (cost-saving, peak-shaving, ), as the current charging policy approximates the optimum policies of preceding episodes, which can be trained for any objective. We consider the case of load-flattening to test these linear cost functions against the quadratic cost function to answer q:costfunctiondef (Impact of the cost function definition on the learning speed and performance of the learned policy?).

§.§ State-Action Value Function

Solving the MDP means finding an optimum control policy

$\pi$ : $S \to U$ that minimizes the expected $T$-step cost, which for a policy $\pi$ at timestep $t$ is given in eq:RL:Ereturn.   The control time horizon in our setting is given by $T=$ . The policy can be identified by evaluating a state-action value function, the $Q$-function, and selecting the action that minimizes it at each timestep. This $Q$-function is provided in eq:RL:Qfunc.

\begin{equation}\label{eq:RL:Ereturn}
J^{\pi}_T(s) =\mathbb{E} \left[\sum_{i=t}^{t+T}{C(\underbrace{(t,\textbf{x}_s)}_{s},\textbf{u}_{s},\underbrace{(t+1,\textbf{x}_{s'})}_{s'})}\right]
\end{equation}

\begin{equation}\label{eq:RL:Qfunc}
Q^{\pi}(s,\textbf{u}_s) =\mathbb{E} \left[C(s,\textbf{u}_s,s')+J^{\pi}_T(s')\right].
\end{equation}

The $Q$-function corresponding to the optimum policy represented by $Q^{*}(s,\textbf{u}_s)$  = $\min_{\pi}Q^{\pi}(s,\textbf{u}_s)$ can be calculated if the transition probabilities between states are known. However, these are unknown in our setting, hence we use a learning algorithm to approximate the optimum $Q$-function as $\widehat{Q}^{*}(s,\textbf{u}_s)$. In the next section, we provide details of the batch reinforcement learning algorithm used to learn $\widehat{Q}^{*}(s,\textbf{u}_s)$.

§ BATCH REINFORCEMENT LEARNING

We employ batch mode reinforcement learning to learn the $Q$-function, $\widehat{Q}^{*}(s,\textbf{u}_s)$. In batch reinforcement learning algorithms, optimization is performed on data collected in past experiences rather than online interactions from the environment. We use the historical EV data (arrivals, departures, and required energy) and a random policy to collect past experiences. Each experience is defined in terms of

* an initial state $s$,

* the action taken ,

* the resulting state $s'$ after taking the action, and

* the associated costs $C(s,$$,s')$
An experience set denoted by $\mathcal{F}$ contains tuples $(s,$$,s',C(s,$$,s'))$ and is generated based on the state representation, action representation, and cost function.

Fitted Q-iteration (FQI):

We use the Fitted Q-iteration <cit.> algorithm to learn $\widehat{Q}^{*}(s,\textbf{u}_s)$ from $\mathcal{F}$.
A fully connected Artificial Neural network (ANN) is used as function approximation for $\widehat{Q}^*(s,\textbf{u}_s)$.

State-Action space:

The past experience set $\mathcal{F}$ is generated by taking actions (randomly or deterministically) given a state $s$. The number of all possible actions given a state $s$ is given by eq:RL:stateacspace, where the second term reflects the single “choice” we have for the cars without flexibility ( = 0).

\begin{equation}\label{eq:RL:stateacspace}
\left|\textbf{U}_{s}\right| = \prod_{d=1}^{S_{\textit{max}}-1}\left(N_d + 1 \right).
\end{equation}

§ EXPERIMENT SETUP

In this section, we provide the details of the real-world data used in our experiments. We outline the experiments that were performed to answer our research questions. We also provide performance metrics used to evaluate the trained control policies.

Experience     State     Action     Cost Function     RL Trained     State Space

Set     Representation     Representation          Policy     Complexity

$\mathcal{F}_1$     Matrix (t, )     Locally Scaled ()     Quadratic ()     RL$_{ml}$     $\bigO(S_{max}^2)$

$\mathcal{F}_2$     Vector (t, )     Locally Scaled ()     Quadratic ()    RL$_{vl}$     $\bigO(S_{max})$

$\mathcal{F}_3$     Matrix (t, )     Globally Scaled ()     Quadratic ()    RL$_{mg}$     $\bigO(S_{max}^2)$

$\mathcal{F}_4$     Vector (t, )     Globally Scaled ()     Quadratic ()    RL$_{vg}$     $\bigO(S_{max})$

Experience sets ($\mathcal{F}$) generated for exp:obs (observability) to evaluate the effect of information provided by $state$-$action$ representation on the performance of learned RL control policy.

Experience     State     Action     Cost Function     RL Trained     State Space

Set     Representation     Representation          Policy     Complexity

$\mathcal{F}_5$     Vector (t, )     Globally Scaled ()     Quadratic ()    RL$_{q}$     $\bigO(S_{max})$

$\mathcal{F}_6$     Vector (t, )     Globally Scaled ()     Linear (Average) ()    RL$_{a}$     $\bigO(S_{max})$

$\mathcal{F}_7$     Vector (t, )     Globally Scaled ()     Linear (Median) ()    RL$_{m}$     $\bigO(S_{max})$

Experience sets ($\mathcal{F}$) generated for exp:crdassignment (credit-assignment) to evaluate the effect of different cost functions on the performance of learned RL control policy.

§.§ Data and Model Specifications

We use a real-world dataset to train the RL based control policy. Our dataset is derived from real-world data collected by ElaadNL since 2011, from 2500+ public charging stations <cit.>, from which we selected the data for 2015. We represent this data in an episodic format, such that each episodic `day' starts at 7 am and ends 24 hours later (the day after at 7 am). Further, we assume an empty car park at end of each episode (all s leave the charging stations). Thus, irrespective of the starting state of the episode, we always reach the same terminal state characterized by an empty car park (all elements of the  or  are zero). A terminal state stabilizes the learning process in FQI that adopts a neural network based function approximation <cit.>.
The time granularity is set to  = 2 h, which means  = 12 timeslots in each episodic `day'.
We jointly coordinate  = 10 charging stations,[We select the 10 busiest  charging stations (based on the total number of transactions).]
at most 10 EVs can be connected simultaneously.

For training the RL agent we start by creating the experience sets $\mathcal{F}$. This set contains the past experience for multiple episodes. For each episode, we start from the first state of a day characterized by ($t_1, x_1$) and randomly choose an action from the set of possible actions in each state and observe the next state and the associated state transition cost until the terminal state is reached (i.e., ($t_T, x_T$)). This single sequence of states and actions is referred to as a trajectory. Each transition in this trajectory is saved in the experience set in the form of tuples $(s,$$,s',C(s,$$,s'))$. We randomly generate 5000 trajectories for each episode.

An artificial neural network (ANN) architecture is used to estimate the $Q$-function from the experience set $\mathcal{F}$ using FQI. This network consists of an input layer and 2 hidden layers with ReLU activation functions.  There are
128 and 64 neurons in the first and second hidden layers
respectively. The output layer has a single neuron with a linear activation function. The input of the network is a vector that is created by combining the state and action. In case of matrix state representation we concatenate the matrix rows to obtain an input vector of length
145 (()$^2$ +  + 1), and in the case of vector state representation, the length of the input vector is 25 ( +  + 1). We use Huber
loss <cit.> instead of mean-squared-error for improving the stability in learning in our algorithm <cit.>. All experiments are run on a system with an Intel Xeon E5645 3.1 GHz processor and 16 GB RAM. We outline two experiments below that are used to answer our research questions.

Increasing window validation used in exp:obs

Rolling window validation used in exp:crdassignment

Train and test data selected in different validation methods used in experiments

§.§ Experiments

We define two experiments utilizing the ElaadNL transactions data of 2015 to answer our research questions. A dataset of transactions from episode $a$ to $b$ is represented by $\mathcal{B}_{a}^{b}$. A validation set thus contains a training dataset $\mathcal{B}_{a}^{b}$ and a testing dataset $\mathcal{B}_{c}^{d}$. We evaluate the performance of RL based control policies across all validation sets.

We design an experiment to evaluate the impact of different $state$-$action$ representations and answer q:impactofmdp (Impact of MDP formulation on the performance of the RL policy?) and a part of q:parametersettings (What is the impact of varying parameter settings during training the RL agent?).
Based on different $state$-$action$ representations defined in sec:state and sec:action, we generate 4 different experience sets. The details of these experience sets are summarized in table:SArepExpsets. Each experience set is used to learn a control policy. For example, RL$_{ml}$ is a trained control policy from experience set $\mathcal{F}_1$ which has matrix state representation and locally scaled action representation.

The $state$-$action$ representations affect the space complexity of an experience set ($\mathcal{F}$), and the learning speed of the control policy. To compare different $state$-$action$ representations (table:SArepExpsets), we perform an increasing window validation where the size of training datasets are different (fig:increasingwindow). The training datasets are generated from $\{30, 60,\dots,270\}$ episodes, and we test on the immediate next 30 episodes. For example, the first validation set has training data $\mathcal{B}_{1}^{30}$ (data from {1, …, 30} episodes or 1 Jan 2015 to 30 Jan 2015) and testing data $\mathcal{B}_{31}^{60}$ (data from {31, …, 60} episodes).

Credit Assignment:

We define another experiment to investigate the impact of the cost definition on the training and performance of the learned optimum policy to answer q:parametersettings (What is the impact of varying parameter settings during training on the performance of RL agent?). Credit is assigned to each transition (taking an action on a given state) based on the defined cost function in the MDP formulation. Based on the different cost functions defined in sec:costfun, we generate 3 different experience sets.

summarized in table:CAExpSets. Each experience set is used to train a control policy, for example, RL$_{q}$ is a trained control policy from experience set $\mathcal{F}_5$ which uses a quadratic cost function.

In the case of different cost functions, the space complexity of the experience set ($\mathcal{F}$) is not affected. Linear cost functions are dependent on the optimal charging policies for the preceding $E \in \{1,5,10\}$ days (eq:RL_linavgcost and eq:RL_linmedcost).
To train the policies on the same size of data, but with different preceding days, we evaluate the cost functions using a rolling window validation where the size of training sets is kept fixed (fig:rollingwindow).

Data from used for weekdays, which have similar  session characteristics (shown previously in <cit.>). The training dataset has data from weekdays of 90 episodes, the testing dataset has weekdays of 30 episodes, and the rolling window comprises 30 episodes.

§.§ Performance Evaluation

Policy Performance:

To evaluate the performance of the learned policy, we use a metric defined as normalized load,
which is relative to the load achieved by the optimal policy (obtained from formulating the load flattening problem as a quadratic optimization problem). The quadratic load incurred in an episode $e$ by using policy $\pi$ is defined by eq:policyload.

The normalized load for episode $e$ is calculated using eq:RL:normalizedload. If the trained control policy $\pi$ reaches the optimal policy, then $\tilde{L}_{\pi}^{e}$ = 1.

\begin{equation}
L_{\pi}^{e} = \sum\limits_{T} \left( \sum\limits^{S_{max}-1}_{d=0} N_d \cdot \textbf{u}_{s}^d   \right)^{2}
\label{eq:policyload}
\end{equation}

\begin{equation}\label{eq:RL:normalizedload}
\tilde{L}_{\pi}^{e}=\frac{L_{\pi}^{e}}{L_{\text{opt}}^{e}}
\end{equation}

Furthermore, for performance comparison we include the normalized load for

* BAU: a business-as-usual (BAU) policy characterized by continuously charging each  upon arrival, and

* Heur: a discrete-action heuristic policy that assumes that individual EVs are charged uniformally over their entire connection time.[Specifically, the heuristic spreads the $c$ slots during which the EV needs to charge over the total number of available slots $d$. This amounts to distributing $d - c$ no-charge slots evenly over the total number of $d$ slots, thus splitting them into $d - c + 1$ parts. Assuming for simplicity that $c \geq d/2$, this means we insert a no-charge slot every $\floor{d / (d - c + 1)}$ other slots.]

Policy Training Time:

Defined as the time it takes for RL agent to be trained. During FQI, we run 12 iterations to train the ANN for each selected training dataset. We record the time for these iterations for all the learned policies.

§ EXPERIMENTAL RESULTS

In this section, we provide the results from exp:obs and exp:crdassignment to answer q:impactofmdp-q:parametersettings. More specifically, we analyze the performance and training time of control policies trained on different $state$-$action$ representations (exp:obs) and different cost functions (exp:crdassignment).

§.§ Observability: State-Action Representation

Normalized load for RL based control policies trained with different $state$-$action$ representations. Each box is constructed from normalized loads of 30 episodes in the test set. (Wilcoxon test p-values: statistically significant difference for p-value < 0.05)

Training time for RL based control policies trained with different $state$-$action$ representations. (Points and solid lines: Average value calculated across all validation sets, Shaded area: 25 to 75 percentile)

We evaluate policies trained on different $state$-$action$ representations by analyzing the results from exp:obs (sec:Experiments). fig:Load_SA_compare provides the normalized load ($\tilde{L}_{\pi}^{e}$) comparison for control policies for different MDPs.

Each box is constructed from 30 normalized loads ($\tilde{L}_{\pi}^{e}$) calculated for each episode in the test set. We also perform a Wilcoxon signed-rank test on these normalized loads to quantify statistically significant difference among different control policies (significant for p-values $\leq$ 0.05). Using RL based demand coordination provides 30%-50% improvement in performance compared to the BAU control policy, depending on the training set size and the underlying $state$-$action$ representation in the MDP formulation.

Locally scaled actions are scaled with , the number s in flexibility bin  = $d$, in contrast to globally scaled actions which are scaled with , maximum system capacity (sec:action). Locally scaled actions train a better performing control policy compared to globally scaled actions. The reason is that locally scaled actions explicitly calculate percentage of s in each flexibility bin, which helps in learning a superior policy, in contrast to globally scaled actions where this information is implicit.
This performance gain increases with the increase in training data size. For a provided action representation, both matrix and vector state representations have similar performance. Furthermore, the performance of the control policies improves with an increase in the training data size, where we see that $RL_{vl}$ (vector state, locally scaled actions) and $RL_{ml}$ (matrix state, locally scaled actions) outperform the other policies.

Training time depends on the MDP formulation as each $state$-$action$ representation has different space complexity. Utilizing vector state representation in MDP formulation leads to linear space complexity $\mathcal{O}(S_{max})$, compared to the quadratic space complexity in matrix states representations, $\mathcal{O}(S_{max}^2)$  (table:SArepExpsets). This results in a reduction in training time of control policies trained using vector state representations compared to matrix state representations, as shown in fig:Time_SA_compare.

Training time increases with the number of episodes in the training data. We note that local scaling of actions decreases the training time compared to global scaling, and the lowest training times are reported for  $RL_{vl}$ (vector state, locally scaled actions). The training time for $RL_{vl}$ policy is 30% less than the training time for $RL_{mg}$.

Policies learned from vector state representations perform similar to the policies learned from matrix state representations. Thus, information about flexibility (vector state representation) is enough to train a good policy, which answers q:stateactionfeatures (What features should be used to define $state$-$action$ representations?).

Furthermore, training a control policy on a partially observable MDP (such as a MDP based on vector state representation and locally scaled actions) takes approximately 20%-30% less time compared to the fully observable MDP. This answers q:impactofmdp (effect of different MDP formulations on RL policy?), where we note that policies trained using MDPs based on vector states and locally scaled actions outperform other polices, are space-efficient, and are computationally less expensive. Furthermore, we notice that performance of RL policies increases with increase in the time span of training data, which answers a part of q:parametersettings (impact of varying parameter settings?).

§.§ Impact of Cost Functions Definitions

Average normalized load per iteration. Linear cost functions with $E$ = 1, optimum solution of one preceding day ($C_{l,a}^1$ and $C_{l,m}^1$ ). (Average of all episodes and all validation test sets)

Normalized load for RL based control policies with linear cost functions that use $E \in \{1,5,10\}$. (Wilcoxon test p-values: statistically significant different for p-value<0.05)

Results for RL based control policies trained with different cost functions

The performance of a trained control policy depends on the cost function, where an effective cost function helps to achieve faster convergence by providing informative rewards. To study the effect of cost functions on performance and convergence, we analyze the results of exp:crdassignment (sec:Experiments). We use the FQI algorithm to train control policies using MDP formulations characterized by the different cost functions defined in sec:costfun.
fig:load_costfuns compares the average normalized load incurred in different control policies. Control policies are evaluated in the test set after each iteration, and the average normalized load is calculated for all episodes in all validation sets. Note that linear cost functions ( and ) are based on the optimum solutions (power consumption with optimum policy  charging demand coordination) of preceding $E$ episodes, and we choose $E = 1$ for this comparison. Similar results are observed for other values of $E$. Furthermore, we also include the average normalized load incurred by a BAU control policy for comparison.

Policy based on quadratic cost function ($RL_{q}$) takes 8-10 iterations of FQI algorithm to converge, whereas, the policies trained on linear cost functions ($RL_{a}$ and $RL_{m}$) take 3-4 iterations to converge. FQI takes longer to converge with the quadratic cost function because the agent has to learn the expected T-step return. This information is indirectly included in the linear cost functions, where we include the optimum policies of preceding days. Furthermore, we notice after a single iteration, both control policies based on linear cost functions perform much better than the policy trained with a quadratic cost function. The RL agent in our case has to learned the 12-step return starting from the root node (based on  = 12). For an $N$-step return ($N\gg12$), a policy trained with the quadratic cost function will take a large number of iterations to converge, whereas we can train a similar policy in fewer iterations using a linear cost function.

fig:load_linearcost shows the normalized load for control policies trained for linear cost functions with $E \in \{1, 5, 10\}$ (average/median of optimum solutions is calculated for preceding $E$ episodes). We also include the p-values for the Wilcoxon signed-rank test to evaluate statistical difference (statistically significant difference for p-values $\leq$ 0.05). We notice similar performance for average () and median () based linear cost functions. Policy trained with average/median of preceding 10 episodes has similar performance to a policy trained with information of a single preceding episode.

FQI converges faster with linear cost functions because they are easier to learn and are based on the optimum policies of preceding episodes. This helps in answering q:costfunctiondef (Impact of the cost function definition on the learning speed and performance of the learned policy?), as we can conclude from fig:load_costfuns that we should utilize the optimum policies of preceding days to define linear cost functions, which prove to be superior to the quadratic cost function. We also answer q:parametersettings (impact of varying parameter settings?) in this section, where we note from fig:load_linearcost that the optimum solution of the immediate preceding episode ($E$ = 1) is as informative as the average of preceding 10 episodes.

§ CONCLUSIONS

In this paper, we explored different aspects of an MDP formulation used to train a reinforcement learning based charging demand coordination to jointly coordinate  the charging demand of a group of  charging stations. We defined

* a new partially observable state representation,

* different action representations, and

* two new cost functions that assign costs based on a posteriori determined optimal charging actions for the preceding days

These $state$-$action$ representations and cost functions are used to define different MDP formulations.

A real-world  charging dataset is used to evaluate the performance of RL based control policies trained using different MDP formulations. We compared our control policies with an optimum policy (an all-knowing policy), a business-as-usual (BAU) control policy (charging fully upon arrival) and a heuristic control policy (spreading out each individual EV's required charging over the time it is connected). The conclusions from our study can be summarized as follows:

* State-Action Representation:

A partially observable vector $state$ representation provides similar performance to a fully observable matrix $state$ across all training set sizes (sec:results_obs). Information about flexibility is sufficient to learn a control policy, as vector state representations are based on aggregate flexibility. Furthermore, we see that local scaling of actions (scaling by the number of s with the same flexibility, $N_{d}$) improves the performance of control policy compared to full scaling (scaling by the system capacity, ).

We conclude that our vector state representation and locally scaled actions are the best choice for $state$-$action$ representation among the considered alternatives.

* Cost Function:

The proposed linear cost functions expedite optimization compared to quadratic cost function by,

* learning a control policy with 10% lower normalized load in a single iteration (sec:results_crd), and

* achieving convergence within fewer iterations as compared to the quadratic cost function
Furthermore, the number of preceding days utilized in linear cost functions does not affect the performance significantly, thus, the optimum solution from a single preceding day is sufficient (fig:creditassignment).

* Space and Computational Complexity:

MDP formulations based on vector states and matrix states have linear and quadratic space complexity respectively, in terms of the total number of decision slots,  (sec:Experiments). Vector state representation and locally scaled actions assist in learning control policies 30% faster compared to all other alternatives (fig:Time_SA_compare).

An MDP formulation based on

* a partially observable vector $state$ representation,

* a locally scaled $action$ representation, and

* a linear cost function
can provide 40%-50% improvement in load flattening compared to the BAU control policy and 20%-30% compared to a simple heuristic control policy for  coordination (fig:Load_SA_compare and fig:load_linearcost).

In future work, we will

* explore possible improvements in the function approximator used to approximate the $Q$-function in the FQI algorithm. The currently used Artificial Neural Network (ANN) can be improved by hyperparameter tuning or using a different neural network architecture. Further,

* we currently use a value iteration based learning approach to train the RL agent, where we learn the $Q$-function based on discrete state-action pairs. We would like to investigate policy iteration methods that learn the policy directly.

§ DECLARATION OF COMPETING INTEREST

The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

§ ACKNOWLEDGEMENTS

Part of this research has received funding from the European Union's Horizon 2020 research and innovation programme for the projects BRIGHT (<https://www.brightproject.eu/> – grant agreement no. 957816) and RENergetic (<https://www.renergetic.eu/> – grant agreement no. 957845).

Manu Lahariya is a doctoral student in the Internet Technology and Data Science Lab (IDLab) at Ghent University - imec, Ghent, Belgium. His doctoral research focuses on the development of machine learning algorithms for modeling Electric Vehicle (EV) session data and the application of deep reinforcement learning such as Q-networks for Model Predictive Control (MPC) of Electric vehicle (EV) charging stations. He also has experience in development of time series algorithms for sales forecasting. He obtained his Masters’ and Bachelors’ degree in Aerospace Engineering from Indian Institute of Technology (IIT) Kharagpur (2012-2017).

Nasrin Sadeghianpourhamami is an AI scientist/researcher at BluWave-Ai with a proven record of successfully applying AI in 4 major industry projects. She received her doctorate in computer science engineering in from Ghent University - imec, Ghent, Belgium (2018). She has worked on statistical modelling of real-world data, developing data-driven control via deep reinforcement learning, and has contributed in facilitating the integration of sustainable energy production/consumption in the evolving power grid.

Chris Develder is associate professor with the research group IDLab in the Dept. of Information Technology (INTEC) at Ghent University - imec, Ghent, Belgium. He currently leads two research teams within IDLab, one on converting text to knowledge (i.e., NLP, mostly information extraction using machine learning), the other on data analytics and machine learning for smart grids. He regularly serves as reviewer/TPC member for international journals and conferences (IEEE/ACM Trans. Networking, IEEE Trans. Smart Grid, Energy and Buildings; EMNLP, ACL, ACM SIGIR, ACM CIKM, IEEE SmartGridComm, etc.). He is Senior Member of IEEE, Member of ACM, and Member of ACL.


Top quark mass corrections to single and double Higgs boson production in
gluon fusion

J. Davies1*

1 Department of Physics and Astronomy, University of Sussex, Brighton, BN1
9HQ, UK

*<EMAIL_ADDRESS>
15th International Symposium on Radiative Corrections:
Applications of Quantum Field Theory to Phenomenology,
FSU, Tallahasse, FL, USA, 17-21 May 2021 10.21468/SciPostPhysProc.?

## Abstract

In this talk we discuss recent computations of the top quark mass dependence
of QCD amplitudes describing Higgs boson production in gluon fusion. We
compute terms in the expansion for a large top quark mass, which reduces the
Feynman diagrams to products of massless integrals and massive tadpole
integrals which contain the top mass dependence. In particular we discuss the
real and virtual corrections to double Higgs production at NNLO, and the
virtual corrections to single Higgs production at N3LO.

##  1 Introduction

One of the numerous tasks of the Large Hadron Collider (LHC) is to
characterize the structure of the Standard Model’s (SM) scalar sector. The
parameter $\lambda$ governs triple and quartic Higgs boson interactions, and
is determined in the SM by the mass and vacuum expectation value of the Higgs
boson. A direct experimental measurement of $\lambda$ will help determine if
the SM’s scalar sector is observed in nature, although such a measurement is
very challenging [1, 2].

It is therefore important to have a good theoretical understanding of
processes which involve a single Higgs boson and two Higgs bosons. Such
processes tend to be dominated by contributions with top quarks propagating in
loops, due to the large value of the top quark’s Yukawa coupling. Multi-loop
amplitudes quickly reach a complexity which cannot currently be handled in an
exact manner, so we turn to approximation methods in order to study them. In
particular, here, we discuss expansions which consider the top quark mass to
be larger than any other scale involved in the problem. The results of such
expansions, in addition to providing a good description of amplitudes below
the top quark threshold, can be combined with information describing other
kinematic regions, to produce approximations which describe amplitudes over a
wider kinematic range, see for e.g. Refs. [3, 4, 5]. A description of the
large-$m_{t}$ expansion method is given in Section 2 and of some of its
applications in Section 3.

##  2 Large Mass Expansion (LME)

The comparatively large value of the mass of the top quark means that
performing an expansion in the limit $m_{t}\to\infty$ leads to a sensible
approximation of scattering amplitudes, particularly for processes in which
contributions due to top quarks dominate. Amplitudes involving Higgs bosons
are examples of such processes; the size of the top quark Yukawa coupling
means that contributions from other quark flavours are relatively unimportant.
The leading term in such an expansion yields the so-called “Higgs effective
field theory” (HEFT), in which the top quark is completely integrated out.
Dependence on its mass appears only logarithmically in the effective couplings
of Higgs bosons and gluons. The goal of the computations discussed in these
proceedings is to include _sub-leading_ terms of the LME, i.e., terms
proportional to powers of $1/m_{t}^{\,2}$.

Such an asymptotic expansion can be performed by the method of “expansion by
subgraph”, which is conveniently implemented in the program exp [6, 7]. The
procedure is to identify all subgraphs of a given Feynman graph which contain
the heavy scale (here, $m_{t}$) and expand them in their small quantities. The
remaining propagators form the “co-subgraph” which does not depend on the
heavy scale. For the problem at hand, this means that each Feynman graph is
reduced to a sum of products of massless graphs and $m_{t}$-dependent vacuum
graphs, after the expansion in the limit $m_{t}\to\infty$. This procedure is
depicted in Fig. 1. For the subgraph identified on the first row, the
propagators are expanded as follows:

$\displaystyle\int\\!\\!\\!$
$\displaystyle\int\mbox{d}^{d}l_{1}\>\mbox{d}^{d}l_{2}\>\frac{1}{l_{2}^{2}}\frac{1}{(l_{2}+q_{1})^{2}}\frac{1}{(l_{2}-q_{2})^{2}}{\color[rgb]{0.5,0,0}\frac{1}{(l_{1}+q_{1})^{2}-m_{t}^{\,2}}\frac{1}{(l_{1}-q_{2})^{2}-m_{t}^{\,2}}\frac{1}{(l_{1}-l_{2})^{2}-m_{t}^{\,2}}}\longrightarrow$
$\displaystyle\>\>\>\>\int\mbox{d}^{d}l_{2}\>\frac{1}{l_{2}^{2}}\frac{1}{(l_{2}+q_{1})^{2}}\frac{1}{(l_{2}-q_{2})^{2}}\int\mbox{d}^{d}l_{1}\\!\left[\frac{1}{(l_{1}^{2}-m_{t}^{\,2})^{3}}+\frac{2(q_{1}\\!\cdot\\!l_{1}-q_{2}\\!\cdot\\!l_{1}-l_{2}\\!\cdot\\!l_{1})+l_{2}\\!\cdot\\!l_{2}}{(l_{1}^{2}-m_{t}^{\,2})^{4}}+\cdots\right]\,,$
(1)

where the “$\cdots$” represent higher-order terms in the expansion. Within the
square brackets, the propagators do not carry external momenta $q_{1}$ or
$q_{2}$, nor the loop momentum $l_{2}$; there is only a sum of one-loop vacuum
integrals with tensor numerators. Such integrals can be computed by the FORM
[8] package MATAD [9], up to three-loop order. For computations which require
four-loop vacuum integrals we make use of FIRE [10], which we also use to
perform integration-by-parts reduction for the massless co-subgraphs. A more
complete description of the computational toolchain is given in the following
section.

Full graph | Subgraph | Co-subgraph $\times$ Expanded subgraph
---|---|---
|  |
|  |
Figure 1: _Starting from the full Feynman graph of the first column, we
identify the subgraphs which contain $m_{t}$-dependent propagators. To perform
the LME, the subgraphs are expanded in the large-$m_{t}$ limit (denoted by the
operator $\mathcal{T}$), leaving only co-subgraphs which are independent of
$m_{t}$. _

###  2.1 Computational Toolchain

For all computations, we begin by generating the necessary Feynman diagrams
with qgraf [11]. From here, the packages q2e and exp [6, 7] are used to
convert the diagrams into a compatible notation and to identify the relevant
subgraphs and co-subgraphs, as described in Section 2. Code is generated for
the expansion to be performed by FORM [8], which also computes the colour
factors using the COLOR package [12]. Vacuum graphs up to three loops are
computed with the MATAD package [9], and four-loop vacuum graphs as well as
the massless integrals of the co-subgraphs are reduced to master integrals
using FIRE [10]. For the computation of phase-space integrals described in
Section 3.1, we use LiteRed [13, 14] and LIMIT [15].

##  3 Applications

In the following, we summarize some recent works which have used the LME
method described above. This includes an NNLO computation of the double-real
and real-virtual corrections to double–Higgs boson production in gluon fusion
[16, 17, 18] in Section 3.1, and N3LO computations of the virtual corrections
to single–Higgs boson production in gluon fusion [19] in Section 3.2, as well
as the decay of a Higgs boson into two photons [20] in Section 3.3.

###  3.1 NNLO real-radiation corrections to double Higgs boson production

In order to compute real-real and real-virtual corrections we make use of the
optical theorem, and compute forward-scattering diagrams which have cuts
through the desired final state particles. The real-real corrections
correspond to cuts through two Higgs bosons and two additional particles, and
the real-virtual corrections to cuts through two Higgs bosons and one
additional particle. Examples of such cuts are given in Fig. 2, where the
three-particle cuts are shown by blue dashed lines and four-particle cuts by
green dashed lines. Some diagrams, such as the first, admit both a three- and
four-particle cut. To generate such diagrams an additional step is required to
post-process the output of qgraf, which can not itself generate only diagrams
containing specified cuts. For this purpose we use the program gen111A. Pak,
Unpublished..

Figure 2: _Forward-scattering diagrams which contribute to the real-real and
real-virtual corrections to NNLO double–Higgs boson production. The blue and
green dashed lines denote three- and four-particle cuts through the final
state particles._

Figure 3: _Forward-scattering diagrams which contribute to the real-real and
real-virtual corrections to NNLO double–Higgs boson production. The blue and
green dashed lines denote three- and four-particle cuts through the final
state particles._

After large-$m_{t}$ expansion, the diagrams of Fig. 2 yield the phase-space
integrals shown in Fig. 3. These integrals are reduced to a basis of master
integrals by LiteRed after the partial fractioning of linearly-dependent
propagators by LIMIT. The master integrals are computed in an expansion around
$\delta=1-4m_{H}^{\,2}/s\to 0$, which corresponds to the production threshold
of the Higgs boson pair. A deep expansion in $\delta$ is obtained efficiently
through the use of differential equations, starting from boundary values
computed for the leading term in the expansion.

The total cross section at NNLO is given by

$\sigma_{ij}^{(2)}=\sigma_{ij,\mathrm{real}}^{(2)}+\sigma_{ij,\mathrm{coll}}^{(2)}+\sigma_{ij,\mathrm{virt}}^{(2)}\,,$
(2)

where $i,j$ denote the contributing partonic channels, $gg$, $gq$, $q\bar{q}$,
$qq$, $qq^{\prime}$, including also all additional anti-quark and ghost
channels. The collinear counterterms are computed through the convolution of
the LO and NLO cross sections with quark or gluon splitting functions. See
Section 2.5 of Ref. [18] for a detailed discussion. The virtual corrections
have been computed in Ref. [21, 22]. After ultra-violet renormalization, the
sum of contributions in Eq. (2) produces a finite result.

Plots for successive orders of the large-$m_{t}$ expansion are shown, for the
$gg$ and $gq$ channels, in Fig. 4. Below the top quark threshold the
large-$m_{t}$ expansion converges well, particularly so close to the
production threshold. Compared to the leading expansion term ($\rho^{0}$),
which corresponds to the HEFT result (which has been previously computed in
Ref. [23]), including the sub-leading terms typically corrects the NNLO
contributions by a factor of two.

Figure 4: _NNLO contributions to the total cross sections of the $gg$ and $gq$
channels. The vertical black line shows the threshold at $\sqrt{s}=2m_{t}$.
The curves show different orders in the large-$m_{t}$ expansion, denoted by
$\rho^{n}=(m_{H}^{\,2}/m_{t}^{\,2})^{n}$._

###  3.2 N3LO virtual corrections to single Higgs boson production

For $2\to 1$ processes, it is computationally feasible to compute virtual
corrections at N3LO, corresponding to four-loop order for loop-induced
processes such as single–Higgs boson production in gluon fusion, and Higgs
boson decay into two photons (see Section 3.3). Here we compute diagrams such
as those shown in Fig. 5. The expansion proceeds in a straightforward manner,
as outlined in Section 2. We define the amplitude to be

$\mathcal{A}=\frac{4\alpha_{s}(\mu)}{3\pi}\frac{T_{F}}{\nu}\delta^{ab}\left(q_{1}\\!\cdot\\!q_{2}\,g_{\vphantom{12}}^{\mu\nu}-q_{1}^{\,\nu\vphantom{\mu}}q_{2}^{\,\mu}\right)\>h(\rho)\,,$
(3)

where $q_{1},q_{2}$ are the momenta of the incoming gluons, $a,b$ their colour
indices, $T_{F}=1/2$, and $\nu$ is the Higgs vacuum expectation value. After
ultra-violet renormalization, the form factor $h(\rho)$ still contains infra-
red poles, however the poles of the rescaled form factor

$F(\rho)=h(\rho)/h^{(1)}(\rho)=1+\mathcal{O}(\alpha_{s})$ (4)

are predicted to factorize and given in the literature [24]. We thus consider

$\log{(F)}=\log{(F)}_{\mathrm{poles}}+\log{(F)}_{\mathrm{finite}}$ (5)

and find that indeed $\log{(F)}_{\mathrm{poles}}$ is independent of $\rho$ and
agrees with Ref. [24], and we may study the numerical impact of the N3LO
corrections to $\log{(F)}_{\mathrm{finite}}$. At a renormalization scale
$\mu=m_{t}$ with an on-shell $m_{t}$ value of 173 GeV, we find that

$\displaystyle\log{(F)}_{\mathrm{finite}}=$
$\displaystyle{}+a_{t}^{\phantom{2}}\left[{}+(11.07-3.06i)+(0.07)+(0.004)\right]$
$\displaystyle{}+a_{t}^{2}\left[{}+(22.59-13.24i)+(1.02-0.13i)+(0.07-0.01i)\right]$
$\displaystyle{}+a_{t}^{3}\left[{}-(73.18+51.55i)+(7.61+0.85i)+(0.70-0.14i)\right]\,,$
(6)

where the $\rho^{0}$, $\rho^{1}$ and $\rho^{2}$ expansion terms have been
displayed individually in round brackets. We observe that the sub-leading
terms in the large-$m_{t}$ expansion become increasingly important at higher
perturbative orders; at N3LO the $\rho^{1}$ and $\rho^{2}$ terms correct the
$\rho^{0}$ term by about 10% and 1%, respectively.

Figure 5: _Virtual corrections contributing to $gg\to H$ at N3LO._

###  3.3 N3LO corrections to Higgs boson decay into photons

From a computational point of view, the decay process $H\to\gamma\gamma$ is
very similar to $gg\to H$ discussed above in Section 3.2. The Feynman diagrams
which contribute are a subset of those of $gg\to H$, i.e., those for which the
external gluons (now photons) couple to a quark line rather than internally
propagating gluons. The first diagram of Fig. 5 is such an example. We can
therefore apply our existing machinery and reduction to master integrals to
this process. We define the partial decay width as

$\Gamma_{H\to\gamma\gamma}=\frac{m_{H}^{\,3}}{64\pi}\left|A(\rho)\right|,$ (7)

and compute $A(\rho)$ in the large-$m_{t}$ expansion. Unlike the form factor
$h(\rho)$ of $gg\to H$, $A(\rho)$ is finite after ultra-violet
renormalization.

For the top quark mass in the on-shell scheme, Fig. 6 shows the dependence on
the renormalization scale of the NLO, NNLO and N3LO corrections, w.r.t. the
leading order. At N3LO the curve becomes slightly flatter, but it does not
overlap with the NNLO curve.

Figure 6: _The scale dependence of the large- $m_{t}$ expansions of the NLO,
NNLO and N3LO corrections to $\Gamma_{H\to\gamma\gamma}$, w.r.t. the exact
leading order. $m_{t}$ is in the on-shell scheme. The vertical black line is
at $\mu=m_{H}$._

The N3LO large-$m_{t}$ result can be combined with the NLO electroweak
corrections [25] as well as the NNLO corrections due to bottom and charm quark
loops [26],

$\displaystyle\Gamma_{H\to\gamma\gamma}\times 10^{6}\text{GeV}^{-1}$
$\displaystyle=9.2581|_{\text{LO}}-0.1502|_{\text{NLO,EW}}+0.1569|_{\text{NLO,t}}+0.0157|_{\text{NLO,bc}}$
$\displaystyle{}+0.0029|_{\text{NNLO,t}}+0.0036|_{\text{NNLO,bc}}-0.0031|_{\text{N${}^{3}$LO,t}}=9.2838\,.$
(8)

We find that the N3LO top quark corrections are about the same size as each of
the NNLO corrections shown in Eq. (3.3), but come with the opposite sign.

##  4 Conclusion

In these proceedings, we have discussed the large-$m_{t}$ expansion and its
application to several scattering processes. For processes involving Higgs
bosons, the size of the top quark Yukawa coupling means that amplitudes with
top quarks running in the loops contribute an important part of the total
cross sections. The expansion allows the effect of the top quark mass to be
well described below the threshold, and including sub-leading terms typically
produces large corrections w.r.t. the leading term alone, which corresponds to
the commonly-used HEFT.

Such expansions can be performed in a semi-automated and systematic way,
allowing us to study multi-loop amplitudes which can not be computed in an
exact manner, either analytically or numerically. As discussed in Section 1,
these expansions form the input for various approximation methods which
combine information from various kinematic regions, in an attempt to describe
multi-loop amplitudes over a wider kinematic range than any one expansion
alone.

## Acknowledgements

The work of JD was partly supported by the Science and Technology Facilities
Council (STFC) under the Consolidated Grant ST/T00102X/1.

## References

  * [1] G. Aad _et al._ ,  _Search for the $HH\rightarrow b\bar{b}b\bar{b}$ process via vector-boson fusion production using proton-proton collisions at $\sqrt{s}=13$ TeV with the ATLAS detector_,  JHEP 07, 108 (2020),  10.1007/JHEP07(2020)108,  [Erratum: JHEP 01, 145 (2021), Erratum: JHEP 05, 207 (2021)],  2001.05178.
  * [2] A. M. Sirunyan _et al._ ,  _Search for nonresonant Higgs boson pair production in final states with two bottom quarks and two photons in proton-proton collisions at $\sqrt{s}$ = 13 TeV_,  JHEP 03, 257 (2021),  10.1007/JHEP03(2021)257,  2011.12373.
  * [3] R. Gröber, A. Maier and T. Rauh,  _Reconstruction of top-quark mass effects in Higgs pair production and other gluon-fusion processes_ ,  JHEP 03, 020 (2018),  10.1007/JHEP03(2018)020,  1709.07799.
  * [4] J. Davies, R. Gröber, A. Maier, T. Rauh and M. Steinhauser,  _Top quark mass dependence of the Higgs boson-gluon form factor at three loops_ ,  Phys. Rev. D 100(3), 034017 (2019),  10.1103/PhysRevD.100.034017,  [Erratum: Phys.Rev.D 102, 059901 (2020)],  1906.00982.
  * [5] M. L. Czakon and M. Niggetiedt,  _Exact quark-mass dependence of the Higgs-gluon form factor at three loops in QCD_ ,  JHEP 05, 149 (2020),  10.1007/JHEP05(2020)149,  2001.03008.
  * [6] R. Harlander, T. Seidensticker and M. Steinhauser,  _Complete corrections of Order alpha alpha-s to the decay of the Z boson into bottom quarks_ ,  Phys. Lett. B 426, 125 (1998),  10.1016/S0370-2693(98)00220-2,  hep-ph/9712228.
  * [7] T. Seidensticker,  _Automatic application of successive asymptotic expansions of Feynman diagrams_ ,  In _6th International Workshop on New Computing Techniques in Physics Research: Software Engineering, Artificial Intelligence Neural Nets, Genetic Algorithms, Symbolic Algebra, Automatic Calculation_ (1999), hep-ph/9905298.
  * [8] B. Ruijl, T. Ueda and J. Vermaseren,  _FORM version 4.2_ (2017),  1707.06453.
  * [9] M. Steinhauser,  _MATAD: A Program package for the computation of MAssive TADpoles_ ,  Comput. Phys. Commun. 134, 335 (2001),  10.1016/S0010-4655(00)00204-6,  hep-ph/0009029.
  * [10] A. V. Smirnov and F. S. Chuharev,  _FIRE6: Feynman Integral REduction with Modular Arithmetic_ ,  Comput. Phys. Commun. 247, 106877 (2020),  10.1016/j.cpc.2019.106877,  1901.07808.
  * [11] P. Nogueira,  _Automatic Feynman graph generation_ ,  J. Comput. Phys. 105, 279 (1993),  10.1006/jcph.1993.1074.
  * [12] T. van Ritbergen, A. N. Schellekens and J. A. M. Vermaseren,  _Group theory factors for Feynman diagrams_ ,  Int. J. Mod. Phys. A 14, 41 (1999),  10.1142/S0217751X99000038,  hep-ph/9802376.
  * [13] R. N. Lee,  _Presenting LiteRed: a tool for the Loop InTEgrals REDuction_ (2012),  1212.2685.
  * [14] R. N. Lee,  _LiteRed 1.4: a powerful tool for reduction of multiloop integrals_ ,  J. Phys. Conf. Ser. 523, 012059 (2014),  10.1088/1742-6596/523/1/012059,  1310.1145.
  * [15] F. Herren,  _Precision Calculations for Higgs Boson Physics at the LHC - Four-Loop Corrections to Gluon-Fusion Processes and Higgs Boson Pair-Production at NNLO_ ,  Ph.D. thesis, KIT, Karlsruhe,  10.5445/IR/1000125521 (2020).
  * [16] J. Davies, F. Herren, G. Mishima and M. Steinhauser,  _NNLO real corrections to $gg\to HH$ in the large-$m_{t}$ limit_,  PoS RADCOR2019, 022 (2019),  10.22323/1.375.0022,  1912.01646.
  * [17] J. Davies, F. Herren, G. Mishima and M. Steinhauser,  _Real-virtual corrections to Higgs boson pair production at NNLO: three closed top quark loops_ ,  JHEP 05, 157 (2019),  10.1007/JHEP05(2019)157,  1904.11998.
  * [18] J. Davies, F. Herren, G. Mishima and M. Steinhauser,  _Real corrections to Higgs boson pair production at NNLO in the large top quark mass limit_ (2021),  2110.03697.
  * [19] J. Davies, F. Herren and M. Steinhauser,  _Top Quark Mass Effects in Higgs Boson Production at Four-Loop Order: Virtual Corrections_ ,  Phys. Rev. Lett. 124(11), 112002 (2020),  10.1103/PhysRevLett.124.112002,  1911.10214.
  * [20] J. Davies and F. Herren,  _Higgs boson decay into photons at four loops_ ,  Phys. Rev. D 104(5), 053010 (2021),  10.1103/PhysRevD.104.053010,  2104.12780.
  * [21] J. Grigo, J. Hoff and M. Steinhauser,  _Higgs boson pair production: top quark mass effects at NLO and NNLO_ ,  Nucl. Phys. B 900, 412 (2015),  10.1016/j.nuclphysb.2015.09.012,  1508.00909.
  * [22] J. Davies and M. Steinhauser,  _Three-loop form factors for Higgs boson pair production in the large top mass limit_ ,  JHEP 10, 166 (2019),  10.1007/JHEP10(2019)166,  1909.01361.
  * [23] D. de Florian and J. Mazzitelli,  _Higgs Boson Pair Production at Next-to-Next-to-Leading Order in QCD_ ,  Phys. Rev. Lett. 111, 201801 (2013),  10.1103/PhysRevLett.111.201801,  1309.6594.
  * [24] T. Gehrmann, E. W. N. Glover, T. Huber, N. Ikizlerli and C. Studerus,  _Calculation of the quark and gluon form factors to three loops in QCD_ ,  JHEP 06, 094 (2010),  10.1007/JHEP06(2010)094,  1004.3653.
  * [25] S. Actis, G. Passarino, C. Sturm and S. Uccirati,  _NNLO Computational Techniques: The Cases H — $>$ gamma gamma and H —$>$ g g_,  Nucl. Phys. B 811, 182 (2009),  10.1016/j.nuclphysb.2008.11.024,  0809.3667.
  * [26] M. Niggetiedt,  _Exact quark-mass dependence of the Higgs-photon form factor at three loops in QCD_ ,  JHEP 04, 196 (2021),  10.1007/JHEP04(2021)196,  2009.10556.


Jacques Duparc logo_ttlM. Antonia Huertas, João Marcos, María Manzano, Sophie
Pinchinat,
François Schwarzentruber54th International Conference on Tools for Teaching
Logic1127TTL2015

# Easy Proofs of Löwenheim-Skolem Theorems by Means of Evaluation Games

Jacques Duparc  Department of Information, Systems Faculty of Business and
Economics
University of Lausanne, CH-1015 Lausanne Switzerland
<EMAIL_ADDRESS>Mathematics Section, School of Basic Sciences
Ecole polytechnique fédérale de Lausanne, CH-1015 Lausanne Switzerland
<EMAIL_ADDRESS>
###### Abstract.

We propose a proof of the downward Löwenheim-Skolem that relies on strategies
deriving from evaluation games instead of the Skolem normal forms. This proof
is simpler, and easily understood by the students, although it requires, when
defining the semantics of first-order logic to introduce first a few notions
inherited from game theory such as the one of an evaluation game.

###### Key words and phrases:

Model theory, Löwenheim-Skolem, Game Theory, Evaluation Game, First-Order
Logic

###### 1991 Mathematics Subject Classification:

F.4.1 Mathematical Logic

##  1\. Introduction

Each mathematical logic course focuses on first-order logic. Once the basic
definitions about syntax and semantics have been introduced and the notion of
the cardinality of a model has been exposed, sooner or later at least a couple
of hours are dedicated to the Löwenheim-Skolem theorem. This statement holds
actually two different results: the downward Löwenheim-Skolem theorem
(LS$\downarrow$) and the upward Löwenheim-Skolem theorem (LS$\uparrow$).

######  Theorem 1.1 (Downward Löwenheim-Skolem).

Let $\mathcal{L}$ be a first-order language, $T$ some $\mathcal{L}$-theory,
and $\kappa=\max\\{\textit{card}\left(\mathcal{L}\right),\aleph_{0}\\}$.

If $T$ has a model of cardinality $\lambda>\kappa$, then $T$ has a model of
cardinality $\kappa$.

######  Theorem 1.2 (Upward Löwenheim-Skolem).

Let $\mathcal{L}$ be some first-order language with equality, $T$ some
$\mathcal{L}$-theory, and
$\kappa=\max\\{\textit{card}\left(\mathcal{L}\right),\aleph_{0}\\}$.

If $T$ has an infinite model, then $T$ has a model of cardinality $\lambda$,
for any $\lambda>\kappa$.

The proof of the second theorem (LS$\uparrow$) is a simple exercise that
relies on an easy application of the compactness theorem joined with a
straightforward utilization of LS$\downarrow$. The proof of the first theorem
is more involved and not that easy to understand for undergraduate students at
EPFL. For some basic background and notations we refer the reader to [1, 5].

The usual approach to proving LS$\downarrow$ goes through several steps which
involve reducing the original theory $T$ to another theory $T^{\prime}$ on an
extended language $\mathcal{L}^{\prime}$ where all statements are in Skolem
normal form. Then obtaining some $\mathcal{L}^{\prime}$-structure of the right
cardinality that satisfies $T^{\prime}$, from which one goes back to a model
that satisfies $T$.

The burden of going through the Skolem normal forms is regarded as bothersome
by the student.

We would like to advocate that the use of _evaluation games_ greatly
simplifies the proof of LS$\downarrow$. Of course, this requires to talk about
finite two-player perfect games and the related notions of player, strategies,
winning strategies, etc. But it is worth the candle, especially if these games
are introduced for explaining the semantics of first-order logic. Anyhow,
determining whether a first-order formula holds true in a given structure is
very similar to solving the underlying evaluation game as put forward by Jaako
Hintikka [4]. We refer the readers unfamiliar with these notions to [6, 7],
where the tight relations between logic and games are disclosed.

##  2\. Evaluation games for first-order logic

We noticed that when presented with both the classical semantics of first-
order logic and the semantics that makes use of evaluation games, the audience
gets much more involved in the second approach. Indeed, most students are more
eager to solving games than to checking whether a formula holds true.

Moreover, introducing first-order formulas not as (linear) sequences of
symbols, but rather as trees (usually denoted as decomposition tree) makes it
even easier to give evidence in support of the game-theoretical way of dealing
with satisfaction. The reason is twofold:

  1. (1)

the whole arena of the evaluation is very similar to the tree decomposition of
the formula. It has the very same height and the same branching except when
quantifiers are involved, where it depends on the cardinality of the domain of
the model.

  2. (2)

the task of pointing out the occurrences of variables that are bound by a
given quantifier – in order to replace them by an element of the domain chosen
by one of the players – is easily taken care of by taking the path along the
unique branch that leads from a given leaf of the tree where the occurrence of
the variable is situated, to the root of the tree. The first – if any –
quantifier acting on this variable that is encountered is the one that bounds
it.

We recall the definition of the evaluation game for first-order logic.

######  Definition 2.1.

Let $\mathcal{L}$ be a first-order language, ${\phi}$ some closed formula
whose logical connectors are among $\\{\neg,\vee,\wedge\\}$, and $\mathcal{M}$
some $\mathcal{L}$-structure.

The evaluation game $\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\phi}\right)$ is
defined as follows:

  1. (1)

there are two players, called Verifier and Falsifier. Verifier (V) has
incentive to show that the formula holds in the $\mathcal{L}$-structure
($\mathcal{M}\models{\phi}$), whereas the goal of Falsifier (F) is to show
that it does not hold ($\mathcal{M}\not\models{\phi}$).

The moves of the players essentially consist of pushing a token down the tree
decomposition of the formula ${\phi}$ – as a way to choose sub-formulas – and
must comply with the rules below:

if the current position is… whose turn … the game continues with…
${\varphi_{0}\leavevmode\nobreak\ \vee\leavevmode\nobreak\ \varphi_{1}}$ V
chooses $j\in\\{0,1\\}$ ${\varphi_{j}}$ ${\varphi_{0}\leavevmode\nobreak\
\land\leavevmode\nobreak\ \varphi_{1}}$ F chooses $j\in\\{0,1\\}$
${\varphi_{j}}$ ${\neg\varphi}$ F and V switch roles ${\varphi}$ ${\exists
x_{i}\varphi}$ V chooses $a_{i}\in|\mathcal{M}|$ ${\varphi[a_{i}/x_{i}]}$
${\forall x_{i}\varphi}$ F chooses $a_{i}\in|\mathcal{M}|$
${\varphi[a_{i}/x_{i}]}$ V wins
${R(t_{1},\cdots,t_{k})_{[a_{1}/x_{1},\cdots,a_{n}/x_{n}]}}$ the game stops
$\Longleftrightarrow$
$\mathcal{M},a_{1}/x_{1},\cdots,a_{n}/x_{n}\models{R(t_{1},\cdots,t_{k})}$

  2. (2)

The winning condition arises when the remaining formula becomes atomic, i.e.
of the form ${R(t_{1},\cdots,t_{k})_{[a_{1}/x_{1},\cdots,a_{n}/x_{n}]}}$.
Notice that the rules guarantee that, since the initial formula is closed, one
always ends up with an atomic formula that does not contain any more variable
as each of them has been replaced by some element of the domain of the model
111Formally we should not say that we replace each variable $x_{i}$ by some
element $a_{i}$, but rather that we replace $x_{i}$ by some brand new constant
symbol $\texttt{c}_{a_{i}}$, whose interpretation is precisely this element
$a_{i}$ and the formula we reach at the end is of the form
${R(t_{1},\ldots,t_{k})_{[\texttt{c}_{a_{1}}/x_{1},\ldots,\texttt{c}_{a_{n}}/x_{n}]}}$.
.

Player V wins if ${R(t_{1},\ldots,t_{k})}$ is satisfied in the extended
$\mathcal{L}$-structure $\mathcal{M},a_{1}/x_{1},\ldots,a_{n}/x_{n}$
($\mathcal{M},a_{1}/x_{1},\ldots,a_{n}/x_{n}\models{R(t_{1},\ldots,t_{k})}$);
F wins otherwise.

######  Example 2.2.

Suppose we have a language that contains a unary relation symbol $P$, a binary
relation symbol $R$, and a unary function symbol f. We then consider the
formula ${\forall x\Big{(}P(x)\vee\exists yR\big{(}f(x),y\big{)}\Big{)}}$
whose tree decomposition is

the model $\mathcal{M}$ is defined by:

  * •

$|\mathcal{M}|=\\{a,b\\}$,

  * •

$f^{\hbox{\tiny\hbox{$\cal M$}}}(a)=b$.

  * •

$R^{\hbox{\tiny\hbox{$\cal M$}}}=\\{(b,a)\\}$.

  * •

$f^{\hbox{\tiny\hbox{$\cal M$}}}(b)=a$

  * •

$P^{\hbox{\tiny\hbox{$\cal M$}}}=\\{b\\}$,

The game tree that represents the arena for the evaluation game
$\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\forall x\left(P(x)\vee\exists
yR(f(x),y)\right)}\right)$ is played on the arena represented by the following
game tree:

The green leaves are the ones where the atomic formula holds true in the
model, and the opposite for the red ones.

We then proceed by _backward induction_ and assign either the colour green or
the colour red to every node depending on whether the Verifier or the
Ffalsifier has a winning strategy if the game were to start from that
particular node.

We end up this way with the root being coloured green which shows that the
Verifier has a winning strategy. We indicate below by blue arrows such a
winning strategy for the Verifier.

##  3\. The classical proof of LS$\downarrow$ with Skolemization

Given any theory $T$ as in Theorem 1.1, without loss of generality, one first
assumes that every formula ${\phi}\in T$ is in _prenex normal form_ i.e.
$\phi=Q_{1}x_{1}\ldots Q_{k}x_{k}\psi$, where, for all $1\leq i<j\leq k$,
$Q_{i},Q_{j}\in\\{\forall,\exists\\}$, $x_{i}\neq x_{j}$ and $\psi$ is
quantifier free. Then, the usual proof of (LS$\downarrow$) goes through the
following steps

  1. (1)

The _skolemization_ of each such $\phi$, which consists of

    1. (a)

first extending the language by adding, for each existential quantifier that
$\phi$ contains, a new function symbol ${f^{\phi}_{k}}^{(q_{k})}$ of arity
$q_{k}$.

$\mathcal{L}^{\prime}=\mathcal{L}\cup\left\\{{f^{\phi}_{k}}^{(q_{k})}\mid
Q_{k}=\exists,q_{k}=\textit{card}\left(\big{\\{}m\mid 1\leq m<k\wedge
Q_{m}=\forall\big{\\}}\right)\right\\}.$

With this definition $q_{k}$ coincides with the number of universal
quantifiers which precede the existential $Q_{k}$.

    2. (b)

For each existentially quantified variable $x_{k}$, replacing inside $\psi$,
each occurrence of $x_{k}$ by the term222A function symbol whose arity is zero
is simply a constant symbol. $f^{\phi}_{k}\left(x_{p_{1}},\ldots
x_{p_{q_{k}}}\right)$, where $x_{p_{1}},\ldots,x_{p_{q_{k}}}$ are the
universally quantified variables that precede $Q_{k}$. More formally:

$t_{k}=f^{\phi}_{k}\left(x_{p_{1}},\ldots x_{p_{q_{k}}}\right)$

$\textup{ where }\\{x_{p_{1}},\ldots x_{p_{q_{k}}}\\}=\\{m\mid 1\leq m<k\wedge
Q_{m}=\forall\\}$ and the sequence of subscripts $(p_{i})_{1\leq i\leq q_{k}}$
is strictly increasing. We then obtain

$\tilde{\psi}=\psi_{{}_{\left[{}^{t_{k_{1}}}{/x_{k_{1}}},\cdots,{}^{t_{k_{m}}}{/x_{k_{m}}}\right]}}$

where $\\{x_{k_{i}}\mid{1\leq i\leq m}\\}$ is the set of all existentially
quantified variables of $\phi$.

    3. (c)

Removing all universal quantifiers from $\phi$. The Skolem normal form of
$\phi$ – denoted $\sigma_{\phi}$ – becomes:

$\sigma_{\phi}=Q_{i_{1}}x_{i_{1}}\ldots Q_{i_{t}}x_{i_{t}}\tilde{\psi}$

where the sequence of subscripts $(x_{i})_{1\leq i\leq t}$ runs through all
universally quantified variables of $\phi$.

This way, any $\mathcal{L}$-theory $T$ is turned into its skolemized version:
some $\mathcal{L}^{\prime}$-theory $\sigma_{T}=\\{\sigma_{\phi}\mid\phi\in
T\\}$.

  2. (2)

One shows that the cardinality of the set of new function and constant symbols
that have been added to the language is either countable if the language is
finite, and it is the same as the one of the original language $\mathcal{L}$
if it is infinite. Therefore the extended language $\mathcal{L}^{\prime}$ has
cardinality $\max\\{\textit{card}\left(\mathcal{L}\right),\aleph_{0}\\}$.

  3. (3)

One takes any $\mathcal{L}$-structure $\mathcal{M}$ of cardinality
$\lambda>\kappa$ such that $\mathcal{M}\models T$ and construct some
$\mathcal{L}^{\prime}$-structure $\mathcal{M}^{\prime}$ by extending
$\mathcal{M}$ from $\mathcal{L}$ to $\mathcal{L}^{\prime}$. This is done by
providing for every new symbol ${{f^{\phi}_{k}}^{(q_{k})}}$ an interpretation

${{f^{\phi}_{k}}^{(q_{k})}}^{\hbox{\tiny\hbox{$\cal
M$}}}:|\mathcal{M}|^{q_{k}}\mapsto|\mathcal{M}|\leavevmode\nobreak\ \mbox{
such that it satisfies }\leavevmode\nobreak\
\mathcal{M}^{\prime}\models\sigma_{T}.$

With the classical approach, the description of the extension
$\mathcal{M}^{\prime}$ is usually messy, whereas it simply does not exist with
the game-theoretical approach.

  4. (4)

One constructs some $\mathcal{L}^{\prime}$-structure $\mathscr{N}^{\prime}$ of
cardinality $\kappa$ such that $\mathscr{N}^{\prime}\models\sigma_{T}$ holds.
So, one selects some sub-domain of $|\mathcal{M}^{\prime}|$ which is closed
under all interpretations of functions 333Including the constants which are
the ones of arity 0. of $\mathcal{L}^{\prime}$. For this purpose, one starts
with any subset $N_{0}\subseteq|\mathcal{M}^{\prime}|$ of cardinality $\kappa$
which contains all interpretations of constant symbols from
$\mathcal{L}^{\prime}$. We let $\mathscr{F}_{k}(\mathcal{L}^{\prime})$ denote
the set of function symbols of $\mathcal{L}^{\prime}$ of arity $k$. By
induction, one defines

$N_{n+1}=N_{n}\cup\\{f^{\hbox{\tiny\hbox{$\cal
M$}}^{\prime}}(a_{1},\ldots,a_{k})\mid
k\in\mathbb{N},f\in\mathscr{F}_{k}(\mathcal{L}^{\prime}),a_{1},\ldots,a_{k}\in
N_{n}\\},$

and one sets $N_{\omega}=\bigcup_{n\in\mathbb{N}}N_{n}$. One observes that:

    1. (a)

$N_{0}\subseteq N_{1}\subseteq\ldots\subseteq N_{\omega}$.

    2. (b)

For all $n\in\mathbb{N},\
\textit{card}\left(N_{n+1}\right)=\textit{card}\left(N_{n}\right)=\kappa$,
since the induction yields

$\begin{array}[]{lll}\kappa&\leq&\textit{card}\left(N_{n}\cup\\{f^{\hbox{\tiny\hbox{$\cal
M$}}^{\prime}}(a_{1},\ldots,a_{k})\mid
k\in\mathbb{N},f\in\mathscr{F}_{k}(\mathcal{L}^{\prime}),a_{1},\ldots,a_{k}\in
N_{n}\\}\right)\\\ &\leq&\textit{card}\left(\mathcal{L}^{\prime}\times
N_{n}^{<\omega}\right)\\\
&\leq&\textit{card}\left(\kappa\times\kappa^{<\omega}\right)\\\
&\leq&\kappa\cdot\kappa\\\ &\leq&\kappa\end{array}$

    3. (c)

Hence $\textit{card}\left(N_{\omega}\right)=\kappa$ holds, since

$\kappa\leq\textit{card}\left(N_{\omega}\right)\leq\textit{card}\left(\prod_{n\in\omega}N_{n}\right)\leq\textit{card}\left(\aleph_{0}\times\kappa\right)\leq\aleph_{0}\cdot\kappa\leq\kappa.$

    4. (d)

$N_{\omega}$ is closed under all interpretations of function symbols from
$\mathcal{L}^{\prime}$. For if $k\in\mathbb{N}$,
$f\in\mathscr{F}_{k}(\mathcal{L}^{\prime})$, and $a_{1},\ldots,a_{k}\in
N_{\omega}$, there would then exist some $n\in\mathbb{N}$ such that
$a_{1},\ldots,a_{k}\in N_{n}$, henceforth $f^{\hbox{\tiny\hbox{$\cal
M$}}^{\prime}}(a_{1},\ldots,a_{k})\in N_{n+1}\subseteq N_{\omega}$.

Therefore $\mathscr{N}^{\prime}$ is defined by:

     * $\bullet$

$|\mathscr{N}^{\prime}|=N_{\omega}$;

     * $\bullet$

for all constant symbols $c$,
$c^{\mathscr{N}^{\prime}}=c^{\hbox{\tiny\hbox{$\cal M$}}^{\prime}}$;

     * $\bullet$

for all fonction symbols $f$ of arity $k$,
$f^{\mathscr{N}^{\prime}}=f^{\hbox{\tiny\hbox{$\cal
M$}}^{\prime}}|_{{N_{\omega}}^{k}}$;

     * $\bullet$

for all relation symbols $R$ of arity $k$,
$R^{\mathscr{N}^{\prime}}=R^{\hbox{\tiny\hbox{$\cal
M$}}^{\prime}}\cap{(N_{\omega})}^{k}$.

  5. (5)

Finally, one shows that the model $\mathscr{N}$ defined as the restriction of
$\mathscr{N}^{\prime}$ to the language $\mathcal{L}$ satisfies
$\mathscr{N}\models T$. This requires once again to review the construction of
$\mathscr{M}^{\prime}$, by backward this time: another wearisome moment for
the students.

##  4\. An alternative game-theoretical proof of LS$\downarrow$

Compared to the previous proof, the game-theoretical proof that we advocate is
simpler for it only focuses on the original model and fixed winning strategies
that witness that the theory holds in this model. Indeed, this proof contains

  * •

no Skolem normal form

  * •

no extended language $\mathcal{L}^{\prime}$

  * •

no extension $\mathcal{M}^{\prime}$ of $\mathcal{M}$

  * •

no restriction $\mathcal{N}$ of $\mathcal{N}^{\prime}$

In this proof, we start with any model $\mathscr{M}$ such that both
$\textit{card}\left(|\mathscr{M}|\right)\geq\kappa$ and $\mathscr{M}\models T$
hold. We also assume that every formula $\phi\in T$ is in prenex normal
form444We suppose that $T\neq\emptyset$ holds; otherwise, the result is simply
straightforward..

  1. (1)

For each $\phi\in T$ we pick any winning strategy $\sigma_{\phi}$ for the
Verifier in $\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\phi}\right)$. By looking
at the very rules of the game, every student realises immediately that for
each existential $Q_{i}x_{i}$ in $\phi$, the given strategy secures one
element from $|\mathcal{M}|$ that only depends on the previous choices made by
her opponent (Falsifier). Since $\phi$ is in prenex normal form, these choices
made by Falsifier correspond precisely to the universal quantifiers preceding
$Q_{i}x_{i}$. For instance, if $\phi$ is of the form

$\forall x_{1}\exists x_{2}\forall x_{3}\forall x_{4}\forall x_{5}\psi$

then the choices that Verifier makes – following $\sigma_{\phi}$ – of an
element $a_{2}\in|\mathcal{M}|$ for $x_{2}$ and an element
$a_{5}\in|\mathcal{M}|$ for $x_{5}$ depend respectively of the choices made by
Falsifier of an element $a_{1}\in|\mathcal{M}|$ for $x_{1}$, and of elements
$a_{1}\in|\mathcal{M}|$ for $x_{1}$, $a_{3}\in|\mathcal{M}|$ for $x_{3}$,
$a_{4}\in|\mathcal{M}|$ for $x_{4}$. In other words, the winning strategy
picks for $x_{i}$ an element that is function of  – meaning that it only
depends on – the choices made for the universally quantified variables that
come before $x_{i}$. Assuming there is $k$-many such universally quantified
variables, this induces a unique function
$f_{i}^{\sigma_{\phi}}:|\mathscr{M}|^{k}\mapsto|\mathscr{M}|$. So we come up
with a set $\mathscr{F}=\left\\{f_{i}^{\sigma_{\phi}}\mid\phi\in
T\right\\}\cup\left\\{f^{\hbox{\tiny\hbox{$\cal M$}}}\mid
f\in\mathcal{L}\right\\}$ of functions of different arities555Functions of
arity 0 being identified with elements of the domain $|\mathscr{M}|$. whose
cardinality is at most
$\kappa=\max\\{\textit{card}\left(\mathcal{L}\right),\aleph_{0}\\}$.

  2. (2)

We take any subset $N_{0}\subseteq|\mathscr{M}|$ of cardinality $\kappa$ and
proceed as in (4)(a-d) to obtain the least (for inclusion) subset
$N\subseteq|\mathscr{M}|$ of cardinality $\kappa$ that satisfies both
$N_{0}\subseteq N$ and $N$ is closed under all functions in $\mathscr{F}$.

  3. (3)

We form $\mathcal{N}$ as the restriction of $\mathcal{M}$ from $|\mathcal{M}|$
to $N$, and show that $\mathcal{N}\models T$ in a straightforward manner this
time, since for every formula $\phi\in T$ the very same strategy666Strictly
speaking this is the restriction of this strategy to $N$. $\sigma_{\phi}$
which is winning for the Verifier in
$\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\phi}\right)$ is also winning for the
Verifier in $\hbox{$\mathbb{E}v$}\left(\mathcal{N},{\phi}\right)$.

##  5\. An even simpler proof of LS$\downarrow$

This proof does not even require to go through the formulas of $T$ to be in
prenex normal form.

  1. (1)

for each $\phi\in T$, pick any winning strategy $\sigma_{\phi}$ for the
Verifier in $\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\phi}\right)$ and for any
$A\subseteq|\mathcal{M}|$ consider all possible plays in
$\hbox{$\mathbb{E}v$}\left(\mathcal{M},{\phi}\right)$ such that

    1. (a)

Falsifier restricts his $\forall$-moves to choosing elements of $A$, and

    2. (b)

Verifier applies her winning strategy $\sigma_{\phi}$.

set $(A)^{\sigma_{\phi}}$ as the subset of $|\mathcal{M}|$ formed of all the
$\exists$-moves made by Verifier. Set also
$(A)^{\mathscr{F}}=\left\\{f^{\hbox{\tiny\hbox{$\cal M$}}}(\vec{a})\mid
f\in\mathcal{L}\textit{ a function symbol with arity
}k,\vec{a}\in{N^{\mathbf{V}}_{n}}^{k}\right\\}$,

  2. (2)

inductively define $N$ by:

    1. (a)

$N^{\mathbf{F}}_{0}\subseteq|\mathcal{M}|$ any set s.t.
$\textit{card}\left(N^{\mathbf{F}}_{0}\right)=\kappa$,
$\\{c^{\hbox{\tiny\hbox{$\cal M$}}}\mid c\textit{ constant
}\in\mathcal{L}\\}\subseteq N^{\mathbf{F}}_{0}$,

    2. (b)

$N^{\mathbf{F}}_{n+1}=N^{\mathbf{F}}_{n}\cup\left(N^{\mathbf{F}}_{n}\right)^{\mathscr{F}}\cup{\displaystyle\bigcup_{\phi\in
T}}\left(N^{\mathbf{F}}_{n}\right)^{\sigma_{\phi}}$, and
$N={\displaystyle\bigcup_{n\in\mathbb{N}}}N^{\mathbf{F}}_{n}$. Then,

       * •

$\textit{card}\left(N\right)=\kappa$

       * •

$(N)^{\sigma_{\phi}}\subseteq N$

       * •

$(N)^{\mathscr{F}}\subseteq N$.

  3. (3)

Form $\mathcal{N}$ as the restriction of $\mathcal{M}$ to $N$, and easily
verify that $\mathcal{N}\models T$, since the very same $\sigma_{\phi}$ is
winning for Verifier in $\hbox{$\mathbb{E}v$}\left(\mathcal{N},{\phi}\right)$.

##  6\. Conclusion

We tried these proofs on our own students at EPFL. It turns out that they
understand much better the proof of LS$\downarrow$ that we recommend than they
buy the classic one. It also requires much less time to teach, and above all
we deeply believe that this proof highlights what is essential in this result
now devoid of all the technical details of the skolemization. On the other
hand, there is a price to pay in doing so: one has to present the semantics of
first-order logic through evaluation games. But here also we have noticed that
the students learn more easily this other part of the course. Another
advantage of the game-theoretical approach is also that it paves the way for
the back-and-forth method [3] or the Ehrenfeucht-Fraïssé games [2] that are
intensively used in model theory [5].

## References

  * [1] René Cori and Daniel Lascar.  Mathematical Logic: Part 1: Propositional Calculus, Boolean Algebras, Predicate Calculus, Completeness Theorems.  Oxford University Press, 2000.
  * [2] Andrzej Ehrenfeucht.  An application of games to the completeness problem for formalized theories.  Fund. Math, 49(129-141):13, 1961.
  * [3] Roland Fraïssé.  Sur une nouvelle classification des systèmes de relations.  Comptes Rendus Hebdomadaires des Séances de l’Académie des Sciences, 230(11):1022–1024, 1950.
  * [4] Jaakko Hintikka and Esa Saarinen.  Game-theoretical semantics: Essays on semantics, volume 5.  Springer, 1979.
  * [5] David Marker.  Model theory: an introduction.  Springer, 2002.
  * [6] Jouko Väänänen.  Models and games, volume 132.  Cambridge University Press, 2011.
  * [7] Johan van Benthem.  Logic and game theory: Close encounters of the third kind.  In Gregory Mints and Reinhard Anton Muskens, editors, Games, logic, and constructive sets. CSLI Publications, 2003.