3

I have the following proof tree, which latex says is badly specified.

Here is the TeX.

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{prooftree}
\AxiomC{$Sz + t = 0 \dagger$} \AxiomC{$t = 0 \dagger$}
\BinaryInfC{$Sz + 0 = 0$}                                   \AxiomC{$Sz + 0 = Sz$}
                                \BinaryInfC{$Sz = 0$}                                   \AxiomC{$\neg (Sz = 0)$}
                                                        \BinaryInfC{$\bot$}
                                                        \UnaryInfC{$\neg(Sz + t) = 0$}





\AxiomC{$\neg(t = 0)$}
\UnaryInfC{$\exists w (t = Sw)$}    
                                                \AxiomC{$t = Sy \dagger$}   \AxiomC{$Sz + t = 0 \dagger$}
                                                        \BinaryInfC{$S(z + y) = 0$}                     \AxiomC{$\neg(S(z + y) = 0$}
                                                                                    \BinaryInfC{$\bot$}
                                                                                    \UnaryInfC{$\neg(Sz + t = 0)$}


\BinaryInfC{$\neg(Sz + t) = 0$}
\end{prooftree}
\end{document}

There are two proof trees, with conclusions $\neg(Sz + t = 0)$ (both of them), and I want to join those together to conclude $\neg(Sz + t = 0)$. I tested it a bit, and it seems the mistake is in the second tree (If I remove the second tree and conclusion it works), but I can't find it.

Improve this question
6
  • Can you please make your code fragment compilable? And the image of the source isn't really needed.
    – Alan Munn
    Nov 9, 2019 at 16:38
  • @AlanMunn what does fragment compilable mean?
    – user388557
    Nov 9, 2019 at 16:39
  • You have posted a fragment of code, i.e., a small piece of code that cannot by itself be compiled. Instead of doing that, put the code you posted inside a \documentclass{article}\usepackage{bussproofs}\begin{document} ... \end{document}. This way people can just copy the code to play with it. It also loads the correct package for the prooftree environment.
    – Alan Munn
    Nov 9, 2019 at 16:44
  • I'm not quite sure what you want the output to look like, but if you put \DisplayProof after the first tree then the code works. Is that what you are looking for?
    – Alan Munn
    Nov 9, 2019 at 16:45
  • @AlanMunn almost, but not quite. This gives two proof trees under each other, I want to combine those proof trees into a new one with conclusion $\neg(Sz + t = 0)$
    – user388557
    Nov 9, 2019 at 16:48

1 Answer 1

Reset to default
4

The basic problem is that you have two active branches in the second subtree when you give \UnaryInfC as the last line, which won't work because you then have three active branches when you issue \BinaryInfC on the last line of all.

The code can be made to compile in various ways, but it isn't possible to know which is correct without knowing more about the semantics and syntax of the language being used.

Here's one way, just as an illustration.

\documentclass{article}
\usepackage{bussproofs,geometry}
\usepackage{amsmath}
\begin{document}
\begin{prooftree}
  \AxiomC{$Sz + t = 0 \dagger$} \AxiomC{$t = 0 \dagger$}
  \BinaryInfC{$Sz + 0 = 0$}                                   \AxiomC{$Sz + 0 = Sz$}
  \BinaryInfC{$Sz = 0$}                                   \AxiomC{$\neg (Sz = 0)$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\neg(Sz + t) = 0$}

  \AxiomC{$\neg(t = 0) \dagger$}
  \UnaryInfC{$\exists w (t = Sw)$}    
  \UnaryInfC{$t = Sy$}   
  \AxiomC{$Sz + t = 0 \dagger$}
  \BinaryInfC{$S(z + y) = 0$}                     
  \AxiomC{$\neg(S(z + y) = 0$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\neg(Sz + t = 0)$}

  \BinaryInfC{$\neg(Sz + t) = 0$}
\end{prooftree}
\end{document}

One possibly intended result

Improve this answer
1
  • That was exactly what I wanted, thank you.
    – user388557
    Nov 10, 2019 at 13:16

You must log in to answer this question.

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