Defining the linearization operator L.

There is a map L recovering the usual form of a formula. We call  Lin[A] the linear form of A, and L a linearization operator.

We define the linear form Lin[A] of A by recursion over A. We distinguish one case for each operator defining A. If implication is material implication, then Impl[A,B] is A→B, while if implication is constructive implication, then  Impl[A,B] is A⇒B.

In[20]:=

Created by Mathematica  (October 17, 2006)