3

I'd like to draw "flag format" diagrams for lambda derivation as used in the book "Type Theory and Formal Proof: An Introduction". Below is an example in Chapter 2 of the book. How can I do it? Thanks.

Flag format

  • Welcome! Look at the LaTeX for Logicians website. logicmatters.net/latex-for-logicians/nd : see final comment, 'The flagderiv package can be used to set the variant kind of “flag” proofs some computer scientists like.' If you need further help, please add a minimal working example (MWE). – cfr Oct 20 '19 at 1:27
  • Thanks! This is exactly what I want. – markeric Oct 20 '19 at 20:07
  • The website I linked is really good for this stuff. If it isn't there, the chances are it isn't available or it isn't logical ;). – cfr Oct 20 '19 at 20:37
8

As for all things logical, check the LaTeX for Logicians site, find the thing you need and look up the documentation.

Since you've not given any code, I copied an example from page 3 of flagderiv's documentation.

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

flagged derivation

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.