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.

DOI: 10.1007/3-540-44404-1_16