Quantified propositional Gödel logics

Voronkov, Andrei, and Michel Parigot (eds.) Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000. Proceedings, LNAI 1955 (Springer, Berlin, 2000) 240-256
(with Matthias Baaz and Agata Ciabattoni)

It is shown that $$\mathbf{G}^\mathrm{qp}_\uparrow$$, the quantified propositional Gödel logic based on the truth-values set $$V_\uparrow = {1 – 1/n : n = 1, 2, . . .} \cup {1}$$, is decidable. This result is obtained by reduction to Büchi’s theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of $$\mathbf{G}^\mathrm{qp}_\uparrow$$ as the intersection of all finite-valued quantified propositional Gödel logics.

Preprint