No Cover Image

Journal article 343 views 122 downloads

On proving consistency of equational theories in bounded arithmetic

Arnold Beckmann Orcid Logo, YORIYUKI YAMAGATA Orcid Logo

The Journal of Symbolic Logic, Volume: 90, Issue: 1, Pages: 135 - 165

Swansea University Author: Arnold Beckmann Orcid Logo

  • 68749.pdf

    PDF | Accepted Manuscript

    Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).

    Download (389.04KB)

Check full text

DOI (Published version): 10.1017/jsl.2025.6

Abstract

We consider equational theories based on axioms for recursively dening functions, with rules for equality and substitution, but no form of induction|we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook's system PV without its rule for...

Full description

Published in: The Journal of Symbolic Logic
ISSN: 0022-4812 1943-5886
Published: Cambridge University Press (CUP) 2025
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa68749
first_indexed 2025-01-28T14:13:37Z
last_indexed 2025-05-16T09:43:00Z
id cronfa68749
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-05-15T12:41:59.9838821</datestamp><bib-version>v2</bib-version><id>68749</id><entry>2025-01-28</entry><title>On proving consistency of equational theories in bounded arithmetic</title><swanseaauthors><author><sid>1439ebd690110a50a797b7ec78cca600</sid><ORCID>0000-0001-7958-5790</ORCID><firstname>Arnold</firstname><surname>Beckmann</surname><name>Arnold Beckmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-01-28</date><deptcode>MACS</deptcode><abstract>We consider equational theories based on axioms for recursively dening functions, with rules for equality and substitution, but no form of induction|we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook&amp;apos;s system PV without its rule for induction.We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs model-theoretic constructions for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.</abstract><type>Journal Article</type><journal>The Journal of Symbolic Logic</journal><volume>90</volume><journalNumber>1</journalNumber><paginationStart>135</paginationStart><paginationEnd>165</paginationEnd><publisher>Cambridge University Press (CUP)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0022-4812</issnPrint><issnElectronic>1943-5886</issnElectronic><keywords>Bounded Arithmetic; equational theories; separation problem</keywords><publishedDay>1</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-03-01</publishedDate><doi>10.1017/jsl.2025.6</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2025-05-15T12:41:59.9838821</lastEdited><Created>2025-01-28T14:11:20.7764338</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>1</order></author><author><firstname>YORIYUKI</firstname><surname>YAMAGATA</surname><orcid>0000-0003-2096-677x</orcid><order>2</order></author></authors><documents><document><filename>68749__33425__359e8832308f4aa2a756d80956784522.pdf</filename><originalFilename>68749.pdf</originalFilename><uploaded>2025-01-28T14:13:30.0844061</uploaded><type>Output</type><contentLength>398380</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><documentNotes>Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/deed.en</licence></document></documents><OutputDurs/></rfc1807>
spelling 2025-05-15T12:41:59.9838821 v2 68749 2025-01-28 On proving consistency of equational theories in bounded arithmetic 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2025-01-28 MACS We consider equational theories based on axioms for recursively dening functions, with rules for equality and substitution, but no form of induction|we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook&apos;s system PV without its rule for induction.We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs model-theoretic constructions for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest. Journal Article The Journal of Symbolic Logic 90 1 135 165 Cambridge University Press (CUP) 0022-4812 1943-5886 Bounded Arithmetic; equational theories; separation problem 1 3 2025 2025-03-01 10.1017/jsl.2025.6 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2025-05-15T12:41:59.9838821 2025-01-28T14:11:20.7764338 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Arnold Beckmann 0000-0001-7958-5790 1 YORIYUKI YAMAGATA 0000-0003-2096-677x 2 68749__33425__359e8832308f4aa2a756d80956784522.pdf 68749.pdf 2025-01-28T14:13:30.0844061 Output 398380 application/pdf Accepted Manuscript true Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention). true eng https://creativecommons.org/licenses/by/4.0/deed.en
title On proving consistency of equational theories in bounded arithmetic
spellingShingle On proving consistency of equational theories in bounded arithmetic
Arnold Beckmann
title_short On proving consistency of equational theories in bounded arithmetic
title_full On proving consistency of equational theories in bounded arithmetic
title_fullStr On proving consistency of equational theories in bounded arithmetic
title_full_unstemmed On proving consistency of equational theories in bounded arithmetic
title_sort On proving consistency of equational theories in bounded arithmetic
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
YORIYUKI YAMAGATA
format Journal article
container_title The Journal of Symbolic Logic
container_volume 90
container_issue 1
container_start_page 135
publishDate 2025
institution Swansea University
issn 0022-4812
1943-5886
doi_str_mv 10.1017/jsl.2025.6
publisher Cambridge University Press (CUP)
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description We consider equational theories based on axioms for recursively dening functions, with rules for equality and substitution, but no form of induction|we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook&apos;s system PV without its rule for induction.We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs model-theoretic constructions for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.
published_date 2025-03-01T05:26:20Z
_version_ 1851097748999241728
score 11.089572

Similar Items