An Arithmetically Complete Predicate Modal Logic

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic com...

Full description

Bibliographic Details
Main Authors: Yunge Hao, George Tourlakis
Format: Article
Language:English
Published: Lodz University Press 2021-12-01
Series:Bulletin of the Section of Logic
Subjects:
Online Access:https://czasopisma.uni.lodz.pl/bulletin/article/view/8441
_version_ 1811332049307435008
author Yunge Hao
George Tourlakis
author_facet Yunge Hao
George Tourlakis
author_sort Yunge Hao
collection DOAJ
description This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), 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 \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.
first_indexed 2024-04-13T16:30:58Z
format Article
id doaj.art-e11484bbe18647a5b8120a0cf1f21fcf
institution Directory Open Access Journal
issn 0138-0680
2449-836X
language English
last_indexed 2024-04-13T16:30:58Z
publishDate 2021-12-01
publisher Lodz University Press
record_format Article
series Bulletin of the Section of Logic
spelling doaj.art-e11484bbe18647a5b8120a0cf1f21fcf2022-12-22T02:39:35ZengLodz University PressBulletin of the Section of Logic0138-06802449-836X2021-12-0150451354110.18778/0138-0680.2021.188325An Arithmetically Complete Predicate Modal LogicYunge Hao0George Tourlakis1York University, Department of Electrical Engineering and Computer ScienceYork University, Department of Electrical Engineering and Computer ScienceThis paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), 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 \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.https://czasopisma.uni.lodz.pl/bulletin/article/view/8441predicate modal logicarithmetic completenesslogic glsolovay's theoremequational proofs
spellingShingle Yunge Hao
George Tourlakis
An Arithmetically Complete Predicate Modal Logic
Bulletin of the Section of Logic
predicate modal logic
arithmetic completeness
logic gl
solovay's theorem
equational proofs
title An Arithmetically Complete Predicate Modal Logic
title_full An Arithmetically Complete Predicate Modal Logic
title_fullStr An Arithmetically Complete Predicate Modal Logic
title_full_unstemmed An Arithmetically Complete Predicate Modal Logic
title_short An Arithmetically Complete Predicate Modal Logic
title_sort arithmetically complete predicate modal logic
topic predicate modal logic
arithmetic completeness
logic gl
solovay's theorem
equational proofs
url https://czasopisma.uni.lodz.pl/bulletin/article/view/8441
work_keys_str_mv AT yungehao anarithmeticallycompletepredicatemodallogic
AT georgetourlakis anarithmeticallycompletepredicatemodallogic
AT yungehao arithmeticallycompletepredicatemodallogic
AT georgetourlakis arithmeticallycompletepredicatemodallogic