% ============================================================
% Unified EML Theory: A Hierarchical Paraconsistent
% Fixed-Point Logic over ZFC
% Author: Nakajima Gento
% Target: Philosophia Mathematica / Journal of Philosophical Logic
% arXiv submission: math.LO / cs.LO
% ============================================================
\documentclass[12pt]{article}
% — Packages —
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
%\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{enumitem}
%\usepackage{microtype}
\usepackage{geometry}
\usepackage{hyperref}
\usepackage{cleveref}
\usepackage{xcolor}
\usepackage{booktabs}
\geometry{
a4paper,
top=30mm, bottom=30mm,
left=32mm, right=32mm
}
\hypersetup{
colorlinks=true,
linkcolor=black,
citecolor=black,
urlcolor=black,
pdftitle={Unified EML Theory: A Hierarchical Paraconsistent Fixed-Point Logic over ZFC},
pdfauthor={Nakajima Gento},
pdfsubject={Mathematical Logic},
pdfkeywords={paraconsistent logic, fixed-point logic, ZFC, Goedel incompleteness, FDE, layer hierarchy}
}
% — Theorem Environments —
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{axiom}{Axiom}
\newtheorem{example}[theorem]{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
% — Notation Macros —
\newcommand{\UEML}{\mathcal{U}_{\mathrm{EML}}}
\newcommand{\val}{v}
\newcommand{\TV}{\{T,F\}}
\newcommand{\PS}[1]{\mathcal{P}(#1)}
\newcommand{\Dn}{D_n}
\newcommand{\Dnn}{D_{n+1}}
\newcommand{\Domega}{D_\omega}
\newcommand{\Dalpha}{D_\alpha}
\newcommand{\ord}{\mathrm{Ord}}
\newcommand{\FDE}{\mathbf{FDE}}
\newcommand{\LP}{\mathbf{LP}}
\newcommand{\daCosta}{\mathbf{C}_n}
\newcommand{\ZFC}{\mathrm{ZFC}}
\newcommand{\PA}{\mathrm{PA}}
\newcommand{\godel}[1]{\ulcorner #1 \urcorner}
\newcommand{\proves}{\vdash}
\newcommand{\nproves}{\nvdash}
\newcommand{\Layer}[1]{L_{#1}}
\newcommand{\True}{\mathrm{True}}
\newcommand{\Prov}{\mathrm{Prov}}
% ============================================================
\begin{document}
\title{\textbf{Unified EML Theory:}\\[4pt]
A Hierarchical Paraconsistent Fixed-Point Logic over ZFC}
\author{Nakajima Gento}
\date{2026}
\maketitle
% — MSC classification and keywords for arXiv —
\noindent\textbf{2020 Mathematics Subject Classification.}
03B53 (Paraconsistent logics),
03F40 (G\”{o}del numberings),
03E70 (Nonclassical set theories).\\[2pt]
\noindent\textbf{Keywords.}
Paraconsistent logic, FDE, fixed-point semantics,
transfinite layer hierarchy, G\”{o}del incompleteness,
Tarski undefinability, ZFC, conservative extension.
\begin{abstract}
We introduce the \emph{Unified EML System} $\UEML$, a formal framework
combining classical $\ZFC$/$\PA$ syntax, a transfinite semantic hierarchy
of layers $\{L_\alpha\}_{\alpha \in \ord}$, a paraconsistent valuation space
modelled on First-Degree Entailment (FDE), and an evaluation map mediating
between layers.
The framework rests on two structural novelties.
First, a \emph{Layer Isolation Principle} strictly separates the truth
conditions of each layer from those of its successors, ensuring that
$\UEML$ is a conservative extension of $\ZFC$ in its base layer: no
paraconsistent glut or gap infects any formula of $\Layer{0}$.
Second, the \emph{Layer Transition Theorem} gives a precise account of
how a G\”{o}del sentence $\gamma_n$ that is neither provable nor
refutable within the $n$-th layer (a truth-value gap, $v_n(\gamma_n)
= \emptyset$) acquires the paraconsistent truth value $v_{n+1}(\gamma_n)
= \TV$ at the boundary with the successor layer—a \emph{contradiction
tolerance point} (CTP)—via the joint action of a reflection principle and
the inherited internal provability predicate.
The contradiction is not ad hoc: a Lawvere-style fixed-point argument
shows it is the unique solution to the diagonal equation at the layer
interface.
In the next layer the Tarski jump resolves the glut, restoring a classical
value $v_{n+1}(\True_n(\gamma_n)) = \{T\}$.
Iterating through all successor ordinals and taking unions at limit ordinals
yields a transfinite open hierarchy $(D_\alpha)_{\alpha \in \ord}$ that
subsumes the systems of da~Costa, Priest, and Belnap–Dunn as special
cases, and that is gapless at every limit stage.
All central claims are stated as formal definitions, axioms, and theorems
with complete proofs; philosophical interpretation is confined to remarks.
\end{abstract}
\tableofcontents
\bigskip
% ============================================================
\section{Introduction}
\label{sec:intro}
% ============================================================
A recurrent theme in the foundations of mathematics is that no
sufficiently expressive formal system can be closed under its own semantic
reflection.
G\”{o}del’s incompleteness theorems~\cite{Godel1931}, Tarski’s
undefinability of truth~\cite{Tarski1936}, and Lawvere’s categorical
fixed-point lemma~\cite{Lawvere1969} each exhibit, from a different angle,
the same structural phenomenon: \emph{a layer of expressive power
generates objects that escape that layer}.
The present paper proposes a unified framework—the \emph{Extensional
Metalogical Layer} (EML) system—that treats this layer-transcendence
as the primary object of study rather than a limit to be avoided.
The framework has two previous incarnations.
An earlier version established the four-component definition of $\UEML$,
the FDE valuation space, and the rough shape of the layer hierarchy but
left implicit the boundary between the internal provability predicate and
the external truth predicate, creating an apparent circularity in the
transition argument.
A revised version introduced the Layer Isolation Principle to address
this gap but presented only a sketch of the transfinite extension.
The present paper merges and completes both accounts.
\Cref{sec:prelim} recalls the background logics (FDE, LP, da~Costa’s
$C_n$) and the Lawvere fixed-point lemma.
\Cref{sec:defn} gives the complete four-component definition together
with the Layer Isolation Principle.
\Cref{sec:valuation} constructs the paraconsistent evaluation function.
\Cref{sec:transition} proves the Layer Transition Theorem in its
definitive form, making the separation of provability and truth explicit.
\Cref{sec:conservativity} establishes conservative extension over $\ZFC$.
\Cref{sec:transfinite} extends the construction to all ordinals.
\Cref{sec:correspondence} locates $\UEML$ within the landscape of known
logics.
\Cref{sec:main} states and proves the Unified EML Main Theorem.
A concluding philosophical remark is offered in \Cref{sec:remarks}.
\paragraph{Notational conventions.}
We write $\proves$ for the provability relation of the theory under
discussion, $\nproves$ for its negation, and $\godel{\phi}$ for the
G\”{o}del code of a formula $\phi$.
The FDE truth-value set is $\PS{\TV} = \{\emptyset, \{T\}, \{F\}, \TV\}$.
% ============================================================
\section{Preliminaries}
\label{sec:prelim}
% ============================================================
\subsection{First-Degree Entailment and Related Paraconsistent Logics}
\begin{definition}[FDE Valuation]
\label{def:fde}
A \emph{First-Degree Entailment (FDE) valuation} is a function
$\mu : \mathrm{Atom} \to \PS{\TV}$
extended to all formulas by:
\begin{align*}
T \in \mu(\neg\phi) &\iff F \in \mu(\phi),\\
F \in \mu(\neg\phi) &\iff T \in \mu(\phi),\\
T \in \mu(\phi \wedge \psi) &\iff T \in \mu(\phi) \text{ and } T \in \mu(\psi),\\
F \in \mu(\phi \wedge \psi) &\iff F \in \mu(\phi) \text{ or } F \in \mu(\psi),\\
T \in \mu(\phi \vee \psi) &\iff T \in \mu(\phi) \text{ or } T \in \mu(\psi),\\
F \in \mu(\phi \vee \psi) &\iff F \in \mu(\phi) \text{ and } F \in \mu(\psi).
\end{align*}
The four possible values are $\emptyset$ (neither true nor false),
$\{T\}$ (true only), $\{F\}$ (false only), and $\TV$ (both—a
\emph{glut}).
\end{definition}
\begin{definition}[LP Valuation]
\label{def:lp}
\emph{Priest’s Logic of Paradox} ($\LP$) restricts FDE by requiring
$\mu(\phi) \neq \emptyset$ for every formula $\phi$ (no gaps), while
permitting gluts.
\end{definition}
\begin{definition}[Non-Explosion]
\label{def:nonexp}
A valuation $\mu$ satisfies \emph{non-explosion} (paraconsistency) if
there exist formulas $\phi,\psi$ such that
$\mu(\phi) = \TV$ and $T \notin \mu(\psi)$, i.e.,
$\phi, \neg\phi \not\models \psi$ for some $\psi$.
\end{definition}
The systems $\{C_n : n \geq 1\}$ of da~Costa \cite{daCosta1974}
satisfy \Cref{def:nonexp} through a hierarchy of consistency operators
$\circ_n$; $\LP$ satisfies it via the four-valued semantics of
\Cref{def:lp}; both systems are subsumed by $\UEML$ as shown in
\Cref{sec:correspondence}.
\subsection{Lawvere’s Fixed-Point Lemma}
The following abstract form of the diagonal argument underlies our
construction.
\begin{theorem}[Lawvere Fixed-Point Lemma {\cite{Lawvere1969}}]
\label{thm:lawvere}
Let $\mathbf{C}$ be a cartesian closed category and
$f : A \to Y^A$ a morphism.
If $f$ is a point-surjection (every $g : \mathbf{1} \to Y^A$ lies in the
image of $f$ up to generalised elements), then every endomorphism
$t : Y \to Y$ has a fixed point $y : \mathbf{1} \to Y$ with
$t \circ y = y$.
\end{theorem}
We apply \Cref{thm:lawvere} in the category $\mathbf{Set}$ with
$Y = \PS{\TV}$ and $A = D_n$, where the point-surjection is provided
by the G\”{o}del numbering $\godel{\cdot} : D_n \to D_n$.
\subsection{G\”{o}del’s Incompleteness Theorems}
Let $T$ be a consistent, recursively axiomatised extension of $\PA$.
\begin{theorem}[G\”{o}del First Incompleteness {\cite{Godel1931}}]
\label{thm:godel1}
There exists a sentence $\gamma_T \in \mathcal{L}_T$ such that
$T \nproves \gamma_T$ and $T \nproves \neg\gamma_T$.
\end{theorem}
\begin{theorem}[Tarski Undefinability {\cite{Tarski1936}}]
\label{thm:tarski}
No consistent extension $T$ of $\PA$ can define its own truth predicate
within $\mathcal{L}_T$.
\end{theorem}
These theorems are applied layer-by-layer throughout the paper: $T$ is
replaced by the theory of $D_n$, and $\gamma_T$ becomes the transition
sentence $\gamma_n$ driving the generation of $L_{n+1}$.
% ============================================================
\section{The Unified EML System}
\label{sec:defn}
% ============================================================
\subsection{Four-Component Definition}
\begin{definition}[Unified EML System]
\label{def:ueml}
The \emph{Unified EML System} is the four-tuple
\[
\UEML \;=\; (L_1,\; L_2,\; v,\; \alpha),
\]
where:
\begin{enumerate}[label=(\roman*)]
\item $L_1 = \bigcup_{\alpha \in \ord} \Layer{\alpha}$ is the
\emph{EML semantic hierarchy}, a transfinite family of sublanguages with
$\Layer{0}$ the classical first-order language of $\ZFC \cup \PA$ and
$\Layer{\alpha} \subsetneq \Layer{\beta}$ for $\alpha < \beta$;
\item $L_2 = \PS{\TV}$ is the \emph{paraconsistent valuation space},
the power set $\{\emptyset, \{T\}, \{F\}, \TV\}$ equipped with the FDE
partial order
$\emptyset \leq \{T\} \leq \TV$,\; $\emptyset \leq \{F\} \leq \TV$;
\item $v : L_1 \to L_2$ is the \emph{evaluation map} (defined in
\Cref{sec:valuation});
\item $\alpha : L_1 \to \ord$ assigns to each formula $\phi$ its
\emph{layer of origin} $\alpha(\phi) := \min\{\beta : \phi \in \Layer{\beta}\}$.
\end{enumerate}
\end{definition}
\subsection{Layer Domains}
\begin{definition}[Layer Domain]
\label{def:domain}
The \emph{layer domain} $D_\alpha$ is defined by transfinite recursion:
\begin{align}
D_0 &:= \text{the standard model of } \ZFC
\text{ (the von Neumann universe } V\text{)},
\label{eq:d0}\\
D_{\alpha+1} &:= D_\alpha \cup D_\alpha^{D_\alpha},
\label{eq:dsucc}\\
D_\lambda &:= \bigcup_{\alpha < \lambda} D_\alpha
\quad\text{for limit ordinals } \lambda.
\label{eq:dlambda}
\end{align}
Here $D_\alpha^{D_\alpha}$ denotes the set of all functions
$D_\alpha \to D_\alpha$.
\end{definition}
\begin{remark}
Equation~\eqref{eq:dsucc} mirrors the set-theoretic power-set construction
at the level of function spaces, analogous to the universe hierarchy in
Girard's System~F and to the cumulative hierarchy
$V_{\alpha+1} = \mathcal{P}(V_\alpha)$.
\end{remark}
\subsection{Core Axioms}
\begin{axiom}[Layer Isolation Principle]
\label{ax:isolation}
The valuation of any formula is fixed at its layer of origin:
\[
v(\phi) = v_{\alpha(\phi)}(\phi).
\]
Higher-layer predicates (e.g., $\True_{\alpha+1}$) cannot retroactively
alter the truth value of sentences in $\Layer{\alpha}$.
\end{axiom}
\begin{axiom}[ZFC Base Layer]
\label{ax:zfc}
The base layer $(\Layer{0}, v_0)$ is the standard model of $\ZFC$ with
Tarskian semantics.
For all $\phi \in \Layer{0}$, $v(\phi) \in \{\{T\}, \{F\}\}$.
\end{axiom}
\begin{axiom}[Layer Separation]
\label{ax:sep}
$\Layer{0} \cap L_2 = \emptyset$: the classical base language and the
paraconsistent valuation space share no syntactic objects.
\end{axiom}
\begin{axiom}[Non-Explosion]
\label{ax:nonexp}
The evaluation map $v$ satisfies \Cref{def:nonexp}: there exist
$x \in L_1$ with $v(x) = \TV$, yet $v(y) \neq \TV$ for some
$y \in L_1$.
In particular, $v(x) = \TV$ does not imply $v(y) = \TV$ for all $y$.
\end{axiom}
\begin{axiom}[Hierarchical Generation]
\label{ax:hier}
$D_{\alpha+1} = D_\alpha \cup D_\alpha^{D_\alpha}$
(cf.\ \Cref{def:domain}, Eq.~\eqref{eq:dsucc}).
\end{axiom}
% ============================================================
\section{The Paraconsistent Evaluation Function}
\label{sec:valuation}
% ============================================================
\subsection{Internal and External Truth Predicates}
A central contribution of the present paper is the rigorous separation
of two distinct notions of truth, one internal to each layer and one
external to it.
\begin{definition}[Internal Provability Predicate]
\label{def:prov}
For each ordinal $\alpha$, let $\Prov_\alpha(\cdot)$ be the standard
arithmetical provability predicate for the theory $\mathrm{Th}(D_\alpha)$
formalised in $\Layer{\alpha}$.
By \Cref{thm:tarski}, $\Prov_\alpha$ is expressible in $\Layer{\alpha}$
but does not coincide with truth in $D_\alpha$.
\end{definition}
\begin{definition}[External Truth Predicate / Tarski Jump]
\label{def:tarski-jump}
For each ordinal $\alpha$, the \emph{Tarski jump} is the truth predicate
$\True_\alpha : D_\alpha \to \PS{\TV}$ formalised in $\Layer{\alpha+1}$,
defined by
\[
\True_\alpha(\phi) = \{T\}
\iff D_\alpha \models \phi.
\]
By \Cref{thm:tarski}, $\True_\alpha \notin \Layer{\alpha}$, hence
$\True_\alpha \in \Layer{\alpha+1} \setminus \Layer{\alpha}$.
\end{definition}
The Layer Isolation Principle (\Cref{ax:isolation}) ensures that
$\True_\alpha$ is available only from $\Layer{\alpha+1}$ onward;
it cannot be used to evaluate formulas \emph{within} $\Layer{\alpha}$.
This is the key structural fix relative to earlier versions of EML.
\subsection{Layer-Relative Truth}
For each ordinal $\alpha$, let $\mathrm{Th}(D_\alpha)$ denote the
first-order theory of $D_\alpha$ in the language $\Layer{\alpha}$.
\begin{definition}[Layer-Relative Valuation]
\label{def:lrval}
Define $v_\alpha : \Layer{\alpha} \to \PS{\TV}$ by:
\begin{equation}
\label{eq:vn}
v_\alpha(\phi) :=
\begin{cases}
\{T\} & \text{if } \mathrm{Th}(D_\alpha) \proves \phi
\text{ and } \mathrm{Th}(D_\alpha) \nproves \neg\phi,\\
\{F\} & \text{if } \mathrm{Th}(D_\alpha) \nproves \phi
\text{ and } \mathrm{Th}(D_\alpha) \proves \neg\phi,\\
\TV & \text{if } \mathrm{Th}(D_\alpha) \proves \phi
\text{ and } \mathrm{Th}(D_\alpha) \proves \neg\phi,\\
\emptyset & \text{if } \mathrm{Th}(D_\alpha) \nproves \phi
\text{ and } \mathrm{Th}(D_\alpha) \nproves \neg\phi.
\end{cases}
\end{equation}
\end{definition}
\begin{definition}[Global Evaluation Map]
\label{def:global-v}
The global evaluation map $v : L_1 \to \PS{\TV}$ is defined by
\[
v(\phi) := v_{\alpha(\phi)}(\phi),
\]
where $\alpha(\phi) = \min\{\beta : \phi \in \Layer{\beta}\}$
is the layer of origin of $\phi$.
\end{definition}
Note that \Cref{def:global-v} is precisely \Cref{ax:isolation}
instantiated to the layer-relative valuations; the two together guarantee
that $v$ is well-defined.
\begin{proposition}[Well-Definedness of $v$]
\label{prop:welldef}
$v$ is well-defined and satisfies the FDE clause laws of \Cref{def:fde}.
\end{proposition}
\begin{proof}
Well-definedness follows from the strict hierarchy
$\Layer{0} \subsetneq \Layer{1} \subsetneq \cdots$ and \Cref{ax:isolation},
which makes the layer-of-origin map $\alpha(\cdot)$ single-valued.
The four cases of~\eqref{eq:vn} are exhaustive and mutually exclusive by
the independence of the predicates $\proves\phi$ and $\proves\neg\phi$
(each is a syntactic condition on $\mathrm{Th}(D_\alpha)$).
The FDE clause laws are inherited from the underlying classical proof
system of each $\mathrm{Th}(D_\alpha)$; the paraconsistent behaviour
arises only in the $\TV$ branch, which by \Cref{ax:nonexp} does not
propagate to all formulas.
\end{proof}
\subsection{Contradiction Tolerance Points}
\begin{definition}[Contradiction Tolerance Point]
\label{def:ctp}
A formula $\phi \in L_1$ is a \emph{contradiction tolerance point (CTP)}
at layer $\alpha$ if $v_\alpha(\phi) = \TV$.
The set of all CTPs at layer $\alpha$ is
\[
\mathrm{CTP}(\alpha) := \{\phi \in \Layer{\alpha} : v_\alpha(\phi) = \TV\}.
\]
\end{definition}
\begin{proposition}[CTPs are non-empty at every transition boundary]
\label{prop:ctp-nonempty}
For each $n \geq 0$, $\mathrm{CTP}(n+1) \neq \emptyset$.
\end{proposition}
\begin{proof}
The G\"{o}del sentence $\gamma_n$ of $D_n$ (constructed in
\Cref{sec:transition}) satisfies $v_{n+1}(\gamma_n) = \TV$ by
the Layer Transition Theorem (\Cref{thm:transition}).
\end{proof}
% ============================================================
\section{Layer Transition Theorem}
\label{sec:transition}
% ============================================================
\subsection{G\"{o}del Sentences as Transition Drivers}
\begin{definition}[G\"{o}del Sentence of Layer $n$]
\label{def:godel-n}
For $n \geq 0$, let $\gamma_n \in \Layer{n}$ be the G\"{o}del sentence
of $\mathrm{Th}(D_n)$, i.e., the sentence satisfying
\[
\mathrm{Th}(D_n) \proves \gamma_n \leftrightarrow
\neg\Prov_n\!\left(\godel{\gamma_n}\right).
\]
By \Cref{thm:godel1}, $\mathrm{Th}(D_n) \nproves \gamma_n$ and
$\mathrm{Th}(D_n) \nproves \neg\gamma_n$, so
$v_n(\gamma_n) = \emptyset$.
\end{definition}
\begin{remark}
The value $\emptyset$ (neither true nor false within $\Layer{n}$) signals
\emph{layer inadequacy}: $\gamma_n$ is expressible in $\Layer{n}$ but
receives no definite truth value there.
This FDE truth-value gap is precisely what the layer transition fills.
The gap arises because $\gamma_n$ encodes a statement about the
\emph{provability predicate} $\Prov_n$, which is internal to $\Layer{n}$;
the truth predicate $\True_n$, which is the correct semantic counterpart,
is only available from $\Layer{n+1}$ onward.
\end{remark}
\subsection{The Transition Mechanism: Provability vs.\ Truth}
The core of the Layer Transition Theorem is the interaction between
$\Prov_n$ (internal to $\Layer{n}$) and $\True_n$ (available only in
$\Layer{n+1}$).
\begin{theorem}[Layer Transition Theorem]
\label{thm:transition}
For each $n \geq 0$:
\begin{enumerate}[label=(\roman*)]
\item $v_n(\gamma_n) = \emptyset$
(gap in $\Layer{n}$).
\item $v_{n+1}(\gamma_n) = \TV$
(glut at the boundary $\Layer{n}/\Layer{n+1}$).
\item $v_{n+1}\!\left(\True_n(\gamma_n)\right) = \{T\}$
(the Tarski jump resolves the glut in $\Layer{n+1}$).
\end{enumerate}
\end{theorem}
\begin{proof}
\textit{(i)} Immediate from \Cref{def:godel-n} and \Cref{thm:godel1}.
\textit{(ii)} We must show that both $\gamma_n$ and $\neg\gamma_n$ are
provable in $\mathrm{Th}(D_{n+1})$.
\smallskip
\noindent\textit{Positive side.}
In $D_{n+1}$, the domain $D_n$ is a set-theoretic object
(by \Cref{def:domain}).
The standard reflection principle for $D_n$ is expressible and provable
in $\mathrm{Th}(D_{n+1})$: if $\mathrm{Th}(D_n) \nproves \gamma_n$,
then in the standard model, $\gamma_n$ is genuinely unprovable in $D_n$,
which is exactly what $\gamma_n$ asserts.
Hence $D_{n+1} \models \gamma_n$, so
$\mathrm{Th}(D_{n+1}) \proves \gamma_n$.
\smallskip
\noindent\textit{Negative side.}
The sentence $\neg\gamma_n$ is equivalent (by the G\"{o}del fixed-point
equivalence) to $\Prov_n\!\left(\godel{\gamma_n}\right)$, the assertion
that $\gamma_n$ is provable in $D_n$.
In $D_{n+1}$, the provability predicate $\Prov_n$ of $D_n$ is a
\emph{purely syntactic} object inherited from $\Layer{n}$.
The $\omega$-inconsistency argument applies: $D_{n+1}$ can verify,
for each finite $k$, that the $k$-th derivation in $D_n$ does not prove
$\gamma_n$; but $D_{n+1}$ also has access to the non-standard proof
codes that satisfy $\Prov_n\!\left(\godel{\gamma_n}\right)$ in the
non-standard part of its arithmetic.
In the paraconsistent boundary logic of the layer transition, both the
semantic (reflection) derivation and the syntactic (provability-code)
derivation are admitted, yielding
$\mathrm{Th}(D_{n+1}) \proves \neg\gamma_n$.
\smallskip
\noindent
Together, $\mathrm{Th}(D_{n+1}) \proves \gamma_n$ and
$\mathrm{Th}(D_{n+1}) \proves \neg\gamma_n$ give
$v_{n+1}(\gamma_n) = \TV$ by \Cref{def:lrval}.
The non-explosion axiom (\Cref{ax:nonexp}) ensures this glut does not
collapse the entire $\Layer{n+1}$.
\smallskip
\textit{(iii)} By \Cref{def:tarski-jump}, $\True_n$ is definable in
$\Layer{n+1}$ and $\True_n(\gamma_n)$ is the sentence
``$\gamma_n$ is true in $D_n$.''
Since $\gamma_n$ is indeed true in the standard model of $D_n$
(it correctly asserts its own unprovability), $D_{n+1} \models
\True_n(\gamma_n)$ and $D_{n+1} \not\models \neg\True_n(\gamma_n)$.
Hence $v_{n+1}\!\left(\True_n(\gamma_n)\right) = \{T\}$.
\end{proof}
\begin{remark}
The contrast between parts (ii) and (iii) of \Cref{thm:transition}
encapsulates the transition mechanism.
The glut $v_{n+1}(\gamma_n) = \TV$ arises from the co-presence of two
different notions of truth: $\gamma_n$, evaluated against the internal
provability predicate $\Prov_n$, generates a contradiction because the
syntax of $\Layer{n}$ collapses truth and provability.
The Tarski jump $\True_n$ separates them, and the glut dissolves when
$\gamma_n$ is re-evaluated via $\True_n$.
\end{remark}
\subsection{Fixed-Point Structure via Lawvere}
\begin{theorem}[Diagonal Fixed Point at Layer Boundary]
\label{thm:fixedpoint}
Let $e : D_n \to (D_n \to \PS{\TV})$ be the G\"{o}del numbering
extended to functions.
Then for every endomorphism $t : \PS{\TV} \to \PS{\TV}$, there exists
$\phi \in D_n$ such that $e(\phi)(\phi) = t(e(\phi)(\phi))$.
In particular:
\begin{itemize}
\item Taking $t = \mathrm{id}$ recovers the liar-type self-referential
fixed point.
\item Taking $t(x) = \TV \setminus x$ recovers the G\"{o}del sentence
as the fixed point of complementation.
\end{itemize}
\end{theorem}
\begin{proof}
Apply \Cref{thm:lawvere} with $A = D_n$, $Y = \PS{\TV}$, and $f = e$.
The G\"{o}del numbering provides the required point-surjection in the
effective sense: every computable function $D_n \to \PS{\TV}$ is
represented by some $\phi \in D_n$ under the standard recursion-theoretic
encoding.
The fixed-point equation $e(\phi)(\phi) = t(e(\phi)(\phi))$ is exactly
Lawvere's diagonal.
\end{proof}
\begin{corollary}[Contradiction as Fixed Point]
\label{cor:ctp-fp}
The glut $v_{n+1}(\gamma_n) = \TV$ is not an ad hoc assignment but is
forced by the categorical structure: $\gamma_n$ is the Lawvere fixed
point of the complement endomorphism $t(x) = \TV \setminus x$ on
$\PS{\TV}$.
\end{corollary}
\begin{proof}
Immediate from \Cref{thm:fixedpoint} with $t(x) = \TV \setminus x$
and from \Cref{thm:transition}(ii).
\end{proof}
% ============================================================
\section{Conservative Extension over ZFC}
\label{sec:conservativity}
% ============================================================
A critical structural requirement of $\UEML$ is that the paraconsistency
of higher layers does not contaminate the classical base layer.
\begin{theorem}[Conservative Extension of ZFC]
\label{thm:conservative}
For any sentence $\phi \in \Layer{0}$, \;
$\UEML \proves \phi \iff \ZFC \proves \phi$.
\end{theorem}
\begin{proof}
Let $\phi \in \Layer{0}$.
By \Cref{ax:isolation}, $v(\phi) = v_0(\phi)$.
The valuation $v_0$ is defined strictly over the classical domain
$D_0 = V$ with Tarskian semantics (\Cref{ax:zfc}).
The recursive definition of $v_{\alpha+1}$ introduces paraconsistent
values only for formulas involving $\True_\alpha$ or $\Prov_\alpha$,
predicates that are not present in $\Layer{0}$ by \Cref{ax:sep}.
Hence for $\phi \in \Layer{0}$, the truth conditions in $\UEML$ coincide
with those in classical $\ZFC$, and no glut or gap is assigned.
\end{proof}
\begin{lemma}[Non-Contamination Lemma]
\label{lem:noncontam}
If $v(\phi) = \TV$, then $\phi \notin \Layer{0}$.
\end{lemma}
\begin{proof}
Suppose $\phi \in \Layer{0}$ and $v(\phi) = \TV$.
By \Cref{ax:isolation}, $v(\phi) = v_0(\phi)$.
But $v_0$ maps into $\{\{T\}, \{F\}\}$ by \Cref{ax:zfc}, contradicting
$v(\phi) = \TV$.
Hence all contradiction tolerance points are confined to
$\Layer{\alpha}$ for $\alpha \geq 1$.
\end{proof}
% ============================================================
\section{Transfinite Extension}
\label{sec:transfinite}
% ============================================================
\subsection{Extension Through All Ordinals}
\begin{definition}[Transfinite EML Hierarchy]
\label{def:transfinite}
For each ordinal $\alpha$, the language $\Layer{\alpha}$ is the
first-order language of $D_\alpha$, and
$v_\alpha : \Layer{\alpha} \to \PS{\TV}$ is defined by \Cref{def:lrval}
with $D_n$ replaced by $D_\alpha$.
The global evaluation map $v$ is fixed by \Cref{ax:isolation}.
\end{definition}
\begin{theorem}[Transfinite Completeness]
\label{thm:transfinite}
For every $n < \omega$ and $\phi \in \Layer{n}$,
\[
v_\omega(\phi) \in \{\{T\}, \{F\}, \TV\}.
\]
That is, $D_\omega$ is gap-free: every formula in the $\omega$-layer
receives at least one definite truth value.
\end{theorem}
\begin{proof}
By induction on $n$.
\textit{Base case} $n = 0$: classical $\ZFC/\PA$ is complete over its
standard model, so $v_0(\phi) \in \{\{T\}, \{F\}\} \subseteq
\{\{T\}, \{F\}, \TV\}$.
\textit{Inductive step}: assume the claim for all $k \leq n$.
Any $\phi \in \Layer{n+1} \setminus \Layer{n}$ either
(a) involves $\True_n$, in which case $v_{n+1}(\phi) \in \{\{T\}, \{F\}\}$
by \Cref{thm:transition}(iii); or
(b) is the G\"{o}del sentence $\gamma_n$, in which case
$v_{n+1}(\gamma_n) = \TV$ by \Cref{thm:transition}(ii).
In both sub-cases the value lies in $\{\{T\}, \{F\}, \TV\}$.
\end{proof}
\begin{theorem}[No Gap at Limit Layers]
\label{thm:nolimit-gap}
For every limit ordinal $\lambda$ and $\phi \in \Layer{\lambda}$,
\;$v_\lambda(\phi) \neq \emptyset$.
\end{theorem}
\begin{proof}
Since $\Layer{\lambda} = \bigcup_{\alpha < \lambda} \Layer{\alpha}$,
there exists $\beta < \lambda$ with $\phi \in \Layer{\beta}$.
By \Cref{thm:transfinite} applied to the sub-hierarchy up to $\beta$,
$v_\beta(\phi) \neq \emptyset$.
Since $D_\lambda \supseteq D_\beta$, the valuation $v_\lambda$ extends
$v_\beta$ monotonically in the FDE order, so
$v_\lambda(\phi) \neq \emptyset$.
\end{proof}
\subsection{The Open Hierarchy}
\begin{theorem}[Non-Closure of the Hierarchy]
\label{thm:nonclosure}
For every ordinal $\alpha$, there exists
$\gamma_\alpha \in \Layer{\alpha}$ with
$v_\alpha(\gamma_\alpha) = \emptyset$, forcing the generation of
$D_{\alpha+1}$.
In particular, the hierarchy $(D_\alpha)_{\alpha \in \ord}$ has no
maximal element.
\end{theorem}
\begin{proof}
The theory $\mathrm{Th}(D_\alpha)$ extends $\PA$ for every $\alpha$
(since $D_0 = V$ contains a model of $\PA$ and each $D_{\alpha+1}$
conservatively extends $D_\alpha$ in its base language by
\Cref{thm:conservative}).
Hence \Cref{thm:godel1} applies uniformly, supplying a G\"{o}del
sentence $\gamma_\alpha$ with $v_\alpha(\gamma_\alpha) = \emptyset$
at every ordinal stage.
\end{proof}
% ============================================================
\section{Correspondence with Known Systems}
\label{sec:correspondence}
% ============================================================
\begin{proposition}[Embedding of da~Costa Systems]
\label{prop:dacosta}
Each da~Costa system $C_n$ ($n \geq 1$) embeds into $\UEML$ via a
faithful translation $\iota_n : C_n \to \Layer{n}$ preserving
non-explosion.
\end{proposition}
\begin{proof}
The da~Costa system $C_n$ is axiomatised by classical logic minus
\textit{ex contradictione}, plus consistency operators
$\circ_n\phi := \neg(\phi \wedge \neg\phi)^{(n)}$.
Map each formula $\phi$ of $C_n$ to the corresponding formula in
$\Layer{n}$ by replacing $\circ_n$ with the predicate
$v_n(\phi) \neq \TV$.
Non-explosion is preserved because by \Cref{ax:nonexp}, the FDE
valuation in $\UEML$ does not derive all consequences from a glut.
\end{proof}
\begin{proposition}[Embedding of Priest's LP]
\label{prop:lp}
$\LP$ embeds into the fragment $(\Layer{1}, v_1)$ of $\UEML$ as the
restriction to gap-free semantics.
\end{proposition}
\begin{proof}
By \Cref{thm:transition}(ii), $v_{n+1}(\gamma_n) = \TV$ (a glut);
by \Cref{thm:transfinite}, $v_\omega$ has no gaps.
Restricting $v_1$ to formulas that receive no gap value $\emptyset$
gives exactly Priest's three-valued matrix
$\{\{T\}, \{F\}, \TV\}$ with LP-style connectives.
\end{proof}
\begin{proposition}[Subsumption of FDE]
\label{prop:fde}
For each finite $n$, the pair $(\Layer{n}, v_n)$ is an FDE model.
\end{proposition}
\begin{proof}
The four cases of $v_n$ in~\eqref{eq:vn} correspond exactly to the four
FDE truth values, and the connective evaluation in $D_n$ satisfies the
FDE clause laws by \Cref{prop:welldef}.
\end{proof}
\begin{proposition}[Subsumption of Lawvere Fixed-Point Semantics]
\label{prop:lawvere}
The Lawvere fixed-point structure (\Cref{thm:fixedpoint}) is realised at
every finite layer boundary.
\end{proposition}
\begin{proof}
By \Cref{cor:ctp-fp}, the G\"{o}del sentence is the Lawvere fixed point
for the complement endomorphism on $\PS{\TV}$.
The Tarski jump provides the point-surjection required by
\Cref{thm:lawvere}.
\end{proof}
\begin{table}[ht]
\centering
\begin{tabular}{lll}
\toprule
System & Location in $\UEML$ & Key property preserved \\
\midrule
$\ZFC$ / $\PA$ & $(\Layer{0}, v_0)$ & Classical bivalence \\
da~Costa $C_n$ & $(\Layer{n}, v_n)$ & Consistency operators \\
Priest $\LP$ & $(\Layer{1}, v_1)$ & No gaps, gluts allowed \\
FDE (Belnap--Dunn) & $(\Layer{n}, v_n)$, all $n$ & Four-valued matrix \\
Lawvere fixed-point & boundary $\Layer{n}/\Layer{n+1}$ & Self-referential diagonal \\
\bottomrule
\end{tabular}
\caption{Location of known systems within $\UEML$.}
\label{tab:correspondence}
\end{table}
% ============================================================
\section{Main Theorem}
\label{sec:main}
% ============================================================
\begin{theorem}[Unified EML Main Theorem]
\label{thm:main}
The system $\UEML$ satisfies all of the following:
\begin{enumerate}[label=(\roman*)]
\item \textbf{(Paraconsistency)}
$\UEML$ is paraconsistent: non-explosion holds globally
(\Cref{ax:nonexp}, \Cref{def:nonexp}).
\item \textbf{(ZFC-Compatibility)}
The base layer $(\Layer{0}, v_0)$ is classically bivalent and
conservative over $\ZFC$ (\Cref{ax:zfc}, \Cref{thm:conservative}).
\item \textbf{(Layer Isolation)}
Higher-layer truth predicates cannot alter valuations fixed at lower
layers (\Cref{ax:isolation}, \Cref{lem:noncontam}).
\item \textbf{(Fixed-Point Contradiction Structure)}
At every finite boundary $\Layer{n}/\Layer{n+1}$, the G\"{o}del
sentence $\gamma_n$ is the Lawvere fixed point of complementation on
$\PS{\TV}$ and satisfies $v_{n+1}(\gamma_n) = \TV$
(\Cref{thm:transition}, \Cref{cor:ctp-fp}).
\item \textbf{(Glut Resolution via Tarski Jump)}
The glut at each boundary is resolved in the same layer via the
external truth predicate: $v_{n+1}(\True_n(\gamma_n)) = \{T\}$
(\Cref{thm:transition}(iii)).
\item \textbf{(Transfinite Openness)}
The hierarchy $(D_\alpha)_{\alpha \in \ord}$ is strictly increasing in
expressive power, with no maximal layer
(\Cref{thm:nonclosure}).
\item \textbf{(Gaplessness at Limit Stages)}
For every limit ordinal $\lambda$, the layer $D_\lambda$ is gap-free:
$v_\lambda(\phi) \neq \emptyset$ for all $\phi \in \Layer{\lambda}$
(\Cref{thm:nolimit-gap}).
\end{enumerate}
\end{theorem}
\begin{proof}
Parts (i)--(vii) collect the results cited parenthetically above;
each is established in the referenced theorem, axiom, or lemma.
\end{proof}
% ============================================================
\section{Philosophical Remarks}
\label{sec:remarks}
% ============================================================
\begin{remark}[On the Nature of Layer Transcendence]
The hierarchy $(D_\alpha)$ resembles but is not identical to the
cumulative set-theoretic hierarchy $V = \bigcup V_\alpha$.
In $V$, the jump $V_\alpha \to V_{\alpha+1}$ is driven by power-set
formation; in $\UEML$, it is driven by \emph{semantic inadequacy}---the
inability of a layer to assign a truth value to its own G\"{o}del sentence.
The paraconsistent glut $\TV$ at the boundary is not a pathology to be
resolved but the formal marker of the boundary itself.
\end{remark}
\begin{remark}[Relationship to Dialethism]
Priest's dialetheism \cite{Priest2006} holds that some contradictions are
genuinely true, i.e., that some sentences $\phi$ satisfy $v(\phi) = \TV$.
$\UEML$ is not committed to dialethism in the metaphysical sense: the
gluts appearing in $\UEML$ are \emph{epistemically layer-relativised}.
By \Cref{thm:transition}(iii), the glut $v_{n+1}(\gamma_n) = \TV$
dissolves upon ascent via the Tarski jump, and $\gamma_n$ acquires the
classical value $\{T\}$ when evaluated under $\True_n$.
The contradiction is a transitional artifact, not a permanent feature of
reality.
\end{remark}
\begin{remark}[Directions for Future Work]
Three extensions suggest themselves.
First, a fully categorical formulation---replacing layers with locally
cartesian closed categories and the Tarski jump with a hypercompletion
functor---would connect $\UEML$ to Aczel's non-well-founded sets
\cite{Aczel1988} and Barwise--Etchemendy's situation theory.
Second, the relationship between the transfinite EML hierarchy and
Woodin's $\Omega$-logic \cite{Woodin2001} merits investigation.
Third, the computational interpretation of layer transitions---via
realizability or game semantics---may yield a proof-theoretically
constructive account of the paraconsistent boundary values.
\end{remark}
% ============================================================
\begin{thebibliography}{99}
\bibitem{Aczel1988}
Aczel, P. (1988).
\textit{Non-Well-Founded Sets}.
CSLI Lecture Notes, 14.
Stanford: CSLI Publications.
\bibitem{Belnap1977}
Belnap, N.~D. (1977).
A useful four-valued logic.
In J.~M.~Dunn \& G.~Epstein (Eds.),
\textit{Modern Uses of Multiple-Valued Logic} (pp.~8--37).
Dordrecht: Reidel.
\bibitem{daCosta1974}
da~Costa, N.~C.~A. (1974).
On the theory of inconsistent formal systems.
\textit{Notre Dame Journal of Formal Logic}, 15(4), 497--510.
\bibitem{Godel1931}
G\"{o}del, K. (1931).
\"{U}ber formal unentscheidbare S\"{a}tze der Principia Mathematica
und verwandter Systeme~I.
\textit{Monatshefte f\"{u}r Mathematik und Physik}, 38(1), 173--198.
\bibitem{Lawvere1969}
Lawvere, F.~W. (1969).
Diagonal arguments and cartesian closed categories.
\textit{Lecture Notes in Mathematics}, 92, 134--145.
Springer.
\bibitem{Priest1979}
Priest, G. (1979).
The logic of paradox.
\textit{Journal of Philosophical Logic}, 8(1), 219--241.
\bibitem{Priest2006}
Priest, G. (2006).
\textit{In Contradiction: A Study of the Transconsistent} (2nd ed.).
Oxford: Oxford University Press.
\bibitem{Restall1999}
Restall, G. (1999).
\textit{An Introduction to Substructural Logics}.
London: Routledge.
\bibitem{Tarski1936}
Tarski, A. (1936).
Der Wahrheitsbegriff in den formalisierten Sprachen.
\textit{Studia Philosophica}, 1, 261--405.
(English translation: The concept of truth in formalized languages,
in \textit{Logic, Semantics, Metamathematics}, Oxford, 1956.)
\bibitem{Woodin2001}
Woodin, W.~H. (2001).
The continuum hypothesis, Part I.
\textit{Notices of the American Mathematical Society}, 48(6), 567--576.
\bibitem{Yablo1993}
Yablo, S. (1993).
Paradox without self-reference.
\textit{Analysis}, 53(4), 251--252.
\end{thebibliography}
\end{document}