An Arithmetically Complete Predicate Modal Logic
An Arithmetically Complete Predicate Modal Logic

Summary/Abstract: This paper investigates a first-order extension of GL called ML3. We outline briefly the history that led to ML3, its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that ML3 is arithmetically complete. As expanded below, ML3 is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"◻" simulating the the informal classical "⊢"―is also arithmetically complete in the Solovay sense.

• Details
• Contents