Newton da Costa defended in 1963 at the Federal University of Paraná the thesis 'Sistemas Formais Inconsistentes', in which he constructs the first formal systems of paraconsistent logic (the C1-Cn systems): logics in which a contradiction (A and ¬A) does not imply that every proposition is true, thereby blocking classical logic's principle of explosion (ex contradictione quodlibet). Classical logic, since Aristotle, holds that anything follows from a contradiction — which makes any inconsistent system collapse into triviality. Da Costa demonstrates that it is possible to construct mathematically rigorous formal systems that tolerate local contradictions without trivializing. The term 'paraconsistent' was coined in 1976 by the Peruvian philosopher Francisco Miró Quesada at Da Costa's request. Paraconsistent logic has direct applications in artificial intelligence (reasoning with inconsistent information), databases (managing contradictory data without system collapse), robotics, and expert systems. It is the mathematical formalization of the intuition Nāgārjuna had expressed logically 1,800 years earlier.