Translating between Huth/Ryan box and Fitch notations

Question

I have come across proofs using a notation with boxes (Logic in Computer Science by Huth and Ryan), where each assumption is inside its own box:

I would now like to write these proofs using Fitch notation, but I am unable to understand how to do that. I have given it a try (see below), but I am not sure this is correct.

I have looked around quite a lot for a "Fitch notation for dummies" but my knowledge within the field of logical proofs is sparse and I have yet to find anything helpful.

I would greatly appreciate any help in the matter of translating "boxes to Fitch".

Answer 1

Your answer is correct. Actually it is easier just to use your own logical reasoning to write a proof directly in Fitch-style notation. The fundamental requirement is that every syntactic structure involving a $\huge\vdash$ is specifying a subcontext, where what is on top specifies the subcontext, and what is below is what you derive within that subcontext. So for propositional logic every 'assumption' corresponds to creating a new subcontext in which the assumption is true. And you can see easily why the rules of natural deduction are sound, because for example the [$\to$ intro] and [$\to$ elim] rules together capture the meaning of implication because they make it so that, within any context, we have "$A \to B$" is derivable iff "$\begin{array}{|l}A \\\hline B\end{array}$" is derivable.

Unfortunately I couldn't find any precise description of a sound Fitch-style calculus including rules for quantifiers. The headache is usually in specifying what variables are allowed to be used where, to prevent conflicts. So the best I can offer you is my own set of rules (which implement free logic that is the same as conventional first-order logic except that it does not intrinsically forbid an empty domain).

Answer 2

Here is an example of Fitch notation I know, perhaps it is what you meant:

But personally I think it is irrelevant which of these notations (Fitch, yours, or Huth and Ryan) you use. They all seem nice and clear to me (they are basically the same). In particular, the translation you propose seems perfectly fine to me.