Seeking a proof equivalent to the story "She said that I would stop her if she told me why she is leaving, so I decided to stop her anyway!"

Question

I am looking for an interesting mathematical proof which is equivalent to the story:

"She said that I would stop her if she told me why she is leaving, so I decided to stop her anyway!"

Mathematically, I guess, this could be phrased, for a language $\mathcal L$ in propositional logic, as: $$\Big(\exists A\in Prop(\mathcal L) \,\,\text{s.t.}\,\,\vdash A\,\,\&\,\, A\implies B\Big)\implies B. $$

I am no logician and probably am wrong regarding to the last part, so please correct me, as long as my informal description is clear.

Edit: Clearly, there are many situations where you know \begin{align*} \vdash& A\\ \vdash& A\implies B\vee C\\ \vdash& (B\implies D)\&(C\implies D)\\ &\quad\Downarrow\\ \vdash& D\end{align*}

For example, have a function with two fixed points, each of which is rational, and have a convergent recursive sequence defined by this function. You know it converges to a fixed point but you do not know to which, however you do know that the limit is rational.

$\textbf{Edit:}$

In my example, it looks like $A$ could be "She was leaving to save her brother from Dracula" and $B$ is "I stopped her from leaving".

Answer 1

The original phrase

She said that I would stop her if she told me why she is leaving, so I decided to stop her anyway!" $~(0)$

The phrase $(0)$ reads as $(1)$, which is logically equivalent to the statement $B$. In $(1)$, I have symbolized "I stopped her" as $B$, and "she told me why she is leaving" as $W$.

\begin{equation}\tag{1} (W\rightarrow B)~\&~B \end{equation}

Careful reading of $(0)$ shows that the girl did not explain why she was leaving, so it's not necessary for the other person to stop her.

Your statement

\begin{equation}\tag{2} \Big(\exists A\in Prop(\mathcal L) \,\,\text{s.t.}\,\,\vdash A\,\,\&\,\, A\implies B\Big)\implies B \end{equation}

There are a few nuances with (2). To best state explicitly that the right hand side of $(2)$ is a sentence in propositional logic, you should bind both $A$ and $B$, as opposed to just $A$.

Secondly, you have placed the quantification and meta level proof symbol ($\vdash$), in the antecedent of your implication using brackets. This means that $(2)$ is equivilent to $(3)$, which is clearly not what you intended to say.

\begin{equation}\tag{3} \big(\exists A\in Prop(\mathcal L) \,\,\text{s.t.}\,\,\nvdash A\,\,\&\,\, A\implies B\Big)\lor B \end{equation}

A better symbolization of $(3)$ is $(4)$.

\begin{equation}\tag{4} \exists A,B \in Prop(\mathcal L) \,\,\text{s.t.}\,\,\vdash (A\,\,\&\,\, A\implies B)\implies B \end{equation}

Your first edit

Your edit is a lot clearer, and the symbolization for this statement is good. It has a different logical form to $(0)$ however, and appears to be unrelated.