# How to properly align a fitch style proof on Math Exchange?

Is it possible to align a fitch style proof? When I say align, I mean instead of:

$$1: \forall x [P(x)] \rightarrow Q \quad \text{Premise} \\ 2: | \lnot \exists x[P(x) \rightarrow Q] \quad \text{Supposition} \\ 3: |\forall x[ \lnot (P(x) \rightarrow Q)] \quad \text{From 2} \\ 4: |\forall x[ \lnot (\lnot P(x) \land Q)] \\ 5: |\forall x[P(x) \land \lnot Q)] \\ 6: |\forall x[P(x)] \quad \text{From 5} \\ 7: | \lnot Q \quad \text{From 5} \\ 8: |\lnot Q \rightarrow \lnot \forall x [P(x)] \quad \text{From 1} \\ 9: |\lnot \forall x[P(x)] \quad \text{From 7, 8} \\ 10: |\forall x[P(x)] \quad \text{Copy of 6} \\ 11: \exists x[P(x) \rightarrow Q] \quad \text{From contradiction 9, 10}$$

Where the lines are completely centered, we could have only the numbers aligned with each other on the left, then the arguments aligned with each other on the center, and same for the last part on the right.

Is it possible to do that? If yes, how?


$$\FITCH{ \FC{1:} & \forall x[P(x)] \rightarrow Q & \TC{\text{Premise} } \SUBPROOF \FC{ 2:\\ 3:\\ 4:\\ 5:\\ \vdots\ \ \\ 10: } & \SC{ &\lnot \exists x[P(x) \rightarrow Q]\\ &\forall x[ \lnot (P(x) \rightarrow Q)]\\ &\forall x[ \lnot (\lnot P(x) \land Q)]\\ &\forall x[P(x) \land \lnot Q)]\\ &\quad\vdots \\ &\forall x[P(x)]\\ } & \TC{ \text{Supposition}\\ \text{From 2}\\ \\ \\ \vdots\quad\\ \text{Copy of 6} } \SUBPROOF \FC{11:} & \exists x[P(x) \rightarrow Q] & \TC{\text{Contradiction 9, 10}} }$$

and the code:


$$\FITCH{ \FC{1:} & \forall x[P(x)] \rightarrow Q & \TC{\text{Premise} } \SUBPROOF \FC{ 2:\\ 3:\\ 4:\\ 5:\\ \vdots\ \ \\ 10: } & \SC{ &\lnot \exists x[P(x) \rightarrow Q]\\ &\forall x[ \lnot (P(x) \rightarrow Q)]\\ &\forall x[ \lnot (\lnot P(x) \land Q)]\\ &\forall x[P(x) \land \lnot Q)]\\ &\quad\vdots \\ &\forall x[P(x)]\\ } & \TC{ \text{Supposition}\\ \text{From 2}\\ \\ \\ \vdots\quad\\ \text{Copy of 6} } \SUBPROOF \FC{11:} & \exists x[P(x) \rightarrow Q] & \TC{\text{Contradiction 9, 10}} }$$


further nesting is possible (but the line spacing might become slightly odd if you zoom in a lot): $$\FITCH{ \FC{1:} & xyz1 & \TC{\text{abc1}} \SUBPROOF \FC{ 2:\\ 3:\\ 4:\\ 5:\\ 6: } & \SC{ &xyz2 \SUBPROOF &\SC{ &xyz3 \SUBPROOF &\SC{ &xyz4\\ &xyz5 } \SUBPROOF } \SUBPROOF &xyz6 } & \TC{ \text{abc2}\\ \text{abc3}\\ \text{abc4}\\ \text{abc5}\\ \text{abc6} } \SUBPROOF \FC{7:} & xyz7 & \TC{\text{abc7}} \SUBPROOF \FC{ 8:\\ 9:\\ 10: } & \SC{ &xyz8 \SUBPROOF &\SC{ &xyz9 } \SUBPROOF &xyz10 } & \TC{ \text{abc8}\\ \text{abc9}\\ \text{abc10} } \SUBPROOF \FC{11:} & xyz11 & \TC{\text{abc11}} }$$

• oooh, nice! I honestly hadn't realised the $|$ were meant to be a continuous vertical line. However, the colons on the LHS don't line up, and I cannot get them to line up using this idea. (Changing the l's for this column to r's kind of works, but is not perfect. Changing the first l to a c, the 1: to \:\:\:1:, and the second l to an r looks best, but is too hack-ey for my liking - it probably looks awful on other peoples computers.) Oct 8 '20 at 13:33
• @user1729 thanks :) I agree it’s not perfect, on my computer the numbers don’t even align on the left. I will think if there’s a better way for the numbers... Oct 8 '20 at 14:25
• It's very unfortunate that there's this blank space around the arrays, so they don't align correctly. Otherwise, this would be the perfect way to write this kind of proof. Oct 8 '20 at 14:54
• @user1729 by George I think I've got it!!!!!!! Oct 9 '20 at 3:47
• @LuizMartins I think it works now! Oct 9 '20 at 3:47
• Hmm...are em's consistent across browsers and devices? They should be, but I don't trust the internet! This is very nice though :-) Oct 9 '20 at 9:01
• @user1729 probably not. I did test in all math renderers I can use, and they aren't that far off (but since nesting them shows errors, they probably aren't precisely right. Or I'm double counting something, or...) At least, \em should vary somewhat appropriately with the font used? :) Oct 9 '20 at 9:04
• @CalvinKhor As I understand it, \em is linked to the typeface/font. So as long as this hack is only used on Math.SE it should be fine, as the font here is fixed (I think the mobile version uses different fonts in certain places, but not for maths mode). But I'm really just guessing :-) Anyway, to use elsewhere it is only that one line which needs fixed, which is manageable. Oct 9 '20 at 9:38
• @CalvinKhor Damm, good job man, that looks really good. Oct 12 '20 at 20:38
• @LuizMartins thanks! Unfortunately I have no idea what a Fitch style proof is :) But horizontal lines can of course be added like user21820's answer (which is much simpler and easier to use if you don't mind not having numbers and aligning the right column!) Oct 13 '20 at 1:36
• It was strongly recommended to always prefix macro definitions and usage with: \$\require{begingroup} \begingroup\$ and end them with: \$\endgroup\$ to keep the definitions from leaking into other posts. Oct 14 '20 at 18:48
• @g.kov it was strongly recommended but this was fixed in 2019 by automatically enclosing posts in $\begingroup$...$\endgroup$ (same page you linked, newer answer, which by the way is why everything on that page looks fine; it didn't before!) What is currently not OK is \def etc. in titles, but since we already discourage multiline titles, no one should have one of these in their titles. Oct 15 '20 at 2:03
• @g.kov further discussion re titles e.g. here and links therein Oct 15 '20 at 2:06
• @CalvinKhor I've just made a further improvement! I've made it look more fitch-like and further adjusted the spacing, so now it looks exactly as I wished when I first made this question. Thanks a lot for that! I've updated my answer with the result. Oct 28 '20 at 3:27

Another option is to use the align environment \begin{align*}...\end{align*}, rather than the array environment. This environment has more flexibility with spacing, which is useful if you don't want your output to look like a table (although this doesn't seem relevant to your example). The align environment gives an essentially identical output to array here:

\begin{align*} 1:& &&\forall x [P(x)] \rightarrow Q &\text{Premise}\\ 2:& &&| \lnot \exists x[P(x) \rightarrow Q] &\text{Supposition}\\ 3:& &&|\forall x[ \lnot (P(x) \rightarrow Q)] &\text{From 2} \\ 4:& &&|\forall x[ \lnot (\lnot P(x) \land Q)] \\ 5:& &&|\forall x[P(x) \land \lnot Q)] \\ 6:& &&|\forall x[P(x)] &\text{From 5} \\ 7:& &&| \lnot Q &\text{From 5} \\ 8:& &&|\lnot Q \rightarrow \lnot \forall x [P(x)] &\text{From 1} \\ 9:& &&|\lnot \forall x[P(x)] &\text{From 7, 8} \\ 10:& &&|\forall x[P(x)] &\text{Copy of 6} \\ 11:& &&\exists x[P(x) \rightarrow Q] &\text{From contradiction 9, 10} \end{align*}


\begin{align*} 1:& &&\forall x [P(x)] \rightarrow Q &\text{Premise}\\ 2:& &&| \lnot \exists x[P(x) \rightarrow Q] &\text{Supposition}\\ 3:& &&|\forall x[ \lnot (P(x) \rightarrow Q)] &\text{From 2} \\ 4:& &&|\forall x[ \lnot (\lnot P(x) \land Q)] \\ 5:& &&|\forall x[P(x) \land \lnot Q)] \\ 6:& &&|\forall x[P(x)] &\text{From 5} \\ 7:& &&| \lnot Q &\text{From 5} \\ 8:& &&|\lnot Q \rightarrow \lnot \forall x [P(x)] &\text{From 1} \\ 9:& &&|\lnot \forall x[P(x)] &\text{From 7, 8} \\ 10:& &&|\forall x[P(x)] &\text{Copy of 6} \\ 11:& &&\exists x[P(x) \rightarrow Q] &\text{From contradiction 9, 10} \end{align*}

Here, individual lines look like:

1:& &&\forall x [P(x)] \rightarrow Q &\text{Premise}\\

The first a third & are a markers for alignment, the other two break up these markers. For example:

\begin{align*} a&=b& x&=y\\ &=c& &=z \end{align*}


gives \begin{align*}a&=b&x&=y\\&=c&&=z\end{align*}

If we use the array environment, you can see what I mean by the align environment having more flexible spacing, as the a and the =b are separated in an ugly way:

$$\begin{array}{rlrl} a&=b & x&=y\\ &=c & &=z \end{array}$$


gives $$\begin{array}{rlrl}a&=b&x&=y\\&=c&&=z\end{array}$$

• This is also semantically better, since it correctly indicates that you are trying to align the lines of an equation, whereas the {array} environment doesn't know that the cell entries are parts of equations (hence the weird spacing—which can be circumvented, but why not just go with the semantic flow?). Oct 8 '20 at 0:01


Edit: Ever since I've postes this answer, more elaborate (and refined) answers came along using preambles. I've particularly likes Calvin's approach, so I've further the spacing and made the argument look more fitch-like. These are the commands:



And this is an example:

$$\fitch{ \fcol{\fendl 1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22: } & \scol { \startsub\subcol{ f \text{ is a relation } \\ \langle x,y \rangle \in f \\ \hline \forall v[v \in f \rightarrow \exists a \exists b[v = \langle a,b \rangle]] \\ \langle x,y \rangle \in f \rightarrow \exists a \exists b[\langle x,y \rangle = \langle a,b \rangle] \\ \exists a \exists b[\langle x,y \rangle = \langle a,b \rangle] \\ \langle x,y \rangle = \langle a_\alpha,b_\alpha \rangle \\ \langle a_\alpha,b_\alpha \rangle \in f \\ x=a_\alpha \land y=b_\alpha \\ \langle y,x \rangle = \langle y,x \rangle \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \land \langle a_\alpha,b_\alpha \rangle \in f \\ \exists b \exists a [\langle y,x \rangle = \langle b,a \rangle \land \langle a,b \rangle \in f] \\ \langle y,x \rangle \in f^c } \endsub f \text{ is a relation } \land \langle x,y \rangle \in f \rightarrow \langle y,x \rangle \in f^c \startsub \subcol{ \langle y,x \rangle \in f^c \\ \hline f \text{ is a relation } \\ \exists a \exists b [\langle y,x \rangle = \langle b,a \rangle \land \langle a,b \rangle \in f] \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \land \langle a_\alpha,b_\alpha \rangle \in f \\ y = b_\alpha \land x = a_\alpha \\ \langle x,y \rangle \in f } \endsub \langle y,x \rangle \in f^c \rightarrow f \text{ is a relation } \land \langle x,y \rangle \in f \\ f \text{ is a relation } \land \langle x,y \rangle \in f \leftrightarrow \langle y,x \rangle \in f^c \\ } & \tcol{ \fendl f\ \text{P} \fendl x,y\ \text{P} \fendl 1, [1]\ \text{T} \fendl 3\ \text{UG}[v/\langle x,y \rangle] \fendl 2,4\ \text{T} \fendl 5\ \text{ES} \fendl 2,6\ \text{S} \fendl 6\ \text{T} \fendl \text{T} \fendl 8,9\ \text{S} \fendl 7,10\ \text{T} \fendl 11\ \text{EG} \fendl 1,12,[2]\ \text{T} \fendl 1,2,13\ \text{CP} \fendl x,y\ \text{P} \fendl 15,[2]\ \text{T} \fendl 15,[2]\ \text{T} \fendl 17\ \text{ES} \fendl 18\ \text{T} \fendl 18,19\ \text{S} \fendl 15,16,20\ \text{CP} \fendl 14,21\ \text{T} \fendl } }$$

Built with the following code:

$$\fitch{ \fcol{\fendl 1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22: } & \scol { \startsub\subcol{ f \text{ is a relation } \\ \langle x,y \rangle \in f \\ \hline \forall v[v \in f \rightarrow \exists a \exists b[v = \langle a,b \rangle]] \\ \langle x,y \rangle \in f \rightarrow \exists a \exists b[\langle x,y \rangle = \langle a,b \rangle] \\ \exists a \exists b[\langle x,y \rangle = \langle a,b \rangle] \\ \langle x,y \rangle = \langle a_\alpha,b_\alpha \rangle \\ \langle a_\alpha,b_\alpha \rangle \in f \\ x=a_\alpha \land y=b_\alpha \\ \langle y,x \rangle = \langle y,x \rangle \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \land \langle a_\alpha,b_\alpha \rangle \in f \\ \exists b \exists a [\langle y,x \rangle = \langle b,a \rangle \land \langle a,b \rangle \in f] \\ \langle y,x \rangle \in f^c } \endsub f \text{ is a relation } \land \langle x,y \rangle \in f \rightarrow \langle y,x \rangle \in f^c \startsub \subcol{ \langle y,x \rangle \in f^c \\ \hline f \text{ is a relation } \\ \exists a \exists b [\langle y,x \rangle = \langle b,a \rangle \land \langle a,b \rangle \in f] \\ \langle y,x \rangle = \langle b_\alpha,a_\alpha \rangle \land \langle a_\alpha,b_\alpha \rangle \in f \\ y = b_\alpha \land x = a_\alpha \\ \langle x,y \rangle \in f } \endsub \langle y,x \rangle \in f^c \rightarrow f \text{ is a relation } \land \langle x,y \rangle \in f \\ f \text{ is a relation } \land \langle x,y \rangle \in f \leftrightarrow \langle y,x \rangle \in f^c \\ } & \tcol{ \fendl f\ \text{P} \fendl x,y\ \text{P} \fendl 1, [1]\ \text{T} \fendl 3\ \text{UG}[v/\langle x,y \rangle] \fendl 2,4\ \text{T} \fendl 5\ \text{ES} \fendl 2,6\ \text{S} \fendl 6\ \text{T} \fendl \text{T} \fendl 8,9\ \text{S} \fendl 7,10\ \text{T} \fendl 11\ \text{EG} \fendl 1,12,[2]\ \text{T} \fendl 1,2,13\ \text{CP} \fendl x,y\ \text{P} \fendl 15,[2]\ \text{T} \fendl 15,[2]\ \text{T} \fendl 17\ \text{ES} \fendl 18\ \text{T} \fendl 18,19\ \text{S} \fendl 15,16,20\ \text{CP} \fendl 14,21\ \text{T} \fendl } }$$


Further nesting is also possible:

$$\fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } \scol{ \forall y \lnot P(y) \startsub\subcol{ \exists P(x) \startsub\hline\subcol{ P(u) \\ \hline \forall y \lnot P(y) \\ \lnot P(u) \\ \perp } \endsub \perp } \endsub \lnot \exists x P(x) } \tcol{ P \fendl P \fendl P \fendl R,1 \fendl \forall E,4 \fendl \lnot E,4,5 \fendl \exists E, 2 ,3-6 \fendl \lnot I,2-7 \fendl } } \quad \text{or} \quad \fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } \subcol{ \forall y \lnot P(y) \startsub\hline\subcol{ \exists P(x) \startsub\hline\subcol{ P(u) \\ \hline \forall y \lnot P(y) \\ \lnot P(u) \\ \perp } \endsub \perp }\endsub \lnot \exists x P(x) } \tcol{ P \fendl P \fendl P \fendl R,1 \fendl \forall E,4 \fendl \lnot E,4,5 \fendl \exists E, 2 ,3-6 \fendl \lnot I,2-7 \fendl } }$$

Like so:

$$\fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } \scol{ \forall y \lnot P(y) \startsub\subcol{ \exists P(x) \startsub\hline\subcol{ P(u) \\ \hline \forall y \lnot P(y) \\ \lnot P(u) \\ \perp } \endsub \perp } \endsub \lnot \exists x P(x) } \tcol{ P \fendl P \fendl P \fendl R,1 \fendl \forall E,4 \fendl \lnot E,4,5 \fendl \exists E, 2 ,3-6 \fendl \lnot I,2-7 \fendl } }$$

$$\fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } \subcol{ \forall y \lnot P(y) \startsub\hline\subcol{ \exists P(x) \startsub\hline\subcol{ P(u) \\ \hline \forall y \lnot P(y) \\ \lnot P(u) \\ \perp } \endsub \perp }\endsub \lnot \exists x P(x) } \tcol{ P \fendl P \fendl P \fendl R,1 \fendl \forall E,4 \fendl \lnot E,4,5 \fendl \exists E, 2 ,3-6 \fendl \lnot I,2-7 \fendl } }$$


Yes it is. You can do it with MathJax's {array}.

If you write \begin{array}{} aaaa \\ bb \\ cccccc \\ \end{array}, you'll get: $$\begin{array}{} aaaa \\ bb \\ cccccc \\ \end{array}$$

Notice that it's left justified. If you however add an 'r' inside the empty brackets, as in \begin{array}{r} aaaa \\ bb \\ cccccc \\ \end{array}, you'll get: $$\begin{array}{r} aaaa \\ bb \\ cccccc \\ \end{array}$$

Which is right justified. However, you can add more than one. If you use more than one tag, you can separate the alignments on each line with an &. If you type \begin{array}{lr} aaaa & dddd \\ bb & ee \\ cccccc & ffffff \\ \end{array}, you'll get: $$\begin{array}{lr} aaaa & dddd \\ bb & ee \\ cccccc & ffffff \\ \end{array}$$

And of course, you can add as many as you want. \begin{array}{lrlr} aaaa & dddd & 1111 & >>>> \\ bb & ee & 22 & << \\ cccccc & ffffff & 333333 & ====== \\ \end{array} gives:

$$\begin{array}{lrlr} aaaa & dddd & 1111 & >>>> \\ bb & ee & 22 & << \\ cccccc & ffffff & 333333 & ====== \\ \end{array}$$

So, in the case of your example, you can use {array} to get this result:

$$\begin{array}{llr} 1: & \forall x [P(x)] \rightarrow Q & \text{Premise} \\ 2: & \quad | \lnot \exists x[P(x) \rightarrow Q] & \text{Supposition} \\ 3: & \quad |\forall x[ \lnot (P(x) \rightarrow Q)] & \text{From 2} \\ 4: & \quad |\forall x[ \lnot (\lnot P(x) \land Q)] \\ 5: & \quad |\forall x[P(x) \land \lnot Q)] \\ 6: & \quad |\forall x[P(x)] & \text{From 5} \\ 7: & \quad | \lnot Q & \text{From 5} \\ 8: & \quad |\lnot Q \rightarrow \lnot \forall x [P(x)] & \text{From 1} \\ 9: & \quad |\lnot \forall x[P(x)] & \text{From 7, 8} \\ 10: & \quad |\forall x[P(x)] & \text{Copy of 6} \\ 11: & \exists x[P(x) \rightarrow Q] & \text{Contradiction 9, 10} \end{array}$$

• (+1) I've since learned how to form arrays (by clicking "edit" on some answers that appeared formatted as such), but this really would have been useful when I wrote this answer. By clicking "edit", you see that I used spaces \; to get the alignements, but I only did two columns at a time. Oct 6 '20 at 16:35
• @DaveL.Renfro Yeah, i've found how to do it in the same way, and found very weird that nobody had asked this here before, so I created a Q&A. I've seen one guy use an actual finch library to create an absurdly clean looking finch-style argument in a comment. Didn't knew about the edit trick at the time though, and never found the comment again. However, Gonna 100% update this answer if I ever find it (and also encourage anyone that knows how to do it to post an answer as well) Oct 6 '20 at 17:13
• You use 'finch' above, but 'fitch' in the title and question body. \\ Please don't use {array} for equation alignment; that is not its semantic purpose. Please use {align} instead, as recommended by the awesomely named @user1729. Oct 8 '20 at 0:02
• @LSpice I meant fitch, thanks for the correction. Although I can see the appeal in some situations, since you can align in pairs, I don't see is as much different, since you can only align in pairs. So if you have two left alignments, it's still gonna end up looking like a table. Also, since the alignments are clear on the aguments, I find arrays a bit more readable in writing. Tbh though, any of the two works fine in this case. In the case of an equation, as showed in the answer bellow, yeah, you really should go for {align}. Oct 8 '20 at 0:25

If you want real Fitch-style, you could use:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$ $$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$$

This can be nested:

$$\fitch{¬B ∧ (A⇒B)}{ A⇒B \\ ¬B\\ \fitch{A}{ B \\ ¬B \\ ⊥ \\ } \\ ¬A }$$


Output is beautiful!

$$\fitch{¬B ∧ (A⇒B)}{ A⇒B \\ ¬B\\ \fitch{A}{ B \\ ¬B \\ ⊥ \\ } \\ ¬A }$$

See here for an example post where I used this.