如何绘制“标志格式” lambda 推导图，如类型理论和形式证明：导论一书中所用

Question

我想绘制“标志格式”的 lambda 派生图，就像《类型理论和形式证明：导论》一书中使用的那样。下面是本书第 2 章中的一个示例。我该怎么做？谢谢。

Answer 1

至于所有合乎逻辑的事情，检查逻辑学家的 LaTeX站点，查找你需要的东西并查阅文档。

由于您没有提供任何代码，我从中复制了一个例子flagderiv文档的第 3 页。

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,flagderiv}


\begin{document}

\begin{flagderiv}
  \introduce{in-x}{x: \mathbb{N}}{Introduction of $x$}
  \assume{as-x}{x > 5}{Assumption}
  \step{big-x}{x > 1}{Arithmetic on \ref{in-x} and \ref{as-x}}
  \conclude{conc}{x > 5 \implies x > 1}{$\implies$-intro on \ref{as-x} and \ref{big-x}}
  \conclude{}{\forall x \in \mathbb{N}: x > 5 \implies x > 1}{$\forall$-intro on \ref{in-x} and \ref{conc}}
\end{flagderiv}

\end{document}