Description

• Title:
  An Arithmetically Complete Predicate Modal Logic
• Creator:
  Hao, Yunge;
  Tourlakis, George
• Contributor:
  Hao, Yunge - York University, Department of Electrical Engineering and Computer Science;
  Tourlakis, George - York University, Department of Electrical Engineering and Computer Science;
  Hao, Yunge - hyggs@my.yorku.ca;
  Tourlakis, George - gt@cse.yorku.ca
• 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.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2022.03.10;
  2021.08.23
• Type:
  Other
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;4;
  50
• Subject:
  Predicate modal logic;
  arithmetic completeness;
  logic GL;
  Solovay's theorem;
  equational proofs
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/41068 ;
  2449-836X;
  10.18778/0138-0680.2021.18
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  other