From eb0ac1c3704d7c4a5751a89ebc27387975abd269 Mon Sep 17 00:00:00 2001 From: Jacob Walchuk Date: Mon, 7 Jul 2025 13:27:49 +0100 Subject: +1 graphic --- papers/3.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'papers/3.tex') diff --git a/papers/3.tex b/papers/3.tex index 6066649..84a52f1 100644 --- a/papers/3.tex +++ b/papers/3.tex @@ -205,7 +205,7 @@ $\forall x (Xx \ba x=y), Haec(X)(z) \wedge z \neq y \vdash Xy \ba y=y \\ \end{quote} Then, from $\vdash Haec(X)(y) \ra Tra(X)(y)$, we can observe that: \\ \begin{quote} -\begin{tabulary}{\textwidth}{Lr} +\begin{tabulary}{\textwidth}{LR} $\vdash \Box Haec(X)(y) \ra \Box Tra(X)(y)$ & (K) \\ $\vdash \Box \forall x (Xx \ba x=y) \ra \Box \Box \forall x (Xx \ba x=y)$ & (\textbf{4})\\ $\vdash Haec(X)(y) \ra \Box Haec(X)(y)$ & (Chaining conditionals) \\ @@ -214,7 +214,7 @@ $\vdash Haec(X)(y) \ra \Box Tra(X)(y)$ & \end{quote} \subsection{The proof for (o-Tracking)} \begin{quote} -\begin{tabulary}{\textwidth}{Lr} +\begin{tabulary}{\textwidth}{LR} $\vdash Haec(X)(o) \ra Tra(X)(o)$ & (Proved above) \\ $\vdash \exists X Haec(X)(o) \ra \exists X Tra(X)(o)$ & (Derivable from $\forall$ rule) \\ $\vdash \Box \exists X Haec(X)(o) \ra \Box \exists X Tra(X)(o)$ & (K)\\ -- cgit v1.2.3