Translation of infinite-valued QBF to first order logic

57 Views Asked by At

Quantified Boolean Formulas with infinite values are distinct from their usual 2-valued version (proof).

Is there a known way to express such formulas in standard first order logic notation (so that they can be fed to a first order logic theorem prover? What I have in mind is some scheme similar to how modal logics (with infinite number of truth values) can be simulated using the so-called Standard Translation into first order logic. Obviously, a direct translation using a single-argument truth predicate assumes two values and is not applicable in this case, the truth predicate involved probably needs two arguments, as in the Standard Translation. I apologize beforehand for the exploratory nature of the question.