Recent zbMATH articles in MSC 03F30https://www.zbmath.org/atom/cc/03F302021-04-16T16:22:00+00:00WerkzeugOn the inevitability of the consistency operator.https://www.zbmath.org/1456.030912021-04-16T16:22:00+00:00"Montalbán, Antonio"https://www.zbmath.org/authors/?q=ai:montalban.antonio"Walsh, James"https://www.zbmath.org/authors/?q=ai:walsh.james-a|walsh.james-bruce|walsh.james-jThe paper is concerned with recursive monotone functions on the Lindenbaum-Tarski algebra of the elementary arithmetic EA. Denote the equivalence class of a sentence \(\varphi\), modulo EA-provability, by \([\varphi]\). Write \([\psi]\leq[\varphi]\) when \(\mathrm{EA} \vdash\psi\rightarrow\varphi\). A function \(f\) on sentences is \textit{monotone} if \(f([\psi])\leq f([\varphi])\) for every \(\psi\) and \(\varphi\) with \([\psi]\leq[\varphi]\). Note that then \(f\) is also \textit{extensional} in the sense that \(f([\psi])= f([\varphi])\) when \([\psi]=[\varphi]\).
\textit{V. Yu. Shavrukov} and \textit{A. Visser} proved in [Notre Dame J. Formal Logic 55, No. 4, 569--582 (2014; Zbl 1339.03056)] that there exists a recursive extensional function on the Lindenbaum-Tarski algebra of Peano's arithmetic such that it lies strictly between the identity function and the mapping \(\varphi\mapsto\varphi\wedge \mathrm{Con} (\varphi)\). The main result of the present paper is that there is no recursive monotone function on the Lindenbaum-Tarski algebra of Con that lies strictly between the identity function and the mapping \(\varphi\mapsto\varphi\wedge \mathrm{Con}(\varphi)\).
This also negatively answers a question of Shavrukov and Visser in [loc. cit.] which asked if there exists a recursive binary function that is monotonic in both its coordinates and satisfies (i) \([\psi] < g([\psi],[\varphi])<[\varphi]\) if \([\psi]<[\varphi]\), and (ii) \(g([\psi],[\theta]) = g([\varphi],[\theta])\) and \(g([\theta],[\psi]) = g([\theta],[\varphi])\) if \([\psi]=[\varphi]\).
The authors also generalize their results ``to iterates of consistency into the effective transfinite''. They leave open three interesting questions in the paper, one of which is the following: if \(f\) is a recursive monotone \(\Pi_1^0\)(-valued) function such that for every \(\varphi\) we have \([\varphi\wedge\mathrm{Con}^\alpha(\varphi)]\leq[f(\varphi)]\) for some fixed ordinal \(\alpha\), must there exist some \(\beta\leq\alpha\) and some true sentence \(\theta\) such that \([\theta\wedge f(\theta)]=[\theta\wedge\mathrm{Con}^\beta(\theta)]\)?
Reviewer: Saeed Salehi (Tabriz)Interactive learning based realizability and 1-backtracking games.https://www.zbmath.org/1456.030902021-04-16T16:22:00+00:00"Aschieri, Federico"https://www.zbmath.org/authors/?q=ai:aschieri.federicoSummary: We prove that interactive learning based classical realizability (introduced by the author and \textit{S. Berardi} for first order arithmetic [Log. Methods Comput. Sci. 6, No. 3, Paper No. 19, 22 p. (2010; Zbl 1201.03052)]) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games.
For the entire collection see [Zbl 1391.03011].An applicative theory for \textsf{FPH}.https://www.zbmath.org/1456.030612021-04-16T16:22:00+00:00"Kahle, Reinhard"https://www.zbmath.org/authors/?q=ai:kahle.reinhard"Oitavem, Isabel"https://www.zbmath.org/authors/?q=ai:oitavem.isabelSummary: In this paper we introduce an applicative theory which characterizes the polynomial hierarchy of time.
For the entire collection see [Zbl 1391.03011].