Recent zbMATH articles in MSC 03Fhttps://zbmath.org/atom/cc/03F2021-05-28T16:06:00+00:00WerkzeugEquivalence of bar induction and bar recursion for continuous functions with continuous moduli.https://zbmath.org/1459.030912021-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.tatsujiSummary: 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.030902021-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.gabrielEffective strong convergence of the proximal point algorithm in CAT(0) spaces.https://zbmath.org/1459.460702021-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.andreiSummary: 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.031042021-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.lutzSummary: 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.682292021-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.stefanSummary: 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.030112021-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-sSummary: 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.030882021-05-28T16:06:00+00:00"Adamowicz, Zofia"https://zbmath.org/authors/?q=ai:adamowicz.zofiaSummary: 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.680422021-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.dennisSummary: 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.681392021-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-junSummary: 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.030562021-05-28T16:06:00+00:00"Finkel, Olivier"https://zbmath.org/authors/?q=ai:finkel.olivierA real-valued modal logic.https://zbmath.org/1459.030212021-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.lauraSummary: 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.030482021-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.030692021-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.georgeSummary: 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.030282021-05-28T16:06:00+00:00"Gerasimov, Aleksandr Sergeevich"https://zbmath.org/authors/?q=ai:gerasimov.aleksandr-sergeevichOn 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.030872021-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.lukeThe 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.030932021-05-28T16:06:00+00:00"Petrakis, Iosif"https://zbmath.org/authors/?q=ai:petrakis.iosifSummary: 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.920052021-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.maelSummary: 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.030922021-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.helmutSummary: 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.030102021-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.keitaSummary: 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.030552021-05-28T16:06:00+00:00"Finkel, Olivier"https://zbmath.org/authors/?q=ai:finkel.olivierSummary: 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.030942021-05-28T16:06:00+00:00"Kawai, Tatsuji"https://zbmath.org/authors/?q=ai:kawai.tatsujiSummary: 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.030892021-05-28T16:06:00+00:00"Salehi, Saeed"https://zbmath.org/authors/?q=ai:salehi.saeed.1|salehi.saeedThis 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.030622021-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-lSummary: 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.030952021-05-28T16:06:00+00:00"Maschio, Samuele"https://zbmath.org/authors/?q=ai:maschio.samueleIn 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.030962021-05-28T16:06:00+00:00"Laurent, Olivier"https://zbmath.org/authors/?q=ai:laurent.olivierSummary: 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.