Consequence and complexity in infinite-valued logic: a survey

In general, every logic L comes equipped with a syntax, consisting of a finite set A of symbols, called the alphabet, and an inductive definition of which strings over A are to be called formulae of L; a semantics, telling the meaning of each formula, whence in particular, telling when two formulae are equivalent; an algorithmic procedure whereby, given a finite set F of formula, one can in principle obtain all consequences of F. In certain fortunate cases-e.g., in classical logic formulae up to equivalence form an interesting class of algebraic structures. The infinite-valued calculus of Lukasiewicz is such a fortunate case. Our aim in this paper is to review semantic-algorithmic issues for this logic, with particular reference to recent research.