Maranassati Sutta 1

Buddhism
Philosophy
Psychology
Author

Lam Fu Yuan, Kevin

Published

December 25, 2025

Deathlessness

We should “gain a footing in the Deathless” and “have the Deathless as [our] final end” [1.1].

Let \(\text{Τ}\) be the set of non-negative real numbers representing all the moments in time, let \(\tau \in \text{Τ}\) be a variable for a moment in time, and let \(\tau_d \in \text{Τ}\) be the moment in time during which we die. In addition, let \(N\) be a one-place predicate over \(\text{Τ}\) such that \(N(\tau)\) is true if and only if we “gain a footing in the Deathless” and “have the Deathless as [our] final end” by \(\tau\) (or are likely to “gain a footing in the Deathless” and “have the Deathless as [our] final end” by τ; i.e., the probability that we “gain a footing in the Deathless” and “have the Deathless as [our] final end” by \(\tau\) is at least \(\theta\) for some threshold \(\theta\)). Then

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{1.1}\phantom{4.32} & \rlap{\text{O} N(\tau_d)}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A}^{1,2} \end{array} \]

Mindfulness of Death

We “might live for the interval that it takes to swallow having chewed up one morsel of food … for the interval that it takes to breathe out after breathing in, or to breathe in after breathing out” [2.1].

Let \(\tau_n \in \text{T}\) be the moment in time now, and let \(\delta \in \mathbb{R}^+\) be “the interval that it takes to swallow having chewed up one morsel of food … for the interval that it takes to breathe out after breathing in, or to breathe in after breathing out”. Then

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{2.1}\phantom{4.32} & \rlap{\Diamond (\tau_d = \tau_n + \delta)}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A}^{3} \\ \rlap{2.2}\phantom{4.32} & \rlap{\Box \Diamond (\tau_d = \tau_n + \delta)} & & & & & & & 2.1, \text{A5}^{4} \end{array} \]

Deathlessness and Mindfulness of Death

“Mindfulness of death, when developed and pursued […] gains a footing in the Deathless, has the Deathless as its final end” [3.1]. Because we should “gain a footing in the Deathless” and “have the Deathless as [our] final end” [1.1], we should “develop mindfulness of death” [3.7].

Let \(M\) be a predicate over \(\text{T}\) such that \(M(\tau)\) is true if and only if we “develop mindfulness of death” during \(\tau\). Then

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{3.1}\phantom{4.32} & \rlap{\Box[\exists \tau M(\tau) \leftrightarrow N(\tau_d)]}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A}^{5} \\ \rlap{3.2}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{3.3}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow N(\tau_d)} & & & & & & 3.1, \Box\text{E}^{6} \\ \rlap{3.4}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau M(\tau)} & & & & & & 3.3, \leftrightarrow \text{E}^{7} \\ \rlap{3.5}\phantom{4.32} & \rlap{\Box[N(\tau_d) \to \exists \tau M(\tau)]} & & & & & & & 3.2\text{--}3.4, \Box\text{I}^{8} \\ \rlap{3.6}\phantom{4.32} & \rlap{\text{O} N(\tau_d) \to \text{O} \exists \tau M(\tau)} & & & & & & & 3.5, \text{RM}'^{9} \\ \rlap{3.7}\phantom{4.32} & \rlap{\text{O} \exists \tau M(\tau)} & & & & & & & 1.1, 3.6, \to \text{E}^{10} \end{array} \]

Timeline for Developing Mindfulness of Death

Because we had not developed mindfulness of death in the past [4.1], and we cannot develop mindfulness of death after our death [4.2], we develop mindfulness of death if and only if we do so between now and our death [4.31].

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{4.1}\phantom{4.32} & \rlap{\Box \forall \tau \neg [M(\tau) \wedge \tau < \tau_n]}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A} \\ \rlap{4.2}\phantom{4.32} & \rlap{\Box \forall \tau \neg [M(\tau) \wedge \tau \geq \tau_d]} & & & & & & & \text{A} \\ \rlap{4.3}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{4.4}\phantom{4.32} & | & \rlap{\forall \tau \neg [M(\tau) \wedge \tau < \tau_n]} & & & & & & 4.1 \\ \rlap{4.5}\phantom{4.32} & | & \rlap{\forall \tau \neg [M(\tau) \wedge \tau \geq \tau_d]} & & & & & & 4.2 \\ \rlap{4.6}\phantom{4.32} & | & | & \rlap{\exists \tau \, M(\tau)} & & & & & \text{H} \\ \rlap{4.7}\phantom{4.32} & | & | & | & \rlap{M(t)} & & & & \text{H} \\ \rlap{4.8}\phantom{4.32} & | & | & | & \rlap{\neg [M(t) \wedge t < \tau_n]} & & & & 4.4, \forall \text{E}^{11} \\ \rlap{4.9}\phantom{4.32} & | & | & | & \rlap{\neg [M(t) \wedge t \geq \tau_d]} & & & & 4.5, \forall \text{E} \\ \rlap{4.10}\phantom{4.32} & | & | & | & \rlap{(t < \tau_n) \vee (t \geq \tau_d)} & & & & \text{H} \\ \rlap{4.11}\phantom{4.32} & | & | & | & | & \rlap{t < \tau_n} & & & \text{H} \\ \rlap{4.12}\phantom{4.32} & | & | & | & | & \rlap{\neg M(t)} & & & 4.8, 4.11, \text{DM, MI, } \to \text{E} \\ \rlap{4.13}\phantom{4.32} & | & | & | & \rlap{(t < \tau_n) \to \neg M(t)} & & & & 4.11, 4.12, \to \text{I} \\ \rlap{4.14}\phantom{4.32} & | & | & | & | & \rlap{t \geq \tau_d} & & & \text{H} \\ \rlap{4.15}\phantom{4.32} & | & | & | & | & \rlap{\neg M(t)} & & & 4.9, 4.14, \text{DM, MI, } \to \text{E} \\ \rlap{4.16}\phantom{4.32} & | & | & | & \rlap{(t \geq \tau_d) \to \neg M(t)} & & & & 4.14, 4.15, \to \text{I} \\ \rlap{4.17}\phantom{4.32} & | & | & | & \rlap{\neg M(t)} & & & & 4.10, 4.13, 4.16, \text{CD}^{12}, \text{TT}^{13} \\ \rlap{4.18}\phantom{4.32} & | & | & | & \rlap{M(t) \wedge \neg M(t)} & & & & 4.7, 4.17, \wedge \text{I} \\ \rlap{4.19}\phantom{4.32} & | & | & \rlap{\tau_n \leq t < \tau_d} & & & & & 4.10\text{--}4.18, \neg \text{I}^{14} \\ \rlap{4.20}\phantom{4.32} & | & | & \rlap{M(t) \wedge (\tau_n \leq t < \tau_d)} & & & & & 4.7, 4.19, \wedge \text{I} \\ \rlap{4.21}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & 4.20, \exists \text{I}^{15} \\ \rlap{4.22}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 4.6\text{--}4.21, \exists \text{E}^{16} \\ \rlap{4.23}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 4.6\text{--}4.22, \to \text{I} \\ \rlap{4.24}\phantom{4.32} & \rlap{\Box \{\exists \tau M(\tau) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]\}} & & & & & & & 4.3\text{--}4.23, \Box \text{I} \\ \rlap{4.25}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{4.26}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & \text{H} \\ \rlap{4.27}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau) \wedge \exists \tau (\tau_n \leq \tau < \tau_d)} & & & & & 4.26, \exists \wedge \exists \text{ }^{17} \\ \rlap{4.28}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 4.27, \wedge \text{E} \\ \rlap{4.29}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \to \exists \tau M(\tau)} & & & & & & 4.26\text{--}4.28, \to \text{I} \\ \rlap{4.30}\phantom{4.32} & | & \rlap{\Box \{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \to \exists \tau M(\tau)\}} & & & & & & 4.25\text{--}4.29, \Box \text{I} \\ \rlap{4.31}\phantom{4.32} & \rlap{\Box \{\exists \tau M(\tau) \leftrightarrow \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]\}} & & & & & & & 4.24, 4.30, \wedge \text{I}, \text{D}\Box \wedge^{18}, \leftrightarrow \text{I} \end{array} \]

Deathelessness and Timeline for Developing Mindfulness of Death

Because we “gain a footing in the Deathless” and “have the Deathless as [our] final end” only if we “develop mindfulness of death” [3.5], and we develop mindfulness of death only if we do so between now and our death [4.24], we are “gain a footing in the Deathless” and “have the Deathless as [our] final end” if and only if we “develop mindfulness of death” between now and our death [5.17].

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{5.1}\phantom{4.32} & | & \rlap{\Box} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \\ \rlap{5.2}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow N(\tau_d)} & & & & & & 3.1, \Box\text{E} \\ \rlap{5.3}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \to N(\tau_d)} & & & & & & 5.2, \leftrightarrow \text{E} \\ \rlap{5.4}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau M(\tau)} & & & & & & 5.2, \leftrightarrow \text{E} \\ \rlap{5.5}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 4.31, \Box\text{E} \\ \rlap{5.6}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 5.5, \leftrightarrow \text{E} \\ \rlap{5.7}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \to \exists \tau M(\tau)} & & & & & & 5.5, \leftrightarrow \text{E} \\ \rlap{5.8}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & \text{H} \\ \rlap{5.9}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 5.7, 5.8, \to \text{E} \\ \rlap{5.10}\phantom{4.32} & | & | & \rlap{N(\tau_d)} & & & & & 5.3, 5.9, \to \text{E} \\ \rlap{5.11}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \to N(\tau_d)} & & & & & & 5.8\text{--}5.10, \to \text{I} \\ \rlap{5.12}\phantom{4.32} & | & | & \rlap{N(\tau_d)} & & & & & \text{H} \\ \rlap{5.13}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 5.4, 5.12, \to \text{E} \\ \rlap{5.14}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & 5.6, 5.13, \to \text{E} \\ \rlap{5.15}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 5.12\text{--}5.14, \to \text{I} \\ \rlap{5.16}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \leftrightarrow N(\tau_d)} & & & & & & 5.11, 5.15, \leftrightarrow \text{I}^{19} \\ \rlap{5.17}\phantom{4.32} & \rlap{\Box \{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \leftrightarrow N(\tau_d)\}} & & & & & & & 5.1\text{--}5.16, \Box\text{I} \end{array} \]

Heedlessness and Heedfulness

If we “dwell heedlessly”, then we “develop mindfulness of death slowly” (i.e., “for a day and night … for a day … for the interval that it takes to eat a meal … for the interval that it takes to swallow having chewed up four morsels of food”) [6.1]. If so, then we might not “gain a footing in the Deathless” and “have the Deathless as [our] final end” [6.43].

Let \(HL\) be a zero-place predicate such that \(HL\) is true if and only if we “dwell heedlessly”. Then

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{6.1}\phantom{4.32} & \rlap{\Box \{HL \to \neg \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A} \\ \rlap{6.2}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{6.3}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & 4.31, \Box\text{E} \\ \rlap{6.4}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & & \text{H} \\ \rlap{6.5}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau) \wedge (\tau_d = \tau_n + \delta)} & & & & & \text{H} \\ \rlap{6.6}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 6.5, \wedge \text{E} \\ \rlap{6.7}\phantom{4.32} & | & | & \rlap{\tau_d = \tau_n + \delta} & & & & & 6.5, \wedge \text{E} \\ \rlap{6.8}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)]} & & & & & 6.4, 6.6, \to \text{E} \\ \rlap{6.9}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & 6.7, 6.8, = \text{E}^{20} \\ \rlap{6.10}\phantom{4.32} & | & \rlap{[\exists \tau M(\tau) \wedge (\tau_d = \tau_n + \delta)] \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & 6.5\text{--}6.9, \to \text{I} \\ \rlap{6.11}\phantom{4.32} & \rlap{\Box \{[\exists \tau M(\tau) \wedge (\tau_d = \tau_n + \delta)] \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}} & & & & & & & 6.2\text{--}6.10, \Box\text{I} \\ \rlap{6.12}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{6.13}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow N(\tau_d)} & & & & & & 3.1, \Box\text{E} \\ \rlap{6.14}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau M(\tau)} & & & & & & 6.13, \leftrightarrow \text{E} \\ \rlap{6.15}\phantom{4.32} & | & \rlap{[\exists \tau M(\tau) \wedge (\tau_d = \tau_n + \delta)] \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & 6.11, \Box\text{E} \\ \rlap{6.16}\phantom{4.32} & | & | & \rlap{\tau_d = \tau_n + \delta} & & & & & \text{H} \\ \rlap{6.17}\phantom{4.32} & | & | & \rlap{N(\tau_d)} & & & & & \text{H} \\ \rlap{6.18}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 6.14, 6.17, \to \text{E} \\ \rlap{6.19}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau) \wedge (\tau_d = \tau_n + \delta)} & & & & & 6.16, 6.18, \wedge \text{I} \\ \rlap{6.20}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & 6.15, 6.19, \to \text{E} \\ \rlap{6.21}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & 6.17\text{--}6.20, \to \text{I} \\ \rlap{6.22}\phantom{4.32} & | & \rlap{(\tau_d = \tau_n + \delta) \to \{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}} & & & & & & 6.16\text{--}6.21, \to \text{I} \\ \rlap{6.23}\phantom{4.32} & \rlap{\Box \{(\tau_d = \tau_n + \delta) \to \{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}\}} & & & & & & & 6.12\text{--}6.22, \Box\text{I} \\ \rlap{6.24}\phantom{4.32} & \rlap{\Diamond (\tau_d = \tau_n + \delta) \to \Diamond \{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}} & & & & & & & 6.23, \Box \to \Diamond^{21} \\ \rlap{6.25}\phantom{4.32} & \rlap{\Diamond \{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}} & & & & & & & 2.1, 6.24, \to \text{E} \\ \rlap{6.26}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{6.27}\phantom{4.32} & | & \rlap{HL \to \neg \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & 6.1, \Box\text{E} \\ \rlap{6.28}\phantom{4.32} & | & \rlap{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & \text{H} \\ \rlap{6.29}\phantom{4.32} & | & \rlap{\neg \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)] \to \neg N(\tau_d)} & & & & & & 6.28, \text{TR}^{22} \\ \rlap{6.30}\phantom{4.32} & | & \rlap{HL \to \neg N(\tau_d)} & & & & & & 6.27, 6.29, \text{HS}^{23} \\ \rlap{6.31}\phantom{4.32} & \rlap{\{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\} \to [HL \to \neg N(\tau_d)]} & & & & & & & 6.28\text{--}6.30, \to \text{I} \\ \rlap{6.32}\phantom{4.32} & \rlap{\Box (\{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\} \to [HL \to \neg N(\tau_d)])} & & & & & & & 6.26\text{--}6.31, \Box\text{I} \\ \rlap{6.33}\phantom{4.32} & \rlap{\Diamond \{N(\tau_d) \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\} \to \Diamond [HL \to \neg N(\tau_d)]} & & & & & & & 6.32, \Box \to \Diamond \\ \rlap{6.34}\phantom{4.32} & \rlap{\Diamond [HL \to \neg N(\tau_d)]} & & & & & & & 6.25, 6.33, \to \text{E} \end{array} \]

If we “dwell heedfully”, then we “develop mindfulness of death acutely” (i.e., “for the interval that it takes to swallow having chewed up one morsel of food … for the interval that it takes to breathe out after breathing in, or to breathe in after breathing out”) [6.44]. If so, then we “gain a footing in the Deathless” and “have the Deathless as [our] final end” [6.50].

Let \(HF\) be a zero-place predicate such that \(HF\) is true if and only if we “dwell heedfully”. Then

\[ \begin{array}{@{} l @{\hspace{1em}} l l l l l l l l} \rlap{6.35}\phantom{4.32} & \rlap{\Box \{HF \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\}}\phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{|} & \phantom{\Box[\exists \tau M(\tau) \to N(\tau_d)] \wedge \neg \Box[\neg \exists \tau M(\tau) \to N(\tau_d)]} & \phantom{||} & \text{A} \\ \rlap{6.36}\phantom{4.32} & | & \rlap{\Box} & & & & & & \\ \rlap{6.37}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \leftrightarrow N(\tau_d)} & & & & & & 5.17, \Box\text{E} \\ \rlap{6.38}\phantom{4.32} & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_d)] \to N(\tau_d)} & & & & & & 6.37, \leftrightarrow \text{E} \\ \rlap{6.39}\phantom{4.32} & | & \rlap{HF \to \exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & & 6.35, \Box\text{E} \\ \rlap{6.40}\phantom{4.32} & | & | & \rlap{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]} & & & & & \text{H} \\ \rlap{6.41}\phantom{4.32} & | & | & | & \rlap{M(t) \wedge (\tau_n \leq t < \tau_n + \delta)} & & & & \text{H} \\ \rlap{6.42}\phantom{4.32} & | & | & | & \rlap{M(t)} & & & & 6.41, \wedge \text{E} \\ \rlap{6.43}\phantom{4.32} & | & | & | & \rlap{\exists \tau M(\tau)} & & & & 6.42, \exists \text{I} \\ \rlap{6.44}\phantom{4.32} & | & | & \rlap{\exists \tau M(\tau)} & & & & & 6.40\text{--}6.43, \exists \text{E} \\ \rlap{6.45}\phantom{4.32} & | & \rlap{\{\exists \tau [M(\tau) \wedge (\tau_n \leq \tau < \tau_n + \delta)]\} \to \exists \tau M(\tau)} & & & & & & 6.40\text{--}6.44, \to \text{I} \\ \rlap{6.46}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \leftrightarrow N(\tau_d)} & & & & & & 3.1, \Box\text{E} \\ \rlap{6.47}\phantom{4.32} & | & \rlap{\exists \tau M(\tau) \to N(\tau_d)} & & & & & & 6.46, \leftrightarrow \text{E} \\ \rlap{6.48}\phantom{4.32} & | & \rlap{HF \to \exists \tau M(\tau)} & & & & & & 6.39, 6.45, \text{HS} \\ \rlap{6.49}\phantom{4.32} & | & \rlap{HF \to N(\tau_d)} & & & & & & 6.47, 6.48, \text{HS} \\ \rlap{6.50}\phantom{4.32} & \rlap{\Box [HF \to N(\tau_d)]} & & & & & & & 6.36\text{--}6.49, \Box\text{I} \end{array} \]

Notes
  1. Let \(\text{O}\) stand for “It is obligatory that”.
  2. Let \(\Box\) stand for “It is necessary that”.
  3. Let \(\Diamond \overset{\text{def}}{=} \neg\Box\neg\) stand for “It is possible that”.
  4. A5 (Axiom 5): \(\Diamond\phi \to \Box\Diamond\phi\)
  5. “Mindfulness of death, when developed and pursued […] gains a footing in the Deathless”. In other words, the development of mindfulness of death causes the gaining of a footing in the Deathless. If we do develop mindfulness of death, then we do “gain a footing in the Deathless” (or are likely to “gain a footing in the Deathless”). However, if we do not develop mindfulness of death, then we do not “gain a footing in the Deathless” (or are not likely to “gain a footing in the Deathless”).
  6. \(\Box\)E (Necessity Elimination): If \(\Box\phi\) is available in the subproof previous to a boxed subproof, infer \(\phi\) in the boxed subproof.
  7. \(\leftrightarrow\) E (Biconditional Elimination): From \(\phi \leftrightarrow \psi\), infer either \(\phi \to \psi\) or \(\psi \to \phi\).
  8. \(\Box\)I (Necessity Introduction): If \(\phi\) is derived in a boxed subproof, close the boxed subproof and infer \(\Box\phi\) outside the boxed subproof.
  9. RM’ (Theorem RM’): \(\Box(\phi \to \psi) \to (O\phi \to O\psi)\)
  10. \(\to\) E (Conditional Elimination): From \(\phi\) and \(\phi \to \psi\) infer \(\psi\).
  11. \(\forall\)E (Universal Elimination): From \(\forall\alpha\phi\) infer \(\phi\alpha/\beta\) (i.e., the result of replacing each occurrence of \(\beta\) in \(\phi\) with \(\alpha\)).
  12. CD (Constructive Dilemma): From \(\phi \vee \psi\), \(\phi \to \chi\) and \(\psi \to \omega\) infer \(\chi \vee \omega\).
  13. TT (Tautology): \(\phi \leftrightarrow (\phi \vee \phi)\) (Tautology)
  14. \(\neg\)I (Negation Introduction): From the derivation of an absurdity from the hypothesis \(\phi\) discharge \(\phi\) and infer \(\neg\phi\).
  15. \(\exists\)I (Existential Introduction): From \(\phi\) containing \(\alpha\) infer \(\exists\beta\phi\beta/\alpha\) (i.e., the result of replacing all occurrences of \(\alpha\) in \(\phi\) with \(\beta\) not already in \(\phi\)).
  16. \(\exists\)E (Existential Elimination): From \(\exists\beta\phi\) and the derivation of \(\psi\) from the hypothesis \(\phi\alpha/\beta\) (i.e., the result of replacing each occurrence of \(\beta\) in \(\phi\) with some \(\alpha\) not already in \(\phi\)) discharge \(\phi\alpha/\beta\) and infer \(\psi\). A may not occur in \(\psi\), in any assumption or in any hypothesis that is in effect at the line at which \(\exists\)E is applied.
  17. \(\exists \wedge \exists\) (Distribution of Existential Quantifier over Conjunction): From \(\exists\beta(\phi \wedge \psi)\) infer \(\exists\beta\phi \wedge \exists\beta\psi\).
  18. \(\Box \wedge \Box\) (Distribution of Necessity over Conjunction): \(\Box(\phi \wedge \psi) \leftrightarrow (\Box\phi \wedge \Box\psi)\)
  19. \(\leftrightarrow\) I (Biconditional Introduction): From \(\phi \to \psi\) and \(\psi \to \phi\) infer \(\phi \leftrightarrow \psi\).
  20. = E (Identity Elimination): From \(\phi\) containing \(\alpha\) and either \(\alpha = \beta\) or \(\beta = \alpha\) infer \(\phi\beta/\alpha\) (i.e., the result of replacing one or more occurrences of \(\alpha\) in \(\phi\) with \(\beta\)).
  21. \(\Box \to \Diamond\) (Distribution of Necessity over Conditional 1): \(\Box(\phi \to \psi) \to (\Diamond\phi \to \Diamond\psi)\)
  22. TR (Transposition): \((\phi \to \psi) \leftrightarrow (\neg\psi \to \neg\phi)\)
  23. HS (Hypothetical Syllogism): From \(\phi \to \psi\) and \(\psi \to \chi\), infer \(\phi \to \chi\).