Construction of models of bounded arithmetic by restricted reduced powers
type: Item
instance of: scholarly article
title: Construction of models of bounded arithmetic by restricted reduced powers
zbMATH Open document ID: 1380.03070
author: Michal Garlík
published in: Archive for Mathematical Logic
publication date: 2017-02-02T00:00:00Z
review text: The paper is devoted to models of bounded arithmetic. The general aim is to construct extensions of models that preserve the set of lengths (and, consequently, polynomial-time computable properties) and satisfy some amount of bounded induction, yet are not elementary, so that they can be utilized, e.g., to prove independence results. Specifically, the author studies variants of \textit{restricted reduced powers}. He presents two constructions of such powers. Construction A is simple, but appears to be of limited applicability; nevertheless, the author shows how it can be used to reprove a form of Buss's witnessing theorem. Construction B is technically more complicated (both in the statement and in the proof), but it is more flexible than Construction A. The paper includes an interesting application of Contruction B to the open problem of separating the theory \(R^1_2\) from its strict variant: it is shown in the relativized setting that \(\mathrm{strict }R^1_2(\alpha)\neq R^1_2(\alpha)\), assuming that the existence of one-way permutations is hard for polynomial-size circuits (on any non-negligible subset of the domain). In fact, the author proves that under this assumption \(\mathrm{strict }R^1_2(\alpha)\) does not prove the bounded choice/collection/replacement schema \(\mathrm{BB }\Sigma^b_1(\alpha)\), which is well known to be provable in \(R^1_2(\alpha)\). Furthemore, if one can find such a one-way permutation definable by a term in the language of \(R^1_2\), we obtain even the unrelativized separation \(\mathrm{strict }R^1_2\neq R^1_2\).
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03C20
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 03H15
zbMATH DE Number: 6680062
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: ultraproduct
zbMATH Keywords: sharply bounded collection
MaRDI profile type: Publication
full work available at URL: s00153-016-0484-9
OpenAlex ID: W2341717488
cites work: Generalizations of the Compactness Theorem and Gödel’s Completeness Theorem for Nonstandard Finite Structures
cites work: Non-standard models of Peano arithmetic
cites work: Arithmetizing uniform \(NC\)
cites work: Q3794177
cites work: Bounded arithmetic for NC, ALogTIME, L and NL
cites work: The strength of replacement in weak arithmetic
cites work: A new proof of Ajtai's completeness theorem for nonstandard finite structures
cites work: Q5286672
cites work: Q4944913
cites work: Q4856172
cites work: Nondeterministic polynomial-time computations and models of arithmetic
DOI: 10.1007/S00153-016-0484-9
Recommended article: Q5693580
Recommended article: Q3128124
Recommended article: Q5393641
Recommended article: On embedding models of arithmetic of cardinality \aleph1into reduced powers
Recommended article: Theories of arithmetics in finite models
Recommended article: Automorphisms of models of bounded arithmetic
Recommended article: Q3826539
Recommended article: Q4348126
Recommended article: Structures interpretable in models of bounded arithmetic
Recommended article: Models of arithmetic and upper bounds for arithmetic sets
description: scientific article; zbMATH DE number 6680062