15
$\begingroup$

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?

| |
$\endgroup$
12
$\begingroup$

You can't nest align environments but you can nest arrays (apparently, this requires $$...$$). Why would you bother? Because you can recreate the vertical line. Partial copy of the example of Luiz Martins: $%PREAMBLE \newcommand{\FITCH}[1]{\begin{array}{rlr}#1\end{array}} \newcommand{\FC}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \newcommand{\SC}[1]{\begin{array}{c|l}#1\end{array}} %SecondColumn \newcommand{\TC}[1]{\begin{array}{r}#1\end{array}} %ThirdColumn \newcommand{\SUBPROOF}{\\[-0.27em]} %adjusts line spacing slightly $

$$ \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:

$%PREAMBLE
\newcommand{\FITCH}[1]{\begin{array}{rlr}#1\end{array}}
\newcommand{\FC}[1]{\begin{array}{r}#1\end{array}} %FirstColumn
\newcommand{\SC}[1]{\begin{array}{c|l}#1\end{array}} %SecondColumn
\newcommand{\TC}[1]{\begin{array}{r}#1\end{array}} %ThirdColumn
\newcommand{\SUBPROOF}{\\[-0.27em]} %adjusts line spacing slightly
$

$$
\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}} } $$

| |
$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – user1729 Oct 8 at 13:33
  • $\begingroup$ @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... $\endgroup$ – Calvin Khor Oct 8 at 14:25
  • $\begingroup$ 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. $\endgroup$ – Luiz Martins Oct 8 at 14:54
  • $\begingroup$ @user1729 by George I think I've got it!!!!!!! $\endgroup$ – Calvin Khor Oct 9 at 3:47
  • 1
    $\begingroup$ @LuizMartins I think it works now! $\endgroup$ – Calvin Khor Oct 9 at 3:47
  • 2
    $\begingroup$ Hmm...are em's consistent across browsers and devices? They should be, but I don't trust the internet! This is very nice though :-) $\endgroup$ – user1729 Oct 9 at 9:01
  • $\begingroup$ @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? :) $\endgroup$ – Calvin Khor Oct 9 at 9:04
  • $\begingroup$ @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. $\endgroup$ – user1729 Oct 9 at 9:38
  • $\begingroup$ @CalvinKhor Damm, good job man, that looks really good. $\endgroup$ – Luiz Martins Oct 12 at 20:38
  • 2
    $\begingroup$ @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!) $\endgroup$ – Calvin Khor Oct 13 at 1:36
  • $\begingroup$ 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. $\endgroup$ – g.kov Oct 14 at 18:48
  • 1
    $\begingroup$ @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. $\endgroup$ – Calvin Khor Oct 15 at 2:03
  • $\begingroup$ @g.kov further discussion re titles e.g. here and links therein $\endgroup$ – Calvin Khor Oct 15 at 2:06
23
$\begingroup$

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}

| |
$\endgroup$
  • 2
    $\begingroup$ 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?). $\endgroup$ – LSpice Oct 8 at 0:01
  • 1
    $\begingroup$ P.S. Your username is fantastic. $\endgroup$ – LSpice Oct 8 at 0:02
19
$\begingroup$

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 rearrange it like:
\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}
and get the 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} $$

| |
$\endgroup$
  • 1
    $\begingroup$ (+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. $\endgroup$ – Dave L. Renfro Oct 6 at 16:35
  • $\begingroup$ @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) $\endgroup$ – Luiz Martins Oct 6 at 17:13
  • 1
    $\begingroup$ 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. $\endgroup$ – LSpice Oct 8 at 0:02
  • 1
    $\begingroup$ @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}. $\endgroup$ – Luiz Martins Oct 8 at 0:25
3
$\begingroup$

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.

| |
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .