Do you have the deduction theorem available? Even if you don’t, you’ll want to try to derive $\neg \neg P \vdash P$. Then, you’ll use the substitution instance $\neg P/P$ and the third axiom to get $P \to \neg \neg P$. Assuming you can prove $\neg \neg P \to (\neg P \to Q)$ using axioms 1 and 3, the proof becomes pretty clear. I suspect that an actual formal proof even without using substitution as an inference rule would be well over 50 lines.

@PW_246 Until now, I guess the deduction theorem wasn't mentioned in the book.

Another possible approach: using the first two axioms, it should be possible to prove that $(B \rightarrow (A \rightarrow C)) \rightarrow (A \rightarrow (B \rightarrow C))$. So, using modus ponens and an instance of this topology, it suffices to prove $\lnot A \rightarrow (A \rightarrow B)$. But then, you also have that $(\lnot B \rightarrow \lnot A) \rightarrow (A \rightarrow B)$ and also $\lnot A \rightarrow (\lnot B \rightarrow \lnot A)$. So, you can then use an instance of the tautology $(A\rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$...

which can also be proved using the first two axioms.

Hmm, using some SK combinator calculus type language for Hilbert proofs, and the corresponding abstraction procedure (along with some peephole optimizations along the way), I came up with a proof involving about 15 steps (though as usual, the intermediate steps are absolutely horrible looking).

i.stack.imgur.com/uezxw.png for a screenshot of the web tool I used to check it -- in case anybody might want to take that and type out the corresponding linear proof.

@DanielSchepler I'm curious: How do we deal with logical expressions in terms of topology? What are the open sets and the closed sets?

@DanielSchepler Oh, I once saw this book in a library but never had the time to look at it. I thought you knew something in that direction.

@DanielSchepler What substitution is happening here?

@RedBanana That is Axiom 1 with ~A being substituted for B, and the antecedent for A. What program is that? The Incredible Proof Machine?

@RedBanana I'm not that familiar with that book; but it sounds like it might be along the lines of: there are applications of topology to proof theory and model theory. For example, you can put a topology on the set of models of some first-order language, where each basic open set is the subset of models satisfying some finite set of axioms. The compactness theorem in model theory is then closely related to the compactness of this topological space.

Also, the mention of "logic of finite observations" is reminiscent of a certain topological point of view of the method of forcing, or of the philosophy of constructing Kripke models of modal logic or of intuitionistic logic.

@Bram28 What program? I made a silly code to make substitutions in Mathematica (which is shown in the question), Schepler uses this Incredible Proof Machine which sounds pretty interesting but I'm not sure what it actually is, I just know that it's possible to handle some kinds of proofs in it.

@DanielSchepler I did it in my program looking at the proof you showed me. Thanks!

The Incredible Proof Machine is at incredible.pm . It just provides a way to lay out proof trees of different proof systems pictorially. (It also has a mode for natural deduction style proofs.) The feature I made heavy use of is: as you lay out the nodes and start wiring them together, it can infer the necessary intermediate steps to make that layout work (or signal an error where the layout is impossible to satisfy by turning some arrows red).

That combined nicely with the fact that the SK-combinator expression calculation told me what the form of the proof would be, but left out the details of what the intermediate steps were.

(Incidentally, the Incredible Proof Machine's reference solution to proving $(A\rightarrow B) \rightarrow ((\lnot A\rightarrow B) \rightarrow B)$ appears to be about 81 steps!)