View source for Implicative normal form

{{TEX|done}}
A [[Propositional form|propositional form]] of the type

$$C_1\supset(C_2\supset\dotsb(C_n\supset\bot)\cdots),$$

where all the $C_i$, $i=1,\dotsc,n$, have the form

$$C_{i1}\supset(C_{i2}\supset\dotsb(C_{im_i}\supset\bot)\cdots).$$

Here, each $C_{ij}$ ($i=1,\dotsc,m$; $j=1,\dotsc,m_i$) is either a variable or the negation of a variable, and $\bot$ is the logical symbol denoting falsehood. For each propositional formula $A$ one can construct an implicative normal form $B$ classically equivalent to it and containing the same variables as $A$. Such a $B$ is called an implicative normal form of $A$.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR></table>