Como demonstar em lógicas modais manuseando polinômios

Uma das ideias mais interessantes que me ocorreu foi tratar expressões lógicas por meio
de polinômios formais sobre corpos finitos. Mostrei que isso pode ser feito com lógicas polivalentes
finitárias em geral (incluindo a lógica clássica, obviamente), com lógicas paraconsistentes, e com o fragmetno monádico da lógica de primeira ordem. Recetnemente, com meu ex-estudante Juan Calos Agudelo, agora professor
em Bogotá, Colômbia, mostramos que várias lógicas modais podem ser tratadas por meio de polinômnios,
inclusive (por meio da conhecida tradução de Gödel) a lógica intuicionista.

O artigo "Semantics and Proof Method for Modalities" (Juan Carlos Agudelo e Walter Carnielli) vai sair no "The Review of Symbolic Logic", e já apareceu online:

The Review of Symbolic Logic
doi: 10.1017/S1755020310000213
Published online: 14 Set 201

----------------------------------------------------------
Abstract

A new (sound and complete) proof style adequate for modal logics is defined from the polynomial ring calculus (PRC). The new semantics not only expresses truth conditions of modal formulas by means of polynomials, but also permits to perform deductions through polynomial handling. This paper also investigates relationships among the PRC here defined, the algebraic semantics for modal logics, equational logics, the Dijkstra–Scholten equational-proof style, and rewriting systems. The method proposed is throughly exemplified for S5, and can be easily extended to other modal logics.
----------------------------------------------------------