Journal article 73 views 10 downloads
ON PROVING CONSISTENCY OF EQUATIONAL THEORIES IN BOUNDED ARITHMETIC
,
YORIYUKI YAMAGATA
The Journal of Symbolic Logic, Pages: 1 - 31
Swansea University Author:
Arnold Beckmann
-
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)
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...
| 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 |
| 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 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. |
|---|---|
| Keywords: |
Bounded Arithmetic; equational theories; separation problem |
| College: |
Faculty of Science and Engineering |
| Start Page: |
1 |
| End Page: |
31 |