diff options
| -rw-r--r-- | papers/3.tex | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/papers/3.tex b/papers/3.tex index 52d364b..6b3f574 100644 --- a/papers/3.tex +++ b/papers/3.tex @@ -194,7 +194,7 @@ $\vdash \Box \forall x (Xx \ba x=y) \ra \neg \Diamond \exists z (Haec(X)(z) \wed $\vdash Haec(X)(y) \ra Tra(X)(y)$& \\ \end{tabulary} % terrible hack but it fixed the rendering, I am very sorry Mohit \end{quote} -Now I will show the first line. \\ +Now I will show the first line. \begin{quote} $\forall x (Xx \ba x=y), Haec(X)(z) \wedge z \neq y \vdash Xy \ba y=y \\ \forall x (Xx \ba x=y), Haec(X)(z) \wedge z \neq y \vdash Xy \ba z=y \\ @@ -205,18 +205,21 @@ $\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} -$\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)$ \\ -\vdash Haec(X)(y) \ra \Box Tra(X)(y)$ +\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) \\ +$\vdash Haec(X)(y) \ra \Box Tra(X)(y)$ & +\end{tabulary} \end{quote} \subsection{The proof for (o-Tracking)} - \begin{quote} -$\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)\\ -$\vdash \Box \exists X Tra(X)(o)$ \ \ \ \ (MP, o-Haecceity) +\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)\\ +$\vdash \Box \exists X Tra(X)(o)$ & (MP, $o$-Haecceity) +\end{tabulary} \end{quote} |