diff options
| author | Jacob Walchuk <jpw24@st-andrews.ac.uk> | 2025-07-07 13:27:49 +0100 |
|---|---|---|
| committer | Jacob Walchuk <jpw24@st-andrews.ac.uk> | 2025-07-07 13:27:49 +0100 |
| commit | eb0ac1c3704d7c4a5751a89ebc27387975abd269 (patch) | |
| tree | 7411cc23c9abb8abdf35194b43930aa628333df2 /papers/3.tex | |
| parent | f7cee7212ad9626541dcc922a0cd762eb7450a38 (diff) | |
+1 graphic
Diffstat (limited to 'papers/3.tex')
| -rw-r--r-- | papers/3.tex | 4 |
1 files changed, 2 insertions, 2 deletions
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)\\ |