LECTURE NOTES Proof theory for contemporary logic by handling polynomials over finite fields
The present notes intend to be an introduction to a new algebraic proof method for general sentential logics which is particularly apt for finitely-many-valued logics and its particularization for PC, based on reducing polynomials over finite elds. The method can also be extended to cover certain non-finitely valued logics as well, provided they can be characterized by two-valued dyadic semantics. This is the case of modal logics and paraconsistent logics (and also of intuitionistic logic).
In principle, the method also works for first-order and higher-order logics, but we only deal with the monadic fragment of first-order logic. This is particularly interesting, because it give a polynomial approach to the classical syllogisms. The resulting mechanizable proof method suggested here is of interest for automatic proof theory and offer some hope on finding some heuristic methods in logic, and seems also to be appropriate for investigating some questions on complexity.