Parsing a nested inference rule syntax

Question

Consider this expression.

$$\dfrac{\dfrac{\dfrac{\dfrac{}{\textsf{zero nat}}}{\textsf{succ(zero) nat}}}{\textsf{succ(succ(zero)) nat}}}{\textsf{succ(succ(succ(zero))) nat}}$$

I see several applications of an infix operator $\frac{\blacksquare}{\blacksquare}$. What are its syntactic properties: how tightly does it bind and how does it associate?

Does this read

a is always true. If a is true then b is true. If "if a is true then b is true" then c is true. If "If 'if a is true then b is true' then c is true" is true then d is true.

so that the third bar from the top includes both bars above it,

or is it something else? How can I write this with parentheses in normal non-latex characters?

Answer 1

$$\dfrac{\dfrac{\dfrac{\dfrac{}{\textsf{zero nat}}}{\textsf{succ(zero) nat}}}{\textsf{succ(succ(zero)) nat}}}{\textsf{succ(succ(succ(zero))) nat}}$$

I see several applications of an infix operator $\tfrac{~\blacksquare~}{\blacksquare}$. What are its syntactic properties: how tightly does it bind and how does it associate?

In a Gentzen-style proof tree, $\tfrac{~A~}{B}$ indicates that statement $B$ can be derived from statement $A$.   Further $\tfrac{~A~~B~}{C}$ indicates that statement $C$ can be derived from statements $A$ and $B$, an so on.   Also $\overline{~B~}$ indicates that $B$ is a theorem.

They associate transitively. $\tfrac{~\tfrac {A}{B}~}{~C~}$ indicates that $C$ can be derived from $B$, and $B$ can be derived from $A$; which means we have a proof that $C$ can be derived from $A$.

Thus your tree appears to read:

• zero is a natural, therefore the zero's successor is a natural, therefore zero's successor's successor is a natural, therefore zero's successor's successor's successor is a natural.
• Or: zero's successor's successor's successor is a natural, by the theorem that zero is a natural, and the (unstated) rule that the successor of any natural is a natural.