J 1 J 2 ⋯ J n J name {\displaystyle {\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}}
n ∈ N p n wff atom {\displaystyle {\frac {n\in \mathbb {N} }{{\text{p}}_{n}{\hbox{ wff}}}}\ {\hbox{atom}}}
X wff Y wff ( X ↑ Y ) wff ↑ -wff {\displaystyle {\frac {X{\hbox{ wff}}\qquad Y{\hbox{ wff}}}{(X\uparrow Y){\hbox{ wff}}}}\ \uparrow {\hbox{-wff}}}
