09/02/2015, 11:00— Room P3.10, Mathematics Building
Walter Carnielli, CLE / UNICAMP - Brazil
TITLE: Towards a new way to algebraize FOL (and several others).
ABSTRACT: The algebraic method for theorem proving based on the reduction of first-order formulas within certain rings (commutative rings with unity) equipped with infinitary operations is shown to indicate a possible didate for a new version of algebrization of FOL, at the same time where the notion of logical derivability is characterized by the notion of algebraic solubility. The topics I intend to discuss are the following: i) the polynomial ring method as an alternative to algebraizing logic; ii) the notion of M-ring, that allows us to operate with some kind of infinitary version of Boolean sums and products; iii) FOL in polynomial version; iv) soundness and completeness of the polynomial ring method for FOL.
Work in progress, joint with M. Matulovic and H. L. Mariano.