The syntax of Linear logic
Cheong Kye-Seop · Journal for History of Mathematics · 2012
As a product of modern proof theory, linear logic is a new form of logic developed for the purpose of enhancing programming language by Professor Jean-Yves Girard of Marseille University (France) in 1987 by supplementing intuitionist logic in a sophisticated manner. Thus, linear logic' s connectives can be explained using information processing terms such as sequentiality and parallel computation. For instance, AB shows two processes, A and B, carried out one after another. AB linear negative exhibits synchronization, that is, in order for the process A to be carried out, both A and have to be accomplished simultaneously. Since the field of linear logic is not very active in Korea at present, this paper deals only with syntax aspect of linear logic in order to arouse interest in the subject, leaving semantics and proof nets for future studies.