LOCALLY NILPOTENT POLYNOMIALS OVER $\mathbb{Z}$
Sayak Sengupta
Department of Mathematics and Statistics, Binghamton University - SUNY,
Binghamton, New York, USA
<EMAIL_ADDRESS>

Abstract

For a polynomial $u=u(x)$ in $\mathbb{Z}[x]$ and $r\in\mathbb{Z}$, we consider
the orbit of $u$ at $r$ denoted and defined by
$\mathcal{O}_{u}(r):=\\{u(r),u(u(r)),\ldots\\}$. We ask two questions here:
(i) what are the polynomials $u$ for which $0\in\mathcal{O}_{u}(r)$, and (ii)
what are the polynomials for which $0\not\in\mathcal{O}_{u}(r)$ but, modulo
every prime $p$, $0\in\mathcal{O}_{u}(r)$? In this paper, we give a complete
classification of the polynomials for which (ii) holds for a given $r$. We
also present some results for some special values of $r$ where (i) can be
answered.

##  1 Introduction

In Example 1 of [2], A. Borisov set up a polynomial map, called the additive
trap, $F_{at}:\mathbb{A}_{\mathbb{Z}}^{2}\to\mathbb{A}_{\mathbb{Z}}^{2}$,
which maps $(x,y)\mapsto(x^{2}y,x^{2}y+xy^{2})$. This polynomial map satisfies
many interesting properties. In particular,
$F_{at}^{(p)}(x,y)\equiv(0,0)\pmod{p}$ for every
$(x,y)\in\mathbb{A}^{2}_{\mathbb{F}_{p}}$ and for all primes $p$, where
$F_{at}^{(p)}$ is the $p$th iteration of $F_{at}$. To prove this, suppose that
$p$ is a prime. Note that all points $(x,y)\in\mathbb{A}_{\mathbb{F}_{p}}^{2}$
with either $x=0$ or $y=0$ are taken to (0,0) by $F_{at}$. Let
$x\in\mathbb{F}_{p}^{*}$. Then for any $y\in\mathbb{F}_{p}^{*}$ we get

$\frac{x^{2}y+xy^{2}}{x^{2}y}=\frac{y}{x}+1.$

So, after at most $p-1$ iterations, the second coordinate becomes 0 and thus,
applying $F_{at}$ once more, we reach (0,0). Since $p$ is arbitrary, the proof
follows. For more details see [2]. One can see from the discussion that the
$p$th iteration of $F_{at}$ modulo $p$ is the zero map, which follows from the
fact that the polynomial $u(x)=x+1$ has the following property: for every
$n\in\mathbb{N}$, $u^{(n)}(x)=x+n$, so that, in particular, for every prime
$p$, $u^{(p-1)}(1)=p\equiv 0\pmod{p}$. Throughout this paper, by $\mathbb{N}$
we will mean the set of all positive integers, and by $u^{(n)}$, we will mean
$\underbrace{u\circ u\circ\cdots\circ u}_{n\text{ times}}$, the $n$th
iteration of $u$. We can write our first definition now which is motivated by
the behavior of the polynomial $u(x)=x+1$. Suppose $r\in\mathbb{Z}$ and $A$ is
a finite subset of the set of all prime numbers. If, for every prime $p$ not
contained in $A$, there exists an $m\in\mathbb{N}$ such that $u^{(m)}(r)\equiv
0\pmod{p}$, we will say that $u$ is weakly locally nilpotent at $r$ outside
$A$. The set of all weakly locally nilpotent polynomials at $r$ outside $A$ of
degree $d$ will be denoted by $L_{r,A}^{d}$ and $L_{r,A}$ is the union of
$L_{r,A}^{d}$’s, where the union is taken over all degrees $d\in\mathbb{N}$.
When $A=\emptyset$, i.e., for all primes $p$, $m$ exists satisfying
$u^{(m)}(r)\equiv 0\pmod{p}$, we say that $u$ is locally nilpotent at $r$.
Thus $u(x)=x+1$ is locally nilpotent at $1$, i.e., $x+1\in
L_{1,\emptyset}^{1}$. If, in particular, a polynomial $u$ is such that
$u^{(n)}(r)=0,$ for some $n\in\mathbb{N}$, then we will say that $u$ is
nilpotent at $r$ and the nilpotency index is the least of such $n^{\prime}s$.
We denote the set of all nilpotent polynomials at $r$ of degree $d$ and
nilpotency index $i$ by $N_{r,i}^{d}$. Also, $N_{r}$ is the union of all such
$N_{r,i}^{d}$, where the union is taken over $i,d\in\mathbb{N}$. Thus
$u(x)=x-1$ is nilpotent at 1 of nilpotency index 1, i.e., $x-1\in
N_{1,1}^{1}$. One of the principal goals of this paper is to understand the
polynomials that are locally nilpotent without being nilpotent at $r$, i.e.,
$0$ is not in the orbit of a polynomial $u$ at $r$ but modulo every prime $p$,
some iteration of $u$ at $r$ hits $0$. This is an interesting question and it
has been answered completely here. To classify these polynomials we have used
Theorem 5 of [4]. In particular, if we take
$K=\mathbb{Q},g=1,A_{1}=\\{0\\},T_{1}=\\{r\\},\varphi_{1}=u\text{ polynomial}$
in this theorem, we get Fact 1.1 in our paper which says:

######  Fact 1.1.

If $u$ is a polynomial that is of degree at least 2 and it is weakly locally
nilpotent at $r$ outside some finite set of primes $A$, then it must be
nilpotent at $r$. Equivalently, if there is a polynomial $u$ such that it is
weakly locally nilpotent at $r$ outside $A$ but not nilpotent at $r$, then it
must be a linear polynomial.

It should be noted that Theorem 5 of [4] was built upon the work of Silverman
in [7], and the works of Benedetto-Ghioca-Kurlberg-Tucker-Zannier in Lemma 4.1
of [5]. It should also be noted that the question of when an orbit passes
through a given point modulo a prime came naturally from the study of the
Dynamical Mordell-Lang (DML) Conjecture, which is a major open question in
arithmetic dynamics. The paper [4] was developed to prove certain special
cases of the DML Conjecture. Interested readers can also look at [6].

From Fact 1.1 it is imperative to study the behavior of linear polynomials in
order to understand locally nilpotent polynomials which are not nilpotent.
This is where we use Theorem 1 of [3] and derive a Lemma, which we call CRS
Lemma (Lemma 3.2). This Lemma has been stated and proved in section 3.

The paper contains four main results:

  1. 1.

Complete classification of all polynomials in $L_{r,\emptyset}$, when
$r\in\\{0,-1,1\\}$. This can be found in Theorems 4.1, 4.4 and Corollary 4.2.

  2. 2.

Complete classification of all polynomials in $L_{1,A}^{1}$ for any given
finite subset $A$ of the set of prime numbers. This can be found in Theorem
5.1. To establish this we have used Lemma 3.2.

  3. 3.

Complete classification of all polynomials in $S_{r}$ which can only be linear
polynomials by Fact 1.1, where $S_{r}:=L_{r,\emptyset}\setminus N_{r}$. This
can be found in Corollaries 4.3, 4.5, 5.4 and Theorem 5.3. Lemma 3.2 has also
been used to establish this.

The main tools that we have used here are the following (see section 3 for
details):

  1. 1.

Facts 1.1 and 3.1,

  2. 2.

Lemma 3.2,

  3. 3.

The reduction of polynomials, a technique described after Remark 3.3.

This paper has 6 sections in total. Section 1 is the introduction. In sections
2 and 3, respectively, we formalize the definitions and introduce the main
tools. Section 4 contains the main results listed in (1) above. Section 5 is
dedicated to the classification of polynomials in $S_{r}$. The last section
has some open questions and discussions that arose from the study of the
polynomials in this paper. Interested reader can also look at the works of
Shallit, Vasiga in [8] and Odoni in [9].

##  2 Definitions, notation and terminology

We will start by formally defining the polynomials mentioned in the
introduction and fixing some basic terminology that we will use throughout
this paper. Let $\mathcal{P}$ be the set of all positive primes in
$\mathbb{Z}$. For a finite subset $A$ of $\mathcal{P}$ and for
$a\in\mathbb{Z}$, we define

$\mathcal{P}_{A}:=\mathcal{P}\setminus
A\;\;\textup{and}\;\;P_{A}(a):=\\{p\in\mathcal{P}_{A}~{}|~{}p\text{ divides
}a\\}\;\;\textup{and}\;\;P(a):=P_{\emptyset}(a).$

So $P(a)$ is the set of all positive primes that divides $a$. For
$u=u(x)\in\mathbb{Z}[x]$ of degree at least 1, we define the polynomials
$u^{(1)}(x):=u(x)$ and $u^{(n+1)}(x):=u(u^{(n)}(x))$, $n\in\mathbb{N}$. Having
fixed $r$ in $\mathbb{Z}$, $A$ a finite subset of $\mathcal{P}$, $d$ in
$\mathbb{N}$ a degree and $i$ in $\mathbb{N}$ an index, we define the
following:

  1. 1.

We will say that $u(x)$ is a weakly locally nilpotent polynomial at $r$
outside $A$ if for each $p\in\mathcal{P}_{A}$, there exists $m\in\mathbb{N}$
(possibly depending on $p$) such that $u^{(m)}(r)\equiv 0\pmod{p}$. For each
$p\in\mathcal{P}_{A}$, we let $m_{p}$ be the least of all such $m^{\prime}$s.
We fix the following notation for weakly locally nilpotent polynomials at $r$
outside $A$:
$L_{r,A}^{d}:=\\{u~{}|~{}u\textup{, of degree }d,\textup{ is weakly locally
nilpotent at }r\textup{ outside }A\\},$
$L_{r,A}:=\sqcup_{d=1}^{\infty}L_{r,A}^{d}~{}$.

  2. 2.

If $A=\emptyset$ in (1), then we will just drop the terms “weakly” and
“outside $A$”.

  3. 3.

We will say that $u(x)$ is a nilpotent polynomial at $r$ if $\text{there
exists an}~{}n\in\mathbb{N}$ such that $u^{(n)}(r)=0$. We will call the
smallest of all such $n^{\prime}$s the nilpotency index/index of nilpotency of
$u(x)$ at $r$. If $u^{(n)}(r)\neq 0$ for all $n\in\mathbb{N}$, we will say
that $u$ is non-nilpotent at $r$. We fix the following notations for nilpotent
polynomials at $r$:
$N_{r,i}^{d}:=\\{u~{}|~{}u\textup{ is nilpotent at }r\textup{ of nilpotency
index }i\textup{ and degree }d\\},$
$N_{r,i}:=\sqcup_{d=1}^{\infty}N_{r,i}^{d}~{},$
$N_{r}:=\sqcup_{i=1}^{\infty}N_{r,i}~{}.$

  4. 4.

The rest of the notation are as follows:
$S_{r}:=L_{r}\setminus N_{r}$.

For integers $a,b,c~{}(c\neq 0)$, we will write $a\equiv_{c}b$ to mean
$a\equiv b\pmod{c}$.

######  Remark 2.1.

It is clear that $N_{r}\subset L_{r,\emptyset}$. But it turns out that, for
every given $r\in\mathbb{Z}$, $S_{r}$ is non-empty (see Corollaries 4.3, 4.5
and 5.4, and Theorem 5.3 below).

###  2.1 Some examples

  1. a.

Let $r\in\mathbb{Z}$. For each non-zero $q(x)\in\mathbb{Z}[x]$, $(x-r)q(x)\in
N_{r,1}$.

  2. b.

If $u(x)=-2x-4$, then $u(-1)=-2,~{}u(-2)=0$. So $u(x)\in N_{-1,2}^{1}$. If
$r\in\mathbb{Z}\setminus\\{-1\\}$, $u_{r}(x):=-(r+1)x+(r+1)^{2}\in
N_{r,2}^{1}$, and if $r\in\mathbb{Z}\setminus\\{0\\}$, $u_{r}(x):=-2x+4r\in
N_{r,2}^{1}$. Also if $r\in\mathbb{Z}\setminus\\{0\\}$, $u(x)=x\pm 1\in
N_{r,r}^{1}$, where we use the negative sign when $r$ is positive and positive
sign otherwise.

  3. c.

Let $u(x)=-2x^{2}+7x-3$. Then $u(1)=2,~{}u(2)=3$ and $u(3)=0$. So $u(x)\in
N_{1,3}^{2}$. From this and Fact 3.1 (stated and proved below) it follows that
$v(x):=2x^{2}+7x+3\in N_{-1,3}^{2}$.

  4. d.

The polynomial $u(x)=-x^{3}+9x^{2}-25x+25\in N_{2,4}^{3}$.

  5. e.

This example shows the existence of non-nilpotent, locally nilpotent
polynomials at 1. Let $u(x)=x+1$. Then by induction it is easy to see that
$u^{(n)}(1)=n+1$, for every $n\in\mathbb{N}$, and hence $u\notin N_{1}$. For
each $p\in\mathcal{P}$, $u^{(p-1)}(1)=p\equiv_{p}0$. Thus $u(x)\in S_{1}$. In
Corollary 4.3 we will see that $S_{1}=\\{x+1\\}$.

  6. f.

For every $a\in\mathbb{Z}\setminus\\{0\\}$, let $u_{a}=u_{a}(x):=x+a$. By
induction, we get $u_{a}^{(n)}(0)=na$. So it is clear that $u_{a}\notin
N_{0}$. For each prime $p$, $u_{a}^{(p)}(0)=pa\equiv_{p}0$. Thus $u_{a}\in
S_{0}$.

  7. g.

Let $u(x)=4x-2$. Then $u(1)=2$ and $u(2)=6\equiv_{5}1$. This means that
$u^{(n)}(1)$ is either 1 or 2$\pmod{5}$, for every $n\in\mathbb{N}$. This
shows that $u(x)\notin L_{1,A}$, for every finite subset
$A\subset\mathcal{P}_{\\{5\\}}$.

  8. h.

Let $u(x)$ be as in example (g). Then by induction we have
$u^{(n)}(0)=\frac{2}{3}(1-4^{n})$, which cannot be zero for any
$n\in\mathbb{N}$ and so the above polynomial is not in $N_{0}$. Clearly
$m_{2}=1,~{}m_{3}=3$. For every prime $p\in\mathcal{P}_{\\{2,3\\}}$, we have
that $u^{(p-1)}(0)\equiv_{p}0$, by Fermat’s little theorem and so $u(x)\in
S_{0}$.

######  Remark 2.2.

The computation of polynomial iterations are very complicated. But the linear
polynomials have a nice and easy-to-understand iteration formula: let
$u(x)=ax+b$ be a linear polynomial, i.e., $a\in\mathbb{Z}\setminus\\{0\\}$.
Then by induction it follows that for every $n\geq 1$,

$u^{(n)}(x)=a^{n}x+b\left(\sum\limits_{i=0}^{n-1}a^{i}\right),~{}~{}n\in\mathbb{N}.$

So $u^{(n)}(r)=a^{n}r+b\left(\sum\limits_{i=0}^{n-1}a^{i}\right)$, for each
$n\in\mathbb{N}$. Throughout this paper we will refer to this formula as the
linear iteration formula.

##  3 The main tools

In this section we will develop the necessary tools. We begin with the proof
of Fact 3.1, which indicates that for our purposes it is enough to study the
polynomials at non-negative values of $r$. In particular, it shows that there
is a one-to-one correspondence between $S_{r}$ and $S_{-r}$.

######  Fact 3.1.

Let $u(x)$ be a polynomial of degree $d$ and let
$r\in\mathbb{Z}\setminus\\{0\\}$. Define $v(x):=-u(-x)$. Then $u(x)\in
L_{r,\emptyset}^{d}\iff v(x)\in L_{-r,\emptyset}^{d}$. Similarly, $u(x)\in
N_{r,n}^{d}\iff v(x)\in N_{-r,n}^{d}$, and $u(x)\in S_{r}\iff v(x)\in S_{-r}$.

###### Proof.

Since $v(-x)=-u(x)$, by induction one sees that $v^{(n)}(-r)=-u^{(n)}(r)$,
from which the fact follows.∎

We will now state and prove the CRS Lemma which was mentioned in the
introduction. We will also justify its importance in understanding linear
locally nilpotent polynomials.

######  Lemma 3.2 (CRS Lemma).

Let $\alpha,\beta,\gamma\in\mathbb{Z}\setminus\\{0\\}$ be such that there is
no $k\in\mathbb{Z}$ such that $\frac{\beta}{\gamma}=\alpha^{k}$. Then
$\mathcal{P}\setminus\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)$ is an
infinite set.

###### Proof.

Suppose, if possible, that
$\mathcal{P}\setminus\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)$ is a
finite set. This means that the set
$\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)$ contains all but finitely
many primes. Then $\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)\setminus
P(\gamma)$ also contains all but finitely many primes. So, for almost all
$p\in\mathcal{P}_{P(\gamma)},~{}\alpha^{n_{p}}\equiv_{p}\beta\gamma^{-1}$ for
some $n_{p}\in\mathbb{N}$ (choice of $n_{p}$ possibly depends on $p$). So, if
$k\in\mathbb{N}$ is such that $\alpha^{k}\equiv_{p}1$, then
$(\beta\gamma^{-1})^{k}\equiv_{p}(\alpha^{n_{p}})^{k}\equiv_{p}1$. Thus taking
$\alpha=x$, $\beta\gamma^{-1}=y$ and $F=\mathbb{Q}$ in Theorem 1 of [3], we
arrive at a contradiction! Thus
$\mathcal{P}\setminus\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)$ is an
infinite set. ∎

######  Remark 3.3 (Importance of the CRS lemma).

Let $r\in\mathbb{Z}\setminus\\{0\\}$ and $u=u(x)=ax+b\in L_{r,\emptyset}^{1}$
with $a\neq\pm 1$. By the linear iteration formula, we get

$u^{(n)}(r)=\frac{a^{n}(r-ar-b)+b}{1-a}.$

Since $u\in L_{r,\emptyset}^{1}$, we can say that
$\mathcal{P}\setminus\cup_{n\in\mathbb{N}}P(\gamma\alpha^{n}-\beta)$ is a
finite set (in fact, it is an empty set), where $\alpha=a,\beta=-b$ and
$\gamma=r-ar-b$. Then it follows from the Lemma 3.2 that either
$\frac{\beta}{\gamma}$ or $\frac{\gamma}{\beta}$ is a power of $\alpha$, i.e.,
$b=-a^{m}(r-ar-b),$ for some $m\in\mathbb{Z}$. Moreover, if $m\in\mathbb{N}$
we can say that $u\in N_{r}$. So, to summarize, if $u$ is in $S_{r}$ (with
$a\notin\\{\pm 1\\}$), then $\text{there exists}~{}m\in\mathbb{N}\cup\\{0\\}$
such that $a^{m}b=b+ar-r$.

#### Reduction of polynomials.

Let $r\in\mathbb{N}$ and $u=u(x)\in\mathbb{Z}[x]$ such that $r|u(0)$. Define
$v=v(x):=\frac{1}{r}u(rx)$. Note that $v$ is a polynomial over $\mathbb{Z}$ of
the same degree as $u$ and $rv(1)=u(r)$. Using induction one can see that
$rv^{(n)}(1)=u^{(n)}(r),\text{ for all}~{}n\in\mathbb{N}$. Then it follows
that $u(x)$ is weakly locally nilpotent at $r$ outside some $A$ iff $v(x)$ is
weakly locally nilpotent at 1 outside $A\cup P(r)$, and also $u(x)$ is
nilpotent at $r$ iff $v(x)$ is nilpotent at 1. Thus we can reduce any
polynomial $u(x)$ in $L_{r,\emptyset}^{d}$ with the extra condition that
$r|u(0)$ to a polynomial $v(x)$ in $L_{1,P(r)}^{d}$. We will call this the
reduction of $u(x)$ to $v(x)$, where, of course, $u$ and $v$ are as above.

##  4 Arbitrary $d$ and $r\in\\{0,1,-1\\}$

In this section, we state and prove two theorems that provide the
classification of all locally nilpotent polynomials at $r$ when $r\in\\{0,\pm
1\\}$. We start with the $r=1$ case.

######  Theorem 4.1.

The following is the list of all polynomials in $L_{1,\emptyset}$:

  1. (1)

$(x-1)p(x)$, with $p(x)\in\mathbb{Z}[x]\setminus\\{0\\}$ (Nilpotent of
nilpotency index 1).

  2. (2)

$-2x+4+p(x)(x-1)(x-2)$, with $p(x)\in\mathbb{Z}[x]$ (Nilpotent of nilpotency
index 2).

  3. (3)

$-2x^{2}+7x-3+p(x)(x-1)(x-2)(x-3)$, with $p(x)\in\mathbb{Z}[x]$ (Nilpotent of
nilpotency index 3).

  4. (4)

$x+1$ (Locally nilpotent but not nilpotent).

###### Proof.

Let $u=u(x)\in L_{1,\emptyset}^{d}$. We will consider the following three
cases:

#### Case 1. $u(1)-1\not\in\\{\pm 1\\}$.

Then $P(u(1)-1)\neq\emptyset$ and for each $p\in P(u(1)-1)$ we have
$u(1)\equiv_{p}1$, i.e., for each $p\in P(u(1)-1)$, $m_{p}$ does not exist.
This is a contradiction to the hypothesis that $u\in L_{1,\emptyset}^{d}$!

#### Case 2. $u(1)-1=-1$.

These are just the polynomials listed in (1).

#### Case 3. $u(1)-1=1\textup{ or }u(1)=2$.

We now explore the possibilities for $u(2)$. If $u(2)=0$, then $u(x)$ is of
the form listed in (2). So suppose that $u(2)\neq 0$. Of course
$u(2)\notin\\{1,2\\}$ as otherwise we get $u^{(n)}(1)=$ 1 or 2, for every
$n\in\mathbb{N}$ and hence it cannot be in $L_{1,\emptyset}^{d}$. Thus $u(2)$
is either $\leq-1$ or $\geq 3$, i.e., $|u(2)-1|\geq 2$. In other words,
$P(u(2)-1)\neq\emptyset$. Let $p\in P(u(2)-1)$. Then $u(2)\equiv_{p}1$. As $u$
is locally nilpotent at $1$, $p$ must be 2 so that $u(2)-1$ must be of the
form $\pm 2^{t}$, for some $t\in\mathbb{N}$. To arrive at a contradiction
suppose that $u(2)\neq 3$. That means $u(2)$ is either $\geq 4$ or $\leq-1$.
So we consider these two possibilities one by one.

Possibility 1. $u(2)\geq 4$. We know that $u(2)-1=2^{t}$, i.e., $u(2)$ is odd.
So, in fact, $u(2)\geq 5$. Thus there exists $p\in\mathcal{P}_{\\{2\\}}$ such
that $p\in P(u(2)-2)$ and $u^{(n)}(2)\equiv_{p}2$, for every $n\in\mathbb{N}$,
a contradiction to the hypothesis that $u\in L_{1,\emptyset}^{d}$!

Possibility 2. $u(2)\leq-1$. We know that $u(2)-1=-2^{t}$, i.e., $u(2)$ is odd
so that $u(2)-2$ is odd as well and less or equal to $-3$. Using the same
argument as in possibility 1 we get a contradiction!

Thus $u(2)$ must be 3. Next, we look at $u(3)$. If $u(3)=0$, then $u(x)$ is of
the form listed in (3). So suppose that $u(3)\neq 0$. For the same reason as
above $u(3)\notin\\{0,1,2,3\\}$. Thus $u(3)$ is either $\leq-1$ or $\geq 4$.
To get to a contradiction suppose that $u(3)\neq 4$. Then either
$u(3)-3\leq-4$ or $\geq 2$. In any case, $P(u(3)-3)\neq\emptyset$. Let $p\in
P(u(3)-3)$. Then $u(3)\equiv_{p}3$ so that $p\in\\{2,3\\}$, which follows
because $u\in L_{1,\emptyset}^{d}$. If $p=2$ then $u(1)\equiv_{p}0$. Then
$u(3)\equiv_{p}3\equiv_{p}1\not\equiv_{p}u(1)$, which is an impossibility as
$3\equiv_{p}1$ must imply $u(3)\equiv_{p}u(1)$! This means $p=3$ and
$u(3)-3=\pm 3^{s}$, for some $s\in\mathbb{N}$. For similar reason,
$P(u(3)-1)\neq\emptyset$ and for each $q\in P(u(3)-1)$, $u(3)\equiv_{q}1$
which implies $q\in\\{2,3\\}$. But $q|u(3)-1=2\pm 3^{s}$, which is a
contradiction to the fact that $q\in\\{2,3\\}$! Thus $u(3)=4$.

Next, we look at $u(4)$. We claim that no further iteration of $u$ at $1$ can
be zero and we would like to prove this by showing that $u(n-1)=n$, $\text{
for all}~{}n\geq 4$ and that would mean $u(x)=x+1$. We use mathematical
induction to prove this claim. Let $u(j-1)=j$, for every $2\leq j\leq n$, for
some $n\geq 4$ and we want to show that $u(n)=n+1$. Since
$u(1)=2,~{}u(2)=3,~{}u(3)=4,~{}\ldots,u(n-1)=n$, there is a polynomial $p(x)$
such that $u(x)=x+1+p(x)(x-1)(x-2)(x-3)\cdots(x-n+1)$. So
$u(n)=n+1+p(n)\cdot(n-1)!$, which must be different from 0 as $n\geq 4$. If
$u(n)=i$ for some $i\in\\{1,\ldots,n\\}$, then the iterations
$u^{(m)}(1)\in\\{1,\ldots,n\\}$, for every $m\in\mathbb{N}$ and that means for
only finitely many primes $p$, $m_{p}$ can exist. Thus $u$ cannot be locally
nilpotent at $1$ and $u(n)\not\in\\{0,\ldots,n\\}$. This means $u(n)$ is
either $\geq n+1$ or $\leq-1$. For a contradiction, suppose that $u(n)\neq
n+1$. Then, either $u(n)-n\geq 2$ or $u(n)-n\leq-(n+1)$. In any case, we get
$P(u(n)-n)\neq\emptyset$. For each $p\in P(u(n)-n)$ we have $u(n)\equiv_{p}n$,
which is an impossibility unless $p\leq n$. Suppose, if possible, $p<n$. Then
$n\equiv_{p}a$ for some $a\in\\{1,\ldots,p-1\\}$. Note that $a$ cannot be zero
as otherwise $n\equiv_{p}0$, so that
$u(0)\equiv_{p}u(n)\equiv_{p}n\equiv_{p}0$, i.e., $p|u(0)$ and so
$p|u(p)=p+1$, an impossibility! Now by the induction hypothesis we have
$u(a)=a+1$ and also $a\equiv_{p}n\equiv_{p}u(n)\equiv_{p}u(a)$, i.e.,
$u(a)\equiv_{p}a$, which is absurd as this means $m_{p}$ does not exist! So
$p=n$, i.e., $n$ is prime and $u(n)=n\pm n^{s}$, for some $s\in\mathbb{N}$.
For similar reason, $P(u(n)-1)\neq\emptyset$. So for every $q\in P(u(n)-1)$,
$u(n)\equiv_{q}1$ and it follows that $q$ is less than or equal to $n$. But if
$q=n$, then $n=q|u(n)-1=(n-1)\pm n^{s}$ and so $n|1$, an impossibility! So, in
fact, we have $q\leq n-1$. We can choose $b\in\\{0,\ldots,q-1\\}$ such that
$n\equiv_{q}b+1$. By the induction hypothesis $u(b+1)=b+2$ and also
$u(b+1)\equiv_{q}u(n)\equiv_{q}1$. These two relations together imply
$b+1\equiv_{q}0$, i.e., $q|n$. But, since $n$ is a prime, $n=q$, which is an
impossibility, and hence $u(n)=n+1$.∎

######  Corollary 4.2.

It follows from Fact 3.1 and Theorem 4.1 that the following is the list of all
polynomials in $L_{-1,\emptyset}$:

  1. (1)

$(x+1)p(x)$, with $p(x)\in\mathbb{Z}[x]\setminus\\{0\\}$ (Nilpotent of
nilpotency index 1).

  2. (2)

$-2x-4+p(x)(x+1)(x+2)$, with $p(x)\in\mathbb{Z}[x]$ (Nilpotent of nilpotency
index 2).

  3. (3)

$2x^{2}+7x+3+p(x)(x+1)(x+2)(x+3)$, with $p(x)\in\mathbb{Z}[x]$ (Nilpotent of
nilpotency index 3).

  4. (4)

$x-1$ (Locally nilpotent but not nilpotent).

######  Corollary 4.3.

The sets $S_{1}$ and $S_{-1}$ are singleton sets.

###### Proof.

Let $u(x)\in S_{1}$. Then by Theorem 4.1, $u(x)$ must be $x+1$ as all the
other polynomials in the list (1)-(4) in there are in $N_{1}$. Now by Fact
3.1, it follows that $S_{-1}=\\{x-1\\}$. ∎

We end this section by looking at the case when $r=0.$

######  Theorem 4.4.

The following is the list of all polynomials in $L_{0,\emptyset}$:

  1. (1)

$x+b$, with $b\in\mathbb{Z}\setminus\\{0\\}$ (Locally nilpotent but not
nilpotent).

  2. (2)

$ax+b$, with $P(b)\supseteq P(a)\neq\emptyset$ and $b\neq 0$ (Locally
nilpotent but not nilpotent).

  3. (3)

$xp(x)$, with $p(x)\in\mathbb{Z}[x]\setminus\\{0\\}$ (Nilpotent of nilpotency
index 1).

  4. (4)

$(x-a)p(x)$, with $a\in\mathbb{Z}\setminus\\{0\\}$ and $p(x)\in\mathbb{Z}[x]$
s.t $p(0)=-1$ (Nilpotent of nilpotency index 2).

###### Proof.

First suppose that $u$ is nilpotent of nilpotency index $m$, for some
$m\in\mathbb{N}$. If $u(0)=0$, then $m=1$ and $u(x)=xp(x),$ for some non-zero
$p(x)\in\mathbb{Z}[x]$, which is (3) in the list. So suppose that $u(0)\neq
0$. Define

$u_{0}:=u(0),~{}u_{n}:=u^{(n+1)}(0)-u^{(n)}(0),~{}n\in\mathbb{N}.$

Then $u_{n+1}=u^{(n+2)}(0)-u^{(n+1)}(0)=u(u^{(n+1)}(0))-u(u^{(n)}(0)).$ That
means $u_{n}$ divides $u_{n+1},\text{ for all}~{}n\in\mathbb{Z}_{\geq 0}$. We
also have $u^{(m)}(0)=0$ so that
$u_{m}=u^{(m+1)}(0)-u^{(m)}(0)=u^{(m+1)}(0)=u_{0}$. As
$u_{0}|u_{1}|\ldots|u_{m}=u_{0},$ it follows that $u_{n}=\pm u_{0},$ for all
$n.$ Also note that $u_{0}+\cdots+u_{m-1}=u^{(m)}(0)=0$. This means $m$ must
be even and half of these integers is positive and the other half is negative
(since $|u_{n}|=|u_{0}|,\text{ for all}~{}n$). So there exists
$k\in\\{1,\ldots,m-1\\}$ such that $u_{k-1}=-u_{k},$ i.e.,
$u^{(k)}(0)-u^{(k-1)}(0)=u^{(k)}(0)-u^{(k+1)}(0),$ i.e.,
$u^{(k+1)}(0)=u^{(k-1)}(0)$. Thus $u^{(n+2)}(0)=u^{(n)}(0),\text{ for
all}~{}n\geq k-1$ and so, in particular,
$0=u^{(m)}(0)=u^{(m+2)}(0)=u^{(2)}(0)$. Hence, $m=2$ and $u(x)=(x-a)p(x)$,
with $a\in\mathbb{Z}\setminus\\{0\\}$ and $p(x)\in\mathbb{Z}[x]$ with
$p(0)=-1$; here $a=u(1),$ which is (4) in the list.

Now suppose that $u\in S_{0}$. Then by Fact 1.1, it must be linear. Let
$u(x):=ax+b,a\neq 0$. Note that if $b\neq 0$ as otherwise $u$ would be
nilpotent. When $a=1$, every $u(x)\in S_{0}$: in fact if $u(x)=x+b$, then by
the linear iteration formula, $u^{(n)}(0)=b(1+\cdots+1)=bn$, which is non-zero
$\text{ for all}~{}n\in\mathbb{N}$ and for each prime $p$,
$u^{(p)}(0)=bp\equiv_{p}0$. When $a=-1$, $u^{(2)}(0)=0$. So $a$ must be
different from $-1$. Thus we can assume that $|a|\geq 2$, i.e., $P(a)$ is a
non-empty, finite set. Again, using the linear iteration formula, we get
$u^{(n)}(0)=b(1+\cdots+a^{n-1}),~{}n\in\mathbb{N}$. Suppose, if possible,
there exists some prime $p$ in $P_{P(b)}(a)$, i.e., there is a prime $p$ such
that $p|a$ but $p\nmid b$. Then $u^{(n)}(0)\equiv_{p}b$, for every
$n\in\mathbb{N}$ and that means $u$ cannot be locally nilpotent. Thus
$P(b)\supseteq P(a)\neq\emptyset$. If $p\in P(b)$, then $m_{p}=1$.
If $p\notin P(b)\cup P(a-1)$, then
$u^{(p-1)}(0)=\frac{b}{a-1}(a^{p-1}-1)\equiv_{p}0$, which follows from
Fermat’s little theorem.
Finally if $p\in P(a-1)$, then
$u^{(p)}(0)=b(1+\cdots+a^{p-1})\equiv_{p}b(1+\cdots+1)\equiv_{p}0$. Thus
$m_{p}$ exists for every $p\in\mathcal{P}$.∎

######  Corollary 4.5.

The following is the list of all polynomials in $S_{0,\emptyset}$:

  1. (1)

$x+b$, with $b\in\mathbb{Z}\setminus\\{0\\}$.

  2. (2)

$ax+b$, with $P(b)\supseteq P(a)\neq\emptyset$ and $b\neq 0$.

##  5 Linear case $d=1$

In this section we classify all polynomials that are locally nilpotent but
non-nilpotent at $r$. Since the cases $r=0$ and $r=\pm 1$ have been covered in
the previous section, here our focus would be on the values of $r$ that lie in
$\mathbb{Z}\setminus\\{0,\pm 1\\}$. First, we state and prove a classification
theorem for polynomials which are weakly locally nilpotent at 1 outside some
given finite subset $A$ of $\mathcal{P}$. We will use this theorem to prove
our final main result, Theorem 5.3.

######  Theorem 5.1.

Let $A=\\{q_{1},\ldots,q_{k}\\}$, where $q_{1},\ldots,q_{k}$ are $k$ distinct
primes. Then the following is the list of all the polynomials in
$L_{1,A}^{1}$:

  1. (1)

$x\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where
$s_{i}\in\mathbb{N}\cup\\{0\\}$.

  2. (2)

$\alpha(x-1)$, $\alpha\in\mathbb{Z}\setminus\\{0\\}$.

  3. (3)

$\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}x+1$, where
$s_{i}\in\mathbb{N}\cup\\{0\\}$ such that $\sum s_{i}\geq 1$.

  4. (4)

$-2x-1$ (only when $2\in A$).

  5. (5)

$-2x+4$.

###### Proof.

Let $u=u(x)\in L_{1,A}^{1}$. Then by Fact 1.1 it must be linear, say $ax+b$.
It is clear that $b\neq 0$ as otherwise $u^{(n)}(1)$ would just be $a^{n}$ and
it cannot be divisible by any prime $p\in\mathcal{P}_{P(a)}$. By the linear
iteration formula, $u^{(n)}(1)=a^{n}+b(1+\cdots+a^{n-1})$, for every
$n\in\mathbb{N}$.

$\displaystyle\text{Note that if }a=1,~{}u^{(m_{p})}(1)$
$\displaystyle=1+bm_{p}\equiv_{p}0,\text{ for every prime }p\notin A,$
$\displaystyle\implies$ $\displaystyle bm_{p}\equiv_{p}-1,\text{ for every
prime }p\notin A,$ $\displaystyle\implies$ $\displaystyle b\text{ is
invertible in }\mathbb{F}_{p},\text{ for every prime }p\notin A,$
$\displaystyle\implies$ $\displaystyle b=\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}},\text{ for some }s_{i}^{\prime}s\textup{ in
}\mathbb{N}\cup\\{0\\}.\hskip 57.0pt$

One can check that the polynomials $x\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$
are indeed in $L_{1,A}^{1}$, for $s_{i}\in\mathbb{N}\cup\\{0\\}$.

If $a=-1$, $u(x)=-x+b$ and $u^{(2)}(x)=x$. So $u$ cannot be in $L_{1,A}^{1}$
unless $b=1$, and in that case, it is in fact in $N_{1,1}^{1}$. Thus we can
assume that $|a|\geq 2$. Similar to the proof of Theorem 4.1, we can break
down these polynomials into the following three cases:

#### Case 1. $u(1)-1\notin\\{\pm 1\\}$.

This means that $P(u(1)-1)\neq\emptyset$. So $a+b=1\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}}$, i.e., $b=1-a\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, for some
$s_{i}\in\mathbb{N}\cup\\{0\\}$ with $\sum s_{i}\geq 1$. Then by the linear
iteration formula, we have

$u^{(n)}(1)=\frac{b\pm a^{n}(1-a-b)}{1-a}$

and it follows from Remark 3.3 that $\text{there exists an }m\in\mathbb{Z}$
such that $b=\pm a^{m}(1-a-b)$. If $m=0$, then $b=\pm(1-a-b)$, i.e., $a+2b=1$
or $a=1$. Since $|a|\geq 2$, we deduce that $a+2b=1$.We also have $a+b=1\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$. Solving $a$ and $b$ from these two
equations we get $a=1\pm 2q_{1}^{s_{1}}\cdots q_{k}^{s_{k}},~{}b=\mp
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$. So $u(x)=(1\pm 2q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})x\mp q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$ and so
$u^{(n)}(1)=\frac{1+(1\pm 2q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})^{n}}{2},~{}n\in\mathbb{N}$. Letting $\alpha=1\pm
2q_{1}^{s_{1}}\cdots q_{k}^{s_{k}},\beta=-1$ and $\gamma=1$, it is clear that
neither $\frac{\beta}{\gamma}$ nor $\frac{\gamma}{\beta}$ is a power of
$\alpha$. So it follows from the Lemma 3.2 that $(1\pm 2q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})x\mp q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}\notin L_{1,A}^{1}$. Thus
$m$ must be a non-zero integer. We consider the following four possibilities:

If $m\in\mathbb{N}$ and $b=a^{m}(1-a-b)$, then $b(1+a^{m})=a^{m}(1-a)$. Since
$\gcd(a^{m},a^{m}+1)=1$, we must have $a^{m}+1|1-a$ which is only possible if
$m=1$.

If $m\in\mathbb{N}$ and $b=-a^{m}(1-a-b)$, then $b(1-a^{m})=-a^{m}(1-a)$,
i.e., $b(1+\cdots+a^{m-1})=-a^{m}$. Since $\gcd(1+\cdots+a^{m-1},a^{m})=1$, we
must have $1+\cdots+a^{m-1}=\pm 1$ which is only possible if $m\in\\{1,2\\}$.

If $m=-n,\text{ with }n\in\mathbb{N}$ and $b=a^{m}(1-a-b)$, then
$ba^{n}=1-a-b$, i.e., $b(a^{n}+1)=1-a$. It follows from above that this is
only possible if $n=1$.

If $m=-n,\text{ with }n\in\mathbb{N}$ and $b=-a^{m}(1-a-b)$, then
$ba^{n}=-(1-a-b)$, i.e., $b(a^{n}-1)=a-1$. Again using the same logic as
above, we conclude that $n\in\\{1,2\\}$.

Thus we only need to look at $m=\pm 1,\pm 2$, which we investigate in the
following four subcases:

Subcase 1. $m=-1$.
Here we have $ba=\pm(1-a-b)$. First suppose that $ba=1-a-b$, i.e.,
$b(a+1)=1-a$. This means that $a+1|a-1$ and this is only possible if $a=-2$
and $a=-3$. These values generate the polynomials $u(x)=-2x-3$ and
$u(x)=-3x-2$, respectively. When $u(x)=-2x-3$, the linear iteration formula
gives

$u^{(n)}(1)=2(-2)^{n}-1.$

Letting $\alpha=-2,\beta=1$ and $\gamma=2$, it is clear that neither
$\frac{\beta}{\gamma}$ nor $\frac{\gamma}{\beta}$ is a power of $\alpha$. So,
by the Lemma 3.2, $-2x-3\notin L_{1,A}^{1}$. Similarly we can show that
$-3x-2\notin L_{1,A}^{1}.$

Now suppose $ba=-(1-a-b)$. This gives $b=1$ and hence $a=\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$. Thus $u(x)=\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}}x+1$ and it follows from the linear iteration formula that

$u^{(n)}(1)=(\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}})^{n}+[1+\cdots+(\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}})^{n-1}]=\frac{1-(\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})^{n+1}}{1-(\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})},~{}n\in\mathbb{N}.$

If $p\in P_{A}(1-(\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}))$, then
$u^{(p)}(1)\equiv_{p}p\equiv_{p}0$. So suppose that $p\notin P_{A}(1-(\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}))$. Now if $2\in A$, then the existence of
$m_{2}$ is not a concern and if $2\notin A$, then $2\in P_{A}(1-(\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}))$ which was covered above. Finally, if $p$
is in ${A\cup\\{2\\}}$, then $u^{(p-2)}(1)\equiv_{p}0$, by Fermat’s little
theorem. So $u(x)=\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}x+1$ is in
$L_{1,A}^{1}$.

Subcase 2. $m=1$.
Here we have $b=\pm a(1-a-b)$. First suppose that $b=a(1-a-b)$, i.e.,
$b(a+1)=a(1-a)$. The same reasoning as above implies $a+1|a-1$ so that the
only possibilities we get are $a=-2,~{}b=6$ or $a=-3,~{}b=6$. These values
produce the polynomials $u(x)=-2x+6$ and $u(x)=-3x+6$, respectively. When
$u(x)=-2x+6$, the linear iteration formula gives

$u^{(n)}(1)=-(-2)^{n}+2.$

Letting $\alpha=-2,\beta=-2$ and $\gamma=-1$, it is clear that neither
$\frac{\beta}{\gamma}$ nor $\frac{\gamma}{\beta}$ is a power of $\alpha$. So,
by the Lemma 3.2, $-2x+6\notin L_{1,A}^{1}$. Similarly, we can show that
$-3x+6\notin L_{1,A}^{1}$.

Subcase 3. $m=-2$.
Here we have $ba^{2}=\pm(1-a-b)$. First suppose $ba^{2}=1-a-b$, i.e.,
$b(a^{2}+1)=1-a$. This means that $a^{2}+1|a-1$ which is not possible as
$|1-a|\leq 1+|a|<1+a^{2}$. Thus $ba^{2}=-(1-a-b)$, i.e., $b(a+1)=1$, i.e.,
$b=a+1=\pm 1$. So $u(x)=-2x-1$. It follows from the linear iteration formula
that

$u^{(n)}(1)=(-2)^{n}-[1+\cdots+(-2)^{n-1}]=\frac{(-2)^{n+2}-1}{3},~{}n\in\mathbb{N}.$

It is easy to see that $m_{2}$ does not exist, $m_{3}=1$ and for all
$p\in\mathcal{P}_{\\{2,3\\}}$, $u^{(p-3)}(1)\equiv_{p}0$. So $-2x-1$ is in
$L_{1,A}^{1}$ iff $2\in A$.

Subcase 4. $m=2$.
Here we have $b=\pm a^{2}(1-a-b)$. First suppose that $b=a^{2}(1-a-b)$, i.e.,
$b(1+a^{2})=a^{2}(1-a)$. Since $\gcd(1+a^{2},a^{2})=1$, we must have
$1+a^{2}|1-a$, which is impossible (see the subcase 3 above). So
$b=-a^{2}(1-a-b)$, i.e., $b(a+1)=-a^{2}$ which means $a+1=\pm 1$ and $b=\mp
a^{2}$. Since $|a|\geq 2$, this means $a=-2$ and $b=4$. But then
$u(1)-1=1\in\\{\pm 1\\},$ an impossibility in this case!

This wraps us case 1. Now we look at the remaining two cases.

#### Case 2. $u(1)-1=-1$, i.e., $u(1)=0$.

These are the polynomials in $N_{1,1}^{1}$.

#### Case 3. $u(1)-1=1$, i.e., $u(1)=2$.

If $u(2)=0$, then $u(x)=-2x+4$. So we can suppose that
$u(2)\notin\\{0,1,2\\}$, i.e., $u(2)$ is either $\leq-1$ or $\geq 3$, i.e.,
$|u(2)-1|\geq 2,$ i.e., $P(u(2)-1)\neq\emptyset$. If $u(2)=3$, then
$u(x)=x+1\in S_{1}$. So we can further assume that $u(2)\neq 3$. Since
$u(1)=2,~{}b=2-a$ and so $u(x)=ax+(2-a)$. Then by the linear iteration
formula, we get

$u^{(n)}(1)=\frac{2-a-a^{n}}{1-a},~{}~{}n\in\mathbb{N}.$

Since $u\in L_{1,A}^{1}$ it follows from Remark 3.3 that $2-a=a^{m}$, for some
$m\in\mathbb{Z}$. Note that $m$ cannot be a non-positive integer as otherwise
it would follow that $a$ must be equal to $\pm 1$. Thus $m\in\mathbb{N}$ and
$2=a(1+a^{m-1})$. Therefore $a=\pm 2$ and $1+a^{m-1}=\pm 1,$ i.e.,
$a^{m-1}=-2$, i.e., $a=-2$. But $a=-2$ implies that $b=4$ and hence
$u(2)=2a+b=0$, which cannot happen as we have already said that
$u(2)\not\in\\{0,1,2,3\\}$. Thus $ax+(2-a)\notin L_{1,A}^{1}$. ∎

The next corollary follows directly from the computations in the proof of
Theorem 5.1:

######  Corollary 5.2.

Let $A=\\{q_{1},\ldots,q_{k}\\}$ and $q_{1},\ldots,q_{k}$ be $k$ distinct
primes. Then the following is the list of all polynomials in
$L_{1,A}^{1}\setminus N_{1}$:

  1. (1)

$x+q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$.

  2. (2)

$x-q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$
such that $\sum s_{i}\geq 1$.

  3. (3)

$\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}x+1$, where
$s_{i}\in\mathbb{N}\cup\\{0\\}$ such that $\sum s_{i}\geq 1$.

  4. (4)

$-2x-1$ (only when $2\in A$).

Finally we state and prove the last (main) result of this paper.

######  Theorem 5.3.

Let $r$ be a natural number greater than or equal to 2 and
$r=q_{1}^{a_{1}}\cdots q_{k}^{a_{k}}$ be the prime decomposition. Then the
following is the list of all polynomials in $S_{r}$:

  1. (1)

$x+q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$.

  2. (2)

$x-q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$
with at least one $j\in\\{1,\ldots,k\\}$ s.t. $s_{j}>a_{j}$.

  3. (3)

$\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}x+r$, where
$s_{i}\in\mathbb{N}\cup\\{0\\}$ with $\sum\limits_{i}s_{i}\geq 1$.

  4. (4)

$-2x-r$ (only when $r$ is even).

###### Proof.

Let $u=u(x)\in S_{r}$ and $A:=P(r)$. Then by Fact 1.1 $u$ must be linear, say
$ax+b$. First we will look at the instances when $a=\pm 1$.

$\displaystyle\text{Note that if }a=1,~{}u^{(m_{p})}(1)=$ $\displaystyle
1+bm_{p}\equiv_{p}0,\text{ for every prime }p\notin A,$
$\displaystyle\implies$ $\displaystyle bm_{p}\equiv_{p}-1,\text{ for every
prime }p\notin A,$ $\displaystyle\implies$ $\displaystyle b\text{ is
invertible in }\mathbb{F}_{p},\text{ for every prime }p\notin A,$
$\displaystyle\implies$ $\displaystyle b=\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}},\text{ for some }s_{i}^{\prime}s\textup{ in
}\mathbb{N}\cup\\{0\\}.\hskip 57.0pt$

So, when $a=1$, we expect $u(x)$ to be of the form $x\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}}$. First suppose that $u(x)=x+q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$.
Then by the linear iteration formula, $u^{(n)}(r)=q_{1}^{a_{1}}\cdots
q_{k}^{a_{k}}+n\cdot q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, which is always non-
zero for every $n\in\mathbb{N}$. One can check that these polynomials are
locally nilpotent and they are in (1) in the list above. Now suppose that
$u(x)=x-q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$. Then by the linear iteration
formula $u^{(n)}(r)=q_{1}^{a_{1}}\cdots q_{k}^{a_{k}}-n\cdot
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}},~{}n\in\mathbb{N}$. If, for all
$i\in\\{1,\ldots,k\\}$, $s_{i}\leq a_{i}$, then $u^{(q_{1}^{a_{1}-s_{1}}\cdots
q_{k}^{a_{k}-s_{k}})}(r)=0$, which is a contradiction as $u$ is non-nilpotent!
That means we must have at least one $j\in\\{1,\ldots,k\\}$ such that
$a_{j}<s_{j}$. One can now check that $u$ is non-nilpotent but locally
nilpotent and so we get the polynomials in (2) in the list above.

If $a=-1$, $u(x)=-x+b$ and $u^{(2)}(x)=x$. So $u$ cannot be in
$L_{r,\emptyset}^{1}$ unless $b=r$, and in that case, it is in fact in
$N_{r,1}^{1}$, a contradiction! So $a\neq-1$. Thus we suppose $|a|\geq 2$. It
follows from Remark 3.3 that $\text{there exists an
}~{}m\in\mathbb{N}\cup\\{0\\}$ such that $a^{m}b=b+ar-r$. If $m=0$ then
$r(1-a)=0$ which is an impossibility as $r\neq 0$ and $|a|\geq 2$. That means
that $m\in\mathbb{N}$ and $b(a^{m}-1)=r(a-1),$ i.e., $b(1+\cdots+a^{m-1})=r$
so that $b|r$.

We want to show that $u(r)-r\notin\\{\pm 1\\}$. Suppose otherwise, i.e.,
$u(r)=r\pm 1$. This means that $b=r-ar\pm 1$, i.e., $u(x)=ax+(r-ar\pm 1)$. We
will only consider the possibility $b=r-ar-1$ as the other possibility can be
rejected using the same argument. Applying the linear iteration formula, we
get

$u^{(n)}(r)=\frac{a^{n}+r-ar-1}{1-a}=\frac{a^{n}+b}{1-a},~{}\text{ for all
}n\in\mathbb{N}.$

From Remark 3.3 it follows that $r-ar-1=-a^{t}$, for some $t\in\mathbb{Z}$. It
is clear that $t\neq 0$, as otherwise $r-ar=0,$ i.e., $r(1-a)=0,$ i.e., either
$r=0$ or $a=1$, which is not true! If $t=-n$ for some $n\in\mathbb{N}$, then
$a^{n}(r-ar-1)=-1,$ again an impossibility as $|a|\geq 2$! Thus
$t\in\mathbb{N}$ and $r(1-a)=1-a^{t}$, i.e., $r=1+\cdots+a^{t-1}$. So $t\geq
2$, $a|r-1$ and $u^{(t)}(r)=0$, i.e., $u$ is nilpotent at $r$, a
contradiction! Thus $u(r)-r$ cannot be a unit and $u(r)=r\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, for a suitable collection of
$s_{i}^{\prime}s$ in $\mathbb{N}\cup\\{0\\}$ with $\sum\limits_{i}s_{i}\geq
1$. So $b=r-ar\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$. But then $b|r$ implies
that $b|q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, i.e., $\text{there
exists}~{}t_{i}\in\mathbb{N}\cup\\{0\\}$, with $t_{i}\leq s_{i}$ for every
$i$, such that $b=\pm q_{1}^{t_{1}}\cdots q_{k}^{t_{k}}$. From $b=r-ar\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$ we get $ra=r-b\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}}=r-b(\pm 1\pm q_{1}^{s_{1}-t_{1}}\cdots q_{k}^{s_{k}-t_{k}})$,
i.e., $r|b(\pm 1\pm q_{1}^{s_{1}-t_{1}}\cdots q_{k}^{s_{k}-t_{k}})$.
Suppose, if possible, all the $t_{i}^{\prime}s$ are zero. Then $b=\pm 1$ and
so $r$ must divide $\pm 1\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, which is
clearly absurd as $\gcd(r,\pm 1\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}})=\gcd(q_{1}^{a_{1}}\cdots q_{k}^{a_{k}},\pm 1\pm
q_{1}^{s_{1}}\cdots q_{k}^{s_{k}})=1$. Thus $\sum\limits_{i}t_{i}\geq 1$. All
of these now boil down to the following two cases:

#### Case 1. $There~{}exists~{}j\in\\{1,\ldots,k\\}~{}s.t.~{}s_{j}>t_{j}$.

Since $\gcd(r,\pm 1\pm q_{1}^{s_{1}-t_{1}}\cdots q_{k}^{s_{k}-t_{k}})=1$, $r$
must divide $b$ so that we can deduce $r=\pm b$. So $a_{i}=t_{i}\leq
s_{i},~{}\text{ for all}~{}i\in\\{1,\ldots,k\\}$. We use the technique of
reduction of polynomials here. Define $v=v(x):=\frac{1}{r}u(rx)=ax\pm 1.$ Then

$v(1)=\frac{1}{r}u(r)=\frac{1}{r}(r\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}})=1\pm
q_{1}^{s_{1}-a_{1}}\cdots q_{k}^{s_{k}-a_{k}}$

and $v\in L_{1,A}^{1}\setminus N_{1}$. It follows now from the list in
Corollary 5.2 that we have two possibilities for $v$ (since $|a|\geq 2$):

  1. (i)

$v(x)=\pm q_{1}^{s_{1}-a_{1}}\cdots q_{k}^{s_{k}-a_{k}}x+1$, in which case
$u(x)=\pm q_{1}^{s_{1}-a_{1}}\cdots q_{k}^{s_{k}-a_{k}}x+r$, or

  2. (ii)

$v(x)=-2x-1$ (only when $2\in A$), in which case $u(x)=-2x-r$.

One can check that both (i) and (ii) are indeed in $S_{r}$.

#### Case 2. $For~{}each~{}i\in\\{1,\ldots,k\\},~{}s_{i}=t_{i}$.

Then $\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}=b|r$, i.e., $a_{i}\geq s_{i}$ for
each $i$. From $b=r-ar\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$ we get
$r(1-a)=\pm 2q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}=\pm 2b$. Thus either $r=\pm b$
or $r=\pm 2b$. The first possibility has been taken care of in Case 1\. So we
can assume that $r=2q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}=\pm 2b$. That would mean
$a=2$ and that $2\in A$. Without loss of generality, let $q_{1}=2$ so that
$r=2^{s_{1}+1}\cdots q_{k}^{s_{k}}$. Rewriting $b=r-ar\pm q_{1}^{s_{1}}\cdots
q_{k}^{s_{k}}$ gives us $2r=r-2b$, i.e., $r=-2b$. This means that
$u(x)=2x-\frac{r}{2}$. It follows from the linear iteration formula that

$u^{(n)}(r)=\frac{r}{2}\cdot(2^{n}+1),~{}n\in\mathbb{N}.$

Letting $\alpha=2,\beta=-1,\gamma=1$, we can see that neither
$\frac{\beta}{\gamma}$ nor $\frac{\gamma}{\beta}$ is a power $\alpha$. Thus
from the Lemma 3.2, $\mathcal{P}\setminus P(2^{n}+1)$ is an infinite set so
that $\mathcal{P}\setminus P(\frac{r}{2}\cdot(2^{n}+1))$ is also an infinite
set. So $2x-\frac{r}{2}\not\in S_{r}$. This completes the proof.∎

It follows directly from Fact 3.1 and Theorem 5.3 that:

######  Corollary 5.4.

If $r=-q_{1}^{a_{1}}\cdots q_{k}^{a_{k}}$ is the prime decomposition of an
integer $r\leq-2$, then the following is the list of all polynomials in
$S_{r}$:

  1. (1)

$x-q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$.

  2. (2)

$x+q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}$, where $s_{i}\in\mathbb{N}\cup\\{0\\}$
with at least one $j\in\\{1,\ldots,k\\}$ s.t. $s_{j}>a_{j}$.

  3. (3)

$\pm q_{1}^{s_{1}}\cdots q_{k}^{s_{k}}x-r$, where
$s_{i}\in\mathbb{N}\cup\\{0\\}$ with $\sum\limits_{i}s_{i}\geq 1$.

  4. (4)

$-2x+r$ (only when $r$ is even).

##  6 Some open problems

For $u(x)$, a non-constant polynomial over $\mathbb{Z}$, let

$N(u):=\\{r\in\mathbb{Z}~{}|~{}u\in
N_{r}\\},~{}~{}LN(u):=\\{r\in\mathbb{Z}~{}|~{}u\in L_{r,\emptyset}\\}.$

Then one can look at the following questions:

  1. Q1.

Describe all $u^{\prime}s$ such that $N(u)$ is finite.

  2. Q2.

Describe all $u^{\prime}s$ such that $LN(u)$ is finite.

  3. Q3.

Given $r\in\mathbb{Z}$, describe all $u^{\prime}s$ such that $r\in LN(u)$.

Few words about the open problems. The methods used in the paper are actually
useful for linear polynomials and due to Fact 1.1 we were able to achieve our
goal by studying the linear polynomials only. It is clear that if $u$ is
assumed to be linear, then $N(u)$ is finite for every $u$ except for the
polynomials of the form $\pm x\pm c$, $c\in\mathbb{Z}\setminus\\{0\\}$. This
answers Q1 for linear polynomials $u(x)$. It should be noted that
$LN(u)=N(u)\cup\\{r\in\mathbb{Z}~{}|~{}u\in S_{r}\\}$. So for Q2, due to Fact
1.1 again, if the degree of $u$ is greater than or equal to 2 then $LN(u)$ is
finite so that $N(u)$ is finite. For linear polynomials of the form $\pm x\pm
c$, $c\in\mathbb{Z}\setminus\\{0\\}$, $N(u)$ is infinite and so $LN(u)$ is
infinite. If $u=ax+b$ with $a\neq 1$, then we know that
$u^{(n)}(r)=\frac{a^{n}(r-a-b)+b}{1-a}$. Note that $\frac{b}{a+b-r}=a^{k}$,
for some $k\in\mathbb{Z}$ can only be true for finitely many values of $r$. So
it follows from Lemma 3.2 that
$\mathcal{P}\setminus\cup_{n\in\mathbb{N}}P((r-a-b)a^{n}+b)$ is finite for
only finitely many values of $r$. Thus for these polynomials, $LN(u)$ is
indeed finite. In this paper we have fully classified $S_{r}$, for every
integer $r$. Also given an $r$, using the linear iteration formula it should
be easy enough to describe the linear $u^{\prime}s$ such that $r\in N(u)$. So
we have a partial answer for Q3 here. Thus if one knows enough about the form
of the nilpotent polynomials of degree higher than or equal to 2, one should
potentially be able to answer all of the questions above. This is a work in
progress and it is of course important enough to be considered as a separate
work.

Acknowledgements. The author gratefully acknowledges his advisors Prof.
Alexander Borisov and Prof. Adrian Vasiu for their constant support,
encouragement and very helpful suggestions. The author would also like to
thank Prof. Jeremy Rouse for suggesting [3] which was one of the main tools
used to prove Theorems 5.1 and 5.3 and Prof. Kiran Kedlaya for maintaining a
wonderful archive of William Lowell Putnam Mathematics Competition questions
and answers here https://kskedlaya.org/putnam-archive/, which was very helpful
in the proof of Theorem 4.4. Finally, the author would like to thank Prof.
Thomas Tucker for his suggestion to use Theorem 5 of [4], which led to Fact
1.1 and that was very useful to boil down the possible candidates for locally
nilpotent polynomials.

## References

  * [1] A. Borisov. Geometrically nilpotent subvarieties. Finite Fields Appl., 50 (2018), 366-371
  * [2] A. Borisov. Iterations of integer polynomial maps modulo primes. J. Integer Seq. Vol. 16 (2013), Article 13.8.3
  * [3] C. Corrales-Rodrigáñez and R. Schoof. The support problem and its elliptic analogue. J. Number Theory, 64 (1997), Article No. NT972114, 276-290
  * [4] R.L. Benedetto, D. Ghioca, B. Hutz, P. Kurlberg, T. Scanlon and T.J. Tucker. Periods of rational maps modulo primes. Math. Ann., 355 (2013), 637-660
  * [5] R. Benedetto, D. Ghioca, P. Kurlberg, T. J. Tucker, U. Zannier. A case of the dynamical Mordell-Lang conjecture. (with an appendix by Umberto Zannier) Math. Ann. 352 (2012), 1-26
  * [6] J. P. Bell, D. Ghioca, and T. J. Tucker. The dynamical Mordell-Lang conjecture. Math. Surveys Monogr., 210 (2016), xiv+280 pp
  * [7] J. H. Silverman. Integer points, Diophantine approximation, and iteration of rational maps. Duke Math. J. 71(3) (1993), 793-829
  * [8] J.O. Shallit and M.J.T. Vasiga. On the iteration of certain quadratic maps over GF($p$). Discrete Math., 277 (2004), no. 1-3, 219-240
  * [9] R.W.K. Odoni. The Galois theory of iterates and composites of polynomials. Proc. Lond. Math. Soc. (3) 51 (1985), 385-414


This paper presents a formalization of the classical proof of completeness in Henkin-style
developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models.

The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization.

We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model.

Our implementation is restricted to a system of intuitionistic propositional logic with implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization.
As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. The full source code can be found online at <https://github.com/bbentzen/ipl>.

§ INTRODUCTION

Troelstra and van Dalen [17] propose a completeness proof in Henkin-style for full intuitionistic predicate logic with respect to Kripke models.

Despite being a fairly standard result in the literature, this completeness proof has yet to be formally verified in a proof assistant.

In this paper, we describe a formalization for intuitionistic propositional logic using the Lean theorem prover [13].

Our main goal is to document some challenges encountered along the way and the design choices made to overcome them to obtain a formalized proof that is elegant, intuitive, and better suited for mechanization using the specific techniques available in the Lean programming language, in particular, the  and  methods developed by Bentzen [1].

To the best of our knowledge, our implementation is the first verified Henkin-style proof of strong completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature.

As far as its propositional fragment is concerned, the main ingredient of Troelstra and van Dalen's Henkin-proof is a model construction based on a consistent extension of sets of formulas, which is achieved by going through all disjunctions of the language <cit.>. To carry out this extension, they assume an enumeration of disjunctions with infinite repetitions, also remarking that an alternative approach in which at each stage we treat the first disjunction not yet treated. This variant appears in Van Dalen <cit.>.

Our implementation is based on a third variant of the consistent extension method, which we developed to better suit our needs of formalization. Each propositional formula is only listed once in the enumeration, but we carry out the extension for each of them infinitely many times.

The formalization consists of roughly 800 lines of code and encompasses the syntax and semantics of intuitionistic propositional logic, along with the soundness and strong completeness theorems.

We adopt a Hilbert-style proof system due to its simplicity. The full source code can be found online at <https://github.com/bbentzen/ipl>.

§.§ Related work

The formal verification of completeness proofs for intuitionistic logic can be traced back to Coquand's [3] use of ALF to mechanize a constructive proof of soundness and completeness with respect to Kripke models for the simply typed lambda-calculus with explicit substitutions.

Heberlin and Lee [9] give a constructive completeness proof of Kripke
semantics with constant domain for intuitionistic logic with implication
and universal quantification in Coq. Recently, Hagemeier and Kirst [8]
formalize a constructive proof of completeness for intuitionistic epistemic logic based on a natural deduction system.
They also provide a classical Henkin proof using methods similar to those in Bentzen [1], but they do not present a formalization of the approach of Troelstra and van Dalen [17] as is done in this paper.

Bentzen [1] formalizes the Henkin-style completeness method for modal logic S5 using Lean and From formalizes in Isabelle/HOL a Henkin-style completeness proof for both classical propositional logic [6] and classical first-order logic [7].

Maggesi and Brogi [12] give a formal completeness proof for provability logic in HOL Light.

The formalization presented here is inspired by the work of Bentzen [1], but makes a few improvements regarding design choices, in particular, the use of Prop in the definition of the semantics and the indexing of models to arbitrary types.

§.§ Lean

Lean [13] is an interactive theorem prover based on the version of dependent type theory known as the calculus of constructions with inductive types [15, 4]. Users can construct proof terms directly as in Agda [14], using tactics as in Coq [16] or both proof terms and tactics simultaneously. Lean's built-in logic is constructive, but it supports classical reasoning as well. In fact, our Henkin-style proof is classical since it relies on a nonconstructive use of contraposition.
Therefore, we do not worry about any complexity and computational aspects related to our proof. Our implementation makes use of some results from Lean's standard library and the user-maintained mathematical library  [2].

Throughout the remainder of this paper, Lean code will be used to showcase some design decisions in our formalization.

The syntax and semantics of intuitionistic propositional logic that is the starting point of our formalization is described in <Ref>. We also describe our formalization of a countermodel for the law of excluded middle and sketch a proof of soundness. Then, an informal overview of the Henkin-style proof method as well as a description of our implementation is provided in <Ref>. Finally, some concluding remarks are given in <Ref>.

§ INTUITIONISTIC LOGIC

§.§ The language

The intuitionistic propositional language considered here contains implication, conjunction, disjunction, and falsity as the only primitive logical connectives. The language is defined using inductive types with one constructor for propositional letters, falsum, implication, conjunction, and disjunction, respectively:

inductive form : Type
| atom : $\mathbb{N}$ $\rightarrow$ form
| bot  : form
| impl : form  $\rightarrow$ form  $\rightarrow$ form
| and  : form  $\rightarrow$ form  $\rightarrow$ form
| or   : form  $\rightarrow$ form  $\rightarrow$ form

This code can be found in  file.

Since our language contains countably many propositional letters $p_0, p_1, ...$ we use the type $\mathbb{N}$ of natural numbers to define the constructor  of propositional letters.
The only way to construct a term of type  is
using this atomic constructor() and the constructors for falsum (), implication (), conjunction (), disjunction ().

The elimination rule is an operation that allows us to define functions by recursion from it to any other types, including also the type of propositions , in which case, this elimination rule is an instance of the principle of induction on the structure of the formula.

Constructors are displayed in Polish notation by default, but we define some custom infix notation with the usual Unicode characters for better readability:

prefix   `#`      := form.atom
notation `$\bot$`       := form.bot
infix    `$\supset$`       := form.impl
notation p `   ` q  := form.and p q
notation p `$\vee$` q   := form.or p q
notation ` `:40 p := form.impl p (form.bot )

Contexts are just sets of formulas.  In Lean sets are defined as functions of type  $\to$ . As usual in logic textbooks, we display the formulas in a context in list notation separated by a comma instead of using unions of singletons. We introduce the following notation to make this possible:

notation $\Gamma$ ` $_{_{\grave{}}}$ ` p := set.insert p $\Gamma$

The formalization of the language can be found in the  file.

§.§ The proof system

We define a Hilbert-style system for intuitionistic propositional logic that is best described as a refinement of Heyting's original axiomatization <cit.>. The proof system is implemented with a type of proofs, which is inductively defined as follows:

inductive prf : set form $\to$ form $\to$ Prop
| ax $\Gamma$ p (h : p $\in$ $\Gamma$) : prf $\Gamma$ p
| k $\Gamma$ p q : prf $\Gamma$ (p $\supset$ (q $\supset$ p))
| s $\Gamma$ p q r : prf $\Gamma$ ((p $\supset$ (q $\supset$ r)) $\supset$ ((p $\supset$ q) $\supset$ (p $\supset$ r)))
| exf $\Gamma$ p : prf $\Gamma$ ($\bot$ $\supset$ p)
| mp $\Gamma$ p q (hpq: prf $\Gamma$ (p $\supset$ q)) (hp : prf $\Gamma$ p) : prf $\Gamma$ q
| pr1 $\Gamma$ p q : prf $\Gamma$ ((p     q) $\supset$ p)
| pr2 $\Gamma$ p q : prf $\Gamma$ ((p     q) $\supset$ q)
| pair $\Gamma$ p q : prf $\Gamma$ (p $\supset$ (q $\supset$ (p     q)))
| inr $\Gamma$ p q : prf $\Gamma$ (p $\supset$ (p $\vee$ q))
| inl $\Gamma$ p q : prf $\Gamma$ (q $\supset$ (p $\vee$ q))
| case $\Gamma$ p q r : prf $\Gamma$ ((p $\supset$ r) $\supset$ ((q $\supset$ r) $\supset$ ((p $\vee$ q) $\supset$ r)))

Again, the elimination rule for this type generalizes definition by recursion and induction on the structure of proofs. To follow the usual logical notation, we abbreviate  with $\Gamma \vdash_i p$ as follows:

notation $\Gamma$ ` $\vdash_i$ ` p := prf $\Gamma$  p
notation $\Gamma$ ` $\not \vdash_i$ ` p := prf $\Gamma$  p $\to$ false

To illustrate, we compare a mechanized formal Hilbert-style proof of the identity of implication $p \supset p$ in our implementation:

lemma id p : form  $\Gamma$ :  set form  :
| $\Gamma$ $\vdash_{i}$  p $\supset$ p :=
mp (mp (@s  $\Gamma$ p (p $\supset$ p) p) k) k

with a non-mechanized formal proof written in Lemmon style:

1         $ p \supset ((p \supset p)\supset p) \supset (p \supset (p \supset p)) \supset (p \supset p) $     S

2       $p \supset ((p\supset p)\supset p)$     K

3       $(p \supset (p \supset p)) \supset (p\supset p)$     MP 1, 2

4       $(p \supset (p \supset p))$     K

5       $p \supset p$     MP 3, 4

Notice that the proof structure in our term proof is actually clearer since it indicates how the axiom schemes should be instantiated.

The formalization of the proof system can be found in the  file.

§.§ Semantics

§.§.§ Kripke models

We define the semantics for intuitionistic propositional logic in terms of Kripke semantics as usual [17, 5]. A model $\mathcal{M}$ is a triple $\langle \mathcal{W,\leq}, \mathsf{v} \rangle$ where $\mathcal{W}$ is a set of possible worlds of type $A$, $\leq$ is a reflexive, symmetric and monotonic binary relation on $A$, and $\mathsf{v}$ specifies the truth value of a formula at a world.

In Lean, Kripke models can be defined as inductive types having just  one constructor using the  command. We define it not as a triple but as a 6-tuple, composed of a domain , an accessibility relation , a valuation function , and proofs of reflexivity, transitivity, and monotonicity for the accessibility relation , denoted as , , and :

structure model (A : Type) :=
| (W : set A)
| (R : A  $\to$ A  $\to$ Prop)
| (val : $\mathbb{N}$ $\to$ A $\to$ Prop)
| (refl : $\forall$ w $\in$ W, R w w)
| (trans : $\forall$ w $\in$ W, $\forall$ v $\in$ W, $\forall$ u $\in$ W, R w v $\to$ R v u $\to$ R w u)
| (mono : $\forall$ p, $\forall$ w1 w2 $\in$ W, val p w1 $\to$ R w1 w2 $\to$  val p w2)

In our case, a possible world is a term of type $A$. This allows for more generality in the construction of a model unlike in [1]. What is more, the type of propositions  is used to encode our truth values  or .

§.§.§ Semantic consequence

To formalize the notion of truth at a type, we define a forcing relation $w \Vdash_{\mathcal{M}} p$ that takes as arguments a model $\mathcal{M}$, a formula $p$, and a type $A$ and returns a term of type . As usual, falsity, conjunction, and disjunction are defined truth-functionally and an implication $ p \supset q$ is true at a world $w$ iff if $\mathcal{R}(w,v)$ then $p$ is true implies $q$ is true at $v$, for all $v \in \mathcal{W}$. We also introduce the familiar notation for this forcing relation:

def forces_form A : Type (M : model A) : form $\to$ A $\to$ Prop
| (#p)     := $\lambda$v, M.val p v
| (bot)    := $\lambda$v, false
| (p $\supset$ q)   := $\lambda$v, $\forall$ w $\in$ M.W, v $\in$ M.W $\to$ M.R v w
$\to$ forces_form p w $\to$ forces_form q w
| (p     q)  := $\lambda$v, forces_form p v $\wedge$ forces_form q v
| (p $\vee$ q)   := $\lambda$v, forces_form p v $\vee$ forces_form q v

notation w `$\Vdash$  ` `` M ` ` p := forces_form M p w

To formalize the intuitionistic notion of semantic consequence $\Gamma \vDash_i p$ we first extend this forcing relation to contexts pointwise and then we stipulate that $\Gamma \vDash_i p$ iff for all types $A$, models $\mathcal{M}$ and possible worlds $w \in \mathcal{W}$, $\Gamma$ being true at $w$ in $\mathcal{M}$ implies $p$ being true at $w$ in $\mathcal{M}$:

def forces_ctx A : Type (M : model A) ($\Gamma$ : set form) : A $\to$ Prop :=
$\lambda$w, $\forall$ p, p $\in$ $\Gamma$ $\to$ forces_form M p w

notation w `$\Vdash$` `` M ` ` $\Gamma$ := forces_ctx M $\Gamma$ w

def sem_csq ($\Gamma$ : set form) (p : form) :=
$\forall$ A : Type (M : model A) (w $\in$ M.W), (w $\Vdash$ M $\Gamma$) $\to$ (w $\Vdash$ M p)

notation $\Gamma$ `$\vDash_{i}$` p := sem_csq $\Gamma$ p

It is worth noting that we are overloading the forcing relation notation for formulas  and contexts . There is no ambiguity because Lean will delay the choice until elaboration and determine how to disambiguate the notations depending on the relevant types.

The formalization of the Kripke semantics described above can be found in the  file.

§.§.§ The failure of the law of excluded middle

Before proceeding to prove completeness, it will be helpful to see how we can build models in our implementation. To give a concrete example, let us show how to build the following countermodel for the law of excluded middle <cit.> using the type of booleans true $\mathtt{tt}$ and false $\mathtt{ff}$:

[world] (w) [label=below:ff] ;
[world] (v) [label=below:tt,right=of w] $p$;
[->] (w) edge (v);
[->] (w) edge[reflexive] (w);
[->] (v) edge[reflexive] (v);

Since our possible worlds are always booleans, the domain, accessibility relation, and valuation function are formalized in Lean in a slightly different way. The reflexivity, transitivity, and monotonicity proofs are straightforward, so we shall omit them:

def W : set bool := ff, tt

def R : bool $\rightarrow$ bool $\rightarrow$ Prop := $\lambda$ w v, w = v $\lor$ w = ff

def val : nat $\rightarrow$ bool $\rightarrow$ Prop := $\lambda$ _ w, w = tt

Using this countermodel, we assume that the law of excluded middle holds, that is for any formula $p$, either $\emptyset \models_i p$ or $\emptyset \models_i \neg p$, and then derive a contradiction. This allows us to prove that the law of excluded middle fails in general:

lemma no_lem: $\neg$ $\forall$ p, ($\emptyset$ $\vDash_i$  p $\lor$  p)

The mechanization of the countermodel can be found in the  file.

§.§.§ Soundness

The soundness theorem asserts that if a formula $p$ can be derived from a set of assumptions $\Gamma$ using the inference rules of the logical system, then $p$ is logically valid under any interpretation that satisfies $\Gamma$.

theorem soundness $\Gamma$ :  set form p : form :
($\Gamma$ $\vdash_{i}$ p) $\rightarrow$ ($\Gamma$ $\models_i$  p)

The code for proof of soundness can be found in .

The proof proceeds by using induction to perform case analysis for each inference rule. For each rule, the proof provides a way to derive the conclusion based on the rule and a way to show that the conclusion is logically valid based on the interpretation and the premises.

§ THE COMPLETENESS THEOREM

Now that we have presented the implementation of the syntax and semantics of intuitionistic propositional logic in the previous section, we are prepared to undertake a formal proof of completeness.

The strong completeness theorem, which states that every semantic consequence is a syntactic consequence, can be stated in Lean using our custom notation as follows:

theorem completeness $\Gamma$ :  set form p : form :
($\Gamma$ $\models_i$  p) $\rightarrow$ ($\Gamma$ $\vdash_{i}$ p)

Our implementation follows the original Henkin-style completeness proof given by Troelstra and van Dalen [17] with some small modifications.

The main proof argument runs as follows.

* Assume that $\Gamma \vDash_{i} p$ and  $\Gamma \nvdash_{i} p$ hold;

* Build a model $\mathcal{M}$ such that $w \Vdash_\mathcal{M} p$ iff $w \vdash_i p$ for all worlds $w \in \mathcal{W}$, where we have sets of formulas as possible worlds;

* Show that there is a world $w \in \mathcal{W}$ such that $w \Vdash_{\mathcal{M}} \Gamma$ but  $w \nVdash_{\mathcal{M}} p$;

* Establish a contradiction from our assumption that $\Gamma \vDash_{i} p$.

Our proof appeals to classical reasoning at the metalevel of Lean's logic on two occasions <cit.>, namely,

in our proof of $\Gamma \vdash_{i} p$ where we assume double negation elimination and in our proof of $w \Vdash_\mathcal{M} p$ iff $w \vdash_i p$.

The reader can refer to the  file for the full details of our implementation of the completeness proof.

§.§.§ Consistent prime extensions

The first step of Troelstra and van Dalen's  proof is the definition of what they call a “saturated theory” <cit.>. We shall make use of the equivalent concept of prime theory instead <cit.>, in which the disjunction property is expressed in terms of the membership relation.
We say that a set of formulas $\Gamma$ is a prime theory if $\Gamma$ is closed under derivability and if $p \lor q \in \Gamma$ implies $p \in \Gamma$ or $q \in \Gamma$. In  file, we write:

def is_closed ($\Gamma$ :  set form) :=
$\forall$ p : form, ($\Gamma$ $\vdash_{i}$ p) $\rightarrow$ p $\in$ $\Gamma$

def has_disj ($\Gamma$ :  set form) :=
$\forall$ p q : form, ((p $\lor$ q) $\in$ $\Gamma$) $\rightarrow$ ((p $\in$ $\Gamma$) $\vee$ (q $\in$ $\Gamma$))

def is_prime ($\Gamma$  : set form) :=
is_consist $\Gamma$ $\land$ has_disj $\Gamma$

The second step of Troelstra and van Dalen's completeness proof is the proof of a prime extension lemma <cit.>, which states that if $\Gamma \nvdash r$ then there is a prime theory $\Gamma' \supseteq \Gamma$ such that $\Gamma' \nvdash r$.

Assuming that they have a list of disjunctions $\langle \varphi_{i,1} \lor \varphi_{i,2} \rangle_i$ with infinite repetitions,
they define
$$\Gamma' = \bigcup_{i \in \mathbb{N}} \Gamma_i,$$
where $ \Gamma_0= \Gamma$ and $ \Gamma_{k+1}$ is defined inductively as follows:

* Case 1: $\Gamma_k \vdash \varphi_{k,1} \lor \varphi_{k,2}$. Put

* $\Gamma_{k+1}=\Gamma_k \cup \{\varphi_{k,2}\}$ if $\Gamma_k, \varphi_{k,1} \vdash r$, and

* $\Gamma_{k+1}=\Gamma_k \cup \{\varphi_{k,1}\}$ otherwise

* Case 2: $\Gamma_k \nvdash \varphi_{k,1} \lor \varphi_{k,2}$. Put

* $\Gamma_{k+1}=\Gamma_k $

Since we want to extend $\Gamma$ to a prime theory $\Gamma'$, we want to ensure the disjunctive property that if $\phi \lor \psi \in \Gamma'$ then $\phi \in \Gamma'$ or $\psi \in \Gamma'$.

If there were no infinite repetitions in the list, we could never be sure that we have treated all disjunctions in Case 1, for, at step $k+1$, its disjuncts only get added to the set when $\Gamma_k$ proves the disjunction. It is possible that later the disjunction becomes provable from $\Gamma_{k+m}$, but, we will never go back to it again.

Troelstra and van Dalen mention a simpler variant of the construction that uses an enumeration of disjunctions without requiring infinite repetitions. At stage $k+1$ we simply treat the first disjunction not yet treated. This proof is spelled out by van Dalen in <cit.>. However, the proof method is less suitable for mechanization given that it is difficult to tell a proof assistant how exactly they should find the first disjunction not yet treated.

We implement a simplified version of this method where at each step $k+1$ we always treat all disjunctions in the language once more.

The following Lean code encapsulates the idea of the construction sketched above:

def insert_form ($\Gamma$ :  set form) (p q r : form) :  set form :=
if ($\Gamma$ $_{_{\grave{}}}$ p $\vdash_{i}$ r) then $\Gamma$ $_{_{\grave{}}}$ q else $\Gamma$ $_{_{\grave{}}}$ p

def insert_code ($\Gamma$ :  set form) (r : form) (n : nat) :  set form :=
match encodable.decode (form) n with
| none   := $\Gamma$
| some (p $\lor$ q) := if $\Gamma$ $\vdash_{i}$ p $\lor$ q then insert_form $\Gamma$ p q r else $\Gamma$
| some _ := $\Gamma$

def insertn ($\Gamma$ :  set form) (r : form) : nat $\rightarrow$  set form
| 0     := $\Gamma$
| (n+$1$) := insert_code (insertn n) r n

def primen ($\Gamma$ :  set form) (r : form) : nat $\rightarrow$  set form
| 0     := $\Gamma$
| (n+$1$) := $\bigcup$ i, insertn (primen n) r i

def prime ($\Gamma$:  set form) (r : form) :  set form :=
$\bigcup$ n, primen $\Gamma$ r n

Unlike in Troesltra and van Dalen [17] and van Dalen [5], the enumeration in our formalization lists not just all disjunctions but all propositional formulas in the language. When a formula is not a disjunction we simply ignore it just as in Case 2 above. We follow Bentzen [1] in using  types to enumerate the language.

In Lean, a type $\alpha$ is encodable if there is an encoding function  [style=lean]encode : $\alpha$ $\to$ nat and a (partial) inverse [style=lean]decode : nat $\to$ option $\alpha$ that decodes the encoded term of $\alpha$.

Now that we extended $\Gamma$ to $\Gamma'$, which we denote as , we have to prove it is indeed a prime extension of $\Gamma$.
First, we show that $\Gamma \subseteq \Gamma'$. But this is easy, since for every $\Gamma_n'$  in the family of sets, $\Gamma \subseteq \Gamma_n' \texttt{ n}$.  Therefore, $\Gamma$ must also be included in the union of all $\Gamma_n'$ , which is $\Gamma_n'$.

lemma primen_subset_prime $\Gamma$ :  set form r : form (n):
primen $\Gamma$ r n $\subseteq$  prime $\Gamma$ r

lemma subset_prime_self $\Gamma$ :  set form r : form :
$\Gamma$ $\subseteq$ prime $\Gamma$  r

The next step is to prove that the $\Gamma'$ also has the disjunction property and it is closed under derivability. Let us focus on the former first.

We need to show that $p \lor q \in \Gamma'$ implies $p \in \Gamma'$ or $q \in \Gamma'$. If $p \lor q \in \Gamma'$ then there is some $n \in \mathbb{N}$ such that $p \lor q \in \Gamma_n'$. But then since $\Gamma_n' \vdash p \lor q$, then we know that $p \in \Gamma_{n+1}'$ or $q \in \Gamma_{n+1}'$ because the disjunction was treated at some point. Thus, $p \in \Gamma'$ or $q \in \Gamma'$.

def prime_insertn_disj $\Gamma$:  set form p q r : form (h : (p $\lor$ q)   $\in$ prime $\Gamma$ r) :
$\exists$ n, p $\in$ (insertn (primen $\Gamma$ r n) r (encodable.encode (p $\lor$ q)+$1$)) $\lor$ q $\in$ (insertn (primen $\Gamma$ r n) r (encodable.encode (p $\lor$ q)+$1$))

lemma insertn_to_prime $\Gamma$ :  set form r : form n m : nat :
insertn (primen $\Gamma$ r n) r m $\subseteq$ prime $\Gamma$  r

def prime_has_disj $\Gamma$ :  set form p q r : form :
((p $\lor$ q) $\in$ prime $\Gamma$   r) $\rightarrow$ p $\in$ prime $\Gamma$   r $\vee$ q $\in$ prime $\Gamma$  r

Saying that $\Gamma'$ is closed under derivability means that if we can deduce a formula from $\Gamma'$, it is an element of $\Gamma'$. We use a lemma that states that if we can prove $r \lor p$ from $\Gamma'$, then there exists an $n$ such that $p \in \Gamma_{n+1}$. We use the above lemma  to deduce that $p \in \Gamma'$:

lemma prime_prf_disj_self $\Gamma$ :  set form p r : form :
(prime $\Gamma$ r $\vdash_{i}$   r $\lor$ p) $\rightarrow$ $\exists$ n, p $\in$ (insertn (primen $\Gamma$ r n) r (encodable.encode (r $\lor$ p)+$1$))

def prime_is_closed $\Gamma$ :  set form p q r : form :
(prime $\Gamma$ r $\vdash_{i}$ p) $\rightarrow$ p $\in$ prime $\Gamma$  r

At this moment, we need to prove that $\Gamma'$ still remains consistent. First, we by structural induction on the derivation that if $\Gamma' \vdash r$ then there is some $n$ such that $\Gamma_n \vdash r$. Then we prove by induction on $n$ that if $\Gamma_n \vdash r$ then $\Gamma \vdash r$. The base case is trivial. In the inductive case, we complete the proof by unfolding the definition of $\Gamma_n$ and manipulating the inductive hypothesis. Putting both lemmas together, we prove that $\Gamma' \vdash r$ implies $\Gamma \vdash r$:

def primen_not_prfn $\Gamma$ :  set form r : form n :
(primen $\Gamma$ r n $\vdash_{i}$ r) $\rightarrow$ ($\Gamma$ $\vdash_{i}$ r)

def prime_not_prf $\Gamma$ :  set form r : form :
(prime $\Gamma$ r $\vdash_{i}$ r) $\rightarrow$ ($\Gamma$ $\vdash_{i}$ r)

§.§.§ The canonical model construction

Given a set of formulas $\Gamma$ and $\phi$ such that $\Gamma \nvdash \phi$, the next step is to build a canonical Kripke model $\mathcal{M}$ such that with $w \Vdash_\mathcal{M} \Gamma$ and $w \nVdash_\mathcal{M} \phi$ for some possible world.

We build this model by letting $\mathcal{W}$ be the set of all consistent prime theories; $w \leq v$ iff $w \subseteq v$ for $w,v \in \mathcal{W}$; and $\textsf{v}(w,p)=1$ iff $w\in \mathcal{W} $ and $p \in w$, for a propositional letter $p$.

The following Lean code reflects the model construction:

def domain : set (set form) := w | is_consist w $\land$  ctx.is_prime w

def access : set form $\rightarrow$ set form $\rightarrow$ Prop := $\lambda$ w v, w $\subseteq$ v

def val : $\mathbb{N}$ $\rightarrow$ set form $\rightarrow$ Prop := $\lambda$ q w, w $\in$ domain $\land$ (#q) $\in$ w

The accessibility relation $\leq$ is clearly reflexive and transitive since so is $\subseteq$. Monotonicity is easy to see since $p \in w$ and $w \subseteq v$ means that $q \in v$. We prove these lemmas by  straightforward unfolding the definition of .

Our model is integrated into Lean's code as follows:

def M : model (set form):=
fapply model.mk,
apply domain,
apply access,
apply val,
apply access.refl,
apply access.trans,
apply access.mono

§.§.§ Truth and derivability

It turns out that a formula is true at a world in the canonical model if and only if it can be proved from that world:

lemma model_tt_iff_prf p : form :
$\forall$ (w $\in$ domain), (w $\models$ M p) $ \leftrightarrow$ (w $\vdash_{i}$ p)

We mechanize the proof employing the  tactic, which allows us to use the elimination rule of a type. This approach yields five goals, namely, to prove the case where a formula is a propositional letter, falsity, implication, conjunction, or disjunction. The proof of implication and disjunction deserve some mention.

The disjunction case is simpler, so we shall discuss it first. Lean gives us a biconditional in the following goal:

$\vdash$ $\forall$ (w : set form),
w $\in$ domain $\rightarrow$ (w $\models$ M (p $\lor$ q))  $\leftrightarrow$ (w $\vdash_{i}$  p $\lor$ q))

The proof in the forward direction starts with the introduction of assumptions and then splits the proof into two cases.
In the first case, we assume that $w \models_{\mathcal{M}} p \lor q$ and our goal is $w \vdash_{i} p \lor q$. Through the tactic , which expresses case reasoning, we can finish our goal using some basic facts about disjunctions and the inductive hypotheses in both cases.

In the backward direction, we assume that $w \vdash_{i} p \lor q$. Since $w$ is a prime theory and thus enjoys the disjunctive property, we can reason by cases depending on whether $w \vdash_{i} p$ or $w \vdash_{i} q$. The result follows the inductive hypothesis.

Now we proceed to the implication case. Using the  tactic, we begin by assuming the inductive hypothesis for $p$. If $w$ is a world and it is a prime theory, then by unfolding the true definition of a formula in the model's world, we arrive at a biconditional goal that can be expressed as follows.

$\vdash$ $\forall$ (w : set form),
w $\in$ domain $\rightarrow$ (w $\models_i$ M (p $\supset$ q)) $\leftrightarrow$ (w $\vdash_{i}$ p $\supset$ q))

We split the biconditional proof into two smaller conditionals using the  tactic.
In the forward direction, we first assume that $w \Vdash_{\mathcal{M}} p \supset q$. We reason by cases depending on whether $w \vdash_i p \supset q$ or not, therefore invoking the law of excluded middle. If that is the case, we are done. If not, then we know that $w, p \nvdash q$. We want to derive a contradiction. We extend the context $w, p$ to a prime theory $(w, p)'$ that still does not prove $q$.
By our inductive hypothesis, since $(w, p)'$ is in the domain, we know that $(w,p)' \Vdash_{\mathcal{M}} q \leftrightarrow (w,p)' \vdash_i q$.

To derive a contradiction, we just have to show that $(w,p)' \Vdash_{\mathcal{M}} q$. Recall that our assumption $w \Vdash_{\mathcal{M}} p \supset q$ states that for all $v \in \mathcal{W}$ such that $w \leq v$, if $v \Vdash_{\mathcal{M}} p$ then $v \Vdash_{\mathcal{M}} q$. But, clearly, $w \leq (w,p)'$. To complete the proof, we just have to show that $(w,p)' \Vdash_{\mathcal{M}} p$. By our inductive hypothesis, it suffices to show that $(w,p)' \vdash_i p$. But this is clearly true, since the original set $w,p$ is contained in the prime extension $(w,p)'$ and $w,p \vdash_i p$.

For the backward direction,  what we have to prove is $ w \Vdash_{\mathcal{M}} p \supset q$. This means for all $v \in \mathcal{W}$ such that $w \leq v$,  if $v \Vdash_{\mathcal{M}} p$ then $v \Vdash_{\mathcal{M}} q$. We assume that $v \in \mathcal{W}$ such that $w \leq v$, $v \Vdash_{\mathcal{M}} p$ then  we have to show $ v \Vdash_{\mathcal{M}} q$. Using our inductive hypothesis, we just have to show that $v \vdash_i  q$.

Since we know $w \vdash_i p \supset q$ and $w \subseteq v$, by weakening, we will have $v \vdash_i p \supset q$. We complete the proof by noting that $v \vdash_i p$ by our inductive hypothesis and assumption that $v \Vdash_{\mathcal{M}} p$. The result follows from modus ponens.

We have finished the proof of implication.

§.§.§ The completeness proof

To finish our completeness proof we just have to put together all the above pieces into 27 lines of code. We assume that $\Gamma \nvdash_{i} p$ and $\Gamma \models_i p$, we just need to arrive at a contradiction.

We extend $\Gamma$ to a prime theory $\Gamma'$ such that $\Gamma' \nvdash_{i} p$. Since we know $\Gamma' \Vdash_{\mathcal{M}} q \iff \Gamma' \vdash_{i} q$ for every formula $q$, we can conclude that $\Gamma' \nVdash_{\mathcal{M}} p$. Thus, we contradict our assumption that $\Gamma \models_i p$, given that $\Gamma' \Vdash_{\mathcal{M}} \Gamma$ but $\Gamma' \nVdash_{\mathcal{M}} p$.

§ CONCLUSION

We have used Lean to formally verify the Henkin-style completeness proof for intuitionistic logic proposed by Troesltra and van Dalen [17] restricted to a propositional fragment with implication, falsity, conjunction, disjunction. The propositional proof system we implement is based on a Hilbert-style axiomatization. In future work, we hope to expand our implementation to full intuitionistic first-order logic with existential and universal quantifiers and thus complete the formalization of Troesltra and van Dalen's proof. Our implementation also includes a mechanized proof of soundness and a countermodel for the general validity of the law of excluded middle in intuitionistic propositional logic.

This research was supported in part by the Zhejiang Federation of Humanities and Social Sciences grant 23YJRC04ZD.

[1]
Bentzen, B.: A Henkin-style completeness proof for the modal logic S5. In:
Logic and Argumentation: 4th International Conference, CLAR 2021, Hangzhou,
China, October 20–22, 2021, Proceedings 4. pp. 459–467. Springer (2021)

[2]
Carneiro, M.: The Lean 3 Mathematical Library (mathlib). URL:
<https://robertylewis.com/files/icms/Carneiro_mathlib.pdf> (2018),
international Congress on Mathematical Software

[3]
Coquand, C.: A formalised proof of the soundness and completeness of a simply
typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic
Computation  15(1),  57–90 (2002), URL:

[4]
Coquand, T., Huet, G.: The Calculus of Constructions. Information and
Compututation  76(2-3),  95–120 (1988), URL:

[5]
van Dalen, D.: Logic and structure, vol. 5. Springer (2013)

[6]
From, A.H.: Formalizing Henkin-style completeness of an axiomatic system for
propositional logic. Proceedings of the ESSLLI & WeSSLLI Student Session
pp. 1–12 (2020)

[7]
From, A.H.: A succinct formalization of the completeness of first-order logic.
In: 27th International Conference on Types for Proofs and Programs (TYPES
2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022)

[8]
Hagemeier, C., Kirst, D.: Constructive and mechanised meta-theory of
intuitionistic epistemic logic. In: Logical Foundations of Computer Science:
International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13,
2022, Proceedings. pp. 90–111. Springer (2022)

[9]
Herbelin, H., Lee, G.: Forcing-based cut-elimination for Gentzen-style
intuitionistic sequent calculus. In: H., O., M., K., de Queiroz R. (eds.)
International Workshop on Logic, Language, Information, and Computation. pp.
209–217. Springer, Berlin, Heidelberg (2009), URL:

[10]
Heyting, A.: Die formalen Regeln der intuitionistischen Logik.
Sitzungsbericht Preußische Akademie der Wissenschaften Berlin,
physikalisch-mathematische Klasse II pp. 42–56 (1930)

[11]
Kripke, S.A.: Semantical analysis of intuitionistic logic I. In: Studies in
Logic and the Foundations of Mathematics, vol. 40, pp. 92–130. Elsevier

[12]
Maggesi, M., Brogi, C.P.: A formal proof of modal completeness for provability
logic. arXiv preprint arXiv:2102.05945  (2021)

[13]
de Moura, L., Kong, S., Avigad, J., Van Doorn, F., von Raumer, J.: The Lean
theorem prover (system description). In: Felty, A., Middeldorp, A. (eds.)
International Conference on Automated Deduction. pp. 378–388. Springer, Cham
(2015), URL: <https://doi.org/10.1007/978-3-319-21401-6_26>

[14]
Norell, U.: Dependently typed programming in Agda. In: Koopman, P.,
Plasmeijer, R., Swierstra, D. (eds.) International School on Advanced
Functional Programming. pp. 230–266. Springer, Berlin, Heidelberg (2008),
uRL: <https://doi.org/10.1007/978-3-642-04652-0_5>

[15]
Pfenning, F., Paulin-Mohring, C.: Inductively defined types in the Calculus of
Constructions. In: International Conference on Mathematical Foundations of
Programming Semantics. pp. 209–228. Springer (1989)

[16]
The Coq project: The Coq proof assistant. URL:
<http://www.coq.inria.fr> (2017)

[17]
Troelstra, A.S., van Dalen, D.: Constructivism in mathematics. Vol. I, Studies
in Logic and the Foundations of Mathematics, vol. 121. North-Holland,
Amsterdam (1988)