In usual terminology, is there a difference between the type and similarity type? Is there a general consensus for the definition of the two terms?
Please suggest to me books where I can study these themes. I have to solve problems in which I need to say if a given affirmation is demonstrable or not, and if it is, then demonstrate that. On the other hand, I need to give the necessary similarity type to traduce a formula into first order language. I need to say if a given formula is or not universally valid. Can you recommend to me some references for approaching this particular problem?
In usual terminology, we talk of a type similarity type as a synonym for signature. Recall that given a signature $\Sigma$ we can build a language $L(\Sigma)$ which alphabet usually consists of the predicate (if any), function (if any) and constant symbols (if any) of $\Sigma$ added by the logical symbols and auxiliary symbols of $L$. For a reasonable explanation, see van Dalen Logic and Structure (pp.58-62).