Inhalt
Aktueller Ordner:
/modal6eng.tex
% Options for packages loaded elsewhere
\PassOptionsToPackage{unicode}{hyperref}
\PassOptionsToPackage{hyphens}{url}
\PassOptionsToPackage{dvipsnames,svgnames,x11names}{xcolor}
\documentclass[
ngerman,
11pt,
]{article}
\usepackage{xcolor}
\usepackage[margin=2.5cm]{geometry}
\usepackage{amsmath,amssymb}
\setcounter{secnumdepth}{-\maxdimen} % remove section numbering
\usepackage{iftex}
\ifPDFTeX
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp} % provide euro and other symbols
\else % if luatex or xetex
\usepackage{unicode-math} % this also loads fontspec
\defaultfontfeatures{Scale=MatchLowercase}
\defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1}
\fi
\usepackage{lmodern}
\ifPDFTeX\else
% xetex/luatex font selection
\fi
% Use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
\IfFileExists{microtype.sty}{% use microtype if available
\usepackage[]{microtype}
\UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\makeatletter
\@ifundefined{KOMAClassName}{% if non-KOMA class
\IfFileExists{parskip.sty}{%
\usepackage{parskip}
}{% else
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}}
}{% if KOMA class
\KOMAoptions{parskip=half}}
\makeatother
\usepackage{longtable,booktabs,array}
\usepackage{calc} % for calculating minipage widths
% Correct order of tables after \paragraph or \subparagraph
\usepackage{etoolbox}
\makeatletter
\patchcmd\longtable{\par}{\if@noskipsec\mbox{}\fi\par}{}{}
\makeatother
% Allow footnotes in longtable head/foot
\IfFileExists{footnotehyper.sty}{\usepackage{footnotehyper}}{\usepackage{footnote}}
\makesavenoteenv{longtable}
\ifLuaTeX
\usepackage[bidi=basic,shorthands=off,]{babel}
\else
\usepackage[bidi=default,shorthands=off,]{babel}
\fi
\ifLuaTeX
\usepackage{selnolig} % disable illegal ligatures
\fi
\setlength{\emergencystretch}{3em} % prevent overfull lines
\providecommand{\tightlist}{%
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\usepackage{bookmark}
\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
\urlstyle{same}
\hypersetup{
pdftitle={The Minimality of the Superposition Axioms A Metalogical Investigation into the Independence of ASP1--ASP5},
pdfauthor={Paul Koop},
pdflang={de},
colorlinks=true,
linkcolor={blue},
filecolor={Maroon},
citecolor={Blue},
urlcolor={Blue},
pdfcreator={LaTeX via pandoc}}
\title{The Minimality of the Superposition Axioms\\
A Metalogical Investigation into the Independence of ASP1--ASP5}
\usepackage{etoolbox}
\makeatletter
\providecommand{\subtitle}[1]{% add subtitle to \maketitle
\apptocmd{\@title}{\par {\large #1 \par}}{}{}
}
\makeatother
\subtitle{A Metalogical Investigation into the Independence of
ASP1--ASP5}
\author{Paul Koop}
\date{}
\begin{document}
\maketitle
\begin{abstract}
In modal5.md it was shown: From the basic axioms A1, A4, A11, A12, A13,
A14, A15, the Trinitarian formula does not follow in pure S5. The
extension by the superposition axioms ASP1--ASP5 is sufficient. The
question of whether it is also minimal remained open. The present
treatise answers this question. It shows: ASP1 is derivable from ASP2 in
S5 and is therefore redundant. The minimal subset for the derivation of
the Trinitarian formula is \{ASP3, ASP4, ASP5\}. The full axiomatics is
minimal for the superposition intuition, not for the target statement
alone. The concept of minimality thus proves to be relative: it depends
on what is to be derived and on the intuition to be formalized.
\end{abstract}
{
\hypersetup{linkcolor=}
\setcounter{tocdepth}{3}
\tableofcontents
}
\emph{Past and future are horizons of knowledge.}\\
\emph{The present is the locus of reality.}\\
\emph{Nothing that was, is lost.}
\section{Preface: What This Treatise Is -- And What It Is
Not}\label{preface-what-this-treatise-is-and-what-it-is-not}
This treatise explicitly does not aim to prove the truth of a
metaphysical or theological claim.
It investigates the \textbf{logical structure of an axiomatic system}.
In \texttt{modal5.md} it was shown: From the basic axioms A1, A4, A11,
A12, A13, A14, A15, the Trinitarian formula \(\Box\forall x\,Tr(x)\)
does \textbf{not} follow in pure S5. The extension by the superposition
axioms ASP1--ASP5 is \textbf{sufficient}. The question remained open: Is
it also \textbf{minimal}? Is each of the five axioms indispensable?
The present investigation answers this question. It shows: The
superposition axioms are \textbf{not all indispensable}. ASP1 is
derivable from ASP2. The minimal subset for the derivation of the
Trinitarian formula is \(\{ASP3, ASP4, ASP5\}\).
The investigation is therefore \textbf{metalogical}: It determines the
\textbf{dependency structure} of a sufficient axiomatics. It does not
show that this axiomatics is the only possible one -- other extensions
could also be sufficient. It only shows: \textbf{Within the extension
chosen in \texttt{modal5.md}, the dependency structure is as it is.}
The central claim of this treatise is:
\begin{quote}
\textbf{For the derivation of the Trinitarian formula
\(\Box\forall x\,Tr(x)\), the minimal subset of the superposition axioms
is \(\{ASP3, ASP4, ASP5\}\). ASP1 is derivable from ASP2. ASP2 is not
necessary for the target statement, but is essential for the
superposition intuition.}
\end{quote}
We stand at the beginning of infinity. Other axiomatizations are
possible. What this treatise provides is a \textbf{map of dependencies}
within the structure proposed in \texttt{modal5.md}.
\section{Introduction: Three Forms of
Minimality}\label{introduction-three-forms-of-minimality}
The term ``minimality'' is ambiguous. Before we begin the actual
investigation, we must distinguish precisely.
\subsection{Redundancy}\label{redundancy}
A set of axioms \(\Sigma\) is \textbf{redundant} if there is an axiom
\(\varphi \in \Sigma\) that is derivable from
\(\Sigma \setminus \{\varphi\}\):
\[\Sigma \setminus \{\varphi\} \vdash \varphi\]
Redundancy is a \textbf{defect}: The redundant axiom contributes nothing
to the derivational strength and can be removed without weakening the
theory.
\subsection{Independence}\label{independence}
A set of axioms \(\Sigma\) is \textbf{independent} if for \textbf{no}
axiom \(\varphi \in \Sigma\):
\[\Sigma \setminus \{\varphi\} \vdash \varphi\]
Independence is the \textbf{stronger} property: No axiom is derivable
from the others.
\textbf{Important:} Independence is \textbf{not} the same as minimality
in the sense of power. An independent set of axioms can be larger than
necessary if another, smaller set of axioms generates the same theory.
Independence is an \textbf{internal} property of a given set of axioms.
\subsection{Semantic Indispensability (Sufficient
Minimality)}\label{semantic-indispensability-sufficient-minimality}
A set of axioms \(\Sigma\) is \textbf{semantically indispensable} (or
\textbf{sufficiently minimal}) for a target statement \(\varphi\) if:
\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
\(\Sigma \vdash \varphi\) (sufficiency).
\item
For every proper subset \(\Sigma' \subsetneq \Sigma\):
\(\Sigma' \nvdash \varphi\) (indispensability).
\end{enumerate}
\textbf{This property is stronger than independence.} It does not refer
to the derivability of individual axioms from the others, but to the
\textbf{derivability of the target statement} from subsets.
\subsection{What This Treatise Shows}\label{what-this-treatise-shows}
We show the \textbf{third} form: the \textbf{semantic indispensability}
of the superposition axioms for the Trinitarian formula.
More precisely: For each relevant axiom we construct an S5 model that
satisfies the remaining axioms, but in which
\(\neg\Box\forall x\,Tr(x)\) holds.
The existence of these models shows: The affected axioms are
indispensable for the derivation of \(\Box\forall x\,Tr(x)\) -- at least
within the axiomatics chosen in \texttt{modal5.md}.
\subsection{The Methodological
Self-Restriction}\label{the-methodological-self-restriction}
We do \textbf{not} show:
\begin{itemize}
\tightlist
\item
that the superposition axioms are true,
\item
that there is no other sufficient extension,
\item
that there is no other minimal subset of ASP1--ASP5 (if the axioms are
formulated differently).
\end{itemize}
We show \textbf{only}: In the version chosen in \texttt{modal5.md}, the
dependency structure is as it is. This is an \textbf{independence
result} in the sense of the metalogical tradition.
\section{Formal Language and Logical
Framework}\label{formal-language-and-logical-framework}
\subsection{Modal Logic S5}\label{modal-logic-s5}
We work in first-order modal logic with identity in system S5:
\begin{itemize}
\tightlist
\item
\textbf{Necessity:} \(\Box p\)
\item
\textbf{Possibility:} \(\Diamond p := \neg\Box\neg p\)
\end{itemize}
\textbf{Axioms of S5:}
\begin{itemize}
\tightlist
\item
(K) \(\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)\)
\item
(T) \(\Box p \rightarrow p\)
\item
(4) \(\Box p \rightarrow \Box\Box p\)
\item
(5) \(\Diamond p \rightarrow \Box\Diamond p\)
\end{itemize}
\textbf{Inference Rules:}
\begin{itemize}
\tightlist
\item
\textbf{Modus Ponens:} From \(p\) and \(p \rightarrow q\), infer
\(q\).
\item
\textbf{Necessitation:} From \(p\) (derivable), infer \(\Box p\).
\end{itemize}
\textbf{Tableau Rules for S5:}
\[\begin{aligned}
& (\neg\Box) & \frac{\neg\Box A}{\Diamond\neg A} \\
& (\Diamond) & \frac{\Diamond A}{A @ w_{\text{new}}} \quad \text{(new world)} \\
& (\Box) & \frac{\Box A @ w}{A @ v} \quad \text{for every already existing world } v \\
& (\neg\forall) & \frac{\neg\forall x A}{\exists x \neg A} \\
& (\exists) & \frac{\exists x A}{A[a/x]} \quad \text{(a new)} \\
& (\forall) & \frac{\forall x A}{A[a/x]} \quad \text{(a arbitrary)}
\end{aligned}\]
\subsection{Predicate Logic}\label{predicate-logic}
We use classical first-order predicate logic with identity (\(=\)) and
the usual quantifiers (\(\forall, \exists\)).
\subsection{Models}\label{models}
An \textbf{S5 model} is a tuple \(\mathcal{M} = (W, R, I)\) with:
\begin{itemize}
\tightlist
\item
\(W\): a non-empty set of worlds.
\item
\(R \subseteq W \times W\): an \textbf{equivalence relation} (S5
frame).
\item
\(I\): an interpretation function.
\end{itemize}
An \textbf{S5+SP model} is an S5 model that additionally satisfies the
superposition axioms ASP1--ASP5.
\section{The Basic Axioms (Repetition from
modal5.md)}\label{the-basic-axioms-repetition-from-modal5.md}
We repeat the basic axioms to make the treatise self-contained.
\subsection{A1 -- Monism}\label{a1-monism}
\[\boxed{A1 := \Box\neg\exists x\exists y\, FundamentallySeparated(x,y)}\]
\subsection{A4 -- Existence of a Possible
Reality}\label{a4-existence-of-a-possible-reality}
\[\boxed{A4 := \Diamond\exists w\, World(w)}\]
\subsection{A11 -- Transcendental
Bridge}\label{a11-transcendental-bridge}
\[\boxed{A11 := \forall w \left( \text{WorldSeparatedFromConsciousness}(w) \leftrightarrow \neg \exists c (Consciousness(c) \land c(w)) \right)}\]
\subsection{A12 -- Experienceability and
Realization}\label{a12-experienceability-and-realization}
\[\boxed{A12 := \forall p. \text{Experienceable}(p) \leftrightarrow \exists w. Realized(w, p)}\]
\subsection{A13, A14, A15 -- The Three Implications of the
Cases}\label{a13-a14-a15-the-three-implications-of-the-cases}
\[\boxed{A13 := \Box\forall x(T(x) \rightarrow U(x))}\]
\[\boxed{A14 := \Box\forall x(U(x) \rightarrow S(x))}\]
\[\boxed{A15 := \Box\forall x(S(x) \rightarrow T(x))}\]
\subsection{Definition of the Limit
Structure}\label{definition-of-the-limit-structure}
\[\boxed{T := \{ x \mid U < x < S \}}\]
\[\boxed{U := \lim_{x \to \inf} T}\]
\[\boxed{S := \lim_{x \to \sup} T}\] \[\boxed{Tr := U \land T \land S}\]
\section{The Superposition Axioms (Repetition from
modal5.md)}\label{the-superposition-axioms-repetition-from-modal5.md}
\subsection{ASP1 -- Consciousness in the
Superposition}\label{asp1-consciousness-in-the-superposition}
\[\boxed{ASP1 := C @ w_{\text{super}}}\]
\subsection{\texorpdfstring{ASP2 -- Uniqueness of
\(C\)}{ASP2 -- Uniqueness of C}}\label{asp2-uniqueness-of-c}
\[\boxed{ASP2 := \forall v (w_{\text{super}} R v \rightarrow (C @ v \leftrightarrow v = w_{\text{super}}))}\]
\subsection{ASP3 -- The Superposition Contains All
Tr-Properties}\label{asp3-the-superposition-contains-all-tr-properties}
\[\boxed{ASP3 := \forall x\,Tr(x) @ w_{\text{super}}}\]
\subsection{ASP4 -- Transfer to All
Worlds}\label{asp4-transfer-to-all-worlds}
\[\boxed{ASP4 := \forall v (w_{\text{super}} R v \rightarrow \forall x\,Tr(x) @ v)}\]
\subsection{ASP5 -- Universal
Reachability}\label{asp5-universal-reachability}
\[\boxed{ASP5 := \forall v (v \neq w_{\text{super}} \rightarrow w_{\text{super}} R v)}\]
\section{The Proof Strategy}\label{the-proof-strategy}
\subsection{Goal}\label{goal}
We want to show: For certain axioms of the superposition extension,
there exists an S5 model \(\mathcal{M}\) that satisfies the remaining
axioms, but in which \(\neg\Box\forall x\,Tr(x)\) holds.
\subsection{Construction Principle}\label{construction-principle}
Each model violates \textbf{exactly one} of the superposition
properties. All other superposition properties remain satisfied. The
violation is sufficient to undermine the necessity of the Trinitarian
formula.
\textbf{Important Preliminary Remark:} For \(\neg\Box\forall x\,Tr(x)\)
to hold in \(\mathcal{M}\), it suffices to construct a world \(w^*\) in
which \(\neg\forall x\,Tr(x)\) holds -- i.e., in which there is an
individual \(a\) with \(\neg T(a) \lor \neg U(a) \lor \neg S(a)\).
\subsection{A First Result: ASP2 Implies ASP1 in
S5}\label{a-first-result-asp2-implies-asp1-in-s5}
From ASP2, by instantiation \(v := w_{\text{super}}\):
\[w_{\text{super}} R w_{\text{super}} \rightarrow (C @ w_{\text{super}} \leftrightarrow w_{\text{super}} = w_{\text{super}})\]
In S5, reflexivity holds: \(w_{\text{super}} R w_{\text{super}}\). And
identity: \(w_{\text{super}} = w_{\text{super}}\). Therefore:
\[C @ w_{\text{super}}\]
That is ASP1. \textbf{ASP1 is therefore derivable from ASP2.} In the
full axiomatics, ASP1 is \textbf{redundant}.
\subsection{Consequence for the
Strategy}\label{consequence-for-the-strategy}
The strategy ``one model that violates exactly one axiom'' is
\textbf{not} feasible for all pairs. For ASP1 and ASP2: ASP2 implies
ASP1 in S5. Therefore ASP1 is \textbf{redundant}.
\textbf{Refined Goal:} We show the \textbf{indispensability of ASP3,
ASP4, ASP5} for the derivation of the Trinitarian formula. For ASP1, we
show that in the version of \texttt{modal5.md} it is \textbf{redundant}.
For ASP2, we show that it is not necessary for the target statement, but
is essential for the superposition intuition.
\section{Part A: Minimal Subset for the Target
Statement}\label{part-a-minimal-subset-for-the-target-statement}
\subsection{\texorpdfstring{Theorem A1: \(\{ASP3, ASP4, ASP5\}\) is
Sufficient}{Theorem A1: \textbackslash\{ASP3, ASP4, ASP5\textbackslash\} is Sufficient}}\label{theorem-a1-asp3-asp4-asp5-is-sufficient}
\textbf{Theorem:} In S5:
\[\{ASP3, ASP4, ASP5\} \vdash \Box\forall x\,Tr(x)\]
\textbf{Proof:} Let \(\mathcal{M} = (W, R, I)\) be an S5 model with
ASP3, ASP4, ASP5. Let \(w \in W\) be arbitrary.
\begin{itemize}
\tightlist
\item
\textbf{Case 1:} \(w = w_{\text{super}}\). By ASP3:
\(\mathcal{M}, w \models \forall x\,Tr(x)\).
\item
\textbf{Case 2:} \(w \neq w_{\text{super}}\). By ASP5:
\(w_{\text{super}} R w\). By ASP4:
\(\mathcal{M}, w \models \forall x\,Tr(x)\).
\end{itemize}
In both cases, \(\mathcal{M}, w \models \forall x\,Tr(x)\). Since \(w\)
was arbitrary:
\[\mathcal{M} \models \Box\forall x\,Tr(x)\]
q.e.d.
\subsection{\texorpdfstring{Theorem A2: No Proper Subset of
\(\{ASP3, ASP4, ASP5\}\) is
Sufficient}{Theorem A2: No Proper Subset of \textbackslash\{ASP3, ASP4, ASP5\textbackslash\} is Sufficient}}\label{theorem-a2-no-proper-subset-of-asp3-asp4-asp5-is-sufficient}
We show three countermodels.
\subsubsection{\texorpdfstring{Countermodel for \(\{ASP4, ASP5\}\)
(without
ASP3)}{Countermodel for \textbackslash\{ASP4, ASP5\textbackslash\} (without ASP3)}}\label{countermodel-for-asp4-asp5-without-asp3}
Let \(\mathcal{M}_3 = (W, R, I)\) with:
\begin{itemize}
\tightlist
\item
\(W = \{w_{\text{super}}, w^*\}\)
\item
\(R = W \times W\) (universal)
\item
\(I\):
\begin{itemize}
\tightlist
\item
\(Tr(x) @ w_{\text{super}}\): false for an individual \(a\).
\item
\(Tr(x) @ w^*\): true for all \(x\).
\end{itemize}
\end{itemize}
\textbf{Verification:}
\begin{itemize}
\tightlist
\item
ASP4 satisfied: For all \(v\) with \(w_{\text{super}} R v\),
\(\forall x\,Tr(x) @ v\) holds. In \(w^*\), \(\forall x\,Tr(x)\)
holds, so ASP4 is satisfied.
\item
ASP5 satisfied: For all \(v \neq w_{\text{super}}\),
\(w_{\text{super}} R v\) holds.
\item
ASP3 violated: \(\neg Tr(a) @ w_{\text{super}}\).
\item
\textbf{Target statement:} In \(w_{\text{super}}\), \(\neg Tr(a)\)
holds, hence \(\neg\forall x\,Tr(x)\). Therefore
\(\neg\Box\forall x\,Tr(x)\).
\end{itemize}
\textbf{Thus ASP3 is indispensable.}
\subsubsection{\texorpdfstring{Countermodel for \(\{ASP3, ASP5\}\)
(without
ASP4)}{Countermodel for \textbackslash\{ASP3, ASP5\textbackslash\} (without ASP4)}}\label{countermodel-for-asp3-asp5-without-asp4}
Let \(\mathcal{M}_4 = (W, R, I)\) with:
\begin{itemize}
\tightlist
\item
\(W = \{w_{\text{super}}, w_1\}\)
\item
\(R = W \times W\) (universal)
\item
\(I\):
\begin{itemize}
\tightlist
\item
\(Tr(x) @ w_{\text{super}}\): true for all \(x\).
\item
\(Tr(x) @ w_1\): false for \(a\).
\end{itemize}
\end{itemize}
\textbf{Verification:}
\begin{itemize}
\tightlist
\item
ASP3 satisfied: \(\forall x\,Tr(x) @ w_{\text{super}}\).
\item
ASP4 violated: \(w_{\text{super}} R w_1\), but \(\neg Tr(a) @ w_1\).
\item
ASP5 satisfied: For all \(v \neq w_{\text{super}}\) (i.e., for
\(v = w_1\)), \(w_{\text{super}} R w_1\) holds.
\item
\textbf{Target statement:} In \(w_1\), \(\neg Tr(a)\) holds, hence
\(\neg\forall x\,Tr(x)\). Therefore \(\neg\Box\forall x\,Tr(x)\).
\end{itemize}
\textbf{Thus ASP4 is indispensable.}
\subsubsection{\texorpdfstring{Countermodel for \(\{ASP3, ASP4\}\)
(without
ASP5)}{Countermodel for \textbackslash\{ASP3, ASP4\textbackslash\} (without ASP5)}}\label{countermodel-for-asp3-asp4-without-asp5}
Let \(\mathcal{M}_5 = (W, R, I)\) with:
\begin{itemize}
\tightlist
\item
\(W = \{w_{\text{super}}, w_1\}\)
\item
\(R = \{(w_{\text{super}}, w_{\text{super}}), (w_1, w_1)\}\) (two
isolated worlds)
\item
\(I\):
\begin{itemize}
\tightlist
\item
\(Tr(x) @ w_{\text{super}}\): true for all \(x\).
\item
\(Tr(x) @ w_1\): false for \(a\).
\end{itemize}
\end{itemize}
\textbf{Verification:}
\begin{itemize}
\tightlist
\item
ASP3 satisfied: \(\forall x\,Tr(x) @ w_{\text{super}}\).
\item
ASP4 satisfied: The only world \(v\) with \(w_{\text{super}} R v\) is
\(w_{\text{super}}\) itself, and there \(\forall x\,Tr(x)\) holds.
\item
ASP5 violated: \(w_1 \neq w_{\text{super}}\), but
\(w_{\text{super}} R w_1\) does not hold.
\item
\textbf{Target statement:} In \(w_1\), \(\neg Tr(a)\) holds, hence
\(\neg\forall x\,Tr(x)\). Therefore \(\neg\Box\forall x\,Tr(x)\).
\end{itemize}
\textbf{Thus ASP5 is indispensable.}
\subsection{\texorpdfstring{Theorem A3: \(\{ASP3, ASP4, ASP5\}\) is
Minimal}{Theorem A3: \textbackslash\{ASP3, ASP4, ASP5\textbackslash\} is Minimal}}\label{theorem-a3-asp3-asp4-asp5-is-minimal}
\textbf{Theorem:} The set \(\{ASP3, ASP4, ASP5\}\) is a minimal subset
of \(\{ASP1, \dots, ASP5\}\) that derives \(\Box\forall x\,Tr(x)\).
\textbf{Proof:} From Theorem A1, sufficiency follows. From Theorem A2,
the indispensability of each of the three axioms follows: No proper
subset of \(\{ASP3, ASP4, ASP5\}\) derives \(\Box\forall x\,Tr(x)\).
Hence the set is minimal. q.e.d.
\section{Part B: Role of ASP1 and
ASP2}\label{part-b-role-of-asp1-and-asp2}
\subsection{ASP1 and ASP2 Are Not Necessary for the Target
Statement}\label{asp1-and-asp2-are-not-necessary-for-the-target-statement}
\textbf{Theorem B1:}
\(\{ASP3, ASP4, ASP5\} \vdash \Box\forall x\,Tr(x)\), hence ASP1 and
ASP2 are not required for the target statement.
\textbf{Proof:} Directly from Theorem A1. q.e.d.
\subsection{ASP2 Implies ASP1 in S5}\label{asp2-implies-asp1-in-s5}
\textbf{Theorem B2:} In S5:
\[\{ASP2, \text{reflexivity}\} \vdash ASP1\]
\textbf{Proof:} From ASP2, by instantiation \(v := w_{\text{super}}\):
\[w_{\text{super}} R w_{\text{super}} \rightarrow (C @ w_{\text{super}} \leftrightarrow w_{\text{super}} = w_{\text{super}})\]
In S5, reflexivity holds: \(w_{\text{super}} R w_{\text{super}}\). And
identity: \(w_{\text{super}} = w_{\text{super}}\). Therefore:
\[C @ w_{\text{super}}\]
That is ASP1. q.e.d.
\subsection{Consequence: ASP1 is
Redundant}\label{consequence-asp1-is-redundant}
\textbf{Theorem B3:} In S5, ASP1 is derivable from ASP2. Hence ASP1 is
redundant in the full axiomatics \(\{ASP1, \dots, ASP5\}\).
\textbf{Proof:} Directly from Theorem B2. q.e.d.
\subsection{Role of ASP1 and ASP2 for the Superposition
Intuition}\label{role-of-asp1-and-asp2-for-the-superposition-intuition}
\textbf{Theorem B4:} ASP1 and ASP2 are not redundant for the
\textbf{superposition intuition}, even though they are not required for
the target statement \(\Box\forall x\,Tr(x)\).
\textbf{Justification:} The superposition intuition states that
consciousness (\(C\)) is the self-reflexive moment of the superposition.
This intuition is formalized by ASP1 and ASP2:
\begin{itemize}
\tightlist
\item
ASP1: \(C\) holds in the superposition.
\item
ASP2: \(C\) holds \textbf{only} in the superposition.
\end{itemize}
Without ASP1 and ASP2, the superposition intuition would not be fully
formalized. The axioms ASP3--ASP5 alone say nothing about \(C\).
\textbf{Conclusion:} There are two levels of minimality:
\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
\textbf{Minimality for the target statement:} \(\{ASP3, ASP4, ASP5\}\)
is minimal.
\item
\textbf{Minimality for the superposition intuition:}
\(\{ASP1, \dots, ASP5\}\) is minimal (apart from the redundancy of
ASP1).
\end{enumerate}
\section{Part C: The Dependency Structure of the Superposition
Axioms}\label{part-c-the-dependency-structure-of-the-superposition-axioms}
\subsection{The Structure in a Table}\label{the-structure-in-a-table}
\begin{longtable}[]{@{}llll@{}}
\toprule\noalign{}
Axiom & Function & Necessary for target? & Derivable from others? \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
ASP1 & \(C\) in \(w_{\text{super}}\) & No & Yes (from ASP2) \\
ASP2 & \(C\) only in \(w_{\text{super}}\) & No & No \\
ASP3 & \(Tr\) in \(w_{\text{super}}\) & Yes & No \\
ASP4 & \(Tr\) in all reachable worlds & Yes & No \\
ASP5 & Universal reachability & Yes & No \\
\end{longtable}
\subsection{The Dependency Structure in a
Diagram}\label{the-dependency-structure-in-a-diagram}
ASP1 ← ASP2 (ASP2 implies ASP1) ~/ ~/ ~/ / {[}not necessary for
target{]}
ASP3 ──┐ ├──→ □∀x Tr(x) (jointly sufficient) ASP4 ──┤ │ ASP5 ──┘
text
\subsection{Interpretation}\label{interpretation}
The dependency structure shows:
\begin{itemize}
\tightlist
\item
\textbf{ASP2 is independent} and \textbf{stronger} than ASP1: It
implies ASP1.
\item
\textbf{ASP1 is redundant} in the full axiomatics, but useful for the
clarity of the intuition.
\item
\textbf{ASP3, ASP4, ASP5} form a \textbf{minimal sufficient subset}
for the target statement.
\item
\textbf{ASP3, ASP4, ASP5} are \textbf{mutually independent}.
\end{itemize}
\section{Part D: Consequences for
modal5.md}\label{part-d-consequences-for-modal5.md}
\subsection{The Axiomatics in modal5.md Is Not Minimal for the Target
Statement}\label{the-axiomatics-in-modal5.md-is-not-minimal-for-the-target-statement}
\textbf{Consequence D1:} The superposition axioms in \texttt{modal5.md}
contain redundant elements (ASP1) and elements not required for the
target statement (ASP1, ASP2).
\textbf{Consequence D2:} If the goal is only the derivation of
\(\Box\forall x\,Tr(x)\), then the minimal extension is
\(\{ASP3, ASP4, ASP5\}\).
\textbf{Consequence D3:} If the goal is the complete formalization of
the superposition intuition, then the extension
\(\{ASP1, \dots, ASP5\}\) is appropriate, with the redundancy of ASP1.
\subsection{The Metalogical
Significance}\label{the-metalogical-significance}
\textbf{Consequence D4:} The distinction between ``minimality for a
goal'' and ``minimality for an intuition'' is \textbf{central} to
metalogical analysis. An axiomatics can be minimal for a goal and
non-minimal for an intuition -- and vice versa.
\textbf{Consequence D5:} The analysis shows that the \textbf{choice of
axioms} depends not only on the target statement but also on the
\textbf{intuition} to be formalized. The superposition intuition
requires ASP1 and ASP2, even though these are not necessary for the
target statement.
\subsection{Open Questions}\label{open-questions}
\textbf{Question D6:} Is there another formulation of the superposition
intuition in which ASP1 and ASP2 are \textbf{indispensable}?
\textbf{Question D7:} Is the separation between ASP1/ASP2
(consciousness) and ASP3/ASP4/ASP5 (\(Tr\)) \textbf{systematic} or
accidental?
\textbf{Question D8:} Could the superposition intuition be
\textbf{formulated differently}, so that the target statement follows
from a \textbf{smaller} axiomatics?
\section{Part E: What Has Not Been
Shown}\label{part-e-what-has-not-been-shown}
\subsection{No Statement About Other
Extensions}\label{no-statement-about-other-extensions}
This treatise has \textbf{not} shown that the superposition axioms are
the \textbf{only} sufficient extension. Other extensions of S5 could
also be sufficient, with different dependency structures.
\textbf{Consequence E1:} The non-uniqueness of the extension is the
subject of \textbf{Modal 7}.
\subsection{No Statement About the Truth of the
Axioms}\label{no-statement-about-the-truth-of-the-axioms}
This treatise has \textbf{not} shown that the superposition axioms are
\textbf{true}. It has only shown that they are \textbf{independent} (in
the restricted sense).
\textbf{Consequence E2:} The question of the truth of the axioms is
\textbf{not} a metalogical question. It is a matter for metaphysics,
physics, or hermeneutics.
\subsection{No Statement About Minimality in an Absolute
Sense}\label{no-statement-about-minimality-in-an-absolute-sense}
This treatise has \textbf{not} shown that the superposition axioms are
minimal in an absolute sense. It has only shown that they are minimal
relative to a target statement or an intuition.
\textbf{Consequence E3:} The concept of ``minimality'' is
\textbf{relative}. It depends on what is to be derived.
\subsection{We Stand at the Beginning of
Infinity}\label{we-stand-at-the-beginning-of-infinity}
This treatise has clarified \textbf{one} aspect of the dependency
structure of the superposition axioms. It has \textbf{not} answered the
question of whether these axioms are the right choice for formalizing
the Trinitarian structure. It has \textbf{not} answered the question of
whether the Trinitarian structure exists at all. It has only shown:
\textbf{Within the axiomatics chosen in \texttt{modal5.md}, the
dependency structure is as it is.}
\section{Conclusion: What Has Been
Shown?}\label{conclusion-what-has-been-shown}
The present investigation has shown:
\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
\textbf{ASP2 implies ASP1 in S5.} ASP1 is redundant in the full
axiomatics.
\item
\textbf{The minimal subset for the target statement
\(\Box\forall x\,Tr(x)\) is \(\{ASP3, ASP4, ASP5\}\).} ASP1 and ASP2
are not necessary for the target statement.
\item
\textbf{ASP3, ASP4, and ASP5 are mutually independent.} None is
derivable from the others.
\item
\textbf{The full axiomatics \(\{ASP1, \dots, ASP5\}\) is minimal for
the superposition intuition}, not for the target statement alone.
\item
\textbf{The concept of minimality is relative.} It depends on what is
to be derived and on the intuition to be formalized.
\end{enumerate}
The central claim of this treatise is:
\begin{quote}
\textbf{The superposition axioms in the version of \texttt{modal5.md}
are not all indispensable for the derivation of the Trinitarian formula.
The minimal subset for this derivation is \(\{ASP3, ASP4, ASP5\}\). ASP1
is derivable from ASP2. The full axiomatics is minimal for the
superposition intuition, not for the target statement.}
\end{quote}
The treatise is thus a \textbf{refinement} of \texttt{modal5.md}. It
shows which axioms play which role, and it strictly distinguishes
between:
\begin{itemize}
\tightlist
\item
\textbf{Minimality for the target statement.}
\item
\textbf{Minimality for the superposition intuition.}
\end{itemize}
The question of whether the superposition axioms are the right choice
for formalizing the Trinitarian structure remains open. It is the
subject of \textbf{Modal 7} (Non-uniqueness).
\section{Appendix A: The Formal Structure in an
Overview}\label{appendix-a-the-formal-structure-in-an-overview}
\subsection{Axioms (Complete)}\label{axioms-complete}
\[\begin{aligned}
A1 &:= \Box\neg\exists x\exists y\, FundamentallySeparated(x,y) \\
A4 &:= \Diamond\exists w\, World(w) \\
A11 &:= \forall w \left( \text{WorldSeparatedFromConsciousness}(w) \leftrightarrow \neg \exists c (Consciousness(c) \land c(w)) \right) \\
A12 &:= \forall p. \text{Experienceable}(p) \leftrightarrow \exists w. Realized(w, p) \\
A13 &:= \Box\forall x(T(x) \rightarrow U(x)) \\
A14 &:= \Box\forall x(U(x) \rightarrow S(x)) \\
A15 &:= \Box\forall x(S(x) \rightarrow T(x)) \\
ASP1 &:= C @ w_{\text{super}} \\
ASP2 &:= \forall v (w_{\text{super}} R v \rightarrow (C @ v \leftrightarrow v = w_{\text{super}})) \\
ASP3 &:= \forall x\,Tr(x) @ w_{\text{super}} \\
ASP4 &:= \forall v (w_{\text{super}} R v \rightarrow \forall x\,Tr(x) @ v) \\
ASP5 &:= \forall v (v \neq w_{\text{super}} \rightarrow w_{\text{super}} R v)
\end{aligned}\]
\subsection{Definitions}\label{definitions}
\[\begin{aligned}
\text{WorldSeparatedFromConsciousness}(w) &:= \neg \exists c (Consciousness(c) \land c(w)) \\
\text{Experienceable}(p) &:= \exists w. (\text{Consciousness}(w) \land \text{Realized}(w, p)) \\
T &:= \{ x \mid U < x < S \} \\
U &:= \lim_{x \to \inf} T \\
S &:= \lim_{x \to \sup} T \\
Tr &:= U \land T \land S
\end{aligned}\]
\subsection{Derived Theorems}\label{derived-theorems}
\[\begin{aligned}
& \{ASP2\} \vdash ASP1 \quad \text{(in S5)} \\
& \{ASP3, ASP4, ASP5\} \vdash \Box\forall x\,Tr(x) \\
& \{ASP1, \dots, ASP5\} \vdash \Box\forall x\,Tr(x) \\
& \{ASP3, ASP4, ASP5\} \text{ is minimal for } \Box\forall x\,Tr(x) \\
& \{ASP1, \dots, ASP5\} \text{ is minimal for the superposition intuition}
\end{aligned}\]
\section{Appendix B: The Countermodels in an
Overview}\label{appendix-b-the-countermodels-in-an-overview}
\begin{longtable}[]{@{}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}
>{\raggedright\arraybackslash}p{(\linewidth - 16\tabcolsep) * \real{0.1111}}@{}}
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Model
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
\(W\)
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
\(R\)
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
ASP1
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
ASP2
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
ASP3
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
ASP4
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
ASP5
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Target statement
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
\(\mathcal{M}_3\) & \(\{w_{\text{super}}, w^*\}\) & universal & ✓ & ✓ &
✗ & ✓ & ✓ & ✗ \\
\(\mathcal{M}_4\) & \(\{w_{\text{super}}, w_1\}\) & universal & ✓ & ✓ &
✓ & ✗ & ✓ & ✗ \\
\(\mathcal{M}_5\) & \(\{w_{\text{super}}, w_1\}\) & two isolated classes
& ✓ & ✓ & ✓ & ✓ & ✗ & ✗ \\
\end{longtable}
\textbf{Explanation:} The table shows three models that each satisfy the
full axiomatics except for one axiom, and in which the target statement
\(\Box\forall x\,Tr(x)\) does \textbf{not} hold. Thus each of the three
axioms ASP3, ASP4, ASP5 is indispensable.
\section{Appendix C: The Role of ASP1 and ASP2 in an
Overview}\label{appendix-c-the-role-of-asp1-and-asp2-in-an-overview}
\begin{longtable}[]{@{}llll@{}}
\toprule\noalign{}
Axiom & Function & Necessary for target? & Redundant? \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
ASP1 & \(C\) in \(w_{\text{super}}\) & No & Yes (from ASP2) \\
ASP2 & \(C\) only in \(w_{\text{super}}\) & No & No \\
\end{longtable}
\textbf{Explanation:} ASP1 and ASP2 formalize the role of consciousness
in the superposition. They are not necessary for the target statement
\(\Box\forall x\,Tr(x)\), but they are essential for the superposition
intuition.
\section{Afterword}\label{afterword}
You have read this treatise. Perhaps the formal language remained
foreign to you; perhaps you found it clarifying. Both are perfectly
acceptable. For this text does not seek to proclaim a final truth, but
rather to render a movement of thought comprehensible.
The investigation has shown: The question of minimality is
\textbf{relative}. It depends on what is to be derived. Relative to the
Trinitarian formula, the minimal axiomatics is \(\{ASP3, ASP4, ASP5\}\).
Relative to the superposition intuition, the minimal axiomatics is
\(\{ASP1, \dots, ASP5\}\), with the redundancy of ASP1.
This relativity is \textbf{not a defect}. It is an \textbf{insight}: The
concept of minimality is not absolute. It depends on goal and intuition.
What remains is the insight that the Trinitarian structure \textbf{does
not} follow from monism alone -- it requires additional structure. The
superposition axioms are \textbf{one} such structure. Whether they are
the right one remains open.
One final question:
\begin{quote}
\textbf{Do we dare the leap into openness to the limit -- even though
the limit itself is not formally reachable?}
\end{quote}
\emph{This treatise was written in the spirit of rigorous modal logic,
yet in the language of philosophy -- for truth requires both: the
precision of the formula and the breadth of the concept.}
\end{document}