6

I'm trying to reproduce the following in my document:

enter image description here

But I can't find a way of doing it. The closer that I got was with this code:

\documentclass[a4paper, oneside, 10pt]{extarticle}
\usepackage[inference]{semantic}
\begin{document}

\inference{
    \inference{
        \inference{ p \rightarrow p\;\;\;\;p\rightarrow 
p}{p \rightarrow p\;\;\;\;\;(p/p)p \rightarrow p}[(/ $\rightarrow$)]} 
{(p/p)p(p\backslash p) \rightarrow p}[$(\backslash \rightarrow)$]
}
{(p/p)p \rightarrow p/(p\backslash p)}
[($\rightarrow$ /).]

\end{document}

Which had a quite different result:

enter image description here

How can I reproduce correctly the first image?

4
  • 1
    The bussproofs package may provide a better way to achieve this format.
    – Alan Munn
    Jul 2, 2018 at 23:26
  • 1
    See the LaTeX for Logicians site for other options.
    – cfr
    Jul 2, 2018 at 23:42
  • 1
    bussproofs L4L user guide at logicmatters.net/resources/pdfs/latex/BussGuide2.pdf. Extension package at ucalgary.ca/rzach/blog/2014/05/…. Newer alternatives include ebproof and prftree.
    – cfr
    Jul 2, 2018 at 23:45
  • 2
    The LaTeX for Logicians site is the place for logic stuff. Suggestions made on TeX SE are not generally as good as those made there. (TeX SE is good for many TeX things, but not great for logic.)
    – cfr
    Jul 3, 2018 at 0:22

1 Answer 1

6

Here's a method with the prftree package:

\documentclass[border=10pt,varwidth]{standalone}
\usepackage{prftree}
\begin{document}
\begin{displaymath}
  \prftree[r]{$\scriptstyle(/ \rightarrow)$}
  {\prftree[r]{$\scriptstyle(\backslash \rightarrow)$}
    {\prfassumption{p \rightarrow p}} {\prftree[r]{$\scriptstyle(/ \rightarrow)$}{\prfassumption{p \rightarrow p}}{\prfassumption{p \rightarrow p}}{(p/p)p \rightarrow p}}
    {(p/p)p(p \backslash p) \rightarrow p}}
  {(p/p)p \rightarrow p/(p \backslash p)}
\end{displaymath}
\end{document}

<code>prftree</code> solution

5
  • +1 This looks like a great package.
    – Alan Munn
    Jul 3, 2018 at 0:42
  • @AlanMunn Yes, it does. I just found it on the L4L site. I am pretty sure it was not listed before, though maybe I missed it. (I had thought ebproof was the latest package of this kind.) Documentation seems to work pretty well. It would be nice to have a global option to set the font for rules rather than typing \scriptstyle all the time, but that's just detail.
    – cfr
    Jul 3, 2018 at 0:47
  • @AlanMunn I guess the p->p are assumptions rather than axioms. At least, that's usually a theorem in the axiomatic systems I've seen. (But this is not my area.)
    – cfr
    Jul 3, 2018 at 0:50
  • I like your statement "TeX SE is good for many TeX things, but not great for logic." because it can be read in many ways (+1 ;-)
    – user121799
    Jul 3, 2018 at 1:29
  • 1
    Dwedodd @marmot yr union peth ;).
    – cfr
    Jul 3, 2018 at 1:49

You must log in to answer this question.

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