Recent zbMATH articles in MSC 03F https://zbmath.org/atom/cc/03F 2021-05-28T16:06:00+00:00 Werkzeug Equivalence of bar induction and bar recursion for continuous functions with continuous moduli. https://zbmath.org/1459.03091 2021-05-28T16:06:00+00:00 "Fujiwara, Makoto" https://zbmath.org/authors/?q=ai:fujiwara.makoto "Kawai, Tatsuji" https://zbmath.org/authors/?q=ai:kawai.tatsuji Summary: We compare Brouwer's bar theorem and Spector's bar recursion for the lowest type in the context of constructive reverse mathematics. To this end, we reformulate bar recursion as a logical principle stating the existence of a bar recursor for every function which serves as the stopping condition of bar recursion. We then show that the decidable bar induction is equivalent to the existence of a bar recursor for every continuous function from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ with a continuous modulus. We also introduce fan recursion, the bar recursion for binary trees, and show that the decidable fan theorem is equivalent to the existence of a fan recursor for every continuous function from $\{0, 1 \}^{\mathbb{N}}$ to $\mathbb{N}$ with a continuous modulus. The equivalence for bar induction holds over the extensional version of intuitionistic arithmetic in all finite types augmented with the characteristic principles of Gödel's Dialectica interpretation. On the other hand, we show the equivalence for fan theorem without using such extra principles. De Morgan dual nominal quantifiers modelling private names in non-commutative logic. https://zbmath.org/1459.03090 2021-05-28T16:06:00+00:00 "Horne, Ross" https://zbmath.org/authors/?q=ai:horne.ross "Tiu, Alwen" https://zbmath.org/authors/?q=ai:tiu.alwen-fernanto "Aman, Bogdan" https://zbmath.org/authors/?q=ai:aman.bogdan "Ciobanu, Gabriel" https://zbmath.org/authors/?q=ai:ciobanu.gabriel Effective strong convergence of the proximal point algorithm in CAT(0) spaces. https://zbmath.org/1459.46070 2021-05-28T16:06:00+00:00 "Leuştean, Laurenţiu" https://zbmath.org/authors/?q=ai:leustean.laurentiu "Sipoş, Andrei" https://zbmath.org/authors/?q=ai:sipos.andrei Summary: We apply methods of proof mining to obtain uniform quantitative bounds on the strong convergence of the proximal point algorithm for finding minimizers of convex, lower semicontinuous, proper functions in CAT(0) spaces. Thus, for uniformly convex functions, we compute rates of convergence, while, for totally bounded CAT(0) spaces, we apply methods introduced by \textit{U. Kohlenbach} et al. to compute rates of metastability [Commun. Contemp. Math. 20, No. 2, Article ID 1750015, 42 p. (2018; Zbl 06814506)]. Model theory and proof theory of coalgebraic predicate logic. https://zbmath.org/1459.03104 2021-05-28T16:06:00+00:00 "Litak, Tadeusz" https://zbmath.org/authors/?q=ai:litak.tadeusz "Pattinson, Dirk" https://zbmath.org/authors/?q=ai:pattinson.dirk "Sano, Katsuhiko" https://zbmath.org/authors/?q=ai:sano.katsuhiko "Schröder, Lutz" https://zbmath.org/authors/?q=ai:schroder.lutz Summary: We propose a generalization of first-order logic originating in a neglected work by \textit{C. C. Chang} [Lect. Notes Math. 337, 599--617 (1973; Zbl 0276.02012)]: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, both in comparison with coalgebraic hybrid logics and with existing first-order proposals for special classes of Set-coalgebras (apart from relational structures, also neighbourhood frames and topological spaces). Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes that allow completeness -- and in some cases beyond that. Finally, we discuss a basic sequent system, for which we establish a syntactic cut-elimination result. Long-distance Q-resolution with dependency schemes. https://zbmath.org/1459.68229 2021-05-28T16:06:00+00:00 "Peitl, Tomáš" https://zbmath.org/authors/?q=ai:peitl.tomas "Slivovsky, Friedrich" https://zbmath.org/authors/?q=ai:slivovsky.friedrich "Szeider, Stefan" https://zbmath.org/authors/?q=ai:szeider.stefan Summary: Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system -- which we call long-distance Q(D)-resolution -- is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution. On the generation of quantified lemmas. https://zbmath.org/1459.03011 2021-05-28T16:06:00+00:00 "Ebner, Gabriel" https://zbmath.org/authors/?q=ai:ebner.gabriel "Hetzl, Stefan" https://zbmath.org/authors/?q=ai:hetzl.stefan "Leitsch, Alexander" https://zbmath.org/authors/?q=ai:leitsch.alexander "Reis, Giselle" https://zbmath.org/authors/?q=ai:reis.giselle "Weller, Daniel" https://zbmath.org/authors/?q=ai:weller.daniel-s Summary: In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen's cut-elimination method for sequent calculus. The first step consists of the computation of a compact representation (a so-called decomposition) of Herbrand instances in a cut-free proof. Given a decomposition the problem of computing the corresponding lemmas is reduced to the solution of a second-order unification problem (the solution conditions). It is shown that that there is always a solution of the solution conditions, the canonical solution. This solution yields a sequence of lemmas and, finally, a proof based on these lemmas. Various techniques are developed to simplify the canonical solution resulting in a reduction of proof complexity. Moreover, the paper contains a comprehensive empirical evaluation of the implemented method and gives an application to a mathematical proof. Restricted polynomial induction versus ordinary induction. https://zbmath.org/1459.03088 2021-05-28T16:06:00+00:00 "Adamowicz, Zofia" https://zbmath.org/authors/?q=ai:adamowicz.zofia Summary: We consider conservativity questions between, on the one hand, arithmetical theories in which the operations of successor, addition and multiplication are not provably total and which are fragments of the bounded arithmetic theory $$I\Delta_0$$ and, on the other hand, extensions of those theories to subtheories of Buss's bounded arithmetic $$S_2$$. These questions are related to the problem of finite axiomatizability of a version of $$I\Delta_0$$ in which the totality of the operations is not assumed. Polarized substructural session types. https://zbmath.org/1459.68042 2021-05-28T16:06:00+00:00 "Pfenning, Frank" https://zbmath.org/authors/?q=ai:pfenning.frank "Griffith, Dennis" https://zbmath.org/authors/?q=ai:griffith.dennis Summary: The deep connection between session-typed concurrency and linear logic is embodied in the language SILL that integrates functional and message-passing concurrent programming. The exacting nature of linear typing provides strong guarantees, such as global progress, absence of deadlock, and race freedom, but it also requires explicit resource management by the programmer. This burden is alleviated in an affine type system where resources need not be used, relying on a simple form of garbage collection.{ }In this paper, we show how to effectively support both linear and affine typing in a single language, in addition to the already present unrestricted (intuitionistic) types. The approach, based on Benton's adjoint construction, suggests that the usual distinction between synchronous and asynchronous communication can be viewed through the lens of modal logic. We show how polarizing the propositions into positive and negative connectives allows us to elegantly express synchronization in the type instead of encoding it by extra-logical means. For the entire collection see [Zbl 1320.68027]. Relating reasoning methodologies in linear logic and process algebra. https://zbmath.org/1459.68139 2021-05-28T16:06:00+00:00 "Deng, Yuxin" https://zbmath.org/authors/?q=ai:deng.yuxin "Cervesato, Iliano" https://zbmath.org/authors/?q=ai:cervesato.iliano "Simmons, Robert J." https://zbmath.org/authors/?q=ai:simmons.robert-jun Summary: We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely a labeled transition system and a coinductively defined simulation relation. This result establishes a connection between an approach to reason about process specifications and a method to reason about logic specifications. For the entire collection see [Zbl 1415.68011]. Incompleteness theorems, large cardinals, and automata over finite words. https://zbmath.org/1459.03056 2021-05-28T16:06:00+00:00 "Finkel, Olivier" https://zbmath.org/authors/?q=ai:finkel.olivier A real-valued modal logic. https://zbmath.org/1459.03021 2021-05-28T16:06:00+00:00 "Diaconescu, Denisa" https://zbmath.org/authors/?q=ai:diaconescu.denisa "Metcalfe, George" https://zbmath.org/authors/?q=ai:metcalfe.george "Schnüriger, Laura" https://zbmath.org/authors/?q=ai:schnuriger.laura Summary: A many-valued modal logic is introduced that combines the usual Kripke frame semantics of the modal logic K with connectives interpreted locally at worlds by lattice and group operations over the real numbers. A labelled tableau system is provided and a coNEXPTIME upper bound obtained for checking validity in the logic. Focussing on the modal-multiplicative fragment, the labelled tableau system is then used to establish completeness for a sequent calculus that admits cut-elimination and an axiom system that extends the multiplicative fragment of Abelian logic. End extensions of models of fragments of $$\mathrm{PA}$$. https://zbmath.org/1459.03048 2021-05-28T16:06:00+00:00 "Dimitracopoulos, C." https://zbmath.org/authors/?q=ai:dimitracopoulos.costas|dimitracopoulos.constantine "Paschalis, V." https://zbmath.org/authors/?q=ai:paschalis.vasilis|paschalis.vasileios-s \textit{J. B. Paris} and \textit{L. A. S. Kirby} showed in [Stud. Logic Found. Math. Vol. 96, 199--209 (1978; Zbl 0442.03042)] that for all $$n>1$$, a countable model $$M$$ of bounded induction $$I\Delta_0$$ satisfies the $$\Sigma_n$$-collection schema $$B\Sigma_n$$ if and only $$M$$ has a proper $$\Sigma_n$$-elementary end extension to a model of $$I\Delta_0$$. In an attempt to generalize this to models of arbitrary cardinality, \textit{P. G. Clote} [Fundam. Math. 127, 163--170 (1987; Zbl 0619.03038); Fundam. Math. 158, No. 3, 301--302 (1998; Zbl 0924.03108)] proved that for all $$n>1$$, every model of $$I\Sigma_n$$ has a proper $$\Sigma_n$$-elementary extension to a model of $$I\Delta_0$$. In his proof Clote [loc. cit.], uses a restricted ultrapower construction. The authors give another, detailed proof of Clote's result [loc. cit.] using a subtle version of the arithmetized completeness theorem. In Section 3 of the paper, that proof is modified to obtain a new result: every model of $$I\Sigma_1$$ has an proper end extension satisfying $$I\Delta_0$$. The authors acknowledge that the same result can be proved using the results in [\textit{A. Enayat} and \textit{T. L. Wong}, Ann. Pure Appl. Logic 168, No. 6, 1247--1283 (2017; Zbl 1422.03080)]. The notoriously difficult problem whether every model of $$B\Sigma_1$$ has an proper end extension satisfying $$I\Delta_0$$ is still open. The paper concludes with a list of interesting related open problems. Reviewer: Roman Kossak (New York) Weihrauch-completeness for layerwise computability. https://zbmath.org/1459.03069 2021-05-28T16:06:00+00:00 "Pauly, Arno" https://zbmath.org/authors/?q=ai:pauly.arno-m "Fouché, Willem" https://zbmath.org/authors/?q=ai:fouche.willem-louw "Davie, George" https://zbmath.org/authors/?q=ai:davie.george Summary: We introduce the notion of being Weihrauch-complete for layerwise computability and provide several natural examples related to complex oscillations, the law of the iterated logarithm and Birkhoff's theorem. We also consider hitting time operators, which share the Weihrauch degree of the former examples but fail to be layerwise computable. Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic. https://zbmath.org/1459.03028 2021-05-28T16:06:00+00:00 "Gerasimov, Aleksandr Sergeevich" https://zbmath.org/authors/?q=ai:gerasimov.aleksandr-sergeevich On the basis of the calculus $$\mbox{G}Ł\forall$$ of \textit{M. Baaz} and \textit{G. Metcalfe} in [J. Log. Comput. 20, No. 1, 35--54 (2010; Zbl 1188.03014); \textit{G. Metcalfe} et al., Proof theory for fuzzy logics. Dordrecht: Springer (2009; Zbl 1168.03002)] and tableau calculi by the author in [Algebra Logic 55, No. 2, 103--127 (2016; Zbl 1386.03025)], the author introduced in [Sib. Adv. Math. 28, No. 2, 79--100 (2018; Zbl 1413.03003] the analytic hypersequent calculi $$\mbox{G}^{1}Ł\forall$$ and $$\mbox{G}^{2}Ł\forall$$ for the first-order rational Pavelka logic $$\mbox{RPL}\forall$$ and hence for the first-order infinite-valued Łukasiewicz logic $$Ł\forall$$. The calculi $$\mbox{G}^{1}Ł\forall$$ and $$\mbox{G}^{2}Ł\forall$$ do not have structural rules; the latter is a noncumulative variant of the former, which is cumulative, i.e., preserves the conclusion of each inference rule in its premises. Any $$\mbox{G}Ł\forall$$- or $$\mbox{G}^{2}Ł\forall$$-provable sentence is provable in $$\mbox{G}^{1}Ł\forall$$; any prenex $$\mbox{RP}\forall$$-sentence is $$\mbox{G}^{1}Ł\forall$$ -provable iff it is $$\mbox{G}^{2}Ł\forall$$-provable; and any prenex $$Ł\forall$$-sentence is provable or unprovable in $$\mbox{G}Ł\forall$$, $$\mbox{G}^{1}Ł\forall$$ and $$\mbox{G}^{2}Ł\forall$$ simultaneously. Also in [the author, 2018, loc. cit.], a family of proof search algorihms is described. Given a prenex $$\mbox{G}^2Ł\forall$$-provable sentence, such an algorithm constructs some proof for it in a tableau modification of the calculus $$\mbox{G}^{2}Ł\forall$$. However this only works well for prenex sentences. A defect of $$\mbox{G}^{2}Ł\forall$$ causes repeating designations of multisets of formulas in each premise of two quantifier rules. This causes repeated decomposition of the same formulas from the multisets during bottom-up proof search, and prevents establishing desirable proof-theoretic properties for the calculus $$\mbox{G}^{2}Ł\forall$$. The present paper introduces an analytic hypersequent calculus $$\mbox{G}^{3}Ł\forall$$ for the first-order infinite-valued Łukasiewicz logic $$Ł\forall$$ and for the logic $$\mbox{RPL}\forall$$. There are no structural rules in the calculus, and designations of multisets of formulas are not repeated in any premise of its rules. The calculus $$\mbox{G}^{3}Ł\forall$$ proves any sentence that is provable in at least one of the previously known analytic calculi for $$Ł\forall$$ or $$\mbox{RPL}\forall$$, including Baaz and Metcalfe's [loc. cit.] hypersequent calculus $$\mbox{G}Ł\forall$$ for $$Ł\forall$$. Proof-theoretic properties of $$\mbox{G}^{3}Ł\forall$$ are considered and foundations for proof search algorithms are given. A proof of the completeness of the $$\mbox{G}Ł\forall$$-based infinitary calculus for prenex $$Ł\forall$$-sentences is given. The completeness of a $$\mbox{G}^{3}Ł\forall$$-based infinitary calculus for prenex $$\mbox{RPL}\forall$$-sentences is established. Reviewer: Albert Hoogewijs (Gent) Characterising tree-like Frege proofs for QBF. https://zbmath.org/1459.03087 2021-05-28T16:06:00+00:00 "Beyersdorff, Olaf" https://zbmath.org/authors/?q=ai:beyersdorff.olaf "Hinde, Luke" https://zbmath.org/authors/?q=ai:hinde.luke The article is well organized, written, and clear. It combines strategy size with round-base strategy extraction algorithm in order to give a lower bound on any tree-like P+$$\forall$$red proof system, not only that, it is the only way to show such lower bound which does not require showing a lower bound for dag-like P+$$\forall$$red. On page 4, paragraph 1, there is a typo, instead of $$\forall$$ reduction must be $$\forall$$-reduction. Finally, on page 4, Definition 5, it would be appropriate, in order to clarify, to give the explicit definition of \textit{range}, not only mention it, because the concept is used in the rest of the article many times. Reviewer: Ariel Germán Fernández (Buenos Aires) A density theorem for hierarchies of limit spaces over separable metric spaces. https://zbmath.org/1459.03093 2021-05-28T16:06:00+00:00 "Petrakis, Iosif" https://zbmath.org/authors/?q=ai:petrakis.iosif Summary: In this paper, we show, almost constructively, a density theorem for hierarchies of limit spaces over separable metric spaces. Our proof is not fully constructive, since it relies on the constructively not acceptable fact that the limit relation induced by a metric space satisfies Urysohn's axiom for limit spaces. By adding the condition of strict positivity to Normann's notion of probabilistic projection we establish a relation between strictly positive general probabilistic selections on a sequential space and general approximation functions on a limit space. Showing that Normann's result, that a (general and strictly positive) probabilistic selection is definable on a separable metric space, admits a constructive proof, and based on the constructively shown in [the author, Ann. Pure Appl. Logic 167, No. 9, 737--752 (2016; Zbl 1432.03083)] Cartesian closure property of the category of limit spaces with general approximations, our quite effective density theorem follows. This work, which is a continuation of [loc. cit.], is within computability theory at higher types and Normann's Program of Internal Computability. For the entire collection see [Zbl 1360.68012]. From logic to biology via physics: a survey. https://zbmath.org/1459.92005 2021-05-28T16:06:00+00:00 "Longo, Giuseppe" https://zbmath.org/authors/?q=ai:longo.giuseppe "Montévil, Maël" https://zbmath.org/authors/?q=ai:montevil.mael Summary: This short text summarizes the work in biology proposed in our book, \textit{Perspectives on Organisms}, where we analyse the unity proper to organisms by looking at it from different viewpoints. We discuss the theoretical roles of biological time, complexity, theoretical symmetries, singularities and critical transitions. We explicitly borrow from the conclusions in some key chapters and introduce them by a reflection on incompleteness'', also proposed in the book. We consider that incompleteness is a fundamental notion to understand the way in which we construct knowledge. Then we will introduce an approach to biological dynamics where randomness is central to the theoretical determination: randomness does not oppose biological stability but contributes to it by variability, adaptation, and diversity. Then, evolutionary and ontogenetic trajectories are continual changes of coherence structures involving symmetry changes within an ever-changing global stability. A bound for Dickson's lemma. https://zbmath.org/1459.03092 2021-05-28T16:06:00+00:00 "Berger, Josef" https://zbmath.org/authors/?q=ai:berger.josef "Schwichtenberg, Helmut" https://zbmath.org/authors/?q=ai:schwichtenberg.helmut Summary: We consider a special case of Dickson's lemma: for any two functions $$f,g$$ on the natural numbers there are two numbers $$i<j$$ such that both $$f$$ and $$g$$ weakly increase on them, i.e., $$f_i\leq f_j$$ and $$g_i \leq g_j$$. By a combinatorial argument (due to the first author) a simple bound for such $$i,j$$ is constructed. The combinatorics is based on the finite pigeon hole principle and results in a descent lemma. From the descent lemma one can prove Dickson's lemma, then guess what the bound might be, and verify it by an appropriate proof. We also extract (via realizability) a bound from (a formalization of) our proof of the descent lemma. The strength of the SCT criterion. https://zbmath.org/1459.03010 2021-05-28T16:06:00+00:00 "Frittaion, Emanuele" https://zbmath.org/authors/?q=ai:frittaion.emanuele "Steila, Silvia" https://zbmath.org/authors/?q=ai:steila.silvia "Yokoyama, Keita" https://zbmath.org/authors/?q=ai:yokoyama.keita Summary: We undertake the study of size-change analysis in the context of reverse mathematics. In particular, we prove that the SCT criterion [\textit{C. S. Lee} et al., in: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL'01. New York, NY: Association for Computing Machinery (ACM). 81--92 (2001; Zbl 1323.68216), Theorem 4] is equivalent to $$\mathsf {I}\varSigma ^0_{2}$$ over $$\mathsf {RCA}_0$$. For the entire collection see [Zbl 1360.68012]. Incompleteness theorems, large cardinals, and automata over finite words. https://zbmath.org/1459.03055 2021-05-28T16:06:00+00:00 "Finkel, Olivier" https://zbmath.org/authors/?q=ai:finkel.olivier Summary: We prove that one can construct various kinds of automata over finite words for which some elementary properties are actually independent from strong set theories like $$T_n =:\mathbf{ZFC} +$$ There exist (at least) $$n$$ inaccessible cardinals'', for integers $$n\geq 0$$. In particular, we prove independence results for languages of finite words generated by context-free grammars, or accepted by 2-tape or 1-counter automata. Moreover we get some independence results for weighted automata and for some related finitely generated subsemigroups of the set $$\mathbb {Z}^{3\times 3}$$ of 3-3 matrices with integer entries. Some of these latter results are independence results from the Peano axiomatic system \textbf{PA}. For the entire collection see [Zbl 1360.68012]. Localic completion of uniform spaces. https://zbmath.org/1459.03094 2021-05-28T16:06:00+00:00 "Kawai, Tatsuji" https://zbmath.org/authors/?q=ai:kawai.tatsuji Summary: We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set $$X$$ equipped with a family of generalised metrics on $$X$$, where a generalised metric on $$X$$ is a map from the product of $$X$$ to the upper reals satisfying zero self-distance law and triangle inequality. For a symmetric generalised uniform space, the localic completion lifts its generalised uniform structure to a point-free generalised uniform structure. This point-free structure induces a complete generalised uniform structure on the set of formal points of the localic completion that gives the standard completion of the original gus with Cauchy filters. We extend the localic completion to a full and faithful functor from the category of locally compact uniform spaces into that of overt locally compact completely regular formal topologies. Moreover, we give an elementary characterisation of the cover of the localic completion of a locally compact uniform space that simplifies the existing characterisation for metric spaces. These results generalise the corresponding results for metric spaces by Erik Palmgren. Furthermore, we show that the localic completion of a symmetric gus is equivalent to the point-free completion of the uniform formal topology associated with the gus. We work in Aczel's constructive set theory CZF with the Regular Extension Axiom. Some of our results also require Countable Choice. On the diagonal lemma of Gödel and Carnap. https://zbmath.org/1459.03089 2021-05-28T16:06:00+00:00 "Salehi, Saeed" https://zbmath.org/authors/?q=ai:salehi.saeed.1|salehi.saeed This paper provides a proof of a semantic, nonconstructive version -- for it states the existence of two positive integers that cannot be made explicit -- of Gödel's diagonal lemma, which is sufficiently strong for proving Gödel's first incompleteness theorem for sound and definable theories, and also for proving the semantic form of Tarski's theorem on the undefinability of the truth of the set of the (Gödel codes of the) arithmetical sentences'', and of a weak version of the syntactic formulation of the diagonal lemma. Reviewer: Victor V. Pambuccian (Glendale) First order theories of some lattices of open sets. https://zbmath.org/1459.03062 2021-05-28T16:06:00+00:00 "Kudinov, Oleg" https://zbmath.org/authors/?q=ai:kudinov.oleg-victorovich "Selivanov, Victor" https://zbmath.org/authors/?q=ai:selivanov.victor-l Summary: We show that the first order theory of the lattice of open sets in some natural topological spaces is $$m$$-equivalent to second order arithmetic. We also show that for many natural computable metric spaces and computable domains the first order theory of the lattice of effectively open sets is undecidable. Moreover, for several important spaces (e.g., $$\mathbb{R}^n$$, $$n\geq 1$$, and the domain $$P\omega$$) this theory is $$m$$-equivalent to first order arithmetic. Natural density and probability, constructively. https://zbmath.org/1459.03095 2021-05-28T16:06:00+00:00 "Maschio, Samuele" https://zbmath.org/authors/?q=ai:maschio.samuele In this paper, the author, relying on the frequentist interpretation of probability from a constructive point of view, and using the sequential nature of events in the frequentist approach, introduces the determination of their probability in a very direct way. This approach allows him to recognize some properties of probability designed in this way. Then, the author correlates the newly designed concept of density in such a chosen probability determination with the limited principle of omniscience (LPO). Reviewer: Daniel Romano (Banja Luka) Focusing in orthologic. https://zbmath.org/1459.03096 2021-05-28T16:06:00+00:00 "Laurent, Olivier" https://zbmath.org/authors/?q=ai:laurent.olivier Summary: We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add constraints on proofs and to optimise proof search. We demonstrate how to take benefits from the new systems in automatic proof search for orthologic.