I’m currently reading through Visser’s “A Propositional Logic with Explicit Fixed Points“ (1980) and am having trouble proving a seemingly basic result.
The system is the analogue to GL modal logic on the same Gödel-Tarski translation as from Intuitionism to S4.
I’ve been trying to prove $(\top \to (p \to q)) \to (\neg q \to \neg p)$. The proof is simple in GL since the negation operator is classical, but this one is weaker than intuitionistic negation in that it does not validate $\neg (p \land \neg p)$. The closest I can get is $\neg q \to (\top \to \neg p)$, but since $(\top \to A) \to A$ is invalid, I don’t see how to proceed. Any insight would be appreciated.
Edit**
A useful lemma would be
$((\neg q \to \neg p) \to (p \to q)) \to (\neg q \to \neg p)$
which is is valid in FPL. If I could prove it, the result would follow pretty easily by the transitivity of implication, however the main formula in question is valid in transitive frames, so I shouldn’t need the above lemma.
Note that $\top$ is an abbreviation for $\bot\to\bot$, and $\lnot p$ is an abbreviation for $p\to \bot$. So the formula you want to prove is $((\bot\to\bot)\to(p\to q))\to ((q\to \bot)\to (p\to \bot))$.
The quick summary of the proof is this: Assuming $\top\to (p\to q)$, we will prove $\lnot q\to \lnot p$. Since $\lnot q\to \top$, by our assumption also $\lnot q\to (p\to q)$. Together with $\lnot q\to \lnot q$, we get $\lnot q\to ((p\to q)\land \lnot q)$ by "formalized" $\land$ introduction. By "formalizing" transitivity, $((p\to q)\land \lnot q)\to \lnot p$ (since $\lnot q$ is $q\to\bot$ and $\lnot p$ is $p\to \bot$). So $\lnot q\to \lnot p$, as desired.
Here's the entirely formal version: \begin{align*} 1. &\quad [(\bot\to\bot)\to(p\to q)]&\text{Assumption}\\ 2. &\quad\quad [(q\to \bot)] &\text{Assumption}\\ 3. &\quad\quad\quad [\bot] &\text{Assumption}\\ 4. &\quad\quad\bot\to \bot &\text{$\to$I, 3-3}\\ 5. &\quad(q\to \bot)\to (\bot\to\bot) &\text{$\to$I, 2-4}\\ 6. &\quad(q\to\bot)\to (p\to q) &\text{Tr, 1, 5}\\ 7. &\quad\quad [(q\to \bot)] &\text{Assumption}\\ 8. &\quad(q\to \bot)\to (q\to\bot) &\text{$\to$I, 7-7}\\ 9. &\quad(q\to \bot)\to ((p\to q)\land (q\to \bot)) & \text{$\land$If, 6, 8}\\ 10. &\quad \quad [(p\to q)\land (q\to \bot)] &\text{Assumption}\\ 11. &\quad \quad p\to q &\text{$\land$E, 10}\\ 12. &\quad \quad q\to \bot &\text{$\land$E, 10}\\ 13. &\quad\quad p\to \bot &\text{Tr, 11, 12}\\ 14. &\quad ((p\to q)\land (q\to \bot))\to (p\to \bot)&\text{$\to$I, 10-13}\\ 15. &\quad (q\to \bot)\to (p\to \bot)&\text{Tr, 9, 14}\\ 16. &((\bot\to\bot)\to(p\to q))\to ((q\to \bot)\to (p\to \bot)) &\text{$\to$I, 1-15} \end{align*}
Note that this a proof in BPL, since we didn't use Löb's rule.
Because working without modus ponens is so counterintuitive, I had some trouble finding this proof at first. I eventually looked up this paper, which contains sequent calculi for BPL and FPL. It was easy to find a proof in the sequent calculus for BPL, which I then worked out how to translate back to Visser's original natural deduction system, with some simplifications. This is not the most efficient path to a proof! But I thought it might be useful to know something about how I found the solution. In retrospect, the summary I gave above seems very natural, and feel like I should have seen it more easily.