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 candidate 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:

1. the polynomial ring method as an alternative to algebraizing logic;
2. the notion of $M$-ring, that allows us to operate with some kind of infinitary version of Boolean sums and products;
3. FOL in polynomial version;
4. soundness and completeness of the polynomial ring method for FOL.

Work in progress, joint with M. Matulovic and H. L. Mariano.