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...
Main Authors: | , |
---|---|
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 |