alg-syntax.tex

\documentclass[reqno]{amsart}

\usepackage{amssymb}
\usepackage{hyperref}
\usepackage{mathtools}
\usepackage[all]{xy}
\usepackage{verbatim}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{turnstile}
\usepackage{etex}

\hypersetup{colorlinks=true,linkcolor=blue}

\renewcommand{\turnstile}[6][s]
    {\ifthenelse{\equal{#1}{d}}
        {\sbox{\first}{$\displaystyle{#4}$}
        \sbox{\second}{$\displaystyle{#5}$}}{}
    \ifthenelse{\equal{#1}{t}}
        {\sbox{\first}{$\textstyle{#4}$}
        \sbox{\second}{$\textstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{s}}
        {\sbox{\first}{$\scriptstyle{#4}$}
        \sbox{\second}{$\scriptstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{ss}}
        {\sbox{\first}{$\scriptscriptstyle{#4}$}
        \sbox{\second}{$\scriptscriptstyle{#5}$}}{}
    \setlength{\dashthickness}{0.111ex}
    \setlength{\ddashthickness}{0.35ex}
    \setlength{\leasturnstilewidth}{2em}
    \setlength{\extrawidth}{0.2em}
    \ifthenelse{%
      \equal{#3}{n}}{\setlength{\tinyverdistance}{0ex}}{}
    \ifthenelse{%
      \equal{#3}{s}}{\setlength{\tinyverdistance}{0.5\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{d}}{\setlength{\tinyverdistance}{0.5\ddashthickness}
        \addtolength{\tinyverdistance}{\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{t}}{\setlength{\tinyverdistance}{1.5\dashthickness}
        \addtolength{\tinyverdistance}{\ddashthickness}}{}
        \setlength{\verdistance}{0.4ex}
        \settoheight{\lengthvar}{\usebox{\first}}
        \setlength{\raisedown}{-\lengthvar}
        \addtolength{\raisedown}{-\tinyverdistance}
        \addtolength{\raisedown}{-\verdistance}
        \settodepth{\raiseup}{\usebox{\second}}
        \addtolength{\raiseup}{\tinyverdistance}
        \addtolength{\raiseup}{\verdistance}
        \setlength{\lift}{0.8ex}
        \settowidth{\firstwidth}{\usebox{\first}}
        \settowidth{\secondwidth}{\usebox{\second}}
        \ifthenelse{\lengthtest{\firstwidth = 0ex}
            \and
            \lengthtest{\secondwidth = 0ex}}
                {\setlength{\turnstilewidth}{\leasturnstilewidth}}
                {\setlength{\turnstilewidth}{2\extrawidth}
        \ifthenelse{\lengthtest{\firstwidth < \secondwidth}}
            {\addtolength{\turnstilewidth}{\secondwidth}}
            {\addtolength{\turnstilewidth}{\firstwidth}}}
        \ifthenelse{\lengthtest{\turnstilewidth < \leasturnstilewidth}}{\setlength{\turnstilewidth}{\leasturnstilewidth}}{}
    \setlength{\turnstileheight}{1.5ex}
    \sbox{\turnstilebox}
    {\raisebox{\lift}{\ensuremath{
        \makever{#2}{\dashthickness}{\turnstileheight}{\ddashthickness}
        \makehor{#3}{\dashthickness}{\turnstilewidth}{\ddashthickness}
        \hspace{-\turnstilewidth}
        \raisebox{\raisedown}
        {\makebox[\turnstilewidth]{\usebox{\first}}}
            \hspace{-\turnstilewidth}
            \raisebox{\raiseup}
            {\makebox[\turnstilewidth]{\usebox{\second}}}
        \makever{#6}{\dashthickness}{\turnstileheight}{\ddashthickness}}}}
        \mathrel{\usebox{\turnstilebox}}}

\newcommand{\axlabel}[1]{(#1) \phantomsection \label{ax:#1}}
\newcommand{\axtag}[1]{\label{ax:#1} \tag{#1}}
\newcommand{\axref}[1]{(\hyperref[ax:#1]{#1})}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#3~\ref{#2:##1}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\ref{#2:##1}}
\expandafter\newcommand\csname n#2\endcsname[1]{\ref{#2:##1}}
\newenvironmentx{#2}[2][1=,2=]{
\ifthenelse{\equal{##2}{}}{\begin{h#2}}{\begin{h#2}[##2]}
\ifthenelse{\equal{##1}{}}{}{\label{#2:##1}}
}{\end{h#2}}
}

\newref[section]{thm}{Theorem}{Theorem}
\newref{lem}{Lemma}{Lemma}
\newref{prop}{Proposition}{Proposition}
\newref{cor}{Corollary}{Corollary}
\newref{cond}{Condition}{Condition}

\theoremstyle{definition}
\newref{defn}{Definition}{Definition}
\newref{example}{Example}{Example}

\theoremstyle{remark}
\newref{remark}{Remark}{Remark}

\newcommand{\fs}[1]{\mathrm{#1}}
\newcommand{\Term}{\fs{Term}}
\newcommand{\RTerm}{\fs{RTerm}}
\newcommand{\FV}{\fs{FV}}
\newcommand{\subst}{\fs{subst}}
\newcommand{\Hom}{\fs{Hom}}
\newcommand{\wk}{\fs{wk}}
\newcommand{\Id}{\fs{Id}}
\newcommand{\refl}{\fs{refl}}
\newcommand{\El}{\fs{El}}
\newcommand{\emptyCtx}{\cdot}
\newcommand{\ft}{\fs{ft}}
\newcommand{\ty}{\fs{ty}}
\newcommand{\Ty}{\fs{Ty}}
\newcommand{\ctx}{\fs{ctx}}
\newcommand{\tm}{\fs{tm}}
\newcommand{\sub}{\fs{Sub}}
\newcommand{\id}{\fs{id}}

\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand{\Th}{\cat{Th}}
\newcommand{\algtt}{\cat{TT}}

\numberwithin{figure}{section}

\newcommand{\pb}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\po}[1][dr]{\save*!/#1+1.2pc/#1:(1,-1)@^{|-}\restore}

\begin{document}

\title{Syntax of Algebraic Dependent Type Theories}

\author{Valery Isaev}

\begin{abstract}
TODO
\end{abstract}

\maketitle

\section{Introduction}

TODO

\section{Preliminaries}

In this section, we recall definitions from \cite{PHL} and \cite{alg-tt} and describe a generalization of the notion of algebraic Type theories.
A many sorted first-order signature $(\mathcal{S},\mathcal{F},\mathcal{P})$ consists of a set $\mathcal{S}$ of sorts,
a set $\mathcal{F}$ of function symbols and a set $\mathcal{P}$ of predicate symbols.
Each function symbol $\sigma$ is equipped with a signature of the form $\sigma : s_1 \times \ldots \times s_k \to s$, where $s_1$, \ldots $s_k$, $s$ are sorts.
Each predicate symbol $R$ is equipped with a signature of the form $R : s_1 \times \ldots \times s_k$.
If $V$ is an $\mathcal{S}$-set, then the $\mathcal{S}$-set of terms of $T$ with free variables in $V$ will be denoted by $\Term^\ft_\mathcal{F}(V)$ or by $\Term^\ft_T(V)$.

An atomic formula is an expression either of the form $t_1 = t_2$ or of the form $R(t_1, \ldots t_n)$,
where $R$ is a predicate symbol and $t_1$, \ldots $t_n$ are terms.
We abbreviate $t = t$ to $t\!\downarrow$.
A Horn formula is an expression of the form $\varphi_1 \land \ldots \land \varphi_n$, where $\varphi_1$, \ldots $\varphi_n$ are atomic formulas.
The conjunction of the empty set of atomic formulas is denoted by $\top$.
A sequent is an expression of the form $\varphi \sststile{}{x_1, \ldots x_n} \psi$, where $x_1$, \ldots $x_n$ are variables
and $\varphi$ and $\psi$ are Horn formulas such that $\FV(\varphi) \cup \FV(\psi) \subseteq \{ x_1, \ldots x_n \}$.
We also write $\varphi \ssststile{}{V} \psi$ to denote the pair of sequents $\varphi \sststile{}{V} \psi$ and $\psi \sststile{}{V} \varphi$.
A \emph{partial Horn theory} consists of a signature and a set of Horn sequents in this signature.

The rules of \emph{partial Horn logic} are listed below.
A \emph{theorem} of a partial Horn theory $T$ is a sequent derivable from $T$ in this logic.
We will write $\varphi \sststile{T}{V} \psi$ to denote the fact that sequent $\varphi \sststile{}{V} \psi$ is derivable in $T$.

\begin{center}
\AxiomC{}
\RightLabel{\axlabel{nv}}
\UnaryInfC{$\varphi \sststile{}{V} x\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} a = b$}
\RightLabel{\axlabel{ns}}
\UnaryInfC{$\varphi \sststile{}{V} b = a$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{}
\RightLabel{\axlabel{nh}}
\UnaryInfC{$\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \varphi_i$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} a = b$}
\AxiomC{$\varphi \sststile{}{V} \psi[a/x]$}
\RightLabel{\axlabel{nl}}
\BinaryInfC{$\varphi \sststile{}{V} \psi[b/x]$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\varphi \sststile{}{V} R(t_1, \ldots t_n)$}
\RightLabel{\axlabel{np}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \sigma(t_1, \ldots t_n)\!\downarrow$}
\RightLabel{\axlabel{nf}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\end{center}
where $R$ is a predicate symbol of the theory and $\sigma$ is its function symbol.
Note that this system derives only sequents in which the conclusion is atomic.
For this reason, we will consider only such sequents.

Finally, for every axiom $\psi_1 \land \ldots \land \psi_n \sststile{}{x_1 : s_1, \ldots x_k : s_k} \chi_1 \land \ldots \land \chi_m$
and for all terms $t_1 : s_1$, \ldots $t_k : s_k$, we have the following rules for all $1 \leq j \leq m$:
\smallskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} t_i\!\downarrow$, $1 \leq i \leq k$}
\AxiomC{$\varphi \sststile{}{V} \psi_i[t_1/x_1, \ldots t_k/x_k]$, $1 \leq i \leq n$}
\RightLabel{\axlabel{na}}
\BinaryInfC{$\varphi \sststile{}{V} \chi_j[t_1/x_1, \ldots t_k/x_k]$}
\DisplayProof
\end{center}

Now, we define a generalization of the theory of substitutions defined in \cite{alg-tt}.
The \emph{theory of substitutions} (without unique types) $T_S$ has sorts $\mathcal{S} = \{ \ctx, \tm \} \times \mathbb{N}$.
We write $(\ty,n)$ for the sort $(\ctx,n+1)$.
The set of function symbols is defined as follows:
\begin{align*}
\emptyCtx      & : (\ctx,0) \\
\ft_{p,n}      & : (p,n) \to (\ctx,n) \text{, } p \in \{ \tm, \ty \} \\
v_{n,i}        & : (\ctx,n) \to (\tm,n) \text{, } 0 \leq i < n \\
\subst_{p,n,k} & : (\ctx,n) \times (p,k) \times (\tm,n)^k \to (p,n) \text{, } p \in \{ \tm, \ty \}
\end{align*}
The theory also has the following predicate symbols:
\[ \Ty_n : (\tm,n) \times (\ty,n) \]

We let $\ft^i_n : (\ctx,n+i) \to (\ctx,n)$ and $\ft^i_{p,n} : (p,n+i) \to (\ctx,n)$ be the following derived operations:
\begin{align*}
\ft^0_n(A)      & = A \\
\ft^{i+1}_n(A)  & = \ft^i_n(\ft_{\ty,n+i}(A)) \\
\ft^i_{p,n}(t) & = \ft^i_n(\ft_{p,n}(t))
\end{align*}
We write $(\ty,n)$ for $(\ctx,n+1)$.
We also define a formula $\Hom_{n,k} : (\ctx,n) \times (\ctx,k) \times (\tm,n)^k$ as follows:
\[ \Hom_{n,k}(B, A, a_1, \ldots a_k) = \bigwedge_{1 \leq i \leq k} \Ty_n(a_i, \subst_{ty,n,i-1}(B, \ft^{k-i}_i(A), a_1, \ldots a_{i-1})). \]

Now, we can describe the set of axioms of $T_S$:
\begin{align*}
& \sststile{}{x} x = \emptyCtx \\
& \Hom_{n,k}(B, \ft_{p,k}(a), a_1, \ldots a_k) \ssststile{}{B, a, a_i}  \subst_{p,n,k}(B, a, a_1, \ldots a_k) \downarrow \\
& \Hom_{n,k}(B, \ft_{p,k}(a), a_1, \ldots a_k) \sststile{}{B, a, a_i} \ft_{p,n}(\subst_{\ty,n,k}(B, a, a_1, \ldots a_k)) = B \\
& \sststile{}{A} \ft_{\tm,n}(v_{n,i}(A)) = A \\
& \sststile{}{A} \Ty_n(v_{n,i}(A), \subst_{\ty,n,n-i-1}(A, \ft^i_{n-i}(A), v_{n,n-1}(A), \ldots v_{n,i+1}(A))) \\
& \Ty_k(a,A) \sststile{}{B, a, A, a_i} \Ty_n(\subst_{tm,n,k}(B, a, a_1, \ldots a_k), \subst_{\ty,n,k}(B, A, a_1, \ldots a_k)) \\
& \sststile{}{a} \subst_{p,n,n}(\ft_{p,n}(a), a, v_{n,n-1}(\ft_{p,n}(a)), \ldots v_{n,0}(\ft_{p,n}(a))) = a \\
& \Hom_{n,k}(B, A, a_1, \ldots a_k) \sststile{}{B, a_i, A} \subst_{\tm,n,k}(B, v_{k,i}(A), a_1, \ldots a_k) = a_{k-i} \\
& \Hom_{n,k}(C, B, b_1, \ldots b_k) \land \Hom_{k,m}(B, \ft_{p,m}(a), a_1, \ldots a_m) \sststile{}{C, b_i, B, a_i, a} \\
& \subst_{p,n,k}(C, \subst_{p,k,m}(B, a, a_1, \ldots a_m), b_1, \ldots b_k) = \\
& \quad \subst_{p,n,m}(C, a, \subst_{tm,n,k}(C, a_1, b_1, \ldots b_k), \ldots \subst_{\tm,n,k}(C, a_m, b_1, \ldots b_k))
\end{align*}

Let $\mathcal{F}_0$ be a set of function symbols and let $\mathcal{P}_0$ be a set of predicate symbols.
We call elements of these sets basic function symbols and basic predicate symbols, respectively.
Then we define the full sets of function and predicate symbols:
\begin{align*}
\mathcal{F} = \{ & \sigma_m : (\ctx,m) \times (p_1,m+n_1) \times \ldots \times (p_k,m+n_k) \to (p,m+n) \mid \\
                 & m \in \mathbb{N}, \sigma \in \mathcal{F}_0, \sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n) \} \\
\mathcal{P} = \{ & R_m : (\ctx,m) \times (p_1,m+n_1) \times \ldots \times (p_k,m+n_k) \mid \\
                 & m \in \mathbb{N}, R \in \mathcal{P}_0, R : (p_1,n_1) \times \ldots \times (p_k,n_k) \}
\end{align*}

\begin{defn}[alg-tt]
An \emph{algebraic dependent type theory} is a theory of the form $(\mathcal{S}, \mathcal{F}_s \cup \mathcal{F}, \mathcal{P}, \mathcal{A}_s \cup \mathcal{A})$, where $\mathcal{S}$, $\mathcal{F}$, and $\mathcal{P}$ are defined above,
$\mathcal{F}_s$ is the set of function symbols of the theory of substitutions, $\mathcal{A}_s$ is the set of its axioms, and $\mathcal{A}$ is an arbitrary set of axioms such that the following sequents are derivable for every $\sigma_m \in \mathcal{F}$ and $R_m \in \mathcal{P}$
\begin{align*}
\sigma_m(\Gamma, x_1, \ldots x_k)\!\downarrow\ & \sststile{}{\Gamma, x_1, \ldots x_k} \ft^n_{p,m}(\sigma_m(\Gamma, x_1, \ldots x_k)) = \Gamma \\
\sigma_m(\Gamma, x_1, \ldots x_k)\!\downarrow\ & \sststile{}{\Gamma, x_1, \ldots x_k} \bigwedge_{1 \leq i \leq k} \ft^{n_i}_{p_i,m}(x_i) = \Gamma \\
R_m(\Gamma, x_1, \ldots x_k) & \sststile{}{\Gamma, x_1, \ldots x_k} \bigwedge_{1 \leq i \leq k} \ft^{n_i}_{p_i,m}(x_i) = \Gamma
\end{align*}
and $\subst$ commutes with every function symbol (for a precise definition, see \cite[Definition~4.5]{alg-tt}).
\end{defn}

Let $T$ be an algebraic dependent type theory.
We define $P_M$ as the set of pairs $V,\varphi$ such that $V = \{ x_1, \ldots x_k \}$ and $\varphi = \varphi_1 \land \ldots \land \varphi_k$, where $\varphi_i$ equals to $\Ty_n(x_i,t_i)$ (resp., $\ft_{\ty,n}(x_i) = t_i$) if $x_i : (\tm,n)$ (resp., $x_i : (\ty,n)$),
where $t_i$ is a term of $T$ with free variables in $\{ x_1, \ldots x_{i-1} \}$ such that for every $1 \leq i \leq k$,
the sequent $\varphi_1 \land \ldots \land \varphi_{i-1} \sststile{}{x_1, \ldots x_{i-1}} t_i\!\downarrow$ is derivable in $T$.
We will be mostly interested in theorems of the form $\varphi \sststile{}{V} \psi$ where $(\varphi,V) \in P_M$ for reasons explained in \cite{morita-equiv}.

A \emph{restricted term} is a term $t$ together with a formula $\varphi$.
We denote such a restricted term by $t|_\varphi$.
The $\mathcal{S}$-set of restricted terms (with free variables in $V$) will be denoted by $\RTerm^\ft(V)$.
Let $T$ and $T'$ be two theories with the same set of sorts.
An \emph{interpretation} of $T$ in $T'$ is a function $f$ such that the following conditions hold:
\begin{itemize}
\item For every basic function symbol $\sigma : s_1 \times \ldots \times s_k \to s$ of $T$,
the function $f$ defines a restricted term $f(\sigma(x_1, \ldots x_k))$ of $T'$ of sort $s$ such that $\FV(f(\sigma(x_1, \ldots x_k)))$ equals to $\{ x_1 : s_1, \ldots x_k : s_k \}$.
\item For every basic predicate symbol $P : s_1 \times \ldots \times s_k$,
the function $f$ defines a formula $f(P(x_1, \ldots x_k))$ of $T'$ such that $\FV(f(P(x_1, \ldots x_k)))$ equals to $\{ x_1 : s_1, \ldots x_k : s_k \}$.
\item For every axiom $\varphi \sststile{}{V} \psi$ of $T$, the sequent $f(\varphi) \sststile{}{V} f(\psi)$ is derivable in $T'$.
Formulas $f(\varphi)$ and $f(\psi)$ are defined inductively using $f(\sigma(x_1, \ldots x_k))$ and $f(P(x_1, \ldots x_k))$ in the obvious way.
\end{itemize}

We will say that formulas $\varphi$ and $\psi$ are \emph{equivalent} if the sequents $\varphi \ssststile{}{\FV(\varphi) \cup \FV(\psi)} \psi$ are derivable.
Two restricted terms $t|_\varphi$ and $t'|_\psi$ are equivalent if the following sequents are derivable:
\begin{align*}
\varphi \land t\!\downarrow\ & \sststile{}{\FV(t|_\varphi) \cup \FV(t'|_\psi)} \psi \land t = t' \\
\psi \land t'\!\downarrow\ & \sststile{}{\FV(t|_\varphi) \cup \FV(t'|_\psi)} \varphi \land t = t'
\end{align*}
We will write $t \simeq t'$ if $t$ and $t'$ are equivalent.
Two interpretations $f$ and $f'$ are equivalent if $f(S_n(\Gamma, x_1, \ldots x_k))$ and $f'(S_n(\Gamma, x_1, \ldots x_k))$ are equivalent for every symbol $S$.
A \emph{morphism} of theories $T$ and $T'$ is an equivalence class of interpretations of $T$ in $T'$.
The identity morphism is defined in the obvious way: $\id(\sigma(x_1, \ldots x_k)) = \sigma(x_1, \ldots x_k)|_\top$ and $\id(R(x_1, \ldots x_k)) = R(x_1, \ldots x_k)$.
The composition of morphisms is defined as follows: $(g \circ f)(S(x_1, \ldots x_k))$ = $g(f(S(x_1, \ldots x_k)))$.
It is easy to see that this defines the structure of a category on algebraic dependent type theories.
We will denote this category by $\algtt^\ft$.

Let $T_\ty$ be the theory with one basic function symbol $\ty : (\tm,0) \to (\ty,0)$ and one axiom $\Ty_n(a,A) \ssststile{}{a,A} \ty_n(a) = A$.
Then there is at most one map from $T_\ty$ to any other type theory.
We will say that a type theory $T$ \emph{has unique types} if there is a map $T_\ty \to T$.
The full subcategory of type theories with unique types will be denoted by $\algtt^\ft_\ty$.
This subcategory is reflective; the reflector is given by $T \mapsto T_\ty \amalg T$.

\begin{remark}
The category of type theories with unique types is equivalent to the category of type theories defined in \cite[Definition~4.5]{alg-tt}.
\end{remark}

\begin{remark}
The category $\algtt^\ft$ is locally finitely presentable.
This was proved for $\algtt^\ft_\ty$ in \cite[Corollary~3.2]{morita-equiv}.
The proof in the general case is the same.
\end{remark}

\section{The $\ft$-free syntax}
\label{sec:contexts}

The syntax we described in the previous section is too verbose.
We can make it closer to the usual presentation of type theories by removing some redundant information.
We define another $\mathcal{S}$-set of terms $\Term^s(V)$ inductively as follows:
\begin{itemize}
\item Every element of $V_s$ is a term of sort $s$.
\item $v_i$ is a term of sort $(\tm,n)$ for every $0 \leq i < n$.
\item If $A_1$, \ldots $A_k$ are terms of sorts $(\ty,0)$, \ldots $(\ty,k-1)$, respectively, $t$ is a term of sort $(p,k)$, where $p \in \{ \ty, \tm \}$, and $t_1, \ldots t_k$ are terms of sort $(\tm,n)$, then $\subst(A_1, \ldots A_k, t, t_1, \ldots t_k)$ is a term of sort $(p,n)$.
\item If $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n)$ is a function symbol of $T$ and $t_i$ is a term of sort $(p_i,m+n_i)$, then $\sigma(t_1, \ldots t_k)$ is a term of sort $(p,m+n)$.
\end{itemize}
These terms will be called \emph{$\ft$-free} terms.
They define a syntax, called the \emph{$\ft$-free syntax}, which has metavariables (elements of $V$), de Bruijn indices ($v_i$), explicit substitutions ($\subst$), and constructions depending on the theory (basic function symbols).

A \emph{context} of length $n$ a sequence of terms of sorts $(\ty,0)$, \ldots $(\ty,n-1)$.
An ($\ft$-free) \emph{judgment} is an expression of one of the following forms:
\[ \Gamma \vdash a : A \qquad \Gamma \vdash t \qquad \Gamma \vdash t \equiv t' \qquad \Gamma \vdash R(t_1, \ldots t_k) \]
where $\Gamma$ is a context of length $m$, $a$ is a term of sort $(\tm,m)$, $A$ is a term of sort $(\ty,m)$,
$t$ and $t'$ are terms of sort $(p,m)$ (where $p \in \{ \ty, \tm \}$), $R : (p_1,n_1) \times \ldots \times (p_k,n_k)$ is a predicate symbol, and $t_1$, \ldots $t_k$ are terms of sorts $(p_1,m+n_1)$, \ldots $(p_k,m+n_k)$, respectively.
All terms above are written in the $\ft$-free syntax.
We will use judgments of the form $\Gamma \vdash$.
If $\Gamma$ is the empty context, this judgment denotes $\top$.
If $\Gamma = (\Gamma', A)$, this judgment denotes $\Gamma' \vdash A$.

Jusgements play the role of atomic formulas in the $\ft$-free syntax.
An ($\ft$-free) \emph{formula} is a finite conjunction of judgments.
Sequents are defined as before.
We will often write sequents in the form of derivation rules.
Thus, $\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \psi$ can be written as
\begin{center}
\AxiomC{$\varphi_1$}
\AxiomC{\ldots}
\AxiomC{$\varphi_n$}
\TrinaryInfC{$\psi$}
\DisplayProof
\end{center}
The set of variables $V$ is implicit in this notation and we let it to be the union of all variables that appear in the premise and in the conclusion.
Also, $\varphi_1 \land \ldots \land \varphi_n \ssststile{}{V} \psi$ will be represented by the following rule:
\begin{center}
\AxiomC{$\varphi_1$}
\AxiomC{\ldots}
\AxiomC{$\varphi_n$}
\doubleLine
\TrinaryInfC{$\psi$}
\DisplayProof
\end{center}

Let $\Gamma$ be a context of length $n$ and let $\Delta_1 = (A_1, \ldots A_k)$, $\Delta_2 = (B_1, \ldots B_k)$ be a pair of sequences of terms of sorts $(\ty,n)$, \ldots $(\ty,n+k)$.
Then we define $\Gamma \vdash \Delta_1 \equiv \Delta_2$ as $\Gamma \vdash A_1 \equiv B_1 \land \ldots \land \Gamma, A_1, \ldots A_{k-1} \vdash A_k \equiv B_k$.
If $\Gamma$ and $\Delta$ are two contexts of the same length, we define $\Gamma \equiv \Delta$ as $\vdash \Gamma \equiv \Delta$.

An ($\ft$-free) \emph{theory} $(\mathcal{F},\mathcal{P},\mathcal{A})$ consists of a set of function symbols $\mathcal{F}$ such that every function symbol has a signature of the form $s_1 \times \ldots \times s_k \to (p,0)$, a set of predicate symbols $\mathcal{P}$, and a set of axioms $\mathcal{A}$.
These sets must satisfy conditions listed in \rdefn{ft-free}.
Each symbol $S$ with $k$ parameters of sorts $(p_1,n_1)$, \ldots $(p_k,n_k)$ is equipped with a collection $\{ \Gamma^S_i(x_1, \ldots x_{i-1}) \}_{1 \leq i \leq k}$ of contexts,
where $\Gamma^S_i(x_1, \ldots x_{i-1})$ is a context of length $n_i$ with free variables in $\{ x_1 : (p_1,n_1), \ldots x_{i-1} : (p_{i-1},n_{i-1}) \}$.
We will write $\Gamma^S_i$ for $\Gamma^S_i(x_1, \ldots x_k)$.
We will also write $\Gamma^S_i(t_1, \ldots t_k)$ for $\Gamma^S_i[t_1/x_1, \ldots t_k/x_k]$.

A \emph{contexted term} is a pair $(\Gamma,t)$, where $\Gamma$ is a context of length $n$ and $t$ is a term of sort $(p,n)$ for some $p \in \{ \ty, \tm \}$.
For every contexted term $(\Gamma,t)$, we can define the set $\sub(\Gamma,t)$ of its contxeted subterms:
\begin{align*}
\sub(\Gamma,t) = & \{ (\Gamma,t) \} \text{ if $t$ is a variable or $v_i$} \\
\sub(\Gamma,\subst(A_1, \ldots A_k, t', t_1, \ldots t_k)) = & \{ (\Gamma,t) \} \cup \sub((A_1, \ldots A_k), t')\ \cup \\
    & \bigcup_{1 \leq i \leq k} \sub(\Gamma,t_i) \cup \sub((A_1, \ldots A_{i-1}), A_i) \\
\sub(\Gamma,\sigma(t_1, \ldots t_k)) = & \{ (\Gamma,t) \} \cup \bigcup_{1 \leq i \leq k} \sub((\Gamma,\Gamma^\sigma_i(t_1, \ldots t_{i-1})), t_i)
\end{align*}
In each of the cases, $(\Gamma,t)$ is the contexted term itself.
So, every contexted term is always a contexted subterm of itself.
Note that the definition of $\sub$ depends on the choice of contexts $\Gamma^\sigma_i$.

We can also define the set of contexted subterms of contexts and formulas:
\begin{align*}
\sub(\cdot) & = \varnothing \\
\sub((\Gamma, A)) & = \sub(\Gamma) \cup \sub(\Gamma,A) \\
\sub(\Gamma \vdash a : A) & = \sub(\Gamma) \cup \sub(\Gamma, a) \cup \sub(\Gamma, A) \\
\sub(\Gamma \vdash t) & = \sub(\Gamma) \cup \sub(\Gamma, t) \\
\sub(\Gamma \vdash t \equiv t') & = \sub(\Gamma) \cup \sub(\Gamma,t) \cup \sub(\Gamma,t') \\
\sub(\Gamma, R(t_1, \ldots t_k)) & = \sub(\Gamma) \cup \bigcup_{1 \leq i \leq k} \sub((\Gamma,\Gamma^R_i(t_1, \ldots t_{i-1})),t_i) \\
\sub(\varphi_1 \land \ldots \land \varphi_n) & = \bigcup_{1 \leq i \leq n} \sub(\varphi_i)
\end{align*}

Now, we can describe the derivation system for the $\ft$-free syntax:
\medskip
\begin{center}
\AxiomC{}
\RightLabel{\axlabel{ch}}
\UnaryInfC{$\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \varphi_i$}
\DisplayProof
\qquad
\AxiomC{}
\RightLabel{, $(\Gamma,t) \in \sub(\varphi)$ \axlabel{cd}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash t$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma, A, \Delta \vdash \psi$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash A \equiv B$}
\RightLabel{\axlabel{cx}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma, B, \Delta \vdash \psi$}
\DisplayProof
\end{center}
where $\psi$ is either a term, an equality, or a predicate symbol applied to some terms.

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash t$}
\RightLabel{\axlabel{cr}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash t \equiv t$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv b$}
\RightLabel{\axlabel{cs}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash b \equiv a$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv b$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash b \equiv c$}
\RightLabel{\axlabel{ct}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv c$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash R(t_1, \ldots t_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Gamma^R_i(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$}
\RightLabel{\axlabel{cp}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash R(t_1, \ldots t_{i-1}, t_i', t_{i+1}, \ldots t_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(t_1, \ldots t_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Gamma^\sigma_i(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$}
\RightLabel{\axlabel{cf}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(t_1, \ldots t_k) \equiv \sigma (t_1, \ldots t_{i-1}, t_i', t_{i+1}, \ldots t_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv a'$}
\RightLabel{\axlabel{cxl}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a' : A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash A \equiv A'$}
\RightLabel{\axlabel{cxr}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a : A'$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(t_1, \ldots t_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Gamma^\sigma_i(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$}
\RightLabel{\axlabel{cf'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \sigma (t_1, \ldots t_{i-1}, t_i', t_{i+1}, \ldots t_k)$}
\DisplayProof
\end{center}
where $\sigma$ is either a function symbol or $\subst$.
We define $\Gamma^\subst_i(x_1, \ldots x_{2k+1})$ as $x_1, \ldots x_{i-1}$ if $i \leq k+1$ and as the empty context otherwise.

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi_i[t_1/x_1, \ldots t_k/x_k]$, $1 \leq i \leq n$}
\RightLabel{\axlabel{ca}}
\UnaryInfC{$\varphi \sststile{}{V} \chi_j[t_1/x_1, \ldots t_k/x_k]$}
\DisplayProof
\end{center}
where $\psi_1 \land \ldots \land \psi_n \sststile{}{x_1 : s_1, \ldots x_k : s_k} \chi_1 \land \ldots \land \chi_m$ is an axiom and $t_1$, \ldots $t_k$ are arbitrary terms.

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash$}
\RightLabel{\axlabel{ev}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash v_i$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} A_1, \ldots A_m \vdash$}
\RightLabel{\axlabel{evt}}
\UnaryInfC{$\varphi \sststile{}{V} A_1, \ldots A_m \vdash v_i : \wk^{i+1}(A_1, \ldots A_{m-i})$}
\DisplayProof
\end{center}
where $\wk^n(A_1, \ldots A_k, a) = \subst(A_1, \ldots A_k, a, v_{n+k-1}, \ldots v_n)$.

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash b$
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\def\extraVskip{2pt}
\RightLabel{\axlabel{es}}
\doubleLine
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \subst(A_1, \ldots A_k, b, a_1, \ldots a_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash b : B$
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\def\extraVskip{2pt}
\RightLabel{\axlabel{est}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \subst(\overline{A}, b, a_1, \ldots a_k) : \subst(\overline{A}, B, a_1, \ldots a_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$}
\RightLabel{\axlabel{esl}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \subst(A_1, \ldots A_k, v_i, a_1, \ldots a_k) \equiv a_{k-i}$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash b$}
\RightLabel{\axlabel{esr}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \subst(\Gamma, b, v_{k-1}, \ldots v_0) \equiv b$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash c$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} B_1, \ldots B_n \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash b_i : \subst(B_1, \ldots B_i, b_1, \ldots b_{i-1})$
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\def\extraVskip{2pt}
\RightLabel{\axlabel{esa}}
\BinaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash \subst(\overline{B}, \subst(\overline{A}, c, \overline{a}), \overline{b}) \equiv \subst(\overline{A}, c, a_1' \ldots a_k')$
\DisplayProof
\end{center}
where $a_i' = \subst(B_1, \ldots B_n, a_i, b_1, \ldots b_n)$.

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash \sigma(b_1, \ldots b_m)$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\def\extraVskip{2pt}
\RightLabel{\axlabel{esf}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \subst(A_1, \ldots A_k, \sigma(b_1, \ldots b_m), a_1, \ldots a_k) \equiv \sigma(b_1', \ldots b_m')$}
\DisplayProof
\end{center}
where $\sigma : (p_1,n_1) \times \ldots \times (p_m,n_m) \to (p,0)$ is a function symbol and
\[ b_i' = \subst(A_1, \ldots A_k, \Gamma^\sigma_i(b_1, \ldots b_{i-1}), b_i, \wk^{n_i}(a_1), \ldots \wk^{n_i}(a_k), v_{n_i-1}, \ldots v_0). \]

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash \sigma(b_1, \ldots b_m)$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\def\extraVskip{2pt}
\RightLabel{\axlabel{esf'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(b_1', \ldots b_m')$}
\DisplayProof
\end{center}
where $\sigma$ is a function symbol and $b_1'$, \ldots $b_m'$ are defined as before.

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\Axiom$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash R(b_1, \ldots b_m)$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_1, \ldots A_i, a_1, \ldots a_{i-1})$
\def\extraVskip{2pt}
\RightLabel{\axlabel{esp}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash R(b_1', \ldots b_m')$}
\DisplayProof
\end{center}
where $R : (p_1,n_1) \times \ldots \times (p_m,n_m)$ is a predicate symbol and $b_1'$, \ldots $b_m'$ are defined as before.
If $\psi = \psi_1 \land \ldots \land \psi_n$, then we will say that $\psi \sststile{}{V} \psi$ is derivable if $\psi \sststile{}{V} \psi_i$ is derivable for every $1 \leq i \leq n$.

We will say that a term or a formula $E$ is \emph{valid} with respect to $(\varphi,V)$ if, for every pair $(\Gamma,x)$ and $(\Delta,x)$ of contexted subterms of $E$ (where $x$ is any variable), the sequent $\varphi \sststile{}{V} \Gamma \equiv \Delta$ is derivable in the empty theory (that is, without \axref{ca}).
A sequent $\varphi \sststile{}{V} \psi$ is \emph{valid} if $\FV(\psi) \subseteq \FV(\varphi)$ and $\varphi \land \psi$ is valid with respect to $(\varphi,V)$.

\begin{defn}[ft-free]
An $\ft$-free \emph{theory} $(\mathcal{F},\mathcal{P},\mathcal{A})$ consists of a set of function symbols $\mathcal{F}$, a set of predicate symbols $\mathcal{P}$, and a set of axioms $\mathcal{A}$
together with a context $\Gamma^S_i(x_1, \ldots x_{i-1})$ for every symbol $S$ with $n$ parameters and every $1 \leq i \leq n$ such that the following conditions hold:
\begin{enumerate}
\item \label{it:ax-consist} For every symbol $S$ with $n$ parameters, all $1 \leq i < j \leq n$, and every $(\Delta,x_i) \in \sub(\Gamma, \Gamma_j^S(x_1, \ldots x_{j-1}))$, the following sequent is derivable:
\[ \Gamma \vdash S(x_1, \ldots x_k) \sststile{}{\Gamma, x_1, \ldots x_k} \Delta \equiv (\Gamma, \Gamma_i^S(x_1, \ldots x_{i-1})) \]
\item \label{it:ax-wf} The following relation on the set of function symbols is well-founded: $\tau \prec \sigma$ if and only if $\tau$ appears in $\Gamma^\sigma_i$ for some $i$.
\item \label{it:ax-valid} All axioms are valid.
\item \label{it:ax-cond} For every axiom $\varphi \sststile{}{V} \psi$ and every contexted subterm $(\Gamma,t)$ of $\psi$, the sequent $\varphi \sststile{}{V} \Gamma \vdash t$ is derivable.
\end{enumerate}
A \emph{theorem} is a derivable sequent $\varphi \sststile{}{V} \psi$ such that $\FV(\psi) \subseteq \FV(\varphi)$ and $\varphi$ is valid with respect to $(\varphi,V)$.
\end{defn}

We do not usually explicitly specify context $\Gamma^S_i$.
Instead, we assume that every symbol $S$ has a unique axiom of the form
\[ \varphi \sststile{}{x_1, \ldots x_k}\ \vdash S(x_1, \ldots x_k) \]
such that there is a unique contexted subterm of $\varphi$ of the form $(\Gamma,x_i)$ for every $i$.
Then we let $\Gamma^S_i$ to be equal to $\Gamma$.

\begin{example}
The theory of $\Pi$-types is defined as follows:
\begin{center}
\AxiomC{$\Gamma, A \vdash B$}
\UnaryInfC{$\Gamma \vdash \Pi(A,B)$}
\DisplayProof
\qquad
\AxiomC{$\Gamma, A \vdash b$}
\UnaryInfC{$\Gamma \vdash \lambda(A,b)$}
\DisplayProof
\qquad
\AxiomC{$\Gamma, A \vdash b : B$}
\UnaryInfC{$\Gamma \vdash \lambda(A,b) : \Pi(A,B)$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\Gamma, A \vdash B$}
\AxiomC{$\Gamma \vdash f : \Pi(A,B)$}
\AxiomC{$\Gamma \vdash a : A$}
\doubleLine
\TrinaryInfC{$\Gamma \vdash \fs{app}(A,B,f,a)$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\Gamma, A \vdash B$}
\AxiomC{$\Gamma \vdash f : \Pi(A,B)$}
\AxiomC{$\Gamma \vdash a : A$}
\TrinaryInfC{$\Gamma \vdash \fs{app}(A, B,f,a) : \subst(\Gamma, A, B, v_{n-1}, \ldots v_0, a)$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\Gamma, A \vdash b : B$}
\AxiomC{$\Gamma \vdash a : A$}
\BinaryInfC{$\Gamma \vdash \fs{app}(A, B,\lambda(A,b),a) \equiv \subst(\Gamma, A, b, v_{n-1}, \ldots v_0, a)$}
\DisplayProof
\end{center}
\medskip
\end{example}

\begin{lem}[derived-cong-lem]
Let $t$ and $t'$ be terms, let $\Gamma$ be a context of length $n$, and let $A$ be a term of sort $(p,n)$.
Suppose that $\varphi \sststile{}{V} \Delta[t/x] \vdash t \equiv t'$ is derivable for every $\Delta$ such that $(\Delta,x) \in \sub(\Gamma,A)$.
If the sequent $\varphi \sststile{}{V} \Delta \vdash s$ is derivable for every $(\Delta,s) \in \sub(\Gamma,A[t/x])$, then so is the sequent $\varphi \sststile{}{V} \Gamma \vdash A[t/x] \equiv A[t'/x]$.
\end{lem}
\begin{proof}
The proof is by induction on $A$.
If $A = x$, it is obvious.
If $A = \sigma(t_1, \ldots t_k)$, let
\[ T_i = \sigma(t_1[t/x], \ldots t_{i-1}[t/x], t_i[t'/x], \ldots t_k[t'/x]). \]
Since $T_{k+1} = A[t/x]$ and $T_1 = A[t'/x]$, it is enough to show that, for every $1 \leq i \leq k$, sequents $\varphi \sststile{}{V} \Gamma \vdash T_{i+1} \equiv T_i$ and $\varphi \sststile{}{V} \Gamma \vdash T_i$ are derivable whenever $\varphi \sststile{}{V} \Gamma \vdash T_{i+1}$ is.
By \axref{cf} and \axref{cf'}, it is enough to show that $\varphi \sststile{}{V} \Gamma, \Gamma^\sigma_i(t_1[t/x], \ldots t_{i-1}[t/x]) \vdash t_i[t/x] \equiv t_i[t'/x]$ is derivable, which follows by induction hypothesis.
To apply it, we need to check that the condition of the lemma holds.
Let $(\Delta,x)$ be a contexted subterm of $((\Gamma, \Gamma^\sigma_i(t_1[t/x], \ldots t_{i-1}[t/x])), t_i)$.
Then there exists $\Delta'$ such that $\Delta[t/x] = \Delta'[t/x]$ and $(\Delta',x) \in \sub(\Gamma, \sigma(t_1, \ldots t_k))$, which implies that $\varphi \sststile{}{V} \Delta[t/x] \vdash t \equiv t'$ is derivable.
\end{proof}

\begin{lem}[derived-cong-ctx]
Let $t$ and $t'$ be terms, let $\Gamma$ be a context of length $n$, and let $\Theta$ be a sequence of terms of sorts $(\ty,n)$, \ldots $(\ty,n+m)$.
Suppose that $\varphi \sststile{}{V} \Delta[t/x] \vdash t \equiv t'$ is derivable for every $\Delta$ such that $(\Delta,x) \in \sub(\Gamma,\Theta)$.
If the sequent $\varphi \sststile{}{V} \Delta \vdash s$ is derivable for every $(\Delta,s) \in \sub(\Gamma,\Theta[t/x])$, then so is the sequent $\varphi \sststile{}{V} \Gamma \vdash \Theta[t/x] \equiv \Theta[t'/x]$.
\end{lem}
\begin{proof}
This follows from \rlem{derived-cong-lem} by induction on the length of $\Theta$.
\end{proof}

A rule is \emph{admissible} if its conclusion is derivable whenever its premises are.

\begin{lem}
The following rules are admissible:
\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Delta \vdash \psi$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\RightLabel{\axlabel{cx'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma, \Delta' \vdash \psi$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\RightLabel{\axlabel{cs'}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \Delta' \equiv \Delta$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta' \equiv \Delta''$}
\RightLabel{\axlabel{ct'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta''$}
\DisplayProof
\end{center}
\end{lem}
\begin{proof}
The proof is by easy induction on the length of $\Delta$.
\end{proof}

\begin{lem}[sub-subst]
Let $t$ be a term and let $\rho$ be a substitution defined for every variable in $\FV(t)$.
If $(\Delta,x) \in \sub(\Gamma[\rho],t[\rho])$, then there exists $(\Delta',x') \in \sub(\Gamma,t)$ such that $(\Delta,x) \in \sub(\Delta'[\rho],\rho(x'))$.
\end{lem}
\begin{proof}
By a straightforward induction on $t$.
\end{proof}

\begin{lem}[sub-repl]
If $(\Delta,t') \in \sub(\Gamma,t)$ and $\Gamma'$ is some context, then there exists $\Delta'$ such that $(\Delta',t') \in \sub(\Gamma',t)$ and the following sequent is derivable:
\[ (\Gamma \equiv \Gamma') \land (\Gamma \vdash t) \sststile{}{V} \Delta \equiv \Delta' \]
\end{lem}
\begin{proof}
By a straightforward induction on $t$.
\end{proof}

\begin{prop}
The following rules are admissible:
\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi$}
\RightLabel{$\mathrm{\axlabel{cu}}$}
\UnaryInfC{$\varphi[\rho] \sststile{}{V'} \psi[\rho]$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\psi \sststile{}{V} \chi$}
\RightLabel{$\mathrm{\axlabel{cc}}$}
\BinaryInfC{$\varphi \sststile{}{V} \chi$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi$}
\RightLabel{, $(\Gamma,t) \in \sub(\psi)\ \mathrm{\axlabel{ce}}$}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash t$}
\DisplayProof
\end{center}
\end{prop}
\begin{proof}
The rule \axref{cu} is proved by a straightforward induction on the derivation of $\varphi \sststile{}{V} \psi$.
It is harder to prove the admissibility of the other two rules because they depend on each other.
To solve this problem, we show that \axref{cc} holds only for certain sequents first.

We will say that a sequent $\varphi \sststile{}{V} \psi$ is \emph{good} if $\varphi \sststile{}{V} \Gamma \vdash t$ is derivable for every $(\Gamma,t) \in \sub(\psi)$.
Now, we can prove that $\varphi \sststile{}{V} \chi$ is derivable whenever $\varphi \sststile{}{V} \psi$ is good and derivable and $\psi \sststile{}{V} \chi$ is derivable by induction on the derivation of the latter sequent.
Most of the cases are obvious.
The rule \axref{cd} follows from the assumption that $\varphi \sststile{}{V} \psi$ is good and the rule \axref{ch} follows from the assumption that $\varphi \sststile{}{V} \psi$ is derivable.

Now, we can prove that every derivable sequent is good, which implies both \axref{cc} and \axref{ce}.
We proceed by induction on the derivation.
Most of the cases are trivial since the set of proper contexted subterms of the conclusion is a subset of the set of contexted subterms of the premise.
We consider only non-trivial cases.
First, let us consider \axref{ca}.
Let $\psi \sststile{}{V'} \chi$ be an axiom, let $\rho$ be a substitution, and let $(\Gamma,t)$ be a contexted subterm of $\chi[\rho]$.
Suppose that $\varphi \sststile{}{V} \psi[\rho]$ is derivable and good.
We need to show that $\varphi \sststile{}{V} \Gamma \vdash t$ is derivable.
It is easy to see that there exists a contexted subterm $(\Gamma',t')$ of $\chi$ such that $(\Gamma,t) = (\Gamma'[\rho],t'[\rho])$.
By \eqref{it:ax-cond}, the sequent $\psi \sststile{}{V'} \Gamma' \vdash t'$ is derivable.
By \axref{cu}, the sequent $\psi[\rho] \sststile{}{V} \Gamma \vdash t$ is also derivable.
Since $\varphi \sststile{}{V} \psi[\rho]$ is derivable and good, this implies that $\varphi \sststile{}{V} \Gamma \vdash t$ is derivable.

Now, we consider \axref{cp}, \axref{cf}, and \axref{cf'}.
Assume that $\varphi \sststile{}{V} \Gamma \vdash S(t_1, \ldots t_k)$ is derivable and good and that $\varphi \sststile{}{V} \Gamma, \Gamma_i^S(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$ is derivable.
We need to show that $\varphi \sststile{}{V} \Gamma, \Gamma_j^S(t_1, \ldots t_i', \ldots t_{j-1}) \vdash t_j$ is derivable.
By \axref{cx'}, we just need to show that $\varphi \sststile{}{V} \Gamma \vdash \Gamma_j^S(t_1, \ldots t_{j-1}) \equiv \Gamma_j^S(t_1, \ldots t_i', \ldots t_{j-1})$ is derivable.
This follows from \rlem{derived-cong-ctx}.
Since $\Gamma, \Gamma_j^S(t_1, \ldots t_{j-1})$ is a contexted subterm of $\Gamma \vdash S(t_1, \ldots t_k)$, one of the conidtions of \rlem{derived-cong-ctx} follows from the fact that $\varphi \sststile{}{V} \Gamma \vdash S(t_1, \ldots t_k)$ is good.
We also need to to show that $\varphi \sststile{}{V} \Delta[t_i/x_i] \vdash t_i \equiv t_i'$ is derivable for every $(\Delta,x_i) \in \sub(\Gamma, \Gamma_j^S(t_1, \ldots x_i, \ldots t_{j-1}))$.
By \rlem{sub-subst}, there exists $\Delta'$ such that $(\Delta',x_i) \in \sub(\Gamma,\Gamma_j^S)$ and $\Delta = \Delta'[\rho]$, where $\rho(x_i) = x_i$ and $\rho(x_k) = t_k$ if $k \neq i$.
By \axref{cx'}, we just need to show that $\varphi \sststile{}{V} \Delta'[\rho][t_i/x_i] \equiv (\Gamma, \Gamma_i^S(t_1, \ldots t_{i-1}))$ is derivable.
Since $\varphi \sststile{}{V} \Gamma \vdash S(t_1, \ldots t_k)$ is derivable and good, this follows from \axref{cc} and \eqref{it:ax-consist}.

TODO: consider \axref{esf}, \axref{esf'}, and \axref{esp}.
\end{proof}

\begin{cor}[theorem-ext]
Any theorem can be added to the set of axioms.
This does not change the set of theorems.
\end{cor}
\begin{proof}
Condition~\eqref{it:ax-cond} is exactly the admissibility of \axref{ce}.
We also need to show that \axref{ca} holds for theorems.
This follows from \axref{cu} and \axref{cc}.
Finally, we need to show that theorems are valid.
Let $\varphi \sststile{}{V} \psi$ be a theorem.
If $(\Gamma,x)$ is a contexted subterm of $\psi$, then there exists a contexted subterm $(\Delta,x)$ of $\varphi$.
Thus, it is enough to show that $\varphi \sststile{}{V} \Gamma \equiv \Delta$ is derivable.
It is easy to do this by induction on the derivation of the theorem.
\end{proof}

The following lemma generalizes \rlem{derived-cong-lem}:

\begin{lem}[derived-cong]
Let $t$ and $t'$ be terms, let $\Gamma$ be a context, and let $\psi$ be either a term, an equality, or a predicate symbol applied to some terms.
Suppose that $\varphi \sststile{}{V} \Delta[t/x] \vdash t \equiv t'$ is derivable for every $\Delta[t/x]$ such that $(\Delta,x) \in \sub(\Gamma,\psi)$.
If the sequent $\varphi \sststile{}{V} \Gamma \vdash \psi[t/x]$ is derivable, then so is the sequent $\varphi \sststile{}{V} \Gamma \vdash \psi[t'/x]$.
\end{lem}
\begin{proof}
If $\psi$ is an equality, then this follows from \rlem{derived-cong} and \axref{ce}.
If $\psi$ is a term, then this follows from the previous case by \axref{ce} since $(\Gamma,b) \in \sub(\Gamma \vdash a \equiv b)$.
If $\psi = R(t_1, \ldots t_k)$, then \axref{cp} and \rlem{derived-cong-lem} imply that the following sequent is derivable for every $1 \leq i \leq k$:
\[ \varphi \sststile{}{V} \Gamma \vdash R(t_1[t/x], \ldots t_{i-1}[t/x], t_i[t'/x], \ldots t_k[t'/x]). \]
\end{proof}

\section{The category of $\ft$-free theories}

In this section we define the category of $\ft$-free theories and prove that it is equivalent to a full subcategory of $\algtt^\ft$.
An $\ft$-free \emph{restricted term} is just a pair consisting of an $\ft$-free term $t$ and an $\ft$-free formula $\varphi$, written $t|_\varphi$.
A \emph{contexted restricted term} is a pair $(\Gamma,t|_\varphi)$ such that $(\Gamma,t)$ is a contexted term and $\varphi$ is a formula.

Let $f$ be a function that defines a restricted term $f(\sigma(x_1, \ldots x_k))$ and a formula $f(R(x_1, \ldots x_k))$ for every function symbol $\sigma$ and every predicate symbol $R$ such that $\FV(f(\sigma(x_1, \ldots x_k))) = \{ x_1, \ldots x_k \}$ and $\FV(R(x_1, \ldots x_k)) = \{ x_1, \ldots x_k \}$.
Then we can extend its definition to all terms, formulas, and restricted terms recursively.
The restriction formulas are just lifted to the top.
That is, $\sigma(t_1|_{\varphi_1}, \ldots t_k|_{\varphi_k}) = \sigma(t_1, \ldots t_k)|_{\varphi_1 \land \ldots \land \varphi_k}$ and $R(t_1|_{\varphi_1}, \ldots t_k|_{\varphi_k}) = R(t_1, \ldots t_k) \land \varphi_1 \land \ldots \land \varphi_k$.
We will say that such a function is an \emph{interpretation} of $T$ in $T'$ if the following conditions hold:
\begin{enumerate}
\item \label{it:interp-symb} For every symbol $S$ of $T$, if $(\Delta,x_i) \in \sub(\Gamma,f(S(x_1, \ldots x_k)))$, then the sequent $\Gamma \vdash f(S(x_1, \ldots x_k)) \sststile{}{\Gamma, x_1, \ldots x_k} \Delta \equiv (\Gamma,f(\Gamma^S_i))$ is derivable in $T'$.
\item \label{it:interp-axiom} For every axiom $\varphi \sststile{}{V} \psi$ of $T$, the sequent $f(\varphi) \sststile{}{V} f(\psi)$ is derivable.
\end{enumerate}

The identity interpretation is defined in the obvious way: $\id(\sigma(x_1, \ldots x_k)) = \sigma(x_1, \ldots x_k)|_\top$ and $\id(R(x_1, \ldots x_k)) = R(x_1, \ldots x_k)$.
The composition of interpretations is defined as follows:
\[ (g \circ f)(S(x_1, \ldots x_k)) = g(f(S(x_1, \ldots x_k))) \]

\begin{lem}
The identity map is an interpretation and the composition of interpretations is an interpretation.
\end{lem}
\begin{proof}
It is easy to see that the identity function is an interpretation.
The second property is obvious and the first property follows from \axref{cd}.
Let $f : T_1 \to T_2$ and $g : T_2 \to T_3$ be a pair of interpretations.
We need to show that $g \circ f$ is also an interpretation.
To prove that it satisfies \eqref{it:interp-axiom}, it is enough to show that interpretations preserve theorems.
This follows from the fact that interpretations preserve inference rules.
This is obvious for most of them.
Rule \axref{ca} follows from \rcor{theorem-ext}.
Let us consider rules \axref{cp}, \axref{cf}, and \axref{cf'}.
Let $f$ be an interpretation.
Then we know that the following sequents are derivable: $f(\varphi) \sststile{}{V} f(\Gamma) \vdash f(S(t_1, \ldots t_k))$ and $f(\varphi) \sststile{}{V} f(\Gamma), f(\Gamma_i^S(t_1, \ldots t_{i-1})) \vdash f(t_i) \equiv f(t_i')$.
By \rlem{derived-cong} and \axref{cx'}, it is enough to show that the sequent $f(\varphi) \sststile{}{V} \Delta[t_i/x_i] \equiv (f(\Gamma),f(\Gamma_i^S(t_1, \ldots t_{i-1})))$ is derivable for every $\Delta$ such that $(\Delta,x_i) \in \sub(f(\Gamma), f(S(t_1, \ldots x_i, \ldots t_k)))$.
It is easy to see that there exists $\Delta'$ such that $(\Delta',x_i) \in \sub(f(\Gamma), f(S(x_1, \ldots x_k)))$ and $\Delta = \Delta'[t_1/x_1, \ldots t_{i-1}/x_{i-1}, t_{i+1}/x_{i+1}, \ldots t_k/x_k]$.
Now, the derivability of $f(\varphi) \sststile{}{V} \Delta[t_i/x_i] \equiv (f(\Gamma),f(\Gamma_i^S(t_1, \ldots t_{i-1})))$ follows from \eqref{it:interp-symb}.

Now, let us prove that $g \circ f$ satisfies \eqref{it:interp-symb}.
Since $g$ preserves theorems, it is enough to show that, for every $(\Delta,x_i) \in \sub(\Gamma, g(f(S(x_1, \ldots x_k))))$, there exists $\Delta'$ such that $(\Delta',x_i) \in \sub(\Gamma, f(S(x_1, \ldots x_k)))$ and $\Gamma \vdash g(f(S(x_1, \ldots x_k))) \sststile{}{\Gamma, x_1, \ldots x_k} g(\Delta') \equiv \Delta$ is derivable.
We will prove a more general property: for every contexted term $(\Theta,t)$ and every $(\Delta,x) \in \sub(g(\Theta), g(t))$, there exists $\Delta'$ such that $(\Delta',x) \in \sub(\Theta, t)$ and the sequent $g(\Theta) \vdash g(t) \sststile{}{\FV(\Theta,t)} g(\Delta') \equiv \Delta$ is derivable.
The proof is by induction on $t$.
If $t$ is a variable, this is obvious.
Suppose $t = \sigma(t_1, \ldots t_k)$ (including $\subst$ and $v_i$).
By \rlem{sub-subst}, there exists $\Delta_1$ such that $(\Delta_1,x_i) \in \sub(g(\Theta), g(\sigma(x_1, \ldots x_k)))$ and $(\Delta,x) \in \sub(\Delta_1[g(t_1)/x_1, \ldots g(t_k)/x_k], g(t_i))$.
By \eqref{it:interp-symb}, the following sequent is derivable:
\[ g(\Theta) \vdash g(t) \sststile{}{V} \Delta_1[g(t_1)/x_1, \ldots g(t_k)/x_k] \equiv (g(\Theta), g(\Gamma^\sigma_i(t_1, \ldots t_{i-1}))) \]
By \rlem{sub-repl}, there exists $\Delta'$ such that the sequent $g(\Theta) \vdash g(t) \sststile{}{V} \Delta \equiv \Delta'$ is derivable and $(\Delta',x) \in \sub((g(\Theta), g(\Gamma^\sigma_i(t_1, \ldots t_{i-1}))), g(t_i))$.
Now, the required property follows by induction hypothesis.
\end{proof}

Let $t|_{\Delta \vdash \varphi}$ and $t'|_{\Delta' \vdash \psi}$ be a pair of $\ft$-free restricted terms.
Then we will say that a sequent $\chi \sststile{}{V} \Gamma \vdash t|_{\Delta \vdash \varphi} \simeq t'|_{\Delta' \vdash \psi}$ is derivable if the following seuqnets are:
\begin{align*}
\chi \land (\Gamma, \Delta \vdash \varphi) \land (\Gamma \vdash t) & \sststile{}{V} (\Gamma, \Delta' \vdash \psi) \land (\Gamma \vdash t \equiv t') \\
\chi \land (\Gamma, \Delta' \vdash \psi) \land (\Gamma \vdash t') & \sststile{}{V} (\Gamma, \Delta \vdash \varphi) \land (\Gamma \vdash t \equiv t')
\end{align*}

Two $\ft$-free restricted terms $t$ and $t'$ are \emph{equivalent} in a context $\Gamma$ if the sequent $\sststile{}{\FV(\Gamma) \cup \FV(t) \cup \FV(t')} \Gamma \vdash t \simeq t'$ is derivable.
Two $\ft$-free formulas $\bigwedge_{1 \leq i \leq n} \Gamma_i \vdash \varphi_i$ and $\bigwedge_{1 \leq i \leq k} \Delta_i \vdash \psi_i$ are \emph{equivalent} in a context $\Gamma$
if the following sequent is derivable:
\[ \bigwedge_{1 \leq i \leq n} \Gamma, \Gamma_i \vdash \varphi_i \ssststile{}{\FV(\Gamma) \cup \FV(\varphi) \cup \FV(\psi)} \bigwedge_{1 \leq i \leq k} \Gamma, \Delta_i \vdash \psi_i \]

Interpretations $f$ and $f'$ are \emph{equivalent} if, for every function (resp., predicate) symbol $S$, restricted terms (resp., formulas) $f(S(x_1, \ldots x_k))$ and $f'(S(x_1, \ldots x_k))$ are equivalent in all contexts consisting of variables.
A \emph{morphism} of $\ft$-free theories $T$ and $T'$ is an equivalence class of interpretations of $T$ in $T'$.

\begin{prop}
The composition operation respects the equivalence relation and together with the identity map determines the structure of a category on $\ft$-free theories.
\end{prop}
\begin{proof}
If $f$ and $f'$ are equivalent interpretations, then $g \circ f$ and $g \circ f'$ are equivalent because $g$ preserves theorems.
If $g$ and $g'$ are equivalent interpretations, then we need to show that $g \circ f$ and $g' \circ f$ are equivalent.
It is enough to show that the sequent $g(\varphi) \sststile{}{V} g'(\varphi)$ is derivable for every formula $\varphi$.
By \axref{cp}, \axref{ct}, and \axref{cs}, it is enough to show that the sequent $\Gamma \vdash g(t) \sststile{}{\Gamma,V} \Gamma \vdash g(t) \equiv g'(t)$ is derivable for every term $t$, which is easy to do by induction on $t$ using \axref{cf}.

It is obvious that $f \circ \id = \id \circ f = f$.
To prove that $(h \circ g) \circ f = h \circ (g \circ f)$, it is enough to show that $(h \circ g)(e)$ is equivalent to $h(g(e))$ for every restricted term or formula $e$, which is easy to do by induction on $e$.
\end{proof}

The category of algebraic type theories is denoted by $\algtt$.
We will show that $\algtt$ is equivalent to a full subcategory of $\algtt^\ft$.
First, let us construct a functor $F : \algtt \to \algtt^\ft$.
Let $T = (\mathcal{F},\mathcal{P},\mathcal{A})$ be an $\ft$-free theory.
We define the basic function (resp., basic predicate) symbols of $F(T)$ as $\mathcal{F}$ (resp., $\mathcal{P}$).
We also add function symbols of the theory of substitutions (defined in \cite[Section~3.1]{alg-tt}) to $F(T)$.

A well-founded relation $\prec$ on function symbols can be extended to a well-founded relation $\prec$ on the set of terms (called \emph{recursive path ordering} \cite{mrpo}) such that $t[t_1/x_1, \ldots t_k/x_k] \prec \sigma(t_1, \ldots t_k)$ if $\tau \prec \sigma$ for every function symbol $\tau$ in $t$.
We always have a recursive path ordering on terms by \eqref{it:ax-wf}.

Now, we define a function $F : \Term^\ft(V)_{(\ctx,n)} \times \Term^s(V)_{(p,n)} \to \RTerm^\ft(V)_{(p,n)}$ by induction on the second argument with respect to the recursive path ordering:
\begin{align*}
F(\Gamma, x) & = x|_{\ft_{p,n}(x) = \Gamma} \\
F(\Gamma, v_i) & = v_{n,i}(\Gamma) \\
F(\Gamma, \subst(A_1, \ldots A_k, t, t_1, \ldots t_k)) & = \subst_{p,n,k}(\Gamma, F(F(\cdot,\overline{A}), t), \ldots F(\Gamma, t_i), \ldots) \\
F(\Gamma, \sigma(t_1, \ldots t_k)) & = \sigma_n(\Gamma, \ldots F(F(\Gamma, \Gamma^\sigma_i(t_1, \ldots t_{i-1})), t_i), \ldots)
\end{align*}
where $F(\Gamma, (B_1, \ldots B_m)) = F(\ldots F(F(\Gamma, B_1), B_2) \ldots, B_m)$.
We will write $F(\Delta)$ for $F(\cdot,\Delta)$ and $F(\Delta,E)$ for $F(F(\Delta),E)$, where $\Delta$ is an $\ft$-free context.

For every $\ft$-free formula $\varphi$, we can define a formula $F(\varphi)$ as follows:
\begin{align*}
F(\Gamma \vdash t) & = F(\Gamma,t)\!\downarrow \\
F(\Gamma \vdash t \equiv t') & = (F(\Gamma,t) = F(\Gamma,t')) \\
F(\Gamma \vdash a : A) & = \Ty_n(F(\Gamma,a),F(\Gamma,A)) \\
F(\Gamma \vdash R(t_1, \ldots t_k)) & = R_n(F(\Gamma), \ldots F(F(\Gamma, \Gamma^R_i(t_1, \ldots t_{i-1})), t_i), \ldots) \\
F(\varphi_1 \land \ldots \land \varphi_m) & = F(\varphi_1) \land \ldots \land F(\varphi_m)
\end{align*}
Every $\ft$-free sequent determines $\varphi \sststile{}{V} \psi$ a sequent $F(\varphi) \sststile{}{V} F(\psi)$.
Thus, we can define axioms of $F(T)$ to be the image of axioms of $T$ under this function together with the axioms listed in \rdefn{alg-tt} and the axioms of the theory of substitutions.

\begin{lem}[ftmap-th]
If $\varphi \sststile{}{V} \psi$ is a theorem of $T$, then $F(\varphi) \sststile{}{V} F(\psi)$ is derivable in $F(T)$.
\end{lem}
\begin{proof}
We need to show that $F$ preserves inference rules.
Rule \axref{ch} corresponds to \axref{nh}.
Rule \axref{cr} is preserved trivially.
Rule \axref{cs} corresponds to \axref{ns}.
For every $(\Gamma,t) \in \sub(\varphi)$, the term $F(\Gamma,t)$ is a subterm of $F(\varphi)$.
This implies that \axref{cd} corresponds to \axref{np} and \axref{nf}.
Rules \axref{cx}, \axref{ct}, \axref{cp}, \axref{cf}, \axref{cf'}, \axref{cxl}, and \axref{cxr} follow from \axref{nl}.
Rule \axref{ca} follows from \axref{na}, \axref{np}, and \axref{nf} since the set of free variables of the premise of every axiom is contained in the set free variables of its conclusion.
The rest of the rules are explicitly added to $F(T)$ as axioms.
\end{proof}

\begin{lem}[ftmap-ctx]
The following sequent is derivable:
\[ F(\Gamma,t)\!\downarrow\ \sststile{}{V} \ft_{p,n}(F(\Gamma,t)) = \Gamma \]
\end{lem}
\begin{proof}
Easy case analysis on $t$.
\end{proof}

\begin{lem}[ftmap-subst]
The following restricted terms are equivalent:
\begin{align*}
& F(F(\Gamma)[F(\Delta,t')/x], t[t'/x])|_{\bigwedge_{(\Delta',x) \in \sub(\Gamma,t)} \Delta = F(\Delta'[t'/x])} \\
& F(\Gamma,t)[F(\Delta,t')/x]
\end{align*}
\end{lem}
\begin{proof}
The proof is by induction on $t$ with respect to the recursive path ordering.
If $t$ is a variable and is not equal to $x$, this is obvious.
If $t = x$, then the second term is equal to $F(\Delta,t')|_{\ft_{p,n}(F(\Delta,t')) = \Gamma'}$, where $\Gamma' = F(\Gamma)[F(\Delta,t')/x]$.
By \rlem{ftmap-ctx}, it is equivalent to $F(\Delta,t')|_{\Delta = \Gamma'}$, which is equivalent to the first term $F(\Gamma',t')|_{\Delta = \Gamma'}$.
If $t = v_i$, this is obvious.

Now, suppose $t = \sigma(t_1, \ldots t_k)$, where $\sigma$ is either a function symbol or $\subst$.
Then the first term is equivalent to $s|_\varphi$, where
\begin{align*}
s & = \sigma_n(\Gamma', \ldots, F(F(\Gamma', \Gamma^\sigma_i(t_1, \ldots t_{i-1})[t'/x]), t_i[t'/x]), \ldots) \\
\varphi & = \bigwedge_{1 \leq i \leq k} \bigwedge_{(\Delta',x) \in \sub((\Gamma,\Gamma^\sigma_i(t_1, \ldots t_{i-1})),t_i)} \Delta = F(\Delta'[t'/x])
\end{align*}
By induction hypothesis, the second term is equivalent to $s|_{\varphi \land \psi}$, where
\[ \psi = \bigwedge_{1 \leq i \leq k} \bigwedge_{(\Delta'',x) \in \sub(\Gamma,\Gamma^\sigma_i(t_1, \ldots t_{i-1}))} \Delta = F(\Delta''[t'/x]) \]
If $(\Delta'',x) \in \sub(\Gamma,\Gamma^\sigma_i(t_1, \ldots t_{i-1}))$, then \rlem{sub-subst} implies that there exists $(\Delta',x_j) \in \sub(\Gamma,\Gamma^\sigma_i)$ such that $(\Delta'',x) \in \sub(\Delta'[\rho], t_j)$, where $\rho(x_m) = t_m$.
By \eqref{it:ax-consist}, we have equality $F(\Delta'[\rho]) = F(\Gamma,\Gamma^\sigma_j(t_1, \ldots t_{j-1}))$.
By \rlem{sub-repl}, there exists $\Delta'''$ such that $(\Delta''',x) \in \sub((\Gamma,\Gamma^\sigma_j(t_1, \ldots t_{j-1})), t_j)$ and $F(\Delta'') = F(\Delta''')$.
It follows that $s\!\downarrow \land \varphi \sststile{}{V} \psi$ is derivable.
Thus, $s_{\varphi \land \psi}$ is equivalent to $s_\varphi$.
\end{proof}

Let $f : T \to T'$ be an interpretation, then we can define $F(f) : F(T) \to F(T')$ as follows: $F(f)(S(x_1, \ldots x_k)) = F(f(S(x_1, \ldots x_k)))$.

\begin{lem}[ftmap-term]
If $f : T \to T'$ is an interpretation and $(\Gamma,t)$ is a contexted term, then terms $F(f)(F(\Gamma,t))$ and $F(f(\Gamma),f(t))$ are equivalent.
\end{lem}
\begin{proof}
The proof is by induction on $F(\Gamma,t)$.
If $t = x$ is a variable, then $F(f)(F(\Gamma,t))$ is equal to $x|_{\ft_{p,n}(x) = F(f)(F(\Gamma))}$ and $F(f(\Gamma),f(t))$ is equal to $x|_{\ft_{p,n}(x) = F(f(\Gamma))}$ and these terms are equivalent by induction hypothesis.
If $t = \sigma(t_1, \ldots t_k)$, then
\begin{align*}
F(f)(F(\Gamma,t)) & = \\
F(f)(\sigma_n(F(\Gamma), \ldots F((\Gamma, \Gamma^\sigma_i), t_i), \ldots)) & = \\
F(F(f)(F(\Gamma)), f(\sigma(x_1, \ldots x_k)))[\{ F(f)(F((\Gamma, \Gamma^\sigma_i), t_i))/x_i \}_{1 \leq i \leq k}] & \simeq \\
F(F(f(\Gamma)), f(\sigma(x_1, \ldots x_k)))[\{ F((f(\Gamma), f(\Gamma^\sigma_i)), f(t_i))/x_i \}_{1 \leq i \leq k}].
\end{align*}
By \rlem{ftmap-subst}, this term is equivalent to $F(f(\Gamma),f(t))|_{\bigwedge_{1 \leq j < i \leq k} \varphi_{i,j}}$, where $\varphi_{i,j}$ is the following formula:
\[ \bigwedge_{(\Delta,x_j) \in \sub(f(\Gamma), f(t_i))} F(f(\Gamma), f(\Gamma^\sigma_i(t_1, \ldots t_{i-1}))) = F(\Delta[\{ f(t_l)/x_l \}_{1 \leq l < i}]). \]
Thus, we just need to show that sequents $F(f(\Gamma),f(t)) \sststile{}{V} \varphi_{i,j}$ are derivable, but this follows from \eqref{it:interp-symb} and \rlem{ftmap-th}.
\end{proof}

\begin{lem}[ftmap-form]
If $f : T \to T'$ is an interpretation and $\varphi$ is a formula, then formulas $F(f)(F(\varphi))$ and $F(f(\varphi))$ are equivalent.
\end{lem}
\begin{proof}
This follows from \rlem{ftmap-term} by a similar argument.
\end{proof}

\begin{prop}
If $f : T \to T'$ is an interpretation, then $F(f) : F(T) \to F(T')$ is also interpretation.
Moreover, $F$ respects the equivalence relation on interpretations and it is a functor between $\algtt$ and $\algtt^\ft$.
\end{prop}
\begin{proof}
The facts that $F(f)$ is an interpretation and respects the equivalence relations follow from \eqref{it:interp-axiom}, \rlem{ftmap-th}, and \rlem{ftmap-form}.
It is obvious that $F$ preserves the identity morphism and the fact that it preserves the composition follows from \rlem{ftmap-term} and \rlem{ftmap-form}.
\end{proof}

Let $V$ be an $\mathcal{S}$-set of variables.
Then we define $G(V)$ as $V \amalg \{ x^i \mid x \in V, x : (p,n), 1 \leq i \leq n \}$.
For every term $t$ of sort $(p,n)$ with free variables in $V$ and every $0 \leq i \leq n$, we define an $\ft$-free restricted term $G^i(t)$ with free variables in $G(V)$.
The term $G^i(t)$ has sort $(p,n)$ if $i = 0$ and sort $(\ty,n-i)$ if $i > 0$.
\begin{align*}
G^0(x) & = x \\
G^{i+1}(x) & = x^{i+1} \\
G^i(\ft_n(t)) & = G^{i+1}(t) \\
G^0(v_{n,j}(\Gamma)) & = v_j \\
G^{i+1}(v_{n,j}(\Gamma)) & = G^i(\Gamma) \\
G^0(\subst_{p,n,k}(\Gamma, t, t_1, \ldots t_k)) & = \subst(G^k(t), \ldots G^0(t), G^0(t_1), \ldots G^0(t_k))|_\varphi \\
G^{i+1}(\subst_{p,n,k}(\Gamma, t, t_1, \ldots t_k)) & = G^i(\Gamma)|_\varphi \\
G^0(\sigma_n(\Gamma, t_1, \ldots t_k)) & = \sigma(G^0(t_1), \ldots G^0(t_k))|_\psi \\
G^{i+1}(\sigma_n(\Gamma, t_1, \ldots t_k)) & = G^i(\Gamma)|_\psi
\end{align*}
where $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,0)$ and
\begin{align*}
\varphi & = \bigwedge_{1 \leq i \leq k} (G^{n-1}(\Gamma), \ldots G^0(\Gamma)) \equiv (G^n(t_i), \ldots G^1(t_i)) \\
\psi & = \bigwedge_{1 \leq i \leq k} (G^{n-1}(\Gamma), \ldots G^0(\Gamma), \Gamma^\sigma_i(G^0(t_1), \ldots G^0(t_{i-1}))) \equiv (G^{n+n_i}(t_i), \ldots G^1(t_i))
\end{align*}
If $\Gamma$ is a term of sort $(\ctx,n)$, we will write $G(\Gamma)$ for the context $G^{n-1}(\Gamma), \ldots G^0(\Gamma)$.

\begin{lem}[gmap-term]
If $\Gamma = (B_1, \ldots B_n)$ is a context and $t$ is an $\ft$-free term of sort $(p,n)$ with free variables in $V$, then the following sequents are derivable:
\begin{align*}
\chi & \sststile{}{G(V)} \Gamma \vdash G^0(F(\Gamma,t)) \simeq t \\
\chi & \sststile{}{G(V)} B_1, \ldots B_{n-i-1} \vdash G^{i+1}(F(\Gamma,t)) \simeq B_{n-i}
\end{align*}
where $\chi = \bigwedge_{(\Delta,x) \in \sub((\Gamma,t)), x : (p,m)} \Delta \equiv (x^m, \ldots x^1)$.
Moreover, the following sequent is also derivable:
\[ \Gamma \vdash G^0(F(\Gamma,t)) \sststile{}{G(V)} \chi \]
\end{lem}
\begin{proof}
The proof is by induction on $F(\Gamma,t)$.
If $t = x$ is a variable, then it is obvious since $\Gamma \vdash G^0(F(\Gamma,x))$ is equal to $(\Gamma \vdash x) \land \chi$ and $\Gamma \vdash G^{i+1}(F(\Gamma,x))$ is equal to $(\Gamma \vdash x^{i+1}) \land \chi$ and the equality $B_1, \ldots B_{n-i-1} \vdash x^{i+1} \equiv B_{n-i}$ follows from $\chi$.
Let us consider the case $t = \subst(\overline{A}, t', t_1, \ldots t_k)$; other cases are similar.
First, note that $G^0(F(\Gamma,t))$ is equal to
\[ \subst(G^k(F(\overline{A},t')), \ldots A_k', G^0(F(\overline{A},t')), G^0(F(\Gamma,t_1)), \ldots G^0(F(\Gamma,t_k)))|_\varphi, \]
where $\varphi = \bigwedge_{1 \leq i \leq k} (G^{n-1}(F(\Gamma)), \ldots G^0(F(\Gamma))) \equiv (G^n(F(\Gamma,t_i)), \ldots G^1(F(\Gamma,t_i)))$.
By induction hypothesis, we have equalities $A_1, \ldots A_i \vdash G^{k-i}(F(\overline{A},t')) \equiv A_{i+1}$ for $i < k$ and $A_1, \ldots A_k \vdash G^0(F(\overline{A},t')) \equiv t'$.
Similarly, we have equalities $\Gamma \vdash G^0(F(\Gamma,t_i)) \equiv t_i$.
Thus, we just need to show that $\varphi$ is provable.
This follows from equalities $B_1, \ldots B_i \vdash G(F^{n-i}(\Gamma,t_j)) \equiv B_{i+1}$ and $B_1, \ldots B_i \vdash G^{n-i-1}(F(\Gamma)) \equiv B_{i+1}$.
The last sequent follows from the fact that every free variable belongs to some subterm.
\end{proof}

For every formula $\varphi$ with free variables in $V$, we define an $\ft$-free formula $G(\varphi)$ with free variables in $G(V)$:
\begin{align*}
G(t = t') & = (G(\ft_{p,n}(t)) \equiv G(\ft_{p,n}(t'))) \land (G(\ft_{p,n}(t)) \vdash G^0(t) \equiv G^0(t')) \\
G(\Ty_n(a,A)) & = (G(\ft_{\tm,n}(a)) \equiv G(\ft_{\ty,n}(A))) \land (G(\ft_{\ty,n}(A)) \vdash G^0(a) : G^0(A)) \\
G(R_n(\Gamma, t_1, \ldots t_k)) & = (G(\Gamma) \vdash R(G^0(t_1), \ldots G^0(t_k))) \land \psi \\
G(\varphi_1 \land \ldots \land \varphi_n) & = G(\varphi_1) \land \ldots \land G(\varphi_n)
\end{align*}
 where
 \[ \psi = \bigwedge_{1 \leq i \leq k} (G^{n-1}(\Gamma), \ldots G^0(\Gamma), \Gamma^R_i(G^0(t_1), \ldots G^0(t_{i-1}))) \equiv (G^{n+n_i}(t_i), \ldots G^1(t_i)) \]

\begin{lem}[gmap-form]
For every formulas $\varphi$, formulas $G(F(\varphi))$ and $\varphi \land \chi$ are equivalent,
where $\chi = \bigwedge_{(\Delta,x) \in \sub(\varphi), x : (p,m)} \Delta \equiv (x^m, \ldots x^1)$.
\end{lem}
\begin{proof}
Let us conside the case $\varphi = (\Gamma \vdash t_1 \equiv t_2)$; other cases are similar.
First, note that $G(F(\varphi))$ is equal to $(\Gamma_1 \equiv \Gamma_2) \land (\Gamma_1 \vdash G^0(F(\Gamma,t_1)) \equiv G^0(F(\Gamma,t_2)))$,
where $\Gamma_i$ is equal to $G^n(F(\Gamma,t_i)), \ldots G^1(F(\Gamma,t_i))$.
By \rlem{gmap-term}, the sequent $G^0(F(\Gamma,t_i)) \sststile{}{G(V)} \Delta \equiv (x^m, \ldots x^1)$ is derivable for every $(\Delta,x) \in \sub((\Gamma,t_i))$.
Thus, $G(F(\varphi)) \sststile{}{G(V)} \chi$ is derivable.
By \rlem{gmap-term}, $\Gamma_1$ and $\Gamma_2$ are equal to $\Gamma$ and $G^0(F(\Gamma,t_i))$ is equivalent to $t_i$ in $\Gamma$, which implies that $\varphi \land \chi$ and $G(F(\varphi))$ are equivalent.
\end{proof}

\begin{lem}[gmap-subst]
Formulas $G(\varphi[s/x])$ and $G(\varphi)[G^0(s)/x, G^1(s)/x^1, \ldots G^k(s)/x^k]$ are equivalent.
\end{lem}
\begin{proof}
To prove this, it is enough to show that the following restricted contexted terms are equivalent:
\begin{align*}
& (G(\ft_{p,n}(t[s/x])), G^0(t[s/x])) \\
& (G(\ft_{p,n}(t)), G^0(t))[G^0(s)/x, G^1(s)/x^1, \ldots G^k(s)/x^k]
\end{align*}
This is proved by easy induction on $t$.
\end{proof}

\begin{lem}[gmap-seq]
If $\varphi \sststile{}{\FV(\varphi)} \psi$ is derivable, then $G(\varphi) \sststile{}{G(\FV(\varphi))} G(\psi)$ is also derivable.
\end{lem}
\begin{proof}
We need to show that $G$ preserves inference rules and axioms.
Since all variables belong to $\FV(\varphi)$, the rule \axref{nf} follows from \axref{nh}, \axref{np}, and \axref{nf}.
The rule \axref{nl} follows from \rlem{gmap-subst}.
Other rules are obvious.
Thus, we just need to show that $G$ preserves axioms.

It is easy to see that $G$ preserves axioms listed in \rdefn{alg-tt} and the axioms of the theory of substitutions.
Thus, we just need to prove that $G(F(\varphi)) \sststile{}{G(V)} G(F(\psi))$ is an axiom whenever $\varphi \sststile{}{V} \psi$ is.
This follows from \rlem{gmap-form} since $\FV(\psi) \subseteq \FV(\varphi)$.
\end{proof}

\begin{lem}[gmap-rev-term]
The following sequents are derivable for every term $t$ and every $j$:
\begin{align*}
\ft^j_{p,n}(t) \land \bigwedge_{x \in \FV(t), x : (q,m), 1 \leq i \leq m} x^i = \ft^i_{p,n}(x) & \sststile{}{G(V)} F(\ft^{j+1}_{p,n}(t), G^j(t)) = \ft^j_{p,n}(t) \\
F(\ft^{j+1}_{p,n}(t), G^j(t)) & \sststile{}{G(V)} F(\ft^{j+1}_{p,n}(t), G^j(t)) = \ft^j_{p,n}(t)
\end{align*}
\end{lem}
\begin{proof}
By a straightforward induction on $t$.
\end{proof}

\begin{lem}[gmap-var]
The following sequent is derivable for every term $t$:
\[ G(t) \vdash G^i(t) \sststile{}{G(V)} \bigwedge_{(\Delta,x^j) \in \sub(G(t),G^i(t))} \Delta \equiv (x^n, \ldots x^{j+1}) \]
\end{lem}
\begin{proof}
By a straightforward induction on $t$.
\end{proof}

\begin{thm}
The functor $F : \algtt \to \algtt^\ft$ is fully faithful.
\end{thm}
\begin{proof}
Let $f,g : T \to T'$ be a pair of interpretations of $\ft$-free theories such that $F(f)$ and $F(g)$ are equivalent.
Let $\sigma$ be a function symbol of $T$.
Then $F(\Gamma, f(\sigma(x_1, \ldots x_k)))$ and $F(\Gamma, g(\sigma(x_1, \ldots x_k)))$ are equivalent.
By \rlem{gmap-seq}, the terms $G^0(F(\Gamma, f(\sigma(x_1, \ldots x_k))))$ and $G^0(F(\Gamma, g(\sigma(x_1, \ldots x_k))))$ are equivalent in $\Gamma$.
By \rlem{gmap-term}, the sequent $\chi \sststile{}{G(\{ \Gamma, x_1, \ldots x_k \})} \Gamma \vdash G^0(F(\Gamma, f(\sigma(x_1, \ldots x_k)))) \simeq f(\sigma(x_1, \ldots x_k))$ is derivable,
where $\chi = \bigwedge_{(\Delta,x_i) \in \sub((\Gamma,f(\sigma(x_1, \ldots x_k))))} \Delta \equiv (x^{n_i}_i, \ldots x^1_i)$.
Let $\rho(x_j^i) = B_j^i$, where $f(\Gamma^S_j) = (B^{n_j}_j, \ldots B^1_j)$.
Then the following sequent is derivable by \eqref{it:interp-symb}:
\[ \Gamma \vdash f(\sigma(x_1, \ldots x_k)) \sststile{}{V} \chi[\rho] \]
It follows that $\Gamma \vdash f(\sigma(x_1, \ldots x_k)) \sststile{}{V} \Gamma \vdash f(\sigma(x_1, \ldots x_k)) \equiv g(\sigma(x_1, \ldots x_k))$ is also derivable.
Similarly, $\Gamma \vdash g(\sigma(x_1, \ldots x_k)) \sststile{}{V} \Gamma \vdash f(\sigma(x_1, \ldots x_k)) \equiv g(\sigma(x_1, \ldots x_k))$ is derivable.
Similar argument shows that $f(R(x_1, \ldots x_k))$ and $g(R(x_1, \ldots x_k))$ are also equivalent for every predicate symbol.
It follows that $f$ and $g$ are equivalent.

Let $f : F(T) \to F(T')$ be an interpretation.
We need to define an interpretation $g : T \to T'$ such that $F(g) = f$.
Let $\sigma$ be a function symbol of $T$.
We define $g(\sigma(x_1, \ldots x_k))$ as $G^0(f(\sigma_0(\cdot, x_1, \ldots x_k)))[\rho']$, where $\rho'(x_i^j) = G^{j-1}(f(F(\Gamma^\sigma_i)))$.
We need to show that $F(g)(\sigma_n(\Gamma, x_1, \ldots x_k))$ is equivalent to $f(\sigma_n(\Gamma, x_1, \ldots x_k))$.
First, note that $F(g)(\sigma_n(\Gamma, x_1, \ldots x_k))$ is equivalent to $F(\Gamma, G^0(f(\sigma_n(\Gamma, x_1, \ldots x_k)))[\rho])$, where $\rho(x_i^j) = G^{j-1}(f(F(\Gamma,\Gamma^\sigma_i)))$.
By \rlem{gmap-var} and \rlem{ftmap-th}, the following sequent is derivable:
\[ F(G(t)[\rho], G^0(t)[\rho]) \sststile{}{G(V)} \bigwedge_{(\Delta,x_i^j) \in \sub(G(t), G^0(t))} F(\Delta[\rho]) \equiv F(\rho(x^n), \ldots \rho(x^{j+1})), \]
where $t = f(\sigma_n(\Gamma, x_1, \ldots x_k))$.
Now, \rlem{ftmap-subst} implies that $F(G(t)[\rho], G^0(t)[\rho])$ is equivalent to $F(G(t), G^0(t))[\rho']$, where $\rho'(x_i^j) = F(F(\rho(x_i^n), \ldots \rho(x_i^{j+1})), \rho(x_i^j))$.
Thus, it is enough to show that $F(\ft^{i+1}_{p,n}(t), G^i(t))[\rho']$ is equivalent to $\ft^i_{p,n}(t)$.
If the first term is defined, then we have the required equality by \rlem{gmap-rev-term}.
To prove the second required equality, we can apply the same lemma.
Then we just need to show that the following sequent is derivable for all $i$ and $j$:
\[ t\!\downarrow\ \sststile{}{\Gamma, x_1, \ldots x_k} \rho'(x_i^j) = \ft^j_{p_i,n_i}(x_i) \]
First, note that the sequent $t\!\downarrow\ \sststile{}{\Gamma, x_1, \ldots x_k} \ft_{p_i,n_i}(x_i) = f(F(\Gamma, \Gamma^\sigma_i))$ is derivable.
Thus, we just need to prove the equality $\rho'(x_i^j) = \ft^{j-1}_{p_i,n_i}(f(F(\Gamma, \Gamma^\sigma_i)))$.
This follows from \rlem{gmap-rev-term} by induction on $i$.
Indeed, we can apply it to the term $t_i = f(F(\Gamma, \Gamma^\sigma_i))$ if it holds for terms $t_{i'}$ with $i' < i$ since variables of the form $x_{i'}^j$ can appear in $\FV(t_i)$ only if $i' < i$.
\end{proof}

\section{The $\subst$-free syntax}

The syntax we described in the previous section is too verbose.
We can make it closer to the usual presentation of type theories by removing some redundant information.
We define another $\mathcal{S}$-set of terms $\Term(V)$ inductively as follows:
\begin{itemize}
\item If $X \in V_{(p,k)}$, $p \in \{ \ty, \tm \}$, and $t_1$, \ldots $t_k$ are terms of sort $(\tm,n)$, then $X(t_1, \ldots t_k)$ is a term of sort $(p,n)$.
\item $v_i$ is a term of sort $(\tm,n)$ for every $0 \leq i < n$.
\item If $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,0)$ is a function symbol of $T$ and $t_i$ is a term of sort $(p_i,n+n_i)$, then $\sigma(t_1, \ldots t_k)$ is a term of sort $(p,n)$.
\end{itemize}
These terms will be called \emph{$\subst$-free} terms.

Let $t$ be a term of sort $(p,n)$.
If $m \leq n$, then we define a term $\wk^k_m(t)$ of sort $(p,n+k)$ recursively:
\begin{itemize}
\item If $t = X(t_1, \ldots t_l)$, then $\wk^k_m(t) = X(\wk^k_m(t_1), \ldots \wk^k_m(t_l))$.
\item If $t = v_i$, then $\wk^k_m(v_i) = v_i$ if $i < m$ and $\wk^k_m(v_i) = v_{i+k}$ otherwise.
\item If $t = \sigma(t_1, \ldots t_l)$, where $\sigma : (p_1,n_1) \times \ldots \times (p_m,n_m) \to (p,0)$, then $\wk^k_m(t) = \sigma(\wk^k_{m+n_1}(t_1), \ldots \wk^k_{m+n_l}(t_l))$.
\end{itemize}

Let $t$ be a term of sort $(p,k)$ and let $t_1$, \ldots $t_k$ be terms of sort $(\tm,n)$.
Then we define a term $\subst(t, t_1, \ldots t_k)$ of sort $(p,n)$ recursively:
\begin{itemize}
\item If $t = X(t_1', \ldots t_m')$, then $\subst(t, t_1, \ldots t_k) = X(t_1'', \ldots t_m'')$, where
\[ t_i'' = \subst(t_i', t_1, \ldots t_k). \]
\item If $t = v_i$, then $\subst(t, t_1, \ldots t_k) = t_{k-i}$.
\item If $t = \sigma(t_1', \ldots t_m')$, where $\sigma : (p_1,n_1) \times \ldots \times (p_m,n_m) \to (p,0)$, then $\subst(t, t_1, \ldots t_k) = \sigma(t_1'', \ldots t_m'')$, where
\[ t_i'' = \subst(t_i', \wk^{n_i}_0(t_1), \ldots \wk^{n_i}_0(t_k), v_{n_i-1}, \ldots v_0). \]
\end{itemize}

If $t$ is a term of sort $(p,n+k)$ and $t_1, \ldots t_k$ are terms of sort $(\tm,n)$, then we will write $t[t_1, \ldots t_k]$ for $\subst(t, v_{n-1}, \ldots v_0, t_1, \ldots t_k)$.
If $X$ is a variable, we will write $X$ for $X[]$.

Let $\rho$ be a map $V \to \Term(W)$ and let $t$ be a term with free variables in $V$.
Then we define a term $t[\rho]$ with free variables in $W$ recursively:
\begin{itemize}
\item If $t = X(t_1, \ldots t_k)$, then $t[\rho] = \subst(\rho(X), t_1[\rho], \ldots t_k[\rho])$.
\item If $t = v_i$, then $t[\rho] = v_i$.
\item If $t = \sigma(t_1, \ldots t_k)$, then $t[\rho] = \sigma(t_1[\rho], \ldots t_k[\rho])$.
\end{itemize}

A \emph{context} of length $n$ a sequence of terms of sorts $(\ty,0)$, \ldots $(\ty,n-1)$.
A \emph{contexted term} is a pair $(\Gamma,t)$, where $\Gamma$ is a context of length $n$ and $t$ is a term of sort $(p,n)$ for some $p \in \{ \ty, \tm \}$.
An ($\subst$-free) \emph{judgment} is an expression of one of the following forms:
\[ \Gamma \vdash a : A \qquad \Gamma \vdash t \qquad \Gamma \vdash t \equiv t' \qquad \Gamma \vdash R(t_1, \ldots t_k) \]
where $\Gamma$ is a context of length $m$, $a$ is a term of sort $(\tm,m)$, $A$ is a term of sort $(\ty,m)$,
$t$ and $t'$ are terms of sort $(p,m)$ (where $p \in \{ \ty, \tm \}$), $R : (p_1,n_1) \times \ldots \times (p_k,n_k)$ is a predicate symbol, and $t_1$, \ldots $t_k$ are terms of sorts $(p_1,m+n_1)$, \ldots $(p_k,m+n_k)$, respectively.
All terms above are written in the $\subst$-free syntax.
We will use judgments of the form $\Gamma \vdash$.
If $\Gamma$ is the empty context, this judgment denotes $\top$.
If $\Gamma = (\Gamma', A)$, this judgment denotes $\Gamma' \vdash A$.

Jusgements play the role of atomic formulas in the $\subst$-free syntax.
An ($\subst$-free) \emph{formula} is a finite conjunction of judgments.
A \emph{sequent} is a triple (written as $\varphi \sststile{}{V} \psi$) consisting of formulas $\varphi$ and $\psi$ and a set $V$ of contexted terms in which the term is a variable such that $\FV(\varphi) \cup \FV(\psi) \cup \FV(V) \subseteq \{ X | (\Gamma,X) \in V \}$.
We will often write sequents in the form of derivation rules.
Thus, $\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \psi$ can be written as
\begin{center}
\AxiomC{$\varphi_1$}
\AxiomC{\ldots}
\AxiomC{$\varphi_n$}
\TrinaryInfC{$\psi$}
\DisplayProof
\end{center}
The set of variables $V$ is implicit in this notation and we let it to be the union of all variables that appear in the premise and in the conclusion.
Also, $\varphi_1 \land \ldots \land \varphi_n \ssststile{}{V} \psi$ will be represented by the following rule:
\begin{center}
\AxiomC{$\varphi_1$}
\AxiomC{\ldots}
\AxiomC{$\varphi_n$}
\doubleLine
\TrinaryInfC{$\psi$}
\DisplayProof
\end{center}

Let $\Gamma$ be a context of length $n$ and let $\Delta_1 = (A_1, \ldots A_k)$, $\Delta_2 = (B_1, \ldots B_k)$ be a pair of sequences of terms of sorts $(\ty,n)$, \ldots $(\ty,n+k)$.
Then we define $\Gamma \vdash \Delta_1 \equiv \Delta_2$ as $\Gamma \vdash A_1 \equiv B_1 \land \ldots \land \Gamma, A_1, \ldots A_{k-1} \vdash A_k \equiv B_k$.
If $\Gamma$ and $\Delta$ are two contexts of the same length, we define $\Gamma \equiv \Delta$ as $\vdash \Gamma \equiv \Delta$.

An ($\subst$-free) \emph{theory} $(\mathcal{F},\mathcal{P},\mathcal{A})$ consists of a set of function symbols $\mathcal{F}$ such that every function symbol has a signature of the form $s_1 \times \ldots \times s_k \to (p,0)$, a set of predicate symbols $\mathcal{P}$, and a set of axioms $\mathcal{A}$.
These sets must satisfy conditions listed in \rdefn{subst-free}.
Each symbol $S$ with $k$ parameters of sorts $(p_1,n_1)$, \ldots $(p_k,n_k)$ is equipped with a collection $\{ \Gamma^S_i(x_1, \ldots x_{i-1}) \}_{1 \leq i \leq k}$ of contexts,
where $\Gamma^S_i(x_1, \ldots x_{i-1})$ is a context of length $n_i$ with free variables in $\{ x_1 : (p_1,n_1), \ldots x_{i-1} : (p_{i-1},n_{i-1}) \}$.
We will write $\Gamma^S_i$ for $\Gamma^S_i(x_1, \ldots x_k)$.
We will also write $\Gamma^S_i(t_1, \ldots t_k)$ for $\Gamma^S_i[t_1/x_1, \ldots t_k/x_k]$.

Now, we can describe the derivation system for the $\subst$-free syntax:
\medskip
\begin{center}
\AxiomC{}
\RightLabel{\axlabel{ch}}
\UnaryInfC{$\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \varphi_i$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma, A, \Delta \vdash \psi$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash A \equiv B$}
\RightLabel{\axlabel{cx}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma, B, \Delta \vdash \psi$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash t$}
\RightLabel{\axlabel{cr}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash t \equiv t$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv b$}
\RightLabel{\axlabel{cs}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash b \equiv a$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv b$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash b \equiv c$}
\RightLabel{\axlabel{ct}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv c$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a \equiv a'$}
\RightLabel{\axlabel{cxl}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a' : A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash A \equiv A'$}
\RightLabel{\axlabel{cxr}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a : A'$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash R(t_1, \ldots t_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Gamma^R_i(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$}
\RightLabel{\axlabel{cp}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash R(t_1, \ldots t_{i-1}, t_i', t_{i+1}, \ldots t_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(t_1, \ldots t_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Gamma^\sigma_i(t_1, \ldots t_{i-1}) \vdash t_i \equiv t_i'$}
\RightLabel{\axlabel{cf}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \sigma(t_1, \ldots t_k) \equiv \sigma (t_1, \ldots t_{i-1}, t_i', t_{i+1}, \ldots t_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi_i[t_1/x_1, \ldots t_k/x_k]$, $1 \leq i \leq n$}
\RightLabel{\axlabel{ca}}
\UnaryInfC{$\varphi \sststile{}{V} \chi_j[t_1/x_1, \ldots t_k/x_k]$}
\DisplayProof
\end{center}
where $\psi_1 \land \ldots \land \psi_n \sststile{}{x_1 : s_1, \ldots x_k : s_k} \chi_1 \land \ldots \land \chi_m$ is an axiom and $t_1$, \ldots $t_k$ are arbitrary terms.

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash$}
\RightLabel{\axlabel{cv}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash v_i$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} A_1, \ldots A_m \vdash$}
\RightLabel{\axlabel{cvt}}
\UnaryInfC{$\varphi \sststile{}{V} A_1, \ldots A_m \vdash v_i : A_{m-i}(v_{m-1}, \ldots v_{i+1})$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_i, a_1, \ldots a_{i-1}) \text{, } 1 \leq i \leq k$
\def\extraVskip{2pt}
\RightLabel{, $(A_1, \ldots A_k \vdash X) \in V$ \axlabel{cm}}
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash X(a_1, \ldots a_k)$
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \varphi \sststile{}{V} \Gamma \vdash$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} A_1, \ldots A_k \vdash X : B$
\noLine
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_i, a_1, \ldots a_{i-1}) \text{, } 1 \leq i \leq k$
\def\extraVskip{2pt}
\RightLabel{, $(A_1, \ldots A_k \vdash X) \in V$ \axlabel{cmt}}
\UnaryInf$\fCenter \varphi \sststile{}{V} \Gamma \vdash X(a_1, \ldots a_k) : \subst(B, a_1, \ldots a_k)$
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash X(a_1, \ldots a_k)$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a_i \equiv a_i'$}
\RightLabel{\axlabel{cmc}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash X(a_1, \ldots a_k) \equiv X(a_1, \ldots a_i', \ldots a_k)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash t \equiv t'$}
\RightLabel{\axlabel{ee}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash t$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash S(t_1, \ldots t_k)$}
\RightLabel{\axlabel{ep}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma, \Gamma^S_i(t_1, \ldots t_{i-1}) \vdash t_i$}
\DisplayProof
\end{center}
where $S$ is either a function or a predicate symbol.

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \psi$}
\RightLabel{\axlabel{ec}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\RightLabel{\axlabel{el}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash a : A$}
\RightLabel{\axlabel{er}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash X(a_1, \ldots a_k)$}
\RightLabel{, $(A_1, \ldots A_k \vdash X) \in V$ \axlabel{em}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash a_i : \subst(A_i, a_1, \ldots a_{i-1})$}
\DisplayProof
\end{center}

\begin{defn}[subst-free]
An ($\subst$-free) \emph{theory} $(\mathcal{F},\mathcal{P},\mathcal{A})$ consists of a set of function symbols $\mathcal{F}$, a set of predicate symbols $\mathcal{P}$, and a set of axioms $\mathcal{A}$
together with a context $\Gamma^S_i(x_1, \ldots x_{i-1})$ for every symbol $S$ with $n$ parameters and every $1 \leq i \leq n$ such that
the following relation on the set of function symbols is well-founded: $\tau \prec \sigma$ if and only if $\tau$ appears in $\Gamma^\sigma_i$ for some $i$.
A \emph{theorem} is a derivable sequent.
\end{defn}

We do not usually explicitly specify context $\Gamma^S_i$.
Instead, we assume that every symbol $S$ has a unique axiom of the form
\[ \varphi \sststile{}{x_1, \ldots x_k}\ \vdash S(x_1, \ldots x_k) \]
such that there is a unique contexted subterm of $\varphi$ of the form $(\Gamma,x_i)$ for every $i$.
Then we let $\Gamma^S_i$ to be equal to $\Gamma$.

A rule is \emph{admissible} if its conclusion is derivable whenever its premises are.

\begin{lem}
The following rules are admissible:
\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma, \Delta \vdash \psi$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\RightLabel{\axlabel{cx'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma, \Delta' \vdash \psi$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\RightLabel{\axlabel{cs'}}
\UnaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \Delta' \equiv \Delta$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta'$}
\AxiomC{$\varphi \sststile{}{V} \Gamma \vdash \Delta' \equiv \Delta''$}
\RightLabel{\axlabel{ct'}}
\BinaryInfC{$\varphi \sststile{}{V} \Gamma \vdash \Delta \equiv \Delta''$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi$}
\RightLabel{$\mathrm{\axlabel{cu}}$}
\UnaryInfC{$\varphi[\rho] \sststile{}{V'} \psi[\rho]$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\psi \sststile{}{V} \chi$}
\RightLabel{$\mathrm{\axlabel{cc}}$}
\BinaryInfC{$\varphi \sststile{}{V} \chi$}
\DisplayProof
\end{center}
\end{lem}
\begin{proof}
The proof is by a straightforward induction on the length of $\Delta$ for \axref{cx'}, \axref{cs'}, and \axref{ct'},
on the derivation of $\varphi \sststile{}{V} \psi$ for \axref{cu}, and on the derivation of $\psi \sststile{}{V} \chi$ for \axref{cc}.
\end{proof}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}