Recent zbMATH articles in MSC 03https://www.zbmath.org/atom/cc/032022-01-14T13:23:02.489162ZUnknown authorWerkzeugToward a formal foundation for time travel in stories and gameshttps://www.zbmath.org/1475.000052022-01-14T13:23:02.489162Z"Helvensteijn, Michiel"https://www.zbmath.org/authors/?q=ai:helvensteijn.michiel"Arbab, Farhad"https://www.zbmath.org/authors/?q=ai:arbab.farhadSummary: Time-travel is a popular topic not only in science fiction, but in physics as well, especially when it concerns the notion of ``changing the past''. It turns out that if time-travel exists, it will follow certain logical rules. In this paper we apply the tools of discrete mathematics to two such sets of rules from theoretical physics: the Novikov Self Consistency Principle and the Many Worlds Interpretation of quantum mechanics. Using temporal logic, we can encode the dynamics of a time-travel story or game, and model-check them for adherence to the rules. We also present the first ever game-engine following these rules, allowing the development of technically accurate time-travel games.
For the entire collection see [Zbl 1460.68002].Why pure mathematical truths are metaphysically necessary: a set-theoretic explanationhttps://www.zbmath.org/1475.000112022-01-14T13:23:02.489162Z"Leitgeb, Hannes"https://www.zbmath.org/authors/?q=ai:leitgeb.hannesSummary: Pure mathematical truths are commonly thought to be metaphysically necessary. Assuming the truth of pure mathematics as currently pursued, and presupposing that set theory serves as a foundation of pure mathematics, this article aims to provide a metaphysical explanation of \textit{why} pure mathematics is metaphysically necessary.Open texture and mathematicshttps://www.zbmath.org/1475.000152022-01-14T13:23:02.489162Z"Shapiro, Stewart"https://www.zbmath.org/authors/?q=ai:shapiro.stewart"Roberts, Craige"https://www.zbmath.org/authors/?q=ai:roberts.craigeAccording to Friedrich Waismann a predicate \(P\), from a natural language, exhibits open texture if it is possible for there to be an object \(a\) such that nothing concerning the established use of \(P\), and nothing concerning the nonlinguistic facts, determines that \(P\) holds of \(a\), nor does anything determine that \(P\) fails to hold of \(a\). If \(P\) is open-textured, then the truth of the sentence, or proposition expressed by \(Pa\) is left open by the use of the language and the nonlinguistic facts. The purpose of the paper under review is to explore the extent to which mathematics is subject to open texture and the extent to which mathematics resists open texture. The resistance is tied to the importance of proof and, in particular, rigor, in mathematics.
Reviewer: Roman Murawski (Poznań)Ludwig Wittgenstein. Vienna edition. Vol. 9. Philosophical remarks. Edited by Michael Nedohttps://www.zbmath.org/1475.000162022-01-14T13:23:02.489162Z"Wittgenstein, Ludwig"https://www.zbmath.org/authors/?q=ai:wittgenstein.ludwigThis volume of the Vienna Edition gives a critical edition of the typescript synopsis TS 209 which Wittgenstein himself entitled ``Philosophische Bemerkungen'' (``Philosophical Remarks''). It was the basis of Rush Rhees' edition published in 1964 [\textit{L. Wittgenstein}, Philosophische Bemerkungen. Aus dem Nachlaß, ed.\ R.\ Rhees. Frankfurt a.M.: Suhrkamp (1964)]. Wittgenstein's synopses constituting the so-called Big Typescript were collections of remarks taken from his manuscript volumes and diaries. TS 209 is a new arrangement of TS 208. Wittgenstein attached it to his application for extending his scholarship at Trinity College, Cambridge. It was reviewed by J.E.\ Littlewood and finally led to a research fellowship.\par The bilingual introduction (pp.\ VII--XVIII) presents insights into Wittgenstein's practise of using the collections of thoughts and ideas of his manuscript volumes for dictating typescripts which could be rearranged to new texts. Wittgenstein used this material from the Big Typescript to compile the selections \textit{Philosophische Bemerkungen} (1964) and \textit{Philosophische Grammatik} (1969) published posthumously. Although the publication of these volumes were ``understandable in retrospect, these volumes conceal an essential aspect of Wittgenstein's philosophy: the organic nature of his work, in constant change and development of his thoughts in ever new contexts'' (p.\ IX). The Vienna Edition presents the manuscripts for the first time as Wittgenstein left them.\par In the edited text a broad variety of topics is touched, e.g., epistemological questions and philosophical considerations on the role of language. Most of the remarks concern questions from the philosophies of logic and mathematics. Wittgenstein compares, e.g., calculi with the rules of a game, criticises mathematical theories, questions wordings in mathematics, discusses paradoxes, etc. Most of these remarks appear unrelated to each other.
Reviewer: Volker Peckhaus (Paderborn)Introductionhttps://www.zbmath.org/1475.000222022-01-14T13:23:02.489162ZFrom the text: The Symposia on the Foundations of Mathematics (SOTFOM), whose first edition was held in 2014 in Vienna, were conceived of and organised by the editors of this special issue with the goal of fostering scholarly interaction and exchange on a wide range of topics relating both to the foundations and the philosophy of mathematics.Philosophical methods under scrutiny: introduction to the special issue \textit{philosophical methods}https://www.zbmath.org/1475.000452022-01-14T13:23:02.489162Z(no abstract)Introduction to the special issue ``Logical perspectives on science and cognition''https://www.zbmath.org/1475.000472022-01-14T13:23:02.489162ZFrom the text: This special issue of Synthese is in honor of Gerhard Schurz, our good friend and colleague, who contributed to philosophy in a multitude of novel and interesting ways. The idea to do such a special issue was born at a symposium on the occasion of Gerhard's 60th birthday back then in 2016.New perspectives in metaontology: introduction to the special issuehttps://www.zbmath.org/1475.000732022-01-14T13:23:02.489162ZFrom the text: This special issue covers a wide range of exciting topics in contemporary metaontology.The continuum, the infinitely small, and the law of continuity in Leibnizhttps://www.zbmath.org/1475.010112022-01-14T13:23:02.489162Z"Levey, Samuel"https://www.zbmath.org/authors/?q=ai:levey.samuelLeibniz's differential calculus went beyond the standards of rigor established by ancient authors like Euclid and Archimedes. The problem of its justification was closely related to a multitude of other questions pertinent to philosophy since antiquity: the composition of the continuum, the existence of minimal and infinitesimal elements, the notion of continuity in time and space and how to understand motion. For example: Is a line a mere aggregate of its points? When dealing with these questions, Leibniz distinguished between the reality of matter and the ideal spaces of geometry. With the aim of presenting Leibniz's ideas on these subjects, the author focusses on two important texts from 1676 while also drawing on other sources: the dialogue \textit{Pacidius Philalethi}, which discusses motion, and the treatise \textit{De quadratura arithmetica circuli ellipseos et hyperbolae}, whose Prop. 6 provides a justification for the use of infinitesimals in geometry. Here, the continuity of the curves is tacitely presupposed. Later in his life, Leibniz subsumed continuity arguments under a general principle, the so-called law of continuity, which he applied to mathematics as well as to physics. One of its incarnations can be summarized as follows: When given quantities approach each other, then those resulting from them also do. Leibniz based one of his attempts to justify the differential calculus on this law. But since he only vaguely formulated and motivated the principle itself, the soundness of this attempt remains questionable (p.~153 ff.).
For the entire collection see [Zbl 1454.01002].
Reviewer: Charlotte Wahl (Hannover)Set theory -- a vehicle to modern mathematics in Polandhttps://www.zbmath.org/1475.010302022-01-14T13:23:02.489162Z"Duda, Roman"https://www.zbmath.org/authors/?q=ai:duda.roman
For the entire collection see [Zbl 07327845].Toward the philosophy of mathematics. Logicism, intuitionism, finitism, and Gödel's incompleteness theorems. Translated from the English by Deborah Kant and Thomas Bedürftighttps://www.zbmath.org/1475.030012022-01-14T13:23:02.489162Z"George, Alexander"https://www.zbmath.org/authors/?q=ai:george.alexander"Vellemann, Daniel J."https://www.zbmath.org/authors/?q=ai:vellemann.daniel-jDas Buch ist eine deutsche Übesetzung von: [\textit{A. George} and \textit{D. J. Velleman}, Philosophies of mathematics. Oxford: Blackwell Publishers (2002; Zbl 1032.00005)]. Es gibt eine gute Einführung in die drei wesentlichen mathematikphilosophischen Positionen im 20. Jahrhundert mit eine besonderen Betonung der Gödelschen Sätze. Stärker aus einer mathematischen als philosophischen Perspektive heraus geschrieben, wird es auch der historischen Entwicklung gerecht. Problematisch ist lediglich die annähernde Gleichsetzung von \textit{Finitismus} und \textit{Formalismus}. Insgesamt stellt das Buch eine gute Einführung in das Thema dar, die gerade interessierten Studenten eine Orientierung ermöglicht.
Reviewer: Reinhard Kahle (Lisboa)The bounds of possibility. Puzzles of modal variationhttps://www.zbmath.org/1475.030022022-01-14T13:23:02.489162Z"Dorr, Cian"https://www.zbmath.org/authors/?q=ai:dorr.cian"Hawthorne, John"https://www.zbmath.org/authors/?q=ai:hawthorne.john"Yli-Vakkuri, Juhani"https://www.zbmath.org/authors/?q=ai:yli-vakkuri.juhaniPublisher's description: In general, a given object could have been different in certain respects. For example, the Great Pyramid could have been somewhat shorter or taller; the Mona Lisa could have had a somewhat different pattern of colours; an ordinary table could have been made of a somewhat different quantity of wood. But there seem to be limits. It would be odd to suppose that the Great Pyramid could have been thimble-sized; that the Mona Lisa could have had the pattern of colours that actually characterizes The Scream; or that the table could have been made of the very quantity of wood that in fact made some other table. However, there are puzzling arguments that purport to show that so long as an object is capable of being somewhat different in some respect, it is capable of being radically different in that respect. These arguments rely on two tempting thoughts: first, that an object's capacity for moderate variation is a non-contingent matter, and second, that what is possibly possible is simply possible. The Bounds of Possibility systematically investigates competing strategies for resolving these puzzles, and defends one of them. Along the way it engages with foundational questions about the metaphysics of modality.R-CALCULUS: a logic of belief revisionhttps://www.zbmath.org/1475.030032022-01-14T13:23:02.489162Z"Li, Wei"https://www.zbmath.org/authors/?q=ai:li.wei.4"Sui, Yuefei"https://www.zbmath.org/authors/?q=ai:sui.yuefeiPublisher's description: This book introduces new models based on R-calculus and theories of belief revision for dealing with large and changing data. It extends R-calculus from first-order logic to propositional logic, description logics, modal logic and logic programming, and from minimal change semantics to subset minimal change, pseudo-subformula minimal change and deduction-based minimal change (the last two minimal changes are newly defined). And it proves soundness and completeness theorems with respect to the minimal changes in these logics. To make R-calculus computable, an approximate R-calculus is given which uses finite injury priority method in recursion theory. Moreover, two applications of R-calculus are given to default theory and semantic inheritance networks.
This book offers a rich blend of theory and practice. It is suitable for students, researchers and practitioners in the field of logic. Also it is very useful for all those who are interested in data, digitization and correctness and consistency of information, in modal logics, non monotonic logics, decidable/undecidable logics, logic programming, description logics, default logics and semantic inheritance networks.Medieval logichttps://www.zbmath.org/1475.030042022-01-14T13:23:02.489162Z"Uckelman, Sara L."https://www.zbmath.org/authors/?q=ai:uckelman.sara-lThis article brings to light the unique contributions of medieval logicians to the history of logic by focusing on four topics: (1) The analysis of properties of terms; (2) theories of consequence; (3) the study of sophismata and insolubilia; and (4) disputationes de obligationibus. The article begins with a short description of the reception of Aristotle's logic in the middle ages and then discusses these four topics.
The discussion of the analysis of properties of terms focuses on two issues, signification and supposition. Signification accounts for the relation between a thing, its representation in the soul, and the speaker's association of a concept with its utterance. It also explains the distinction between terms that have a meaning in isolation (e.g. nouns and verbs) from those that do not (e.g. connectives such as `and', `or', `not', and `if', as well as quantifiers such as `all', `some', `none'). Supposition complements this account, by offering a mechanism for directly referring to things and not just to the concepts under which they fall. Medieval logicians distinguished three types of supposition: simple, where a word stands for what it signifies; material, where a word stands for the word itself (i.e. `man' is the three lettered word `man'), and formal, where a word stands for an actual individual thing.
Theories of consequence indiscriminately cover implication, inference, and entailment, and were approached from two viewpoints. (1) Logicians working in the English tradition offered an epistemic definition of consequence in terms of the containment of the consequent in the antecedent (e.g. if \(x\) is a man, \(x\) is an animal), a definition that reflects their understanding of logic as an applied science which should be understood in the context of its application. (2) Logicians of the continental tradition defined consequence in terms of modality and signification, characterizing it as a proposition whose antecedent cannot be true without its consequent being true.
The study of \textit{sophismata} and \textit{isolubilia} turns on sentences whose analysis leads to an apparent contradiction or sentences that admit two equality plausible analyses. The article discusses at length the most notable example of such sentences, the liar paradox. It classifies the attempts to solve this paradox into five families: (1) \textit{secundum quid et simpliciter}, whereby the liar's statement is false with no qualification (\textit{simpliciter}) but true `according to something' (\textit{secundum quid}); (2) \textit{transcasus}, whereby the sentence `I am speaking a falsehood' is not self-referntial, hence can be true or false; (3) a distinction between `exercised act', i.e. the claim that someone makes a statement (e.g. `Plato says that \dots'), and the `signified act', i.e. the statement itself (`Plato is saying something false'); (4) \textit{restrictio} whereby the liar paradox has no truth-value because it is self-referential; and (5) \textit{cassatio} whereby the paradoxical character of the sentence cancels its meaning and therefore it has no truth-value.
\textit{Disputations de obligationibus} are training exercises where an opponent presents a proposition and the respondent is obliged to concede, deny, or doubt. These exercises follow two general rules: (1) A relevant proposition should be conceded if it follows, and denied if its negation follows; (2) an irrelevant proposition should be conceded if it is known to be true, denied if it is known to be false, and doubted if it is neither known to be true nor known to be false.
This overview of medieval logic keeps it promise to show that during the thirteenth and fourteenth centuries logicians developed new insights regarding the nature of language and inference.
For the entire collection see [Zbl 1377.03003].
Reviewer: Orna Harari (Tel Aviv)Editors' introduction: Special issue on non-classical modal and predicate logicshttps://www.zbmath.org/1475.030052022-01-14T13:23:02.489162ZFrom the text: In this volume we present some of the latest work in non-classical modal and predicate logic and, sometimes, non-classical predicate logic with modal operators.Monotonicity in logic and language. Second Tsinghua interdisciplinary workshop on logic, language and meaning, TLLM 2020 Beijing, China, December 17--20, 2020. Proceedingshttps://www.zbmath.org/1475.030062022-01-14T13:23:02.489162ZThe articles of mathematical interest will be reviewed individually.Dynamic logic. New trends and applications. Third international workshop, Dalí 2020, Prague, Czech Republic, October 9--10, 2020. Revised selected papershttps://www.zbmath.org/1475.030072022-01-14T13:23:02.489162ZThe articles of this volume will be reviewed individually. For the preceding workshop see [Zbl 1430.03006].
Indexed articles:
\textit{Aucher, Guillaume}, Expedition in the update universe, 1-16 [Zbl 07437012]
\textit{Barbero, Fausto; Schulz, Katrin; Smets, Sonja; Velázquez-Quesada, Fernando R.; Xie, Kaibo}, Thinking about causation: a causal language with epistemic operators, 17-32 [Zbl 07437013]
\textit{Belardinelli, Gaia; Rendsvig, Rasmus K.}, Awareness logic: a Kripke-based rendition of the Heifetz-Meier-Schipper model, 33-50 [Zbl 07437014]
\textit{van den Berg, Line; Gattinger, Malvin}, Dealing with unreliable agents in dynamic gossip, 51-67 [Zbl 07437015]
\textit{Bílková, Marta; Frittella, Sabine; Majer, Ondrej; Nazari, Sajad}, Belief based on inconsistent information, 68-86 [Zbl 07437016]
\textit{Bolander, Thomas; Lequen, Arnaud}, Parameterized complexity of dynamic belief updates, 87-102 [Zbl 07437017]
\textit{Cassano, Valentin; Fervari, Raul; Areces, Carlos; Castro, Pablo F.}, Default modal systems as algebraic updates, 103-119 [Zbl 07437018]
\textit{van Ditmarsch, Hans; Liu, Mo; Kuijer, Louwe B.; Sedlár, Igor}, Expressivity of some versions of APAL, 120-136 [Zbl 07437019]
\textit{Hatano, Ryo; Sano, Katsuhiko}, Constructive dynamic logic of relation changers, 137-154 [Zbl 07437020]
\textit{Kuznetsov, Stepan}, Complexity of commutative infinitary action logic, 155-169 [Zbl 07437021]
\textit{Lorini, Emiliano; Song, Pengfei}, Grounding awareness on belief bases, 170-186 [Zbl 07437022]
\textit{Marin, Sonia; Pereira, Luiz Carlos; Pimentel, Elaine; Sales, Emerson}, Ecumenical modal logic, 187-204 [Zbl 07437023]
\textit{Punčochář, Vít}, Inquisitive dynamic epistemic logic in a non-classical setting, 205-221 [Zbl 07437024]
\textit{Reiche, Sebastian; Benzmüller, Christoph}, Public announcement logic in HOL, 222-238 [Zbl 07437025]
\textit{Solaki, Anthia}, Bounded multi-agent reasoning: actualizing distributed knowledge, 239-258 [Zbl 07437026]
\textit{Wáng, Yì N.; Ågotnes, Thomas}, Simpler completeness proofs for modal logics with intersection, 259-276 [Zbl 07437027]
\textit{Xiong, Zuojun; Ågotnes, Thomas}, Arbitrary propositional network announcement logic, 277-293 [Zbl 07437028]The challenge of many logics: a new approach to evaluating the role of ideology in Quinean commitmenthttps://www.zbmath.org/1475.030082022-01-14T13:23:02.489162Z"Azzouni, Jody"https://www.zbmath.org/authors/?q=ai:azzouni.jodySummary: Can Quine's criterion for ontological commitment be comparatively applied across different logics? If so, how? Cross-logical evaluations of discourses are central to contemporary philosophy of mathematics and metaphysics. The focus here is on the influential and important arguments of George Boolos and David Lewis that second-order logic and plural quantification don't incur additional ontological commitments over and above those incurred by first-order quantifiers. These arguments are challenged by the exhibition of a technical tool--the truncation-model construction of notational equivalents -- that compares the ontological role and increased expressive strength of non-first-order ideology to first-order ideology.A bitter pill for closurehttps://www.zbmath.org/1475.030092022-01-14T13:23:02.489162Z"Backes, Marvin"https://www.zbmath.org/authors/?q=ai:backes.marvinSummary: The primary objective of this paper is to introduce a new epistemic paradox that puts pressure on the claim that justification is closed under multi premise deduction. The first part of the paper will consider two well-known paradoxes -- the lottery and the preface paradox -- and outline two popular strategies for solving the paradoxes without denying closure. The second part will introduce a new, structurally related, paradox that is immune to these closure-preserving solutions. I will call this paradox, \textit{The Paradox of the Pill}. Seeing that the prominent closure-preserving solutions do not apply to the new paradox, I will argue that it presents a much stronger case against the claim that justification is closed under deduction than its two predecessors. Besides presenting a more robust counterexample to closure, the new paradox also reveals that the strategies that were previously thought to get closure out of trouble are not sufficiently general to achieve this task as they fail to apply to similar closure-threatening paradoxes in the same vicinity.Maximality and ontology: how axiom content varies across philosophical frameworkshttps://www.zbmath.org/1475.030102022-01-14T13:23:02.489162Z"Barton, Neil"https://www.zbmath.org/authors/?q=ai:barton.neil"Friedman, Sy-David"https://www.zbmath.org/authors/?q=ai:friedman.sy-davidSummary: Discussion of new axioms for set theory has often focused on conceptions of \textit{maximality}, and how these might relate to the iterative conception of set. This paper provides critical appraisal of how certain maximality axioms behave on different conceptions of ontology concerning the iterative conception. In particular, we argue that forms of multiversism (the view that any universe of a certain kind can be extended) and actualism (the view that there are universes that cannot be extended in particular ways) face complementary problems. The latter view is unable to use maximality axioms that make use of \textit{extensions}, where the former has to contend with the existence of extensions violating maximality axioms. An analysis of two kinds of multiversism, a Zermelian form and Skolemite form, leads to the conclusion that the \textit{kind} of maximality captured by an axiom differs substantially according to background ontology.Horizontal surgicality and mechanistic constitutionhttps://www.zbmath.org/1475.030112022-01-14T13:23:02.489162Z"Baumgartner, Michael"https://www.zbmath.org/authors/?q=ai:baumgartner.michael"Casini, Lorenzo"https://www.zbmath.org/authors/?q=ai:casini.lorenzo"Krickel, Beate"https://www.zbmath.org/authors/?q=ai:krickel.beateSummary: While ideal (surgical) interventions are acknowledged by many as valuable tools for the analysis of causation, recent discussions have shown that, since there are no ideal interventions on upper-level phenomena that non-reductively supervene on their underlying mechanisms, interventions cannot -- contrary to a popular opinion -- ground an informative analysis of constitution. This has led some to abandon the project of analyzing constitution in interventionist terms. By contrast, this paper defines the notion of a \textit{horizontally surgical intervention}, and argues that, when combined with some innocuous metaphysical principles about the relation between upper and lower levels of mechanisms, that notion delivers a sufficient condition for constitution. This, in turn, strengthens the case for an interventionist analysis of constitution.Truthmaker maximalism and the truthmaker paradoxhttps://www.zbmath.org/1475.030122022-01-14T13:23:02.489162Z"Brendel, Elke"https://www.zbmath.org/authors/?q=ai:brendel.elkeSummary: According to truthmaker maximalism, each truth has a truthmaker. Peter Milne has attempted to refute truthmaker maximalism on mere logical grounds via the construction of a self-referential truthmaker sentence M ``saying'' of itself that it doesn't have a truthmaker. Milne argues that M (similar to a Gödel sentence and different from a paradox-generating Liar sentence) turns out to be a true sentence without a truthmaker and thus provides a counterexample to truthmaker maximalism. In this paper, I show that Milne's refutation of truthmaker maximalism does not succeed. In particular, I argue that the notion of truthmaker meets two structural principles which, if added to a formal language of a theory (that allows for diagonalization), are already sufficient to produce a provable contradiction -- a contradiction that gives rise to a socalled ``Truthmaker paradox''. I also address the question of how to possibly resolve the Truthmaker paradox. I thereby show that the Truthmaker paradox, just as the strengthened Liar paradox, yields a ``revenge problem'' for paracomplete theories and might lead to triviality for Priest's dialetheist account LP if the notion of truthmaker is defined as a certain semantic predicate within LP. But regardless of how one tries to cope with the Truthmaker paradox, this paradox is surely interesting in its own right. However, its significance is completely orthogonal to the question of whether truthmaker maximalism is a philosophically sound view.Two roads to the successor axiomhttps://www.zbmath.org/1475.030132022-01-14T13:23:02.489162Z"Buijsman, Stefan"https://www.zbmath.org/authors/?q=ai:buijsman.stefanSummary: Most accounts of our knowledge of the successor axiom claim that this is based on the procedure of adding one. While they usually don't claim to provide an account of how children actually acquire this knowledge, one may well think that this is how they get that knowledge. I argue that when we look at children's responses in interviews, the time when they learn the successor axiom and the intermediate learning stages they find themselves in, that there is an empirically viable alternative. I argue that they could also learn it on the basis of a method that has to do with the structure of the numeral system. Specifically, that they (1) use the syntactic structure of the numeral system and (2) attend to the leftmost digits, the one with the highest place-value. Children can learn that this is a reliable method of forming larger numbers by combining two elements. First, a grasp of the syntactic structure of the numeral system. That way they know that the leftmost digit receives the highest value. Second, an interpretation of numerals as designating cardinal values, so that they also realise that increasing or adding digits on the lefthand side of a numeral produces a larger number. There are thus two, currently equally well-supported, ways in which children might learn that there are infinitely many natural numbers.Deflationary metaphysics and ordinary languagehttps://www.zbmath.org/1475.030142022-01-14T13:23:02.489162Z"Button, Tim"https://www.zbmath.org/authors/?q=ai:button.timSummary: Amie Thomasson and Eli Hirsch have both attempted to deflate metaphysics, by combining Carnapian ideas with an appeal to ordinary language. My main aim in this paper is to critique such deflationary appeals to ordinary language. Focussing on Thomasson, I draw two very general conclusions. First: ordinary language is a wildly complicated phenomenon. Its implicit ontological commitments can only be tackled by invoking a context principle; but this will mean that ordinary language ontology is not a trivial enterprise. Second: ordinary language often points in different directions simultaneously, so that a wide variety of existence questions cannot be deflated merely by appealing to ordinary language.Undoing things with wordshttps://www.zbmath.org/1475.030152022-01-14T13:23:02.489162Z"Caponetto, Laura"https://www.zbmath.org/authors/?q=ai:caponetto.lauraSummary: Over the last five decades, philosophers of language have looked into the mechanisms for doing things with words. The same attention has not been devoted to how to \textit{undo} those things, once they have been done. This paper identifies and examines three strategies to make one's speech acts undone -- namely, Annulment, Retraction, and Amendment. In annulling an act, a speaker brings to light its fatal flaws. Annulment amounts to \textit{recognizing} an act as null, whereas retraction and amendment amount to \textit{making} it null. Speakers employ retraction to cancel the deontic updates engendered by a given act. They instead use amendment to adjust its degree of strength. I will argue that \textit{annulling}, \textit{retracting}, and \textit{amending} are second-order speech acts, whose felicity conditions vary with the type of illocution they operate on. Undoing is therefore conceived of as a form of doing. Furthermore, I claim that, in calling off our acts, we undo the conventional or illocutionary effects of our words while leaving intact their past causal or perlocutionary outcomes.An epistemic approach to paraconsistency: a logic of evidence and truthhttps://www.zbmath.org/1475.030162022-01-14T13:23:02.489162Z"Carnielli, Walter"https://www.zbmath.org/authors/?q=ai:carnielli.walter-alexandre"Rodrigues, Abilio"https://www.zbmath.org/authors/?q=ai:rodrigues.abilioSummary: The purpose of this paper is to present a paraconsistent formal system and a corresponding intended interpretation according to which true contradictions are not tolerated. Contradictions are, instead, epistemically understood as conflicting evidence, where evidence for a proposition \(A\) is understood as reasons for believing that \(A\) is true. The paper defines a paraconsistent and paracomplete natural deduction system, called the \textit{Basic Logic of Evidence} (\textit{BLE}), and extends it to the \textit{Logic of Evidence and Truth} (\textit{LET}\(_{J}\)). The latter is a logic of formal inconsistency and undeterminedness that is able to express not only preservation of evidence but also preservation of truth. \(\textit{LET}_{J}\) is anti-dialetheist in the sense that, according to the intuitive interpretation proposed here, its consequence relation is trivial in the presence of any true contradiction. Adequate semantics and a decision method are presented for both \textit{BLE} and \(\textit{LET}_{J}\), as well as some technical results that fit the intended interpretation.Identity criteria: an epistemic path to conceptual groundinghttps://www.zbmath.org/1475.030172022-01-14T13:23:02.489162Z"Carrara, Massimiliano"https://www.zbmath.org/authors/?q=ai:carrara.massimiliano"De Florio, Ciro"https://www.zbmath.org/authors/?q=ai:de-florio.ciroSummary: Are identity criteria grounding principles? A \textit{prima facie} answer to this question is positive. Specifically, \textit{two-level identity criteria} can be taken as principles related to issues of identity among objects of a given kind compared with objects of a more basic kind. Moreover, they are grounding \textit{metaphysical} principles of some objects with regard to others. In the first part of the paper we criticise this \textit{prima facie} natural reading of identity criteria. This result does not mean that identity criteria could not be taken as \textit{grounding principles}. In the second part, we propose some basic steps towards a \textit{conceptual reading} of grounding. Such a way of understanding it goes along with an \textit{epistemic reading} of identity criteria.Nothingness, Meinongianism and inconsistent mereologyhttps://www.zbmath.org/1475.030182022-01-14T13:23:02.489162Z"Casati, Filippo"https://www.zbmath.org/authors/?q=ai:casati.filippo-gabrio-edoardo"Fujikawa, Naoya"https://www.zbmath.org/authors/?q=ai:fujikawa.naoyaSummary: Within the framework of Meinongianism, nothingness turns out to have contradictory features -- it seems to be an object and not. In this paper, we explore two different kinds of Meinongian accounts of nothingness. The first one is the \textit{consistent} account, which rejects the contradiction of nothingness, while the second one is the \textit{inconsistent} account, which accepts the contradiction of nothingness. First of all, after showing that the consistent account of nothingness defended by \textit{D. Jacquette} [``About nothing'', Humana Mente 6, No. 25, 95--118 (2013), \url{https://www.humanamente.eu/index.php/HM/article/view/136}] fails, we express some concerns on the general possibility of consistently characterizing nothingness. Secondly, starting from Priest's inconsistent characterization of nothingness [\textit{G. Priest}, One: Being an investigation into the unity of reality and of its part, including the singular object which is nothingness. Oxford: Oxford University Press (2014); Australas. J. Log. 11, No. 2, 146--158 (2014; Zbl 1330.03022)], we will introduce our own inconsistent account. The key idea of our account is to take nothingness as the complement of the totality. Finally, we will make formal sense of it by constructing an inconsistent mereological system, which is the development of the paraconsistent mereology proposed by \textit{Z. Weber} and \textit{A. J. Cotnoir} [Synthese 192, No. 5, 1267--1294 (2015; Zbl 1372.03051)].A partial consequence account of truthlikenesshttps://www.zbmath.org/1475.030192022-01-14T13:23:02.489162Z"Cevolani, Gustavo"https://www.zbmath.org/authors/?q=ai:cevolani.gustavo"Festa, Roberto"https://www.zbmath.org/authors/?q=ai:festa.robertoSummary: Popper's original definition of truthlikeness relied on a central insight: that truthlikeness combines truth and information, in the sense that a proposition is closer to the truth the more true consequences and the less false consequences it entails. As intuitively compelling as this definition may be, it is untenable, as proved long ago; still, one can arguably rely on Popper's intuition to provide an adequate account of truthlikeness. To this aim, we mobilize some classical work on partial entailment in defining a new measure of truthlikeness which satisfies a number of desiderata. The resulting account has some interesting and surprising connections with other accounts on the market, thus shedding new light on current attempts of systematizing different approaches to verisimilitude.Abductive inference within a pragmatic frameworkhttps://www.zbmath.org/1475.030202022-01-14T13:23:02.489162Z"Chiffi, Daniele"https://www.zbmath.org/authors/?q=ai:chiffi.daniele"Pietarinen, Ahti-Veikko"https://www.zbmath.org/authors/?q=ai:pietarinen.ahti-veikkoSummary: This paper presents an enrichment of the Gabbay-Woods schema of Peirce's 1903 logical form of abduction with illocutionary acts, drawing from logic for pragmatics and its resources to model justified assertions. It analyses the enriched schema and puts it into the perspective of Peirce's logic and philosophy.The constituents of an explicationhttps://www.zbmath.org/1475.030212022-01-14T13:23:02.489162Z"Cordes, Moritz"https://www.zbmath.org/authors/?q=ai:cordes.moritzSummary: The method of explication has been somewhat of a hot topic in the last 10 years. Despite the multifaceted research that has been directed at the issue, one may perceive a lack of step-by-step procedural or structural accounts of explication. This paper aims at providing a \textit{structural} account of the method of explication in continuation of the works of Geo Siegwart. It is enhanced with a detailed terminology for the assessment and comparison of explications. The aim is to provide means to talk about explications including their criticisms and their interrelations. There is hope that this treatment will be able to serve as a foundation to a step-by-step guide to be established for explicators. At least it should help to frame and mediate explicative disputes. In closing the enterprise will be considered an explication of `explication', though consecutive explications improving on this one are undoubtedly conceivable.Expressing `the structure of' in homotopy type theoryhttps://www.zbmath.org/1475.030222022-01-14T13:23:02.489162Z"Corfield, David"https://www.zbmath.org/authors/?q=ai:corfield.davidSummary: As a new foundational language for mathematics with its very different idea as to the status of logic, we should expect homotopy type theory to shed new light on some of the problems of philosophy which have been treated by logic. In this article, definite description, and in particular its employment within mathematics, is formulated within the type theory. Homotopy type theory has been proposed as an inherently structuralist foundational language for mathematics. Using the new formulation of definite descriptions, opportunities to express `the structure of' within homotopy type theory are explored, and it is shown there is little or no need for this expression.Is believing for a normative reason a composite condition?https://www.zbmath.org/1475.030232022-01-14T13:23:02.489162Z"Cunningham, J. J."https://www.zbmath.org/authors/?q=ai:cunningham.jessica-jSummary: Here is a surprisingly neglected question in contemporary epistemology: what is it for an agent to believe that p in response to a normative reason for them to believe that p? On one style of answer, believing for the normative reason that q factors into believing that p in the light of the apparent reason that q, where one can be in that kind of state even if q is false, in conjunction with further independent conditions such as q's being a normative reason to believe that p. The primary objective of this paper is to demonstrate that that style of answer cannot be right, because we must conceive of believing for a normative reason as constitutively involving a kind of rationality-involving relation that can be instantiated at all only if there is a known fact on the scene, which the agent treats as a normative reason. A secondary objective, achieved along the way, is to demonstrate that in their [``Prime time (for the basing relation)*'', in: Well-founded belief. London: Routledge. 141--173 (2019; \url{doi:10.4324/9781315145518-9})], \textit{E. Lord} and \textit{K. Sylvan} do not succeed in undermining the factoring picture in general, only a simple-minded version of it.The triviality argument against presentismhttps://www.zbmath.org/1475.030242022-01-14T13:23:02.489162Z"Deasy, Daniel"https://www.zbmath.org/authors/?q=ai:deasy.danielSummary: \textit{Presentism} is typically characterised as the thesis that \textit{everything (unrestrictedly) is present}, and therefore there are (quantifying unrestrictedly) no dinosaurs or Martian presidential inaugurations. Putting aside the vexed question of exactly what it is to be \textit{present} in this context (see [\textit{T. Williamson}, Modal logic as metaphysics. Oxford: Oxford University Press (2013; Zbl 1294.03008); \textit{R. P. Cameron}, ``On characterizing the presentism/eternalism and actualism/possibilism debates'', Anal. Philos. 57, No. 2, 110--140 (2016; \url{doi:10.1111/phib.12083}); the author, Nôus 51, No. 2, 378--397 (2017; Zbl 1432.03006)]), this thesis seems quite straightforward. However, a number of authors -- such as \textit{T. Merricks} [``On the incompatibility of enduring and perduring entities'', Mind 104, No. 415, 521--531 (1995; \url{doi:10.1093/mind/104.415.521})], \textit{U. Meyer} [``The triviality of presentism'', in: R. Cioni (ed.) et al., New papers on the present: Munich: Philosophia Verlag. 67--90 (2013)], \textit{J. C. Tallant} [``Defining existence presentism'', Erkenntnis 79, No. S3, 479--501 (2014; \url{doi:10.1007/s10670-013-9499-3})] and \textit{T. Sakon} [``Presentism and the triviality objection'', Philosophia 43, No. 4, 1089--1109 (2015; \url{doi:10.1007/s11406-015-9648-9})] -- have argued that Presentism so characterised is either trivially true or false even by Presentist lights. This is the so-called \textit{Triviality Argument} against Presentism. In this paper I show that three of the four premises of the Triviality Argument are plausibly false. I conclude that Presentists have nothing to fear from the Triviality Argument.On question-begging and analytic contenthttps://www.zbmath.org/1475.030252022-01-14T13:23:02.489162Z"Elgin, Samuel Z."https://www.zbmath.org/authors/?q=ai:elgin.samuel-zSummary: Among contemporary philosophers, there is widespread (but not universal) consensus that begging the question is a grave argumentative flaw. However, there is presently no satisfactory analysis of what this flaw consists of. Here, I defend a notion of question-begging in terms of analyticity. In particular, I argue that an argument begs the question just in case its conclusion is an analytic part of the conjunction of its premises.Impossible worlds and partial beliefhttps://www.zbmath.org/1475.030262022-01-14T13:23:02.489162Z"Elliott, Edward"https://www.zbmath.org/authors/?q=ai:elliott.edwardSummary: One response to the problem of logical omniscience in standard possible worlds models of belief is to extend the space of worlds so as to include impossible worlds. It is natural to think that essentially the same strategy can be applied to probabilistic models of partial belief, for which parallel problems also arise. In this paper, I note a difficulty with the inclusion of impossible worlds into probabilistic models. Under weak assumptions about the space of worlds, most of the propositions which can be constructed from possible and impossible worlds are in an important sense \textit{inexpressible}; leaving the probabilistic model committed to saying that agents in general have at least as many attitudes towards inexpressible propositions as they do towards expressible propositions. If it is reasonable to think that our attitudes are generally expressible, then a model with such commitments looks problematic.On the nature of presupposition: a normative speech act accounthttps://www.zbmath.org/1475.030272022-01-14T13:23:02.489162Z"García-Carpintero, Manuel"https://www.zbmath.org/authors/?q=ai:garcia-carpintero.manuelSummary: In this paper I provide a new account of linguistic presuppositions, on which they are ancillary speech acts defined by constitutive norms. After providing an initial intuitive characterization of the phenomenon, I present a normative speech act account of presupposition in parallel with Williamson's analogous account of assertion. I explain how it deals well with the problem of informative presuppositions, and how it relates to accounts for the Triggering and Projection Problems for presuppositions. I conclude with a brief discussion of the consequences of the proposal for the adequacy of Williamson's account of assertion.Four ways in which theories of belief revision could benefit from theories of epistemic justificationhttps://www.zbmath.org/1475.030282022-01-14T13:23:02.489162Z"Haas, Gordian"https://www.zbmath.org/authors/?q=ai:haas.gordianSummary: Belief revision theories aim to model the dynamics of epistemic states. Besides beliefs, epistemic states comprise most importantly justificational structures. Typically, belief revision theories, however, model the dynamics of beliefs while neglecting justificational structures over and above logical relations. Despite some awareness that this approach is problematic, how devastating the consequences of this neglect are has not yet been fully grasped. In this paper, I argue that taking justificational structures into account could solve four well-known problems of belief revision.What paradoxes depend onhttps://www.zbmath.org/1475.030292022-01-14T13:23:02.489162Z"Hsiung, Ming"https://www.zbmath.org/authors/?q=ai:hsiung.mingSummary: This paper gives a definition of self-reference on the basis of the dependence relation given by \textit{H. Leitgeb} [J. Philos. Log. 34, No. 2, 155--192 (2005; Zbl 1097.03005)], and the dependence digraph by \textit{T. Beringer} and \textit{T. Schindler} [in: The Logica yearbook 2015. Proceedings of the 29th annual international symposium Logica. London: College Publications. 1--15 (2016; Zbl 1423.03246)]. Unlike the usual discussion about self-reference of paradoxes centering around Yablo's paradox and its variants, I focus on the paradoxes of finitary characteristic, which are given again by use of Leitgeb's dependence relation. They are called `locally finite paradoxes', satisfying that any sentence in these paradoxes can depend on finitely many sentences. I prove that all locally finite paradoxes are self-referential in the sense that there is a directed cycle in their dependence digraphs. This paper also studies the `circularity dependence' of paradoxes, which was introduced by the author [Log. J. IGPL 22, No. 1, 24--38 (2014; Zbl 1343.03006)]. I prove that the locally finite paradoxes have circularity dependence in the sense that they are paradoxical only in the digraph containing a proper cycle. The proofs of the two results are based directly on König's infinity lemma. In contrast, this paper also shows that Yablo's paradox and its \(\forall \exists \)-unwinding variant are non-self-referential, and neither McGee's paradox nor the \(\omega\)-cycle liar has circularity dependence.The C account of assertion: a negative resulthttps://www.zbmath.org/1475.030302022-01-14T13:23:02.489162Z"Kelp, Christoph"https://www.zbmath.org/authors/?q=ai:kelp.christoph"Simion, Mona"https://www.zbmath.org/authors/?q=ai:simion.monaSummary: According to what Williamson labels `the C account of assertion', there is one and only one rule that is constitutive of assertion. This rule, the so-called `\textit{C Rule}', states that one must assert \(p\) only if \(p\) has property C. This paper argues that the C account of assertion is incompatible with any live proposal for C in the literature.Bad company objection to Joongol Kim's adverbial theory of numbershttps://www.zbmath.org/1475.030312022-01-14T13:23:02.489162Z"Kim, Namjoong"https://www.zbmath.org/authors/?q=ai:kim.namjoongSummary: In [Synthese 190, No. 6, 1099--1112 (2013; Zbl 1284.03065)], \textit{J. Kim} defends a logicist theory of numbers. According to him, numbers are adverbial entities, similar to those denoted by ``frequently'' and ``at 100\,mph''. He even introduces new adverbs for numbers: ``1-wise'', ``2-wise'', and so on. For example, ``Fs exist 2-wise'' means that there are (at least) two Fs. Kim claims that, because we can derive Dedekind-Peano axioms from his definition of numbers as adverbial entities, it is a new form of logicism. In this paper, I will, however, argue that his theory is vulnerable to an analogue of the so-called Bad Company objection to neo-Fregeanism. This means that we cannot be sure that numbers are actually given to us by Kim's definition; for, we don't know whether it is indeed a good definition. So, unless Kim, or somebody else, provides a demarcation criterion between good and bad adverbial definitions, Kim's theory will remain incomplete.On causality as the fundamental concept of Gödel's philosophyhttps://www.zbmath.org/1475.030322022-01-14T13:23:02.489162Z"Kovač, Srećko"https://www.zbmath.org/authors/?q=ai:kovac.sreckoSummary: This paper proposes a possible reconstruction and philosophical-logical clarification of Gödel's idea of causality as the philosophical fundamental concept. The results are based on Gödel's published and non-published texts (including Max Phil notebooks), and are established on the ground of interconnections of Gödel's dispersed remarks on causality, as well as on the ground of his general philosophical views. The paper is logically informal but is connected with already achieved results in the formalization of a causal account of Gödel's onto-theological theory. Gödel's main causal concepts are analysed (will, force, enjoyment, God, time and space, life, form, matter). Special attention is paid to a possible causal account of some of Gödel's logical concepts (assertion, privation, affirmation, negation, whole, part, general, particular, subject, predicate, necessary, possible, implication), as well as of logical antinomies. The problem of mechanical and non-mechanical procedures in the work with and on concepts is addressed in terms of Gödel's causal view.Refined nomic truth approximation by revising models and postulateshttps://www.zbmath.org/1475.030332022-01-14T13:23:02.489162Z"Kuipers, Theo A. F."https://www.zbmath.org/authors/?q=ai:kuipers.theo-a-fSummary: Assuming that the target of theory oriented empirical science in general and of nomic truth approximation in particular is to characterize the boundary or demarcation between nomic possibilities and nomic impossibilities, I have presented, in my article [ibid 193, No. 10, 3057--3077 (2016; Zbl 1384.03047)] the `basic' version of generalized nomic truth approximation, starting from `two-sided' theories. Its main claim is that nomic truth approximation can perfectly be achieved by combining two prima facie opposing views on theories: (1) the traditional (Popperian) view: theories are (models of) postulates that exclude certain possibilities from being realizable, enabling explanation and prediction and (2) the model view: theories are sets of models that claim to (approximately) represent certain realizable possibilities. Nomic truth approximation, i.e. increasing truth-content and decreasing falsity-content, becomes in this way revising theories by revising their models and/or their postulates in the face of increasing evidence. The basic version of generalized nomic truth approximation is in many respects as simple as possible. Among other things, it does not take into account that one conceptual possibility may be more similar (or closer) to another than a third one (is to that other). However, for example, one theory may include a possibility that is more similar to a wrongly not included possibility than another theory can offer. Similarly, for wrongly not excluded possibilities. In this article it will be shown that such `refined' considerations can be taken into account by adapted clauses based on a ternary similarity relation between possibilities (structures). This allows again abductive conclusions about refined truth approximation if a theory is persistently more successful in the refined sense than another. It will also be indicated and illustrated that this refined approach enables a specification to the effect that refined truth approximation can be obtained by the method of idealization and subsequent concretization. Finally, the basic and the refined approach will be evaluated with regard to some general principles and objections that have been discussed in the literature.Can we resolve the continuum hypothesis?https://www.zbmath.org/1475.030342022-01-14T13:23:02.489162Z"Lingamneni, Shivaram"https://www.zbmath.org/authors/?q=ai:lingamneni.shivaramSummary: I argue that contemporary set theory, as depicted in the 2011--2012 EFI lecture series, lacks a program that promises to decide, in a genuinely realist fashion, the continuum hypothesis (CH) and related questions about the ``width'' of the universe. We can distinguish three possible objectives for a realist completion of set theory: maximizing structures, maximizing sets, and maximizing interpretive power. However, none of these is allied to a program that can plausibly decide CH. I discuss the implications of this for set theory and other foundational programs.Existentialism, aliens and referentially unrestricted worldshttps://www.zbmath.org/1475.030352022-01-14T13:23:02.489162Z"Longenecker, Michael Tze-Sung"https://www.zbmath.org/authors/?q=ai:longenecker.michael-tze-sungSummary: Existentialism claims that propositions that directly refer to individuals depend on those individuals for their existence. I argue for two points regarding Existentialism. First, I argue that recent accounts of Existentialism run into difficulties accommodating the possibility of there being a lonely alien electron. This problem is distinct from one of the better-known alien problems -- concerning iterated modal properties of aliens -- and can't be solved using a standard response to the iterated case. Second, though the lonely alien electron problem might seem to be reason to reject the sort of Existentialist view at hand, there's a plausible way to preserve the view: accept the existence of possible worlds that directly refer to individuals that don't exist in those worlds. Such a solution might seem incompatible with Existentialism, but I show that Existentialists can avoid the incompatibility and should find the resulting view plausible.Existence predicateshttps://www.zbmath.org/1475.030362022-01-14T13:23:02.489162Z"Moltmann, Friederike"https://www.zbmath.org/authors/?q=ai:moltmann.friederikeSummary: The standard view about existence is that existence is a univocal concept conveyed by the existential quantifier. A less common philosophical view is that existence is a first-order property distinguishing between `nonexistent' and existing objects. An even less common philosophical view is that existence divides into different `modes of being' for different kinds of entities. Natural languages, this paper argues, generally distinguishes among different existence predicates for different types of entities, such as English `exist', `occur', and `obtain'. The paper gives an in-depth discussion and analysis of existence predicates in English within the general project of descriptive metaphysics, or more specifically `natural language ontology'.Truthlikeness: old and new debateshttps://www.zbmath.org/1475.030372022-01-14T13:23:02.489162Z"Niiniluoto, Ilkka"https://www.zbmath.org/authors/?q=ai:niiniluoto.ilkkaSummary: The notion of truthlikeness or verisimilitude has been a topic of intensive discussion ever since the definition proposed by Karl Popper was refuted in 1974. This paper gives an analysis of old and new debates about this notion. There is a fairly large agreement about the truthlikeness ordering of conjunctive theories, but the main rival approaches differ especially about false disjunctive theories. Continuing the debate between Niiniluoto's min-sum measure and Schurz's relevant consequence measure, the paper also gives a critical assessment of Oddie's new defense of the average measure and Kuipers' refined definition of truth approximation.Benacerraf, Field, and the agreement of mathematicianshttps://www.zbmath.org/1475.030382022-01-14T13:23:02.489162Z"Nutting, Eileen S."https://www.zbmath.org/authors/?q=ai:nutting.eileen-sSummary: Hartry Field's epistemological challenge to the mathematical platonist is often cast as an improvement on Paul Benacerraf's original epistemological challenge. I disagree. While Field's challenge is more difficult for the platonist to address than Benacerraf's, I argue that this is because Field's version is a special case of what I call the `sociological challenge'. The sociological challenge applies equally to platonists and fictionalists, and addressing it requires a serious examination of mathematical practice. I argue that the non-sociological part of Field's challenge amounts to a minor reformulation of Benacerraf's original challenge. So, I contend, Field's challenge is not an improvement on Benacerraf's. What is new to Field's challenge is as much a problem for the fictionalist as it is for the platonist.The reductio argument against epistemic infinitismhttps://www.zbmath.org/1475.030392022-01-14T13:23:02.489162Z"Oakley, Tim"https://www.zbmath.org/authors/?q=ai:oakley.timSummary: Epistemic infinitism, advanced in different forms by Peter Klein, Scott Aikin, and David Atkinson and Jeanne Peijnenburg, is the theory that justification of a proposition for a person requires the availability to that person of an infinite, non-repeating chain of propositions, each providing a justifying reason for its successor in the chain. The reductio argument is the argument to the effect that infinitism has the consequence that no one is justified in any proposition, because there will be an infinite chain of reasons supporting any proposition (and similarly, a chain supporting its negation). Four ways of defending infinitism against the reductio argument are considered and found wanting: Peijnenburg and Atkinson's use of probabilistic chains of reasons; Klein's concept of emergent justification; Aikin's insistence that there be non-propositional input in the justification of any proposition; and Klein's use of the distinction between reasons that are and are not available to a person. I contend that, in the absence of some further defence, the reductio argument makes infinitism untenable.Minimalism, supervaluations and fixed pointshttps://www.zbmath.org/1475.030402022-01-14T13:23:02.489162Z"Oms, Sergi"https://www.zbmath.org/authors/?q=ai:oms.sergiSummary: In this paper I introduce Horwich's deflationary theory of truth, called `Minimalism', and I present his proposal of how to cope with the Liar Paradox. The proposal proceeds by restricting the T-schema and, as a consequence of that, it needs a constructive specification of which instances of the T-schema are to be excluded from Minimalism. Horwich has presented, in an informal way, one construction that specifies the Minimalist theory. The main aim of the paper is to present and scrutinize some formal versions of Horwich's construction.Self-ascription and the \textit{de se}https://www.zbmath.org/1475.030412022-01-14T13:23:02.489162Z"Openshaw, James"https://www.zbmath.org/authors/?q=ai:openshaw.jamesSummary: This paper defends \textit{D. Lewis}' [``Attitudes de dicto and de se'', Philos. Rev. 88, No. 4, 513--543 (1979; \url{doi:10.2307/2184843})] influential treatment of \textit{de se} attitudes from recent criticism to the effect that a key explanatory notion -- \textit{self-ascription} -- goes unexplained [\textit{H. Cappelen} and \textit{J. Dever}, The inessential indexical. On the philosophical insignificance of perspective and the first person. Oxford: Oxford University Press (2013); \textit{R. Holton}, ``Primitive self-ascription: Lewis on the de se'', in: The Blackwell companion to David Lewis. Oxford: Blackwell. 399--410 (2015)]. It is shown that Lewis' treatment can be reconstructed in a way which provides clear responses. This sheds light on the explanatory ambitions of those engaged in Lewis' project.Atomic ontologyhttps://www.zbmath.org/1475.030422022-01-14T13:23:02.489162Z"Parisi, Andrew"https://www.zbmath.org/authors/?q=ai:parisi.andrewSummary: The aim of this article is to offer a method for determining the ontological commitments of a formalized theory. The second section shows that determining the consequence relation of a language model-theoretically entails that the ontology of a theory is tied very closely to the variables that feature in that theory. The third section develops an alternative way of determining the ontological commitments of a theory given a proof-theoretic account of the consequence relation for the language that theory is in. It is shown that the proof-theoretic account of ontological commitment does not entail that the ontological commitments of a theory depend on the variables of that theory. The last section of the article discusses how this account of ontological commitment can be used in other philosophical projects such as \textit{C. Wright}'s abstractionism [Frege's conception of numbers as objects. Aberdeen: Aberdeen University Press (1983; Zbl 0524.03005)]. The article concludes with a discussion of the upshots of adopting the proof-theoretic account of ontological commitment for ontology generally.Structured propositions and trivial compositionhttps://www.zbmath.org/1475.030432022-01-14T13:23:02.489162Z"Pickel, Bryan"https://www.zbmath.org/authors/?q=ai:pickel.bryanSummary: Structured propositions are often invoked to explain why intensionally equivalent sentences do not substitute salva veritate into attitude ascriptions. As the semantics is standardly developed -- for example, in [\textit{N. U. Salmon}, Frege's puzzle. Atascadero, CA: Ridgeview (1986); \textit{S. Soames}, ``Direct reference, propositional attitudes, and semantic content'', Philos. Top. 15, No. 1, 47--87 (1987; \url{doi:10.5840/philtopics198715112}); \textit{J. King}, J. Philos. Log. 25, No. 5, 495--521 (1996; Zbl 0875.03013)], the semantic value of a complex expression is an ordered complex consisting of the semantic values of its components. Such views, however, trivialize semantic composition since they do not allow for independent constraints on the meaning of complexes. Trivializing semantic composition risks ``trivializing semantics'' [\textit{J. King} and \textit{J. Stanley}, ``Semantics, pragmatics, and the role of semantic content'', in: Semantics versus pragmatics. Oxford: Oxford University Press. 111--164 (2005; \url{doi:10.1093/acprof:oso/9780199251520.003.0005})]. Yet, proponents of structured propositions suggest a route to reimpose substantive compositionality. While the mapping from a sentence to the structured proposition it expresses is trivially compositional, there is a non-trivial mapping from the structured proposition to its truth-value. This non-trivial level of semantic composition allows the meanings assigned to complex expressions to impose substantive constraints on the meanings of the simple ones. I first articulate the basic desiderata: an account of structured propositions capable of explaining attitude attributions and of delivering a non-trivially compositional semantics. I then show that the two-stage semantics proposed by standard proponents of structured propositions does not satisfy these joint goals.Bolzano and Kim on grounding and unificationhttps://www.zbmath.org/1475.030442022-01-14T13:23:02.489162Z"Roski, Stefan"https://www.zbmath.org/authors/?q=ai:roski.stefanSummary: It is sometimes mentioned that Bernard Bolzano's work on grounding anticipates many insights of the current debate on metaphysical grounding. The present paper discusses a certain part of Bolzano's theory of grounding that has thus far not been discussed in the literature. This part does not so much anticipate what are nowadays common assumptions about grounding, but rather goes beyond them. Central to the discussion will be a thesis of Bolzano's by which he tries to establish a connection between grounding and (deductive) unification. The paper spells out this thesis in detail and discusses the assumptions on which it rests. Next to this mainly historical aim, the paper also presents reasons why philosophers who are not interested in the historical Bolzano should find the thesis interesting by relating it to a certain view on unification and explanation that has been put forward by Kim. A final part of the paper provides a critical evaluation of the thesis against the background of current accounts of grounding.Reverse formalism 16https://www.zbmath.org/1475.030452022-01-14T13:23:02.489162Z"Sanders, Sam"https://www.zbmath.org/authors/?q=ai:sanders.samSummary: In his remarkable paper \textit{A. Robinson} [in: Proceedings of the 1964 international congress on logic, methodology and philosophy of science. Amsterdam: Elsevier/North-Holland. 228--246 (1965; Zbl 0199.00204)], Robinson defends his eponymous position concerning the foundations of mathematics, as follows: Any mention of infinite totalities is literally meaningless. We should act as if infinite totalities really existed. Being the originator of \textit{Nonstandard Analysis}, it stands to reason that Robinson would have often been faced with the opposing position that `some infinite totalities are more meaningful than others', the textbook example being that of infinitesimals (versus less controversial infinite totalities). For instance, Bishop and Connes have made such claims regarding infinitesimals, and Nonstandard Analysis in general, going as far as calling the latter respectively a \textit{debasement of meaning} and \textit{virtual}, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate `meaning' and `computational content', though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the absence of meaning (i.e. computational content). We will debunk the Bishop-Connes critique by establishing the contrary, namely that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the \textit{ubiquitous presence} of computational content. In particular, infinitesimals provide an \textit{elegant shorthand} for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content (not involving Nonstandard Analysis), similar to the `reversals' from the foundational program \textit{Reverse Mathematics}. The latter also plays an important role in gauging the scope of this translation.An indeterminate universe of setshttps://www.zbmath.org/1475.030462022-01-14T13:23:02.489162Z"Scambler, Chris"https://www.zbmath.org/authors/?q=ai:scambler.chrisSummary: In this paper, I develop a view on set-theoretic ontology I call \textit{Universe-Indeterminism}, according to which there is a unique but indeterminate universe of sets. I argue that Solomon Feferman's work on semi-constructive set theories can be adapted to this project, and develop a philosophical motivation for a semi-constructive set theory closely based on Feferman's but tailored to the \textit{Universe-Indeterminist's} viewpoint. I also compare the emergent \textit{Universe-Indeterminist} view to some more familiar views on set-theoretic ontology.A note on Horwich's notion of groundinghttps://www.zbmath.org/1475.030472022-01-14T13:23:02.489162Z"Schindler, Thomas"https://www.zbmath.org/authors/?q=ai:schindler.thomasSummary: In [Deflationism and paradox. Oxford: Oxford University Press. 75--84 (2005)], \textit{P. Horwich} proposes a solution to the liar paradox that relies on a particular notion of grounding -- one that, unlike \textit{S. Kripke}'s notion of grounding [J. Philos. 72, 690--716 (1975; Zbl 0952.03513)], does not invoke any ``Tarski-style compositional principles''. In this short note, we will formalize Horwich's construction and argue that his solution to the liar paradox does not justify certain generalizations about truth that he endorses. We argue that this situation is not resolved even if one appeals to the \(\omega\)-rule. In the final section, we briefly discuss how Horwich might respond to the situation.Grounding and dependencehttps://www.zbmath.org/1475.030482022-01-14T13:23:02.489162Z"Schnieder, Benjamin"https://www.zbmath.org/authors/?q=ai:schnieder.benjaminSummary: The paper deals with the notions of grounding and of existential dependence. It is shown that cases of existential dependence seem to be systematically correlated to cases of grounding and hence the question is raised what sort of tie might hold the two notions together so as to account for the observed correlation. The paper focusses on three possible ties between grounding and existential dependence: identity (as suggested in Jonathan Schaffer's works), definition (as suggested by Fabrice Correia and Benjamin Schnieder), and grounding (as suggested by Kathrin Koslicki and Francesco Orilia). A case for the definitional tie is made.Twelve great papers: comments and replies. Response to a special issue on logical perspectives on science and cognition -- the philosophy of Gerhard Schurzhttps://www.zbmath.org/1475.030492022-01-14T13:23:02.489162Z"Schurz, Gerhard"https://www.zbmath.org/authors/?q=ai:schurz.gerhardSummary: This is a response to the papers in the special issue \textit{Logical Perspectives on Science and Cognition} -- \textit{The Philosophy of Gerhard Schurz}.The bifurcated conception of perceptual knowledge: a new solution to the basis problem for epistemological disjunctivismhttps://www.zbmath.org/1475.030502022-01-14T13:23:02.489162Z"Shaw, Kegan J."https://www.zbmath.org/authors/?q=ai:shaw.kegan-jSummary: Epistemological disjunctivism says that one can know that \(p\) on the rational basis of one's seeing that \(p\). The basis problem for disjunctivism says that that can't be since seeing that \(p\) entails knowing that \(p\) on account of simply being the way in which one knows that \(p\). In defense of their view disjunctivists have rejected the idea that seeing that \(p\) is just a way of knowing that \(p\) (the \(\mathrm{S_wK}\) thesis). That manoeuvre is familiar. In this paper I explore the prospects for rejecting instead the thought that \textit{if} the \(\mathrm{S_wK}\) thesis is true then seeing that \(p\) can't be one's rational basis for perceptual knowledge. I explore two strategies. The first situates disjunctivism within the context of a 'knowledge-first' approach that seeks to reverse the traditional understanding of the relationship between perceptual knowledge and justification (or rational support). But I argue that a more interesting strategy situates disjunctivism within a context that accepts a more nuanced understanding of perceptual beliefs. The proposal that I introduce reimagines disjunctivism in light of a bifurcated conception of perceptual knowledge that would see it cleaved along two dimensions. On the picture that results perceptual knowledge at the judgemental level is rationally supported by perceptual knowledge at the merely functional or `animal' level. This supports a form of disjunctivism that I think is currently off the radar: one that's consistent \textit{both }with the \(\mathrm{S_wK}\) thesis \textit{and} a commitment to a traditional reductive account of perceptual knowledge.Why is the universe of sets not a set?https://www.zbmath.org/1475.030512022-01-14T13:23:02.489162Z"Soysal, Zeynep"https://www.zbmath.org/authors/?q=ai:soysal.zeynepSummary: According to the iterative conception of sets, standardly formalized by ZFC, there is no set of all sets. But why is there no set of all sets? A simple-minded, though unpopular, ``minimal'' explanation for why there is no set of all sets is that the supposition that there is contradicts some axioms of ZFC. In this paper, I first explain the core complaint against the minimal explanation, and then argue against the two main alternative answers to the guiding question. I conclude the paper by outlining a close alternative to the minimal explanation, the conception-based explanation, that avoids the core complaint against the minimal explanation.Defeasible normative reasoninghttps://www.zbmath.org/1475.030522022-01-14T13:23:02.489162Z"Spohn, Wolfgang"https://www.zbmath.org/authors/?q=ai:spohn.wolfgangSummary: The paper is motivated by the need of accounting for the practical syllogism as a piece of defeasible reasoning. To meet the need, the paper first refers to ranking theory as an account of defeasible descriptive reasoning. It then argues that two kinds of ought need to be distinguished, purely normative and fact-regarding obligations (in analogy to intrinsic and extrinsic utilities). It continues arguing that both kinds of ought can be iteratively revised and should hence be represented by ranking functions, too, just as iteratively revisable beliefs. Its central proposal will then be that the fact-regarding normative ranking function must be conceived as the sum of a purely normative ranking function and an epistemic ranking function (as suggested in qualitative decision theory). The distinctions defends this proposal with a comparative discussion of some critical examples and some other distinctions made in the literature. It gives a more rigorous justification of this proposal. Finally, it starts developing the logic of purely normative and of fact-regarding normative defeasible reasoning, points to the difficulties of completing the logic of the fact-regarding side, but reaches the initial aim of accounting for the defeasible nature of the practical syllogism.Pleonastic propositions and the face value theoryhttps://www.zbmath.org/1475.030532022-01-14T13:23:02.489162Z"Steinberg, Alex"https://www.zbmath.org/authors/?q=ai:steinberg.alexSummary: Propositions are a useful tool in philosophical theorizing, even though they are not beyond reasonable nominalistic doubts. Stephen Schiffer's pleonasticism about propositions is a paradigm example of a realistic account that tries to alleviate such doubts by grounding truths about propositions in ontologically innocent facts. Schiffer maintains two characteristic theses about propositions: first, that they are so-called pleonastic entities whose existence is subject to what he calls something-from-nothing transformations (pleonasticism); and, second, that they are the referents of `that'-clauses that function as singular terms in propositional attitude ascriptions (the face value theory). The paper turns the first thesis against the second: if propositions are pleonastic entities, it is argued, we should not take them to be referred to in propositional attitude ascriptions. Rather, propositional attitude ascriptions should be available as bases for propositional something-from-nothing transformations.Plurivaluationism, supersententialism and the problem of the many languageshttps://www.zbmath.org/1475.030542022-01-14T13:23:02.489162Z"Sud, Rohan"https://www.zbmath.org/authors/?q=ai:sud.rohanSummary: According to the plurivaluationist, our vague discourse doesn't have a single meaning. Instead, it has many meanings, each of which is precise -- and it is this plurality of meanings that is the source of vagueness. I believe plurivaluationist positions are underdeveloped and for this reason unpopular. This paper attempts to correct this situation by offering a particular development of plurivaluationism that I call supersententialism. The supersententialist leverages lessons from another area of research -- the Problem of the Many -- in service of the plurivaluationist position. The Problem reveals theoretical reasons to accept that there are many cats where we thought there was one; the supersententialist claims that we are in a similar situation with respect to languages, propositions and sentences. I argue that the parallel suggested by the supersententialist reveals unappreciated advantages and lines of defense for plurivaluationism.A meaning explanation for HoTThttps://www.zbmath.org/1475.030552022-01-14T13:23:02.489162Z"Tsementzis, Dimitris"https://www.zbmath.org/authors/?q=ai:tsementzis.dimitrisSummary: In the Univalent Foundations of mathematics spatial notions like ``point'' and ``path'' are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory (as a formalism for the Univalent Foundations) can be justified intuitively as a theory of shapes in the same way that ZFC (as a formalism for set-theoretic foundations) can be justified intuitively as a theory of collections. I first clarify what such an ``intuitive justification'' should be by distinguishing between formal and pre-formal ``meaning explanations'' in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like ``shape'', ``path'' etc.The neo-Carnapianshttps://www.zbmath.org/1475.030562022-01-14T13:23:02.489162Z"van Inwagen, Peter"https://www.zbmath.org/authors/?q=ai:van-inwagen.peterSummary: This essay defends the neo-Quinean approach to ontology against the criticisms of two neo-Carnapians, Huw Price and Amie Thomasson.Ambiguous signals, partial beliefs, and propositional contenthttps://www.zbmath.org/1475.030572022-01-14T13:23:02.489162Z"Ventura, Rafael"https://www.zbmath.org/authors/?q=ai:ventura.rafaelSummary: As the content of propositional attitudes, propositions are usually taken to help explain the behavior of rational agents. However, a closer look at signaling games suggests otherwise: rational agents often acquire partial beliefs, and many of their signals are ambiguous. Signaling games also suggest that it is rational for agents to mix their behavior in response to partial beliefs and ambiguous signals. But as I show in this paper, propositions cannot help explain the mixing behavior of rational agents: to explain mixing behavior, we need a probabilistic notion of content. I also show that a probabilistic notion of content renders propositions explanatorily idle in the case of unambiguous signals and full beliefs as well. My suggestion is thus that we should abandon propositions in explanations of rational behavior and adopt instead a probabilistic notion of content. The notion of probabilistic content ultimately provides a simpler framework for explanations of rational behavior than the notion of propositional content.A metasemantic challenge for mathematical determinacyhttps://www.zbmath.org/1475.030582022-01-14T13:23:02.489162Z"Warren, Jared"https://www.zbmath.org/authors/?q=ai:warren.jared"Waxman, Daniel"https://www.zbmath.org/authors/?q=ai:waxman.danielSummary: This paper investigates the determinacy of mathematics. We begin by clarifying how we are understanding the notion of determinacy (Sect. 1) before turning to the questions of whether and how famous independence results bear on issues of determinacy in mathematics (Sect. 2). From there, we pose a metasemantic challenge for those who believe that mathematical language is determinate (Sect. 3), motivate two important constraints on attempts to meet our challenge (Sect. 4), and then use these constraints to develop an argument against determinacy (Sect. 5) and discuss a particularly popular approach to resolving indeterminacy (Sect. 6), before offering some brief closing reflections (Sect. 7). We believe our discussion poses a serious challenge for most philosophical theories of mathematics, since it puts considerable pressure on all views that accept a non-trivial amount of determinacy for even basic arithmetic.Back to the actual futurehttps://www.zbmath.org/1475.030592022-01-14T13:23:02.489162Z"Wawer, Jacek"https://www.zbmath.org/authors/?q=ai:wawer.jacek"Malpass, Alex"https://www.zbmath.org/authors/?q=ai:malpass.alexSummary: The purpose of the paper is to rethink the role of actuality in the branching model of possibilities. We investigate the idea that the model should be enriched with an additional factor -- the so-called Thin Red Line -- which is supposed to represent the single possible course of events that gets actualized in time. We believe that this idea was often misconceived which prompted some unfortunate reactions. On the one hand, it suggested problematic semantic models of future tense and and on the other, it provoked questionable lines of criticism. We reassess the debate and point to potential pitfalls, focusing on the semantic dimension of the Thin Red Line theory. Our agenda transcends the semantics, however. We conclude that semantic considerations do not threaten the Thin Red Line theory and that the proper debate should be carried in the domain of metaphysics.A new proposal how to handle counterexamples to Markov causation à la Cartwright, or: fixing the chemical factoryhttps://www.zbmath.org/1475.030602022-01-14T13:23:02.489162Z"Gebharter, Alexander"https://www.zbmath.org/authors/?q=ai:gebharter.alexander"Retzlaff, Nina"https://www.zbmath.org/authors/?q=ai:retzlaff.ninaSummary: In [``Causal diversity and the Markov condition'', Synthese 121, No. 1--2, 3--27 (1999); The dappled world. A study of the boundaries of science. Cambridge: Cambridge University Press (1999; Zbl 1003.00005)], \textit{N. Cartwright} attacked the view that causal relations conform to the Markov condition by providing a counterexample in which a common cause does not screen off its effects: the prominent chemical factory. In this paper we suggest a new way to handle counterexamples to Markov causation such as the chemical factory. We argue that Cartwright's as well as similar scenarios (such as decay processes, EPR/B experiments, or spontaneous macro breaking processes) feature a certain kind of non-causal dependence that kicks in once the common cause occurs. We then develop a representation of this specific kind of non-causal dependence that allows for modeling the problematic scenarios in such a way that the Markov condition is not violated anymore.Correction to: ``Ontological commitments of frame-based knowledge representations''https://www.zbmath.org/1475.030612022-01-14T13:23:02.489162Z"Hommen, David"https://www.zbmath.org/authors/?q=ai:hommen.davidSummary: In [ibid. 196, No. 10, 4155--4183 (2019; Zbl 1474.03062)], I refer to the work of \textit{R. K. Garcia} [``Is trope theory a divided house?'', in: The problem of universals in contemporary philosophy. Cambridge: Cambridge University Press. 133--155 (2015); ``Two ways to particularize a property'', J. Am. Philos. Assoc. 1, No. 4, 635--652 (2015; \url{doi:10.1017/apa.2015.21})]. In this addendum, I would like to supplement additional references to these papers.On the empirical inaccessibility of higher-level modality and its significance for cosmological fine-tuninghttps://www.zbmath.org/1475.030622022-01-14T13:23:02.489162Z"Juhl, Cory"https://www.zbmath.org/authors/?q=ai:juhl.cory-f"Knab, Brian"https://www.zbmath.org/authors/?q=ai:knab.brianSummary: In this paper we propose that cosmological fine-tuning arguments, when levied in support of the existence of Intelligent Designers or Multiverses, are much less interesting than they are thought to be. Our skepticism results from tracking the distinction between merely epistemic or logical possibilities on one hand and nonepistemic possibilities, such as either nomological or metaphysical possibilities, on the other. We find that fine-tuning arguments readily conflate epistemic or logical possibilities with nonepistemic possibilities and we think that this leads to treating the search for an explanation of fine-tuning as analogous to standard empirical theorizing about first-order nomological matters, when in fact the two investigational enterprises are profoundly different. Similar conflation occurs when fine-tuning arguments do not carefully distinguish between different interpretations of probabilities within the arguments. Finally, these arguments often rely on spatial analogies, which are often misleading precisely in that they encourage the conflation of epistemic and nonepistemic possibility. When we pay attention to the distinctions between merely epistemic versus nonepistemic modalities and probabilities, the extant arguments in favor of intelligent designers or multiverses, or even for the nonepistemic improbability of fine-tuning, consist of empirically unconstrained (beyond what is entailed by facts about the actual universe) speculation concerning relevant nonepistemic modal facts.Armchair philosophy naturalizedhttps://www.zbmath.org/1475.030632022-01-14T13:23:02.489162Z"Lutz, Sebastian"https://www.zbmath.org/authors/?q=ai:lutz.sebastianSummary: Carnap suggests that philosophy can be construed as being engaged solely in conceptual engineering. I argue that since many results of the sciences can be construed as stemming from conceptual engineering as well, Carnap's account of philosophy can be methodologically naturalistic. This is also how he conceived of his account. That the sciences can be construed as relying heavily on conceptual engineering is supported by empirical investigations into scientific methodology, but also by a number of conceptual considerations. I present a new conceptual consideration that generalizes Carnap's conditions of adequacy for analytic-synthetic distinctions and thus widens the realm in which conceptual engineering can be used to choose analytic sentences. I apply these generalized conditions of adequacy to a recent analysis of scientific theories and defend the relevance of the analytic-synthetic distinction against criticisms by Quine, Demopoulos, and Papineau.Constrained pseudo-propositional logichttps://www.zbmath.org/1475.030642022-01-14T13:23:02.489162Z"Azizi-Sultan, Ahmad-Saher"https://www.zbmath.org/authors/?q=ai:azizi-sultan.ahmad-saherThe authors consider the constrained pseudo-propositional logic (CPPL), based on pseudo-propositional logic, formulating counting constraints naturally, but keeping its Boolean nature preserved. CPPL is capable of encoding counting constraints, as well as SAT instances, much more succinctly than having them being encoded using conjunctive normal form. Solving SAT problem in CPPL allows for assigning truth values to a variety of propositional variables simultaneously. The resulting calculus in CPPL is similar to the cutting planes proof systems, but in distinction to it, CPPL does not require the set of linear inequalities to be finite. Although this restriction is made dispensable, CPPL is maintained to be sound and complete.
Reviewer: Branislav Boričić (Beograd)Classical harmony and separabilityhttps://www.zbmath.org/1475.030652022-01-14T13:23:02.489162Z"Murzi, Julien"https://www.zbmath.org/authors/?q=ai:murzi.julienSummary: According to logical inferentialists, the meanings of logical expressions are fully determined by the rules for their correct use. Two key proof-theoretic requirements on admissible logical rules, harmony and separability, directly stem from this thesis -- requirements, however, that standard single-conclusion and assertion-based formalizations of classical logic provably fail to satisfy [\textit{M. Dummett}, The logical basis of metaphysics. Harvard, MA: Harvard University Press (1991); \textit{D. Prawitz}, Theoria 43, 2--40 (1977; Zbl 0361.02008); \textit{N. Tennant}, The taming of the true. Oxford: Clarendon Press (1997; Zbl 0929.03001); Humberstone and Makinson, ``Intuitionistic logic and elementary rules'', Mind 120, No. 480, 1035--1051 (2011)]. On the plausible assumption that our logical practice is both single-conclusion and assertion-based, it seemingly follows that classical logic, unlike intuitionistic logic, can't be accounted for in inferentialist terms. In this paper, I challenge orthodoxy and introduce an assertion-based and single-conclusion formalization of classical propositional logic that is both harmonious and separable. In the framework I propose, classicality emerges as a structural feature of the logic.The modality and non-extensionality of the quantifiershttps://www.zbmath.org/1475.030662022-01-14T13:23:02.489162Z"Koslow, Arnold"https://www.zbmath.org/authors/?q=ai:koslow.arnoldSummary: We shall try to defend two non-standard views that run counter to two well-entrenched familiar views. The standard views are (1) the universal and existential quantifiers of first-order logic are not modal operators, and (2) the quantifiers are extensional. If that is correct then the counterclaims create genuine problems for some traditional philosophical doctrines.Possible predicates and actual propertieshttps://www.zbmath.org/1475.030672022-01-14T13:23:02.489162Z"Cook, Roy T."https://www.zbmath.org/authors/?q=ai:cook.roy-tSummary: In [Philos. Math. (3) 21, No. 2, 133--156 (2013; Zbl 1293.03007)], \textit{B. Hale} develops and defends a deflationary conception of properties where a property with particular satisfaction conditions actually (and in fact necessarily) exists if and only if it is possible that a predicate with those same satisfaction conditions exists. He argues further that, since our languages are finitary, there are at most countably infinitely many properties and, as a result, the account fails to underwrite the standard semantics for second-order logic. Here a more lenient version of the view is explored, which allows for the possibility of countably infinite predicates understood as the product of linguistic supertasks. This enriched deflationist account of properties -- the Infinitary Deflationary Conception of Existence -- supports the standard semantics for models with countable first-order domains, and allows one to prove the categoricity of the second-order Peano axioms.Second-order logic: properties, semantics, and existential commitmentshttps://www.zbmath.org/1475.030682022-01-14T13:23:02.489162Z"Hale, Bob"https://www.zbmath.org/authors/?q=ai:hale.bobSummary: Quine's most important charge against second-, and more generally, higher-order logic is that it carries massive existential commitments. The force of this charge does not depend upon Quine's questionable assimilation of second-order logic to set theory. Even if we take second-order variables to range over properties, rather than sets, the charge remains in force, as long as properties are individuated purely extensionally. I argue that if we interpret them as ranging over properties more reasonably construed, in accordance with an abundant or deflationary conception, Quine's charge can be resisted. This interpretation need not be seen as precluding the use of model-theoretic semantics for second-order languages; but it will preclude the use of the standard semantics, along with the more general Henkin semantics, of which it is a special case. To that extent, the approach I recommend has revisionary implications which some may find unpalatable; it is, however, compatible with the quite different special case in which the second-order variables are taken to range over definable subsets of the first-order domain, and with respect to such a semantics, some important metalogical results obtainable under the standard semantics may still be obtained. In my final section, I discuss the relations between second-order logic, interpreted as I recommend, and a strong version of schematic ancestral logic promoted in recent work by Richard Heck. I argue that while there is an interpretation on which Heck's logic can be contrasted with second-order logic as standardly interpreted, when it is so interpreted, its differences from the more modest form of second-order logic I advocate are much less substantial, and may be largely presentational.Fixed-point elimination in the intuitionistic propositional calculushttps://www.zbmath.org/1475.030692022-01-14T13:23:02.489162Z"Ghilardi, Silvio"https://www.zbmath.org/authors/?q=ai:ghilardi.silvio"Gouveia, Maria João"https://www.zbmath.org/authors/?q=ai:gouveia.maria-joao"Santocanale, Luigi"https://www.zbmath.org/authors/?q=ai:santocanale.luigiSummary: It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras -- that is, the algebraic models of the intuitionistic propositional calculus -- always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the \(\mu\)-calculus based on intuitionistic logic is trivial, every \(\mu\)-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given \(\mu\)-formula. The axiomatization of the greatest fixed-pointis simple. The axiomatization of the least fixed-pointis more complex, in particular every monotone formula converges to its least fixed-pointby Kleene's iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such \(n\), depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.
For the entire collection see [Zbl 1333.68011].Truths, inductive definitions, and Kripke-Platek systems over set theoryhttps://www.zbmath.org/1475.030702022-01-14T13:23:02.489162Z"Fujimoto, Kentaro"https://www.zbmath.org/authors/?q=ai:fujimoto.kentaroThe author studies two truth theories -- KF of Kripke and Feferman, and Cantini's VF -- over set theory. It is ``shown that KF and VF are proof-theoretically equivalent over ZF and thus have the same set-theoretic consequences, whereas the former is significantly weaker than the latter over PA'' (p. 869).
Reviewer: Reinhard Kahle (Lisboa)Using Ramsey's theorem oncehttps://www.zbmath.org/1475.030712022-01-14T13:23:02.489162Z"Hirst, Jeffry L."https://www.zbmath.org/authors/?q=ai:hirst.jeffry-l"Mummert, Carl"https://www.zbmath.org/authors/?q=ai:mummert.carlThe paper studies the question of how many applications of one principle are needed to prove another in the context of higher-order reverse mathematics, and its connections to Weihrauch reducibility. The base theory is taken to be \(i\mathsf{RCA}^\omega_0\), consisting of Feferman's system \(\widehat{\mathsf{E\text-HA}}^\omega_\restriction\) of intuitionistic arithmetic of all finite types and the quantifier-free choice schema \(\mathsf{QF\text-AC}^{1,0}\); the extension of this theory to classical logic is the theory \(\mathsf{RCA}^\omega_0\) of \textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)].
Considering problems \(P\) of the form \(\forall x\,(p_1(x)\to\exists y\,p_2(x,y))\), the authors define a natural notion that a theory \(T\supseteq i\mathsf{RCA}^\omega_0\) proves a problem \(Q\) with ``one typical use'' of \(P\). They also consider a formal version \(T\vdash Q\le_WP\) of Weihrauch reducibility between such problems (which differs from actual Weihrauch reducibility \(Q\le_WP\) in that the reduction functionals are not a priori required to be computable).
The main general results are that under suitable syntactic restrictions on \(P\) and \(Q\), \(i\mathsf{RCA}^\omega_0\) proves \(Q\) with one typical use of \(P\) iff \(i\mathsf{RCA}^\omega_0\vdash Q\le_WP\), and that this implies \(Q\le_WP\).
As an application, the paper looks on dependencies between the Ramsey principles \(\mathsf{RT}(n,k)\), asserting that any \(k\)-colouring of \([\mathbb N]^n\) has an infinite monochromatic set. They show that even though \(i\mathsf{RCA}^\omega_0\vdash\mathsf{RT}(2,2)\to\mathsf{RT}(2,4)\), \(i\mathsf{RCA}^\omega_0\) cannot prove \(\mathsf{RT}(2,4)\) with only one typical use of \(\mathsf{RT}(2,2)\), using known results on Weihrauch reducibility between these problems. More generally, for any \(n\ge1\) and \(k>j\ge2\), \(i\mathsf{RCA}^\omega_0\) does not prove \(\mathsf{RT}(n,k)\) with only one typical use of \(\mathsf{RT}(n,j)\).
Surprisingly, the classical theory \(\mathsf{RCA}^\omega_0\) \textit{does} prove \(\mathsf{RT}(2,4)\) with one typical use of \(\mathsf{RT}(2,2)\): the authors show this by a clever use of excluded middle to distinguish whether there exists an infinite bichromatic set or not. More generally, \(\mathsf{RCA}^\omega_0\) proves \(\mathsf{RT}(n,k)\) with one typical use of \(\mathsf{RT}(n,2)\).
Reviewer: Emil Jeřábek (Praha)Interpolant synthesis for quadratic polynomial inequalities and combination with EUFhttps://www.zbmath.org/1475.030722022-01-14T13:23:02.489162Z"Gan, Ting"https://www.zbmath.org/authors/?q=ai:gan.ting"Dai, Liyun"https://www.zbmath.org/authors/?q=ai:dai.liyun"Xia, Bican"https://www.zbmath.org/authors/?q=ai:xia.bican"Zhan, Naijun"https://www.zbmath.org/authors/?q=ai:zhan.naijun"Kapur, Deepak"https://www.zbmath.org/authors/?q=ai:kapur.deepak"Chen, Mingshuai"https://www.zbmath.org/authors/?q=ai:chen.mingshuaiSummary: An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin's transposition theorem is proved, which is used to generate an interpolant between two mutually contradictory conjunctions of polynomial inequalities, using semi-definite programming in time complexity \(\mathcal {O}(n^3+nm)\), where \(n\) is the number of variables and \(m\) is the number of inequalities (This complexity analysis assumes that despite the numerical nature of approximate SDP algorithms, they are able to generate correct answers in a fixed number of calls.). Using the framework proposed
in [\textit{V. Sofronie-Stokkermans}, Log. Methods Comput. Sci. 4, No. 4, Paper 1, 31 p. (2008; Zbl 1170.03018)]
for combining interpolants for a combination of quantifier-free theories which have their own interpolation algorithms, a combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions (EUF).
For the entire collection see [Zbl 1337.68016].Execution time of \(\lambda\)-terms via denotational semantics and intersection typeshttps://www.zbmath.org/1475.030732022-01-14T13:23:02.489162Z"De Carvalho, Daniel"https://www.zbmath.org/authors/?q=ai:de-carvalho.danielParaphrasing the author, there are two main contributions of this paper:
\begin{enumerate}
\item to show that it is possible to know if a \(\lambda\)-term \((v)u\) is head-normalisable, or even normalisable by only referring to the semantics \([[v]]\) and \([[u]]\) of \(v\) and \(u\) respectivelly, and, in case it is, to know the number of steps leading to the principal head normal form;
\item to define in the semantics a natural measure that corresponds to this number of steps.
\end{enumerate}
The paper is structured as follows.
\begin{itemize}
\item Section 2 presents \textit{J.-L. Krivine}'s machine [High.-Order Symb. Comput. 20, No. 3, 199--207 (2007; Zbl 1130.68057)], which is the framework in which the results are presented.
\item Section 3 presents the semantics to be considered in several steps. In Section 3.1, a relational model \(\mathfrak{M}\) of linear logic is presented. In Section 3.2, the induced semantics \(\Lambda(\mathfrak{M})\) of the simply typed \(\lambda\)-calculus is presented. Indeed, the main idea is that since the intuitionistic fragment of linear logic is a refinement of intuitionistic logic, from the categorical structure for interpreting intuitionistic linear logic. it is possible to derive a demotational semantics of intuitionistic logic. Finally, the semantics of the untyped \(\lambda\)-calculus is presented in Section 3.3. Section 3.4 gives an example.
\item Section 4 presents System R, the non-idempotent intersection type system induced by the semantics.
\item Section 5 develops the first main contribution of the paper detailed above (1).
\item Section 6 develops the second main contribution of the paper detailed above (2).
\end{itemize}
Reviewer: Alejandro Díaz-Caro (Buenos Aires)Truncation and semi-decidability notions in applicative theorieshttps://www.zbmath.org/1475.030742022-01-14T13:23:02.489162Z"Jäger, Gerhard"https://www.zbmath.org/authors/?q=ai:jager.gerhard"Rosebrock, Timotej"https://www.zbmath.org/authors/?q=ai:rosebrock.timotej"Kentaro, Sato"https://www.zbmath.org/authors/?q=ai:kentaro.satoIn this paper, a truncation operator is introduced in applicative theories to obtain a natural formalization of partial recursive functions. Applicative theories are the first-order part of Feferman's systems of explicit mathematics. With the use of the truncation operator, the authors can give a fine grained analysis of different recursion-theoretic phenomena in the presence of partiality.
Reviewer: Reinhard Kahle (Lisboa)Announcement as effort on topological spaceshttps://www.zbmath.org/1475.030752022-01-14T13:23:02.489162Z"van Ditmarsch, Hans"https://www.zbmath.org/authors/?q=ai:van-ditmarsch.hans-pieter"Knight, Sophia"https://www.zbmath.org/authors/?q=ai:knight.sophia"Özgün, Aybüke"https://www.zbmath.org/authors/?q=ai:ozgun.aybukeSummary: We propose a multi-agent logic of knowledge, public announcements and arbitrary announcements, interpreted on topological spaces in the style of subset space semantics. The arbitrary announcement modality functions similarly to the effort modality in subset space logics, however, it comes with intuitive and semantic differences. We provide axiomatizations for three logics based on this setting, with \(S\)5 knowledge modality, and demonstrate their completeness. We moreover consider the weaker axiomatizations of three logics with \(S\)4 type of knowledge and prove soundness and completeness results for these systems.Propositional quantification in bimodal S5https://www.zbmath.org/1475.030762022-01-14T13:23:02.489162Z"Fritz, Peter"https://www.zbmath.org/authors/?q=ai:fritz.peterSummary: Propositional quantifiers are added to a propositional modal language with two modal operators. The resulting language is interpreted over so-called products of Kripke frames whose accessibility relations are equivalence relations, letting propositional quantifiers range over the powerset of the set of worlds of the frame. It is first shown that full second-order logic can be recursively embedded in the resulting logic, which entails that the two logics are recursively isomorphic. The embedding is then extended to all sublogics containing the logic of so-called fusions of frames with equivalence relations. This generalizes a result due to \textit{G. A. Antonelli} and \textit{R. H. Thomason} [J. Symb. Log. 67, No. 3, 1039--1054 (2002; Zbl 1034.03014)], who construct such an embedding for the logic of such fusions.In defence of deontic diversityhttps://www.zbmath.org/1475.030772022-01-14T13:23:02.489162Z"Hansson, Sven Ove"https://www.zbmath.org/authors/?q=ai:hansson.sven-oveThis is an overview of the variety of usages of the normative terms of natural language. Case is made that deontic logic can fruitfully be used to pinpoint and enhance our understanding of nuances and distinctions in meaning, which would remain unnoticed otherwise.
Section 2 focuses on prescriptive terms like `must' and `ought'. It starts by contrasting their normative and non-normative usages, and goes on to consider the notion of strength of prescriptive terms, and of their scope, distinguishing between situation-specific and transsituational norms. Next, the well-known distinction between prima facie and overall duties, the notion of action-guiding obligation, and the distinctions between basic and derived obligations, and between objective and subjective obligations are carefully examined.
Section 3 reviews analog distinctions for permissive terms, like `may', `allowed', and `permitted'. It also discusses two distinctions that are particular to permissive terms, that between unilateral and bilateral permissions, and that between free choice and non-choice permissions.
A table summarizes the logical properties found to characterize the above notions.
Reviewer's comment: The paper is based on a keynote given at the DEON 2014 conference. It is very well written with excellent insights, and pointers to topics for future research. The reader is invited to compare the discussion there with his two handbook chapters [in: Handbook of deontic logic and normative systems. London: College Publications. 195--240 (2013; Zbl 1367.03040)]; in: Handbook of deontic logic and normative systems. London: College Publications. 445--497 (2013; Zbl 1367.03041)].
Reviewer: Xavier Parent (Luxembourg)Uniform interpolation and the existence of sequent calculihttps://www.zbmath.org/1475.030782022-01-14T13:23:02.489162Z"Iemhoff, Rosalie"https://www.zbmath.org/authors/?q=ai:iemhoff.rosalieA propositional logic \(L\) has \textit{uniform interpolation} if for every formula \(\phi\) and variable \(p\), there are formulas \(\forall p\,\phi\) and \(\exists p\,\phi\) not containing \(p\) such that
\begin{align*}
\vdash_L\psi\to\phi&\iff\vdash_L\psi\to\forall p\,\phi,\\
\vdash_L\phi\to\psi&\iff\vdash_L\exists p\,\phi\to\psi
\end{align*}
for all formulas \(\psi\) not containing \(p\). It is known that logics with Craig interpolation are few and far between (e.g., only \(7\) out of the \(2^\omega\) intermediate logics have interpolation, due to \textit{L. L. Maksimova} [Algebra Logika 16, 643--681 (1977; Zbl 0403.03047)]), and uniform interpolation is even more scarce (e.g., the well-known modal logics S4 and K4 have interpolation, but not uniform interpolation, due to \textit{S. Ghilardi} and \textit{M. Zawadowski} [Stud. Log. 55, No. 2, 259--271 (1995; Zbl 0831.03008)] and \textit{M. Bílková} [Stud. Log. 85, No. 1, 1--31 (2007; Zbl 1113.03017)]).
In [Arch. Math. Logic 58, No. 1--2, 155--181 (2019; Zbl 07006132)], the author introduced a proof-theoretic method to show uniform interpolation for modal logics that enjoy sequent calculi with certain syntactic properties. Here, the method is extended to intermediate logics and intuitionistic modal logics.
More specifically, in the case of intermediate logics, a notion of \textit{focused} sequent rules is defined in the paper, with the main result being that any logic that has a reductive cut-admissible calculus extending the Dyckhoff-Hudelmaier intuitionistic calculus by focused rules has uniform interpolation. (Here, reductivity is a certain condition ensuring that proof search terminates.) This reproves the result of \textit{A. M. Pitts} [J. Symb. Log. 57, No. 1, 33--52 (1992; Zbl 0763.03009)] that intuitionistic logic has uniform interpolation; however, as only a handful of intermediate logics have uniform interpolation, the main impact of the theorem is that no intermediate logics except possibly the Maksimicent seven may have a sequent calculus of the above-mentioned form.
Similarly, in the case of intuitionistic modal logics (with \(\Box\) but no \(\Diamond\)), the author defines the notion of focused modal rules, and proves that any logic that has a balanced calculus extending a Dyckhoff-like calculus for (\(\Box\)-only) iK with focused and modal focused rules has uniform interpolation. In particular, the \(\Diamond\)-free fragments of the logics iK and iKD have uniform interpolation (which is a new result).
Reviewer: Emil Jeřábek (Praha)Completeness of second-order propositional S4 and H in topological semanticshttps://www.zbmath.org/1475.030792022-01-14T13:23:02.489162Z"Kremer, Philip"https://www.zbmath.org/authors/?q=ai:kremer.philipThe paper presents a duo of two closely related proofs of weak completeness for the extensions of classical modal logic \(S4\) and intuitionistic propositional logic \(\mathsf{IL}\) with propositional quantifiers. The completeness is shown relative to the variant of topological semantics which only allows for an evaluation of formulas by some designated subsets of a topological space specified for every given model; it is thus less expressive than the `full second-order' version of the same semantics which the paper calls modally (resp. intuitionistically) principal, and which is known to induce a non-axiomatizable set of validities.
The axiomatizations obtained in the paper generally re-use the principles familiar from the standard axiomatizations of classical first-order logic. These principles are adapted to the language at hand, which necessitates a somewhat abstract and general preliminary treatment of the operation of substituting a formula \(B\) for a propositional variable \(p\) in a formula \(A\) to get another formula \(A[B/p]\). These axiomatizations are then relativized to certain well-behaved subsets \(\mathsf{F}\) of formulas so that the axioms of the system only include the formulas of the forms \(\forall pA \to A[B/p]\) and \(A[B/p] \to \exists pA\) when \(B \in \mathsf{F}\). For every such \(\mathsf{F}\), its associated axiomatization is shown to be weakly complete relative to the class of models in which every formula \(A \in \mathsf{F}\) gets assigned a designated subset of a model as long as every variable \(p\) in \(A\) is evaluated by a designated subset.
The presented proofs draw on the techniques and results of [\textit{H. Rasiowa} and \textit{R. Sikorski}, The mathematics of metamathematics. Warszawa: Panstwowe Wydawnictwo Naukowe (1963; Zbl 0122.24311)]; in each case, their central construction is an embedding of the Lindenbaum algebra associated to a given axiomatization into a topological space.
The paper then proceeds to mention the older strong completeness results for the systems extending the \(\mathsf{F}\)-versions of axiomatizations (for the few rather special \(\mathsf{F}\)'s) by the Barcan schema (resp. by the constant-domain principle \(\forall p(A \vee B) \to (A \vee \forall p B)\) with \(p\) not free in \(A\)). These results were obtained for the Kripke semantics, and, given that the family of upsets of any given Kripke frame forms an Alexandroff topological space, the existing proofs of these results also show the completeness of the said extensions relative to the more general topological semantics.
The results presented in the paper appear to be correct, their exposition is streamlined, clear, and reasonably concise.
Reviewer: Grigory K. Olkhovikov (Bochum)Coarse deontic logichttps://www.zbmath.org/1475.030802022-01-14T13:23:02.489162Z"Van De Putte, Frederik"https://www.zbmath.org/authors/?q=ai:van-de-putte.frederikThis paper recasts \textit{F. Cariani}'s resolution semantics for ought statements [Nôus 47, No. 3, 534--558 (2013; Zbl 1323.03017)] within the framework of non-normal logic. The key idea underpinning resolution semantics is given by a principle called coarseness: ``\(S\) ought to \(\phi\)'' can be true even though there are impermissible ways of \(\phi\)-ing. The following definition initially put forth by Cariani [loc. cit.], is used: ``\(S\) ought to \(\phi\)'' if \(\phi\) is (i) visible, (ii) optimal, and (iii) strongly permitted. An action is said to be visible if it perfectly divides the options in two classess, the class of those that are ways of performing the action, and the class of those that are not ways of performing the action. The ``ought'' modality (thus defined) does not satisfy the principle of inheritance: If \(\phi\) entails \(\psi\), then ``ought \(\phi\)'' entails ``ought \(\psi\)''. Such a principle is known to give rise to deontic paradoxes, like Ross's paradox. Inheritance is blocked in two ways, thanks to clause (i) and thanks to clause (iii).
The above definition of ``ought'' is formalised in a modal logic with distinct non-normal modal operators for visibility, optimality and permissibility. The paper proposes a neighborhood semantics, which generalizes Cariani's [loc. cit.], in terms of a ranking and a threshold value. Various extensions are considered depending on the conditions imposed on frames. The logic are axiomatized, shown to be decidable and compared with two other related works.
Reviewer: Xavier Parent (Luxembourg)Validity, dialetheism and self-referencehttps://www.zbmath.org/1475.030812022-01-14T13:23:02.489162Z"Pailos, Federico Matias"https://www.zbmath.org/authors/?q=ai:pailos.federico-matiasSummary: It has been argued recently [\textit{J. Beall}, Spandrels of truth. Oxford: Oxford University Press (2009); with \textit{J. Murzi}, ``Two flavors of Curry's paradox'', J. Philos. 110, No. 3, 143--165 (2013; \url{doi:10.5840/jphil2013110336})] that dialetheist theories are unable to express the concept of naive validity. In this paper, we will show that \(\mathbf{LP}\) can be non-trivially expanded with a \textit{naive} validity predicate. The resulting theory, \(\mathbf{LP}^{\mathbf{Val}}\) reaches this goal by adopting a weak self-referential procedure. We show that \(\mathbf{LP}^{\mathbf{Val}}\) is sound and complete with respect to the three-sided sequent calculus \(\mathbf{SLP}^{\mathbf{Val}} \). Moreover, \( mathbf{LP}^{\mathbf{Val}}\) can be safely expanded with a transparent truth predicate. We will also present an alternative theory \(\mathbf{LP}^{\mathbf{Val}^*} \), which includes a non-deterministic validity predicate.The middle ground-ancestral logichttps://www.zbmath.org/1475.030822022-01-14T13:23:02.489162Z"Cohen, Liron"https://www.zbmath.org/authors/?q=ai:cohen.liron"Avron, Arnon"https://www.zbmath.org/authors/?q=ai:avron.arnonSummary: Many efforts have been made in recent years to construct formal systems for mechanizing general mathematical reasoning. Most of these systems are based on logics which are stronger than first-order logic (FOL). However, there are good reasons to avoid using full second-order logic (SOL) for this task. In this work we investigate a logic which is intermediate between FOL and SOL, and seems to be a particularly attractive alternative to both: ancestral logic. This is the logic which is obtained from FOL by augmenting it with the transitive closure operator. While the study of this logic has so far been mostly model-theoretical, this work is devoted to its proof theory (which is much more relevant for the task of mechanizing mathematics). Two natural Gentzen-style proof systems for ancestral logic are presented: one for the reflexive transitive closure, and one for the non-reflexive one. We show that these systems are sound for ancestral logic and provide evidence that they indeed encompass all forms of reasoning for this logic that are used in practice. The two systems are shown to be equivalent by providing translation algorithms between them. We end with an investigation of two main proof-theoretical properties: cut elimination and constructive consistency proof.A measure of inferential-role preservationhttps://www.zbmath.org/1475.030832022-01-14T13:23:02.489162Z"Paseau, A. C."https://www.zbmath.org/authors/?q=ai:paseau.alexander-christopherSummary: The point of formalisation is to model various aspects of natural language. Perhaps the main use to which formalisation is put is to model and explain inferential relations between different sentences. Judged solely by this objective, a formalisation is successful in modelling the inferential network of natural language sentences to the extent that it mirrors this network. There is surprisingly little literature on the criteria of good formalisation, and even less on the question of what it is for a formalisation to mirror the inferential network of a natural language or some fragment of it. This paper takes some exploratory steps towards a quantitative account of the main ingredient in the goodness of a formalisation. We introduce and critically examine a mathematical model of how well a formalisation mirrors natural-language inferential relations.Model completeness for the Real Field with the Weierstrass \(\wp\) functionhttps://www.zbmath.org/1475.030842022-01-14T13:23:02.489162Z"Bianconi, Ricardo"https://www.zbmath.org/authors/?q=ai:bianconi.ricardoSummary: We prove model completeness for the expansion of the real field by the Weierstrass \(\wp\) function as a function of the variable \(z\) and the parameter (or period) \({\tau}\). We need to existentially define the partial derivatives of the \(\wp\) function with respect to the variable \(z\) and the parameter \({\tau}\). To obtain this result, it is necessary to include in the structure function symbols for the unrestricted exponential function and restricted sine function, the Weierstrass \({\zeta}\) function and the quasi-modular form \(E_{2}\) (we conjecture that these functions are not existentially definable from the functions \(\wp\) alone or even if we use the exponential and restricted sine functions). We prove some auxiliary model-completeness results with the same functions composed with appropriate change of variables. In the conclusion, we make some remarks about the non-effectiveness of our proof and the difficulties to be overcome to obtain an effective model-completeness result, and how to extend these results to appropriate expansion of the real field by automorphic forms.Logical properties of random graphs from small addable classeshttps://www.zbmath.org/1475.030852022-01-14T13:23:02.489162Z"Dawar, Anuj"https://www.zbmath.org/authors/?q=ai:dawar.anuj"Kopczyński, Eryk"https://www.zbmath.org/authors/?q=ai:kopczynski.erykA class \(\mathcal{C}\) of finite undirected graphs is addable if it closed under taking connected components and under adding an edge between different connected components. The class \(\mathcal{C}\) is small, respectively smooth, if the number of graphs in \(\mathcal{C}\) with vertex set \(\{1, \ldots, n\}\), denoted \(\mathcal{C}_n\), grows relatively slowly as \(n\) tends to infinity. The notion of smoothness implies the notion of smallness. \textit{C. McDiarmid} et al. [Algorithms Comb. 26, 231--246 (2006; Zbl 1119.05099)] and \textit{G. Chapuy} and \textit{G. Perarnau} [in: Proceedings of the 27th annual ACM-SIAM symposium on discrete algorithms, SODA 2016, Arlington, VA, USA, January 10--12, 2016. Philadelphia, PA: Society for Industrial and Applied Mathematics (SIAM); New York, NY: Association for Computing Machinery (ACM). 1580--1588 (2016; Zbl 1410.05179)] studied smooth, respectively small, addable classes of undirected graphs and proved that the probability (using the uniform distribution) that such graphs have certain properties (e.g. being connected, or containing a given connected component) converges. The authors obtain some more results in this direction and combine them with Ehrenfeucht-Fraisse games to obtain convergence results for events on \(\mathcal{C}_n\) definable by monadic second order logic (MSO) if \(\mathcal{C}\) is a class of finite undirected graphs which is small and addable, or smooth and addable. A corollary to this is that the following classes of graphs satisfy a labelled MSO 0-1 law: the class of all finite connected planar graphs; for each \(k > 0\), the class of all connected graphs of tree-width at most \(k\); for each \(k > 2\), the class of all connected graphs excluding \(K_k\) as a minor.
Reviewer: Vera Koponen (Uppsala)Decidability of the theory of modules over Prüfer domains with dense value groupshttps://www.zbmath.org/1475.030862022-01-14T13:23:02.489162Z"Gregory, Lorna"https://www.zbmath.org/authors/?q=ai:gregory.lorna"L'Innocente, Sonia"https://www.zbmath.org/authors/?q=ai:linnocente.sonia"Toffalori, Carlo"https://www.zbmath.org/authors/?q=ai:toffalori.carloThe authors define relations in a ring \(R\), called \(\mathrm{DPR}(R)\) (double prime radical relation) and \(\mathrm{PP}(R)\) (Point-Prest relation). They show that if \(R\) is an effectively given Prüfer domain such that each localisation at a maximal ideal has a dense value group, \(\mathrm{DPR}(R)\) and \(\mathrm{PP}(R)\) are recursive, then the theory of \(R\)-modules is decidable. In the case of effectively given Bezout domains with the same algebraic property, the decidability of the theory of \(R\)-modules is equivalent to the fact that the defined relations are recursive.
Reviewer: Mihai Prunescu (Bucharest)An Ax-Kochen-Ershov theorem for monotone differential-Henselian fieldshttps://www.zbmath.org/1475.030872022-01-14T13:23:02.489162Z"Hakobyan, Tigran"https://www.zbmath.org/authors/?q=ai:hakobyan.tigran-lIn the well-known work of \textit{T. Scanlon} [J. Symb. Log. 65, No. 4, 1758--1784 (2000; Zbl 0977.03021)] on valued differential fields where the derivation has a strong interaction with the valuation, namely $v(x')\ge v(x)$, the key condition of ``having many constants'' arose from natural examples such as Laurent series field $\mathbf{k} ((t))$ built from a given differential field $\mathbf{k}$ by putting $(\sum c_nt^n)'=\sum c_n' t^n$: every series has the same valuation as a constant with respect to the derivation (e.g. powers of $t$). In this paper, the author shows how to remove the condition ``many constants'' by going to a slightly tighter formalism, involving an extra function which is an additive map from the value group to the residue field with a condition on logarithmic derivatives.
Let $(\mathbf{k}, \partial)$ be a differential field, $\Gamma$ an ordered abelian group, and $K=\mathbf{k}((t^\Gamma))$ the usual field of generalized power series of Hahn with the standard valuation. In the paper, a valued differential field is called monotone if the derivation and the valuation have the strong interaction as above.
From the Introduction: ``In more detail, let $c:\Gamma\to \mathbf{k} $ be an additive map. Then the derivation $\partial$ of $\mathbf{k}$ extends to a derivation $\partial_c$ of $K$ by setting
\[
\partial_c\left(\sum_\gamma a_\gamma t^\gamma\right) := \sum_\gamma (\partial(a_\gamma+c(\gamma)a_\gamma) t^\gamma .
\]
[\dots] Let $K_c$ be the valued differential field $K$ with $\partial_c$ as its distinguished derivation. Assume in addition that $\mathbf{k}$ is linearly surjective. Then $K_c$ is differential-Henselian, and Scanlon's theorem above generalizes as follows:
Theorem 1.1. The theory $\mathrm{Th}(K_c)$ is completely determined by $\mathrm{Th}(\mathbf{k}, \Gamma; c)$, where $(\mathbf{k}, \Gamma; c)$ is the 2-sorted structure consisting of the differential field $\mathbf{k}$, the ordered abelian group $\Gamma$, and the additive map $c:\Gamma \to \mathbf{k}$.
[\dots] The valued differential fields $K_c$ are clearly monotone. We show:
Theorem 1.2. Every monotone differential-Henselian valued field is elementarily equivalent to some $K_c$ as in Theorem 1.1.''
The author gives examples (apparently in Section 4, rather than in Section 3), that in general the extra structure $c$ cannot be removed from Theorem 1.1, in particular for so-called valued differential fields with few constants, i.e. such that the valuation is trivial on the field of constants with respect to the derivation.
The author first works with the embedded field $\mathbf{k}$ from the structure $K_c$ as an extra primitive, but removes it afterwards (Section 6) with the help of the extra axiom: for all $\gamma\in \Gamma$, there is $x\in K$ such that $v(x)=\gamma$ and $\pi(x^\dag)=c(\gamma)$, where $\pi$ is the canonical differential ring morphism from the valuation ring to the residue field and $x^\dag=x'/x$.
Reviewer: Luc Bélair (Montréal)Twisted Galois stratificationhttps://www.zbmath.org/1475.030882022-01-14T13:23:02.489162Z"Tomašić, Ivan"https://www.zbmath.org/authors/?q=ai:tomasic.ivanThis paper develops the theory of twisted Galois stratification in order to describe first-order definable sets in the language of difference rings over algebraic closures of finite fields equipped with powers of the Frobenius automorphism. After introducing basic concepts of the theory of difference schemes and their morphisms, as well as the notions of a (normal) Galois stratification \(\mathcal{A}\) on a difference scheme (\(X, \sigma\)) and the Galois formula associated with \(\mathcal{A}\), the author develops difference algebraic geometry (in particular, the theory of generalized difference schemes). The main result of the paper is a direct image theorem stating that the direct image of a Galois formula by a morphism of difference schemes is equivalent to a Galois formula over fields with powers of Frobenius. As a consequence of this theorem, the author obtains an effective quantifier elimination procedure and a precise algebraic-geometric description of definable sets over fields with Frobenii in terms of twisted Galois formulas associated with finite Galois covers of difference schemes. In addition, the paper presents a number of new results on the category of difference schemes, Babbitt's decomposition, and effective difference algebraic geometry.
Reviewer: Alexander B. Levin (Washington)Axiomatizations of arithmetic and the first-order/second-order dividehttps://www.zbmath.org/1475.030892022-01-14T13:23:02.489162Z"Dutilh Novaes, Catarina"https://www.zbmath.org/authors/?q=ai:dutilh-novaes.catarinaSummary: It is often remarked that first-order Peano Arithmetic is non-categorical but deductively well-behaved, while second-order Peano Arithmetic is categorical but deductively ill-behaved. This suggests that, when it comes to axiomatizations of mathematical theories, expressive power and deductive power may be orthogonal, mutually exclusive desiderata. In this paper, I turn to \textit{J. Hintikka}'s distinction between descriptive and deductive approaches in the foundations of mathematics [``Is there completeness in mathematics after Gödel?'', Philos. Top. 17, No. 2, 69--90 (1989; \url{doi:10.5840/philtopics19891724})] to discuss the implications of this observation for the first-order logic versus second-order logic divide. The descriptive approach is illustrated by Dedekind's `discovery' of the need for second-order concepts to ensure categoricity in his axiomatization of arithmetic; the deductive approach is illustrated by Frege's \textit{Begriffsschrift} project. I argue that, rather than suggesting that any use of logic in the foundations of mathematics is doomed to failure given the impossibility of combining the descriptive approach with the deductive approach, what this apparent predicament in fact indicates is that the first-order versus second-order divide may be too crude to investigate what an adequate axiomatization of arithmetic should look like. I also conclude that, insofar as there are different, equally legitimate projects one may engage in when working on the foundations of mathematics, there is no such thing as the One True Logic for this purpose; different logical systems may be adequate for different projects.Stationarily ordered types and the number of countable modelshttps://www.zbmath.org/1475.030902022-01-14T13:23:02.489162Z"Moconja, Slavko"https://www.zbmath.org/authors/?q=ai:moconja.slavko-m"Tanović, Predrag"https://www.zbmath.org/authors/?q=ai:tanovic.predragThe present paper introduces the notion of a stationarily ordered theory generalizing the notion of weak o-minimality. The work studies Vaught's conjecture on the number of countable models. The authors obtained a very partial result in this direction: they confirm Vaught's conjecture for stationarily ordered theories only in the binary case. Observe that the confirmation of this conjecture for binary weakly o-minimal theories follows independently from the works by B. S. Baizhanov, the reviewer, S. V. Sudoplatov and others.
Reviewer: Beibut Kulpeshov (Almaty)An algorithm for regular solutions of systems of exp-subanalytic equations and o-minimality of \(\mathbb{R}_{\text{an} , \exp}\)https://www.zbmath.org/1475.030912022-01-14T13:23:02.489162Z"Pawłucki, Wiesław"https://www.zbmath.org/authors/?q=ai:pawlucki.wieslaw"Rożen, Zofia"https://www.zbmath.org/authors/?q=ai:rozen.zofiaIn this paper, the authors consider systems of equations of the form \[(S) : \left\{ \begin{array}{ccc} P_1(x, \exp \lambda_{11}(x),\dots,\exp \lambda_{1m}(x) ) & =& 0\\
\vdots &\vdots &\vdots \\
P_n(x, \exp \lambda_{n1}(x),\dots,\exp \lambda_{nm}(x) ) & =& 0 \end{array} \right.\] where the \(P_i\)'s and \(\lambda_{ij}\)'s are global subanalytic \(C^1\) functions, and the unknown \(x\) varies in \(\mathbb R^n\). The article aims to present an algorithm to reduce a system (S) into finitely many systems of subanalytic equations, by means of restrictions and smooth exp-subanalytic change of variables.
The interest of such reduction is justified by a general result of [\textit{J.-M. Lion}, J. Symb. Log. 67, No. 4, 1616--1622 (2002; Zbl 1042.03030)], which deduces o-minimality from a simple finiteness condition (C). Applied in the case of the expansion of the structure \(\mathbb R_{an}\) of global subanalytic sets by the exponential function, the condition (C) becomes to show the finiteness of the number of regular solutions of a system (S) (with affine \(\lambda_{ij}\)'s). For that matter, the authors claim their algorithm allows, together with Lion's result, to recover the o-minimality of the structure \(\mathbb R_{an,\exp}\), which was a breakthrough result in real analytic geometry (see [\textit{L. van den Dries} and \textit{C. Miller}, Isr. J. Math. 85, No. 1--3, 19--56 (1994; Zbl 0823.03017); \textit{A. J. Wilkie}, J. Am. Math. Soc. 9, No. 4, 1051--1094 (1996; Zbl 0892.03013); \textit{L. van den Dries} et al., Ann. Math. (2) 140, No. 1, 183--205 (1994; Zbl 0837.12006); \textit{J.-M. Lion} and \textit{J.-P. Rolin}, Ann. Inst. Fourier 47, No. 3, 859--884 (1997; Zbl 0873.32004)]).
The reduction is mostly based on subanalytic cell decomposition and an intensive use of the preparation theorem for subanalytic functions (see [\textit{J.-M. Lion} and \textit{J.-P. Rolin}, Ann. Inst. Fourier 47, No. 3, 859--884 (1997; Zbl 0873.32004); \textit{A. Parusiński}, Ann. Sci. Éc. Norm. Supér. (4) 27, No. 6, 661--696 (1994; Zbl 0819.32007)]).
Reviewer: Olivier Le Gal (Le Bourget-du-Lac)Computable elements and functions in effectively enumerable topological spaceshttps://www.zbmath.org/1475.030922022-01-14T13:23:02.489162Z"Korovina, Margarita"https://www.zbmath.org/authors/?q=ai:korovina.margarita-vladimirovna"Kudinov, Oleg"https://www.zbmath.org/authors/?q=ai:kudinov.oleg-victorovichIn computable analysis, one looks for ways to represent mathematical objects effectively (in the sense of recursion theory). One represents a basis of effectively coded open sets such that (a) for each two open sets (represented by natural numbers serving as their indices), the intersection is the effective union of other basic open sets and (b) the set of indices of nonempty basic open sets is recursively enumerable. Furthermore, notions to compare such topological sets are introduced. The authors also introduce the notion of decidability of topological spaces (based on properties of the numberings of open sets in the basis) and show that for every Turing degree there is an effectively enumerable \(T_1\)-space which does not have a representation decidable in that Turing degree. They compare their notion of spaces with that of Weihrauch and prove that the notions are different, even for \(T_0\)-spaces. They show that in \(T_0\)-spaces, a point \(x\) is computable iff the set of indices of basic open sets containing \(x\) is recursively enumerable and they provide two further equivalent characterisations of the computable points. Furthermore, they study coeffective points which are those points for which the set of all other points in \(X\) is effectively open. In an Euclidean space, a point is coeffective iff it is computable. Furthermore, the authors introduce computable and strongly computable functions and show that the latter have a principal numbering. They also define for real-valued functions the notion of majorant-computable functions and show that it coincides with the notion of strongly computable functions. As an analogue to Rice's Theorem, the authors show that every nontrivial index set of majorant-computable functions is \(\Pi^0_2\)-hard and can only be \(\Delta^0_2\) for the empty set and the full set. The index set of total functions (the before mentioned functions can be partial) is, as in the case of functions from natural numbers to natural numbers, \(\Pi^0_2\)-complete. For majorant-computable functions from the reals to the reals, the equality problem is even \(\Pi^1_1\)-complete. The last chapter (before the conclusion) deals with computable and effectively compact sets of points in effectively enumerable topological spaces.
Reviewer: Frank Stephan (Singapore)Calculating the closed ordinal Ramsey number \(R^{cl}(\omega \cdot 2,3)\)https://www.zbmath.org/1475.030932022-01-14T13:23:02.489162Z"Mermelstein, Omer"https://www.zbmath.org/authors/?q=ai:mermelstein.omerThe paper under review deals with a certain version of topological Ramsey theory, where one intends to find a homogeneous set which is a closed subset, with respect to the order-topology, of a nonzero ordinal.
For a natural number \(n\), a cardinal \(\kappa\) and ordinals \((\alpha_i)_{i<\kappa}\)'s, let \(R^{cl}(\alpha_i)^n_{i<\kappa}\) denote the least ordinal \(\beta\) such that for every colouring of \(n\)-subsets of \(\beta\) into \(\kappa\) colors, there is \(i<\kappa\), and there is a homogeneous set \(X\) of order type \(\alpha_i\) with color \(i\) such that \(X\) is a closed subset of its supremum. It has been shown by
\textit{A. E. Caicedo} and \textit{J. Hilton} [Contemp. Math. 690, 87--120 (2017; Zbl 1423.03160)]
that the inequalities \(\omega^{k+1}\leq R^{cl}(\omega^2,k)\leq \omega^{\omega}\), and \(\omega^2\cdot 3\leq R^{cl}(\omega\cdot 2,3)\leq \omega^3\cdot 100\) are satisfied. In the paper under review, the author obtains the exact value of \(R^{cl}(w\cdot 2,3)\) that is \(\omega^3\cdot 2\).
The description of the proof (from the original text): ``In order to prove \(R^{cl}(\omega\cdot 2,3)\leq \omega^3\cdot 2\), we must show that for each colouring \(c:[\omega^3\cdot 2]^2\rightarrow 2\) with no homogeneous triples of colour \(1\), there is some homogeneous \(Y\in [\omega^3\cdot 2]^{\omega\cdot 2}\) of colour \(0\), closed in its supremum\dots
We show first that for each \(\delta<\omega^\omega \), \(k\in\mathbb{N}\), and pair-colouring \(c:[\delta]^2\rightarrow k\), there exists some \(X\subseteq\delta\), closed in its supremum with \(\operatorname{ord}(X)=\delta\), such that \(c\restriction [X]^2\) is a canonical colouring (Definition 3.10). A canonical colouring is one such that for ``most'' \(\{\alpha,\beta\}\in [\delta]^2\), the value \(c(\{\alpha,\beta\})\) depends only on the Cantor-Bendixson ranks of the points \(\alpha,\beta\) in the topological space \(\delta\), and on the Cantor normal form of \(\delta\)\dots
The bound \(R^{cl}(\omega\cdot 2,3)\geq \omega^3\cdot 2\) is achieved by describing a single colouring \(c:[\omega^3\cdot 2]^2\rightarrow 2\) such that for each \(\theta<\omega^3\cdot 2\), the colouring \(c\restriction [\theta]^2\) demonstrates \(R^{cl}(\omega\cdot 2,3)>\theta\).''
Reviewer: Rahman Mohammadpour (Paris)Minimal covering sets for infinite set systemshttps://www.zbmath.org/1475.030942022-01-14T13:23:02.489162Z"Komjáth, Péter"https://www.zbmath.org/authors/?q=ai:komjath.peterGiven a set \(V\) and a collection \(\mathcal H\) of non-empty subsets of \(V\), \(M \subseteq V\) is a covering set if \(M \cap A \neq \emptyset\) for all \(A \in \mathcal H\). \(M\) is a minimal covering set if \(M\) is a covering set and no proper subset of \(M\) is a covering set. Covering sets are the topic of a question raised by \textit{T. Banakh} and \textit{D. van der Zypen} [Discrete Math. 342, No. 11, 3043--3046 (2019; Zbl 1419.05156)].
If \(r\) is a fixed natural number and \(\mathcal H\) is a system of sets with the property that \(|A \cap B| \leq r\) for all distinct \(A,B \in \mathcal H\), must \(\mathcal H\) have a minimal covering set?
In 1937, E.W. Miller show that if \(\mathcal H\) is a collection of infinite sets with the intersection property in the question, then \(\mathcal H\) is 2-chromatic. Erdoős and Hajnal generalized this in [\textit{P. Erdős} and \textit{A. Hajnal}, Acta Math. Acad. Sci. Hung. 12, 87--123 (1961; Zbl 0201.32801)].
In this paper, the author applies some of the techniques of Erdős and Hajnal [loc. cit.] to investigate some specific instances of this problem where additional information about the set system \(\mathcal H\) is available. He finds criteria that guarantee an affirmative answer to the question and also shows that, consistently, there are systems \(\mathcal H\) with small intersections that do not have minimal covering sets.
As a sample, the following conditions on \(\mathcal H\) guarantee the existence of a minimal covering set:
\begin{enumerate}
\item \(\mathcal H\) consists of finite sets.
\item \(S\) is a set, \(\mu\) is an infinite cardinal, \(\mathcal H\) consists of \(\mu\)-sized subsets of \(S\), and there is a natural number \(r\) so that \(|A \cap B| \leq r\) for all distinct \(A,B \in \mathcal H\).
\item \(S\) is a set, \(\mu\) is an infinite cardinal, \(\mathcal H\) consists of \(\mu\)-sized subsets of \(S\), and there is a well-ordering \(\prec\) of \(\mathcal H\) so that \(A \not\subseteq \bigcup\{B : B \prec A\}\) for all \(A \in \mathcal H\).
\item \(S\) is a set, \(\mathcal H\) consists of subsets of \(S\), there is a natural number \(r\) so that \(|A \cap B| \leq r\) for all distinct \(A,B \in \mathcal H\), and there is a \(T \subseteq S\) so that \(A \cap T\) is both non-empty and at most countable for all \(A \in \mathcal H\).
\item The \(\omega_1\) version of Martin's axiom holds, \(S\) consists of countable limit ordinals, and \(\mathcal H = \{A_\xi : \xi \in S\}\) is so that \(A_\xi\) is a cofinal subset of \(\xi\) with order type \(\omega\).
\item GCH holds, \(S\) is a set, \(\mu\) is an uncountable regular cardinal, \(\omega \leq \tau < \mu\), \(\square_\lambda\) is true for all singular cardinals \(\lambda\) with cofinality at most \(\tau\), \(\mathcal H\) consists of \(\mu\) sized subsets of \(S\), and \(|A \cap B| < \tau\) for all distinct \(A,B \in \mathcal H\).
\end{enumerate}
The paper also contains the following situations where \(\mathcal H\) has no minimal covering set.
\begin{enumerate}
\item \(\mathcal H = \{A_0,A_1,\cdots\}\), the \(A_n\) are strictly decreasing, and \(\bigcap_n A_n = \emptyset\).
\item \(\mathcal H = \langle A_\alpha : \alpha < \omega_1 \mbox{ is a limit ordinal}\rangle\) is a \(\clubsuit\)-sequence.
\end{enumerate}
They also show that there is a system \(\mathcal H\) of almost disjoint countable sets that has no minimal covering. A greater disparity of size does not necessarily help. They prove that, consistent with a supercompact cardinal, there is a family \(\mathcal H\) consisting of \(\aleph_1\) sized subsets of \(\omega_{\omega+1}\) where distinct \(A, B \in \mathcal H\) have finite intersection, but \(\mathcal H\) has no minimal covering set.
Reviewer: Jared Holshouser (Mobile)On uniformly continuous functions between pseudometric spaces and the axiom of countable choicehttps://www.zbmath.org/1475.030952022-01-14T13:23:02.489162Z"da Silva, Samuel G."https://www.zbmath.org/authors/?q=ai:gomes-da-silva.samuelA (pseudo)metric space is said to be \textit{Atsuji} or UC if every continuous real-valued function defined on the space is uniformly continuous. \textit{M. Atsuji} [Pac. J. Math. 8, 11--16 (1958; Zbl 0082.16207)] was the first to provide equivalent conditions under which continuous functions of a metric space are uniformly continuous. Recently, in the context of ZF set theory (i.e., Zermelo-Fraenkel set theory without the axiom of choice), the property of being UC in the class of metric spaces has been studied by \textit{K. Keremedis} [Topology Appl. 210, 366--375 (2016; Zbl 1355.54035); Bull. Pol. Acad. Sci., Math. 65, No. 2, 113--124 (2017; Zbl 1436.03256); Topol. Proc. 52, 73--93 (2018; Zbl 1398.54046)].
In the paper under review, the author investigates (within ZF) the property UC in the class of pseudometric spaces and obtains some interesting equivalents of the axiom of countable choice \(\mathrm{AC}_{\omega}\) (i.e., every countably infinite family of non-empty sets has a choice function); one of those equivalents being a well-known characterization -- via pairs of sequences -- of uniform continuity of real-valued continuous functions defined on pseudometric spaces (see (2) below).
The main result of this paper is that \(\mathrm{AC}_{\omega}\) is equivalent to each of the following statements:
\begin{enumerate}
\item If \(M,N\) are pseudometric spaces and \(f:M\rightarrow N\) is a continuous function, \(f\) is uniformly continuous, if and only if, for every pair of (not necessarily convergent) sequences \((x_n)\), \((y_n)\) in \(M\) such that \(d_{M}(x_n,y_n)\rightarrow 0\) one has \(d_{N}(f(x_n),f(y_n))\rightarrow 0\).
\item If \(M\) is a pseudometric space and \(f:M\rightarrow\mathbb{R}\) is a continuous function, \(f\) is uniformly continuous, if and only if, for every pair of (not necessarily convergent) sequences \((x_n)\), \((y_n)\) in \(M\) such that \(d_{M}(x_n,y_n)\rightarrow 0\) one has \(|f(x_n)-f(y_n)|\rightarrow 0\).
\item Let \(M,N\) be pseudometric spaces and assume \(M\) to be sequentially compact (i.e., every sequence in \(M\) has a convergent subsequence converging to a point in \(M\)). Then for every function \(f:M\rightarrow N\), \(f\) is continuous, if and only if, it is uniformly continuous.
\item Sequentially compact, pseudometric spaces are UC.
\end{enumerate}
Reviewer: Eleftherios Tachtsis (Karlovassi)On the set-theoretic strength of Ellis' theorem and the existence of free idempotent ultrafilters on \(\omega\)https://www.zbmath.org/1475.030962022-01-14T13:23:02.489162Z"Tachtsis, Eleftherios"https://www.zbmath.org/authors/?q=ai:tachtsis.eleftheriosThis article examines the strength of Ellis' theorem as a weak choice principle over \(\mathsf{ZF}\) and \(\mathsf{ZFA}\). (Recall that Ellis' theorem states every compact Hausdorff right topological semigroup has an idempotent element.) One of the main results of the paper is that in \(\mathsf{ZF}\), Ellis' theorem follows from the Boolean prime ideal theorem (\(\mathsf{BPI}\)). In fact, the author establishes from the \(\mathsf{BPI}\) a strengthening of Ellis' theorem: for every family \(\{S_i :\, i \in I\}\) of nontrivial compact Hausdorff right topological semigroups, there is a choice function on \(I\) that selects an idempotent from \(S_i\) for every \(i \in I\). The author shows that in the theory \(\mathsf{ZFA}\), Ellis' theorem for abelian semigroups, or for linearly ordered semigroups, can be proved from very weak choice principles, known to be strictly weaker than the \(\mathsf{BPI}\) over \(\mathsf{ZFA}\).
Ellis' theorem is perhaps most famous for its role in proving Hindman's theorem, for which what one really needs is the assertion that there exists a free idempotent ultrafilter on \(\omega\). The author proves that this assertion follows from \(\mathsf{BPI}_{\mathbb R}\) (that is, \(\mathsf{BPI}\) for filters on \(\mathbb R\)) or from the statement that the Tychonoff product \(2^{\mathbb R}\) is compact and Loeb.
The article also includes a number of intriguing open questions. Is Ellis' theorem provable in \(\mathsf{ZF}\)? (It is conjectured that the answer is no.) Is the assertion that there exists a free idempotent ultrafilter on \(\omega\) equivalent to the assertion that there exists a free ultrafilter on \(\omega\)? (Again, a negative answer is conjectured, and a plausible model for showing this is put forward.)
Reviewer: Will Brian (Waco)A model of \(\mathsf {ZFA}+ \mathsf {PAC}\) with no outer model of \(\mathsf {ZFAC}\) with the same pure parthttps://www.zbmath.org/1475.030972022-01-14T13:23:02.489162Z"Larson, Paul"https://www.zbmath.org/authors/?q=ai:larson.paul-b"Shelah, Saharon"https://www.zbmath.org/authors/?q=ai:shelah.saharonThe theory $\mathsf{ZFA}$ is a modified version of Zermelo-Fraenkel set theory ($\mathsf{ZF}$) admitting objects other than sets, the so-called atoms. The domain of a model of $\mathsf{ZFA}$, $\mathcal{P}^{\infty,*}(A)$ (in the paper's notation), is defined via a hierarchy over a given set $A$ of atoms (which is a non-empty set such that no member of $A$ is in the transitive closure of any other member), indexed by ordinals, in a similar manner with the cumulative hierarchy $V_{\alpha}$ of the Von Neumann universe:
\[
\begin{aligned}
&\mathcal{P}^{0,*}(A)=A;\\
&\mathcal{P}^{\alpha+1,*}(A)=(\mathcal{P}^{\alpha,*}(A)\cup\mathcal{P}(\mathcal{P}^{\alpha,*}(A)))\setminus\{\emptyset\};\\
&\mathcal{P}^{\beta,*}(A)=\bigcup_{\alpha<\beta}\mathcal{P}^{\alpha,*}(A)\qquad (\beta\text{ limit});\\
&\mathcal{P}^{\infty,*}(A)=\bigcup_{\alpha\in\mathrm{Ord}}\mathcal{P}^{\alpha,*}(A),
\end{aligned}
\]
where an arbitrary element of $A$ is let to represent the empty set, and the other members of $A$ represent atoms. Sets in a model of $\mathsf{ZFA}$ whose transitive closures exclude atoms are called pure sets; these sets form an inner model of $\mathsf{ZF}$. The axiom $\mathsf{PAC}$ asserts that this inner model satisfies the axiom of choice ($\mathsf{AC}$).
In this paper, the authors construct a model of $\mathsf{ZFA}+\mathsf{PAC}$ such that no outer model of $\mathsf{ZFAC}$ (= $\mathsf{ZFA}+\mathsf{AC}$) has the same pure sets. Their method of producing models of $\mathsf{ZFA}$ is different from the usual Fraenkel-Mostowski method; the domains of their models are subclasses of $\mathcal{P}^{\infty,*}(A)$ (for a given set $A$ of atoms) which are constructed over $A$ using certain elements of $\mathcal{P}^{\infty,*}(A)$ as predicates. In particular, given sets $X$ and $B$ in $\mathcal{P}^{\infty,*}(A)$, the authors let Def$_{B}(X)$ denote the collection of non-empty subsets of $X$ which are definable over $X$ using parameters from $X$ and predicates corresponding to members of $B$. Then they define:
\[
\begin{aligned}
&U_{0}^{A,B}=A;\\
&U_{\alpha+1}^{A,B}=U_{\alpha}^{A,B}\cup\mathrm{Def}_{B}(U_{\alpha}^{A,B});\\
&U_{\beta}^{A,B}=\bigcup_{\alpha<\beta}U_{\alpha}^{A,B}\qquad (\beta\text{ limit});\\
&U_{\infty}^{A,B}=\bigcup_{\alpha\in\mathrm{Ord}}U_{\alpha}^{A,B}.
\end{aligned}
\]
Given $a\in A$, they let $\mathbf{U}(a, A, B)$ be the model of $\mathsf{ZFA}$ with domain $U_{\infty}^{A,B}$, where $a$ is interpreted as the empty set. The model $\mathbf{U}(a, A, B)$ is, up to isomorphism, the smallest well-founded proper class model of $\mathsf{ZFA}$ with $A\setminus\{a\}$ as its set of atoms and $a$ as its empty set which is closed under intersections with the members of $B$. Every element of $\mathbf{U}(a, A, B)$ is definable in $\mathbf{U}(a, A, B)$ from a finite set of its ordinals, a finite subset of $A$ and finitely many predicates from $B$.
Under the above terminology, the main result of this paper is the following: ``In a c.c.c. forcing extension $\mathbf{L}[G]$ of $\mathbf{L}$ there is a model $\mathbf{U}$ of $\mathsf{ZFA}$ of the form $\mathbf{U}(a,A,B)$, for some atom set $A$ in $\mathbf{L}$, some element $a$ of $A$ and some $B$ in $\mathcal{P}^{\infty,*}(A)$, such that the pure part of $\mathbf{U}$ is isomorphic to $\mathbf{L}$ and such that in no outer model of $\mathbf{L}[G]$ is there a model of $\mathsf{ZFAC}$ containing $\mathbf{U}$ whose pure part is isomorphic to $\mathbf{L}$.''
The authors' proof of the above theorem (given in Section 2 of this paper) uses a model-theoretic construction due to \textit{G. Hjorth} [J. Math. Log. 2, No. 1, 113--144 (2002; Zbl 1010.03036)] which produces a sentence in $\mathcal{L}_{\aleph_{1},\aleph_{0}}$ homogeneously characterizing $\aleph_{1}$, and is especially beautiful. In Section 3, the authors discuss this construction, and in Section 4, they explain the necessity of such a construction.
Reviewer: Eleftherios Tachtsis (Karlovassi)Large cardinals beyond choicehttps://www.zbmath.org/1475.030982022-01-14T13:23:02.489162Z"Bagaria, Joan"https://www.zbmath.org/authors/?q=ai:bagaria.joan"Koellner, Peter"https://www.zbmath.org/authors/?q=ai:kollner.peter"Woodin, W. Hugh"https://www.zbmath.org/authors/?q=ai:woodin.w-hughWoodin's work on the potential future of inner model theory isolated a few pivotal questions relating the connection between \(\mathrm{HOD}\) and \(V\) under the existence of large cardinals in the level of extendibility (or supercompactness), see [the third author, J. Math. Log. 10, No. 1--2, 101--339 (2010; Zbl 1247.03110)]. The \(\mathrm{HOD}\)-conjecture, stating the an ordinal definable version of the Solovay theorem holds unboundedly often, was shown by the third author [loc. cit.] to have far reaching affects on the structure of the universe, and in particular, limiting the possible large cardinals that can consistently hold without choice.
In this paper, the authors investigate the possible hierarchy of large cardinals which are stronger than Reinhardt cardinals, and thus incompatible with the axiom of choice [\textit{K. Kunen}, J. Symb. Log. 36, 407--413 (1971; Zbl 0272.02087)]. Starting slightly above a Reinhardt cardinal, all those cardinals imply the failure of the \(\mathrm{HOD}\)-conjecture.
Since the classical study of large cardinal use the axiom of choice in a substantial way [\textit{E. L. Bull jun.}, Ann. Math. Logic 15, 161--191 (1978; Zbl 0402.03048)], the paper must lay down carefully the definition of the relevant large cardinal axioms, in order to avoid trivialities or inessential difficulties, see for example [\textit{A. Blass} et al., Fundam. Math. 194, No. 2, 179--189 (2007; Zbl 1116.03045)].
The authors demonstrate some of the implications between those notions, but also illustrate how difficult and non-trivial the study of such large cardinals can be. Finally, two large sections are dedicated to the detailed explanation of the two possible futures of set theory. If the \(\mathrm{HOD}\)-conjecture is true, then most of the hierarchy of large cardinals which contradict choice is outright inconsistent. On the other hand, the consistency of those large cardinals imply the existence of a parallel hierarchy of large cardinal notions which are defined in terms of elementary embeddings from \(\mathrm{HOD}\) to itself. Those large cardinals entail the failure of the \(\mathrm{HOD}\)-conjecture in a strong sense, imply \(V \neq \mathrm{HOD}\), but might still be consistent with the axiom of choice.
The paper contains many intriguing open problems.
Reviewer: Yair Hayut (Jerusalem)A note on the tightness of \(G _{\delta}\)-modificationshttps://www.zbmath.org/1475.030992022-01-14T13:23:02.489162Z"Usuba, Toshimichi"https://www.zbmath.org/authors/?q=ai:usuba.toshimichiFor a topological space \(X\), let \(X_\delta\) denote the \(G_\delta\)-modification of \(X\), which is the space equipped with the topology generated by all \(G_\delta\)-subsets of \(X\). In this paper, the author constructs a normal countably tight \(T_1\)-space \(X\) such that \(t(X_\delta)>2^{\aleph_0}\). This result answers the question asked in [\textit{A. Dow} et al., Acta Math. Hung. 158, No. 2, 294--301 (2019; Zbl 1438.54039)]. Moreover, the author shows that (1) for every countably tight space \(X\), \(t(X_\delta)\) is at most the least \(\omega_1\)-strongly compact cardinal and (2) if there is no weakly Mahlo cardinal \({<}2^{\aleph_0}\) and there is no \(\omega_1\)-strongly compact cardinal below a cardinal \(\nu\), then there is a normal countably tight \(T_1\)-space with \(t(X_\delta)\geq\nu\). The proofs are done by an interesting analysis of fine ultrafilters over \(\mathcal{P}_\kappa\lambda\).
Reviewer: Tetsuya Ishiu (Oxford, Ohio)A continuity principle equivalent to the monotone \(\Pi^0_1\) fan theoremhttps://www.zbmath.org/1475.031002022-01-14T13:23:02.489162Z"Kawai, Tatsuji"https://www.zbmath.org/authors/?q=ai:kawai.tatsujiThe author's strong continuity principle (SC) says that every pointwise continuous function from a complete separable metric space to a metric space is strongly continuous in the sense of [\textit{D.S.~Bridges}, Constructive functional analysis. London etc.: Pitman (1979; Zbl 0401.03027)]: that is, uniformly continuous near every compact image. Working in Bishop-style constructive reverse mathematics, the author shows that SC is tantamount to the fan theorem for monotone \(\Pi^0_1\) bars, and that the latter is equivalent to a variant of the fan theorem, called sc-FAN, related to but stronger than the principle c-FAN from [\textit{J. Berger}, Lect. Notes Comput. Sci. 3988, 35--39 (2006; Zbl 1145.03339)].
Reviewer: Peter M. Schuster (Verona)Production-logical equations on Boolean latticeshttps://www.zbmath.org/1475.031012022-01-14T13:23:02.489162Z"Ivanov, I. Y."https://www.zbmath.org/authors/?q=ai:ivanov.inokentij-y|ivanov.i-yuSummary: The concept of production-logical equation on boolean lattice is introduced which is based on general production-logical relations theory. Some properties of such equations are considered in case of finite lattice. The solution process of an arbitrary production-logical equation on a finite boolean lattice is reduced to solving a set of equations with elementary right-hand members. The concept of canonical relation on distributive lattice is introduced in order to simplify the study of logical connections. An existance of logically equivalent canonical relation for an arbitrary relation is proved in case of finite distributive lattice.A topological approach to MTL-algebrashttps://www.zbmath.org/1475.031022022-01-14T13:23:02.489162Z"Fussner, Wesley"https://www.zbmath.org/authors/?q=ai:fussner.wesley"Ugolini, Sara"https://www.zbmath.org/authors/?q=ai:ugolini.saraTriples decompostions for algebraic structures ha vea long history. In this paper, the authors provide a dualized construction of Aguzzoli-Flaminio-Ugolini of a large class of MTL-algebras from quadruples (\(B,A, \vee_e,\delta\)). The extended Priestley dual of each \(srDL\)-algebra from the Stone space associated to its Boolean skeleton, the extended Priestley dual of its radical, and a collection of connecting maps, via a rotation construction are constructed.
Reviewer: Hongxing Liu (Jinan)Fuzzy UP-ideals and fuzzy UP-subalgebras of UP-algebras in term of level subsetshttps://www.zbmath.org/1475.031032022-01-14T13:23:02.489162Z"Poungsumpao, Polatip"https://www.zbmath.org/authors/?q=ai:poungsumpao.polatip"Kaijae, Waraphorn"https://www.zbmath.org/authors/?q=ai:kaijae.waraphorn"Arayarangsi, Saranya"https://www.zbmath.org/authors/?q=ai:arayarangsi.saranya"Iampan, Aiyared"https://www.zbmath.org/authors/?q=ai:iampan.aiyaredThe authors consider properties of fuzzy UP-subalgebras and fuzzy UP-ideals of UP-algebras, and prove their basic properties.
An algebra \((A,\cdot, 0)\) of type \((2,0)\) is called a UP-algebra if, for all \(x,y,z\in A\),
(UP-1) \((y\cdot z)\cdot ((x\cdot y)\cdot (x\cdot z))=0\),
(UP-2) \(0\cdot x = x\),
(UP-3) \(x\cdot 0 = 0\),
(UP-4) \(x\cdot y = y\cdot x = 0\) implies \(x = y\).
A typical example of UP-algebras is \((\mathcal{P}(X),\cdot, \emptyset)\), where \(X\) is a non-empty set, and \(A\cdot B\) is defined by \[A\cdot B= A-B (= A\cap B^{c}) \ \ \ \ (A,B,\in \mathcal{P}(X)).\] Thus, UP-algebras are closely related to BCK-algebras, BCI-algebras, and so on.
A non-empty subset \(B\) of a UP-algebra \(A\) is called a UP-ideal if it satisfies
\begin{enumerate}
\item \(0\in B\) and
\item \(x\cdot (y\cdot z)\in B\) and \(y\in B\) imply \(x\cdot z\in B\).
\end{enumerate}
A non-empty subset \(B\subseteq A\) is a UP-subalgebra if \(S\) is closed under the operation ``\(\cdot\)''.
From these definitions, a fuzzy \(f\) in \(A\) is called a fuzzy UP-ideal if, for any \(x, y, z\in A\),
1. \(f(0)\ge f(x)\), and
2. \(f(x\cdot z) \ge \min \{f(x\cdot (y\cdot z)), f(y)\}\).
Also, a fuzzy set \(f\) in \(A\) is called a fuzzy UP-subalgebra if, for any \(x, y\in A\), \[f(x\cdot y)\ge \min \{f(x), f(y)\}.\]As expected, the authors prove the following basic theorems:
Theorem 2.1. Every fuzzy UP-ideal is a fuzzy UP-subalgebra.
Theorem 2.5, 2.6. Let \(f\) be a fuzzy set in \(A\). Then the following statements hold:
1. \(f\) is a fuzzy UP-ideal (fuzzy UP-subalgebra) if and only if, for all \(t\in [0, 1]\), \(U(f; t)\neq \emptyset\) implies \(U(f; t)\) is a UP-ideal (fuzzy UP-subalgebra), where \(U(f; t) =\{x\in A \mid f(x) \ge t\}\)
2. \(\bar{f}\) is a fuzzy UP-ideal (fuzzy UP-subalgebra) if and only if, for all \(t\in [0, 1]\), \(L(\bar{f}; t)\neq \emptyset\) implies \(L(\bar{f}; t)\) is a UP-ideal (fuzzy UP-subalgebra), where \(\bar{f}(x)=1-f(x)\) and \(L(f; t) = \{x\in A \mid f(x)\le t\} \). The results above mean that every fuzzy UP-ideal (fuzzy UP-subalgebra) is represented by so-called level-cut UP-ideals (UP-subalgebras) \(U(f; t)\).
Moreover, they prove the following theorems, which roughly mean that an inverse image of a fuzzy UP-ideal (fuzzy UP-subalgebra) by a UP-homomorphism is a fuzzy UP-ideal (fuzzy UP-subalgebra) and an image of a fuzzy UP-ideal (fuzzy UP-subalgebra) is also a fuzzy UP-ideal (fuzzy UP-subalgebra) for a UP-homomorphism satisfying a sup property, that is, for any non-empty \(T\) of \(A\), there exists \(T_0\in T\) such that \(f(t_0) = \sup \{f(t)\}_{t\in T}\):
Theorem 2.14. Let \((A,\cdot, 0)\) and \((B,\cdot,0)\) be UP-algebras and let \(f : A \to B\) a UP-epimorphism. If \(\beta\) is a fuzzy UP-ideal (fuzzy UP-subalgebra) of \(B\), then \(\beta \circ f\) is a fuzzy UP-ideal (fuzzy UP-subalgebra) of A.
Reviewer: Michiro Kondo (Inzai)The operator \(L_n\) on quasivarieties of universal algebrashttps://www.zbmath.org/1475.080022022-01-14T13:23:02.489162Z"Budkin, A. I."https://www.zbmath.org/authors/?q=ai:budkin.aleksandr-ivanovichLet $n$ be an arbitrary natural number and let $M$ be a class of universal algebras. Denote by $L_n(M)$ the class of algebras $G$ such that, for every $n$-generated subalgebra $A$ of $G$, the coset $a/R$ $(a\in A)$ modulo the least congruence $R$ including $A\times A$ is an algebra in $M$. In this paper the following main results are proved:
\begin{itemize}
\item[1.] If $M$ is a hereditary class of algebras then so is $L_n(M)$.
\item[2.] If $M$ is a quasivariety of algebras then so is $L_n(M)$.
\item[3.] If $M$ is a hereditary and multiplicatively closed class of algebras then so is $L_n(M)$.
\item[4.] If $M$ is a hereditary and ultraclosed class of algebras then so is $L_n(M)$.
\item[5.] If $M$ is a universally axiomatizable class of algebras then so is $L_n(M)$.
\item[6.] If $M$ is a congruence-permutable and homomorphically closed class of algebras then $L_n(M)$ is homomorphically closed too.
\item[7.] If $M$ is a congruence-permutable variety of algebras then $L_n(M)$ is a variety too.
\end{itemize}
Reviewer: Yuri Movsisyan (Yerevan)Effective difference elimination and nullstellensatzhttps://www.zbmath.org/1475.120122022-01-14T13:23:02.489162Z"Ovchinnikov, Alexey"https://www.zbmath.org/authors/?q=ai:ovchinnikov.alexey"Pogudin, Gleb"https://www.zbmath.org/authors/?q=ai:pogudin.gleb-a"Scanlon, Thomas"https://www.zbmath.org/authors/?q=ai:scanlon.thomas-jA sequence \((a_{j})_{j=0}^{\infty}\) of elements of a field \(K\) is said to be a solution of a difference equation with constant coefficients if there is a nonzero polynomial \(F(x_{0},\dots, x_{e})\in K[x_{0},\dots, x_{e}]\) such that for every natural number \(j\), one has \(F(a_{j}, a_{j+1},\dots, a_{j+e}) = 0\). This concept can be naturally generalized to systems of difference equations in several variables.
The paper under review answers the following fundamental questions about sequence solutions of systems of ordinary difference equations:
\begin{itemize}
\item[(i)] Under what conditions does such a system have a sequence solution?
\item[(ii)] Can these solutions be made sufficiently transparent to allow for efficient computation?
\item[(iii)] Given a system of difference equations on \((n+m)\)-tuples of sequences, how does one eliminate some of the variables so as to deduce the consequences of these equations on the first \(n\) variables?
\end{itemize}
As the answers to these questions, the authors prove two strong results the first of which (Theorem 3.1 of the paper) can be viewed as effective difference Nullstellensatz; it reduces the problem of solvability of a system of difference equations to the problem of consistency of certain system of finitely many polynomial equations. The second main result of the paper (Theorem 3.4) is an effective difference elimination theorem; it reduces the question of existing/finding a consequence in the \(\mathbf{x}\)-variables of a system of difference equations in \(\mathbf{x}\) and \(\mathbf{u}\) (\(\mathbf{x}=(x_{1},\dots, x_{m})\) and \(\mathbf{u}=(u_{1},\dots, u_{r})\) are two sets of variables) to a question about a polynomial ideal in a polynomial ring in finitely many variables.
Among other important results of the paper, one has to mention is a version of difference Nullstellensatz over an uncountable algebraically closed inversive difference field \(K\). It is shown that if \(F\) is a finite subset of the ring of difference polynomials \(K\{x_{1},\dots, x_{n}\}\), then the following statements are equivalent:
\begin{itemize}
\item[(i)] The system \(F=0\) has a solution in \(K^{\mathbb{Z}}\);
\item[(ii)] \(F=0\) has a solution in \(K^{\mathbb{N}}\);
\item[(iii)] \(F=0\) has finite partial solutions of length \(l\) for sufficiently large \(l\);
\item[(iv)] The difference ideal \(J\) generated by \(F\) in \(K\{x_{1},\dots, x_{n}\}\) does not contain \(1\);
\item[(v)] The reflexive closure of \(J\) in the inversive closure of \(K\{x_{1},\dots, x_{n}\}\) does not contain \(1\);
\item[(vi)] \(F=0\) has a solution in some difference \(K\)-algebra.
\end{itemize}
The paper also contains a number of examples that illustrate applications of the obtained results and counterexamples that show one cannot have a coefficient-independent effective strong Nullstellensatz for systems of difference equations.
Reviewer: Alexander B. Levin (Washington)\(\mathcal{C}^{p}\)-parametrization in o-minimal structureshttps://www.zbmath.org/1475.141132022-01-14T13:23:02.489162Z"Kocel-Cynk, Beata"https://www.zbmath.org/authors/?q=ai:kocel-cynk.beata"Pawłucki, Wiesław"https://www.zbmath.org/authors/?q=ai:pawlucki.wieslaw"Valette, Anna"https://www.zbmath.org/authors/?q=ai:valette-stasica.annaIn this short paper a very intuitive and elementary proof of the uniform $C^p$ parametrization in general o-minimal structures is given. This parametrization was already treated by Yomdin, Gromow and Pila and Wilkie, but he authors give here a very different proof that seems truly elementary. Their approach is clearly related to the approach of Krakow school of late Prof. Łojasiewicz, as it uses induction in a way similar to the Krakow constructions of Whitney stratifications. The very intuitive and well known idea of the cell decomposition is used. The reviewer thinks it would be nice for a reader to start with Proposition 2.8.
In the spirit of Yomdin's work the estimation on the number of parametrizing maps is given in the semialgebraic context.
As the authors mention, all this brings to mind Hironaka's rectilinearization which it generalizes in a sense, the methods used bringing to mind the very interesting work of \textit{W. Pawłucki} [Bull. Pol. Acad. Sci., Math. 32, 555--560 (1984; Zbl 0574.32010)] dealing with Puiseux desingularization of subanalytic sets. The bibliography is very thorough. The paper is certainly worth reading as it stands out by the clarity of geometrical proofs that are becoming rare in modern mathematics.
Reviewer: Zofia Denkowska (Angers)Kappa-slender moduleshttps://www.zbmath.org/1475.160122022-01-14T13:23:02.489162Z"Dimitric, Radoslav"https://www.zbmath.org/authors/?q=ai:dimitric.radoslav-mSummary: For an arbitrary infinite cardinal \(\kappa \), we define classes of \(\kappa \)-cslender and \(\kappa \)-tslender modules as well as related classes of \(\kappa \)-hmodules and initiate a study of these classes.Affine monads and side-effect-freenesshttps://www.zbmath.org/1475.180312022-01-14T13:23:02.489162Z"Jacobs, Bart"https://www.zbmath.org/authors/?q=ai:jacobs.bartSummary: The notions of side-effect-freeness and commutativity are typical for probabilistic models, as subclass of quantum models. This paper connects these notions to properties in the theory of monads. A new property of a monad (``strongly affine'') is introduced. It is shown that for such strongly affine monads predicates are in bijective correspondence with side-effect-free instruments. Also it is shown that these instruments are commutative, in a suitable sense, for monads which are commutative (monoidal).
For the entire collection see [Zbl 1337.68011].Effective metastability for modified Halpern iterations in CAT(0) spaceshttps://www.zbmath.org/1475.470732022-01-14T13:23:02.489162Z"Schade, K."https://www.zbmath.org/authors/?q=ai:schade.k-p|schade.konrad|schade.katharina-clara"Kohlenbach, U."https://www.zbmath.org/authors/?q=ai:kohlenbach.ulrich-wilhelmSummary: We examine convergence results for modified Halpern iterations due to \textit{A. Cuntavepanit} and \textit{B. Panyanak} [ibid. 2011, Article ID 869458, 11 p. (2011; Zbl 1206.47072)]. Following the second author and \textit{L. Leuştean} [Adv. Math. 231, No. 5, 2526--2556 (2012; Zbl 1270.47060)], we extract uniform rates of metastability. This includes extracting rates of asymptotic regularity and replacing an ineffective argument that uses Banach limits.Removahedral congruences versus permutree congruenceshttps://www.zbmath.org/1475.520172022-01-14T13:23:02.489162Z"Albertin, Doriann"https://www.zbmath.org/authors/?q=ai:albertin.doriann"Pilaud, Vincent"https://www.zbmath.org/authors/?q=ai:pilaud.vincent"Ritter, Julian"https://www.zbmath.org/authors/?q=ai:ritter.julianSummary: The associahedron is classically constructed as a removahedron, i.e. by deleting inequalities in the facet description of the permutahedron. This removahedral construction extends to all permutreehedra (which interpolate between the permutahedron, the associahedron and the cube). Here, we investigate removahedra constructions for all quotientopes (which realize the lattice quotients of the weak order). On the one hand, we observe that the permutree fans are the only quotient fans realized by a removahedron. On the other hand, we show that any permutree fan can be realized by a removahedron constructed from any realization of the braid fan. Our results finally lead to a complete description of the type cones of the permutree fans.Construction of ball spaces and the notion of continuityhttps://www.zbmath.org/1475.540012022-01-14T13:23:02.489162Z"Bartsch, René"https://www.zbmath.org/authors/?q=ai:bartsch.rene"Kuhlmann, Katarzyna"https://www.zbmath.org/authors/?q=ai:kuhlmann.katarzyna"Kuhlmann, Franz-Viktor"https://www.zbmath.org/authors/?q=ai:kuhlmann.franz-viktorThe authors discuss the construction of new ball spaces through a set of theoretical operations on the balls. A definition of continuity for functions on ball spaces leads to the notion of quotient spaces. Further, they show the existence of products and coproducts and use this to derive a topological category associated with ball spaces. In the end, an open question is given.
Reviewer: Zoran D. Mitrović (Banja Luka)A synthetic version of Lie's second theoremhttps://www.zbmath.org/1475.580132022-01-14T13:23:02.489162Z"Burke, Matthew"https://www.zbmath.org/authors/?q=ai:burke.matthew-jThe so-called Lie's second theorem states as follows. Let \(G\) and \(H\) be Lie groups with Lie algebras \(\mathfrak{g} = Lie(G)\) and \(\mathfrak{h} = Lie(H)\), with \(G\) is simply connected. If \(f:\mathfrak{g} \to \mathfrak{h}\) is a morphism of Lie algebras, then there is a unique morphism \(F: G \to H\) of Lie groups lifting \(f\), i.e. such that \(f = Lie(F)\). This well-known and classic theorem for Lie groups allows then to integrate Lie algebra morphisms in Lie group morphisms. Now, in more general situations, for example for Lie groupoids, there is as well-known version of this theorem. In the case of Lie groupoids, one has to replace simply connected by source simply connected, a proof of this theorem can be found for instance in [\textit{K. C. H. Mackenzie} and \textit{P. Xu}, Topology 39, No. 3, 445--467 (2000; Zbl 0961.58009)].
In the paper under review, the author gives a synthetic treatment of Lie theory and in particular of Lie's second theorem. In synthetic differential geometry, one replaces the category MAN of smooth manifolds by a well adapted Grothendieck topos \(\mathcal{E}\) explained for example in section 2 of the paper. Working in the context of synthetic differential geometry allows in particular the author to extend Lie theory study for Lie groupoids to at least two interesting types of groupoids in \(\mathcal{E}\), jet groupoids and integral complete groupoids, studied in Section 4 and 6 of the paper under review.
Reviewer: Paulo Carrillo Rouse (Toulouse)From probability measures to each Lévy triplet and backhttps://www.zbmath.org/1475.600892022-01-14T13:23:02.489162Z"Osswald, Horst"https://www.zbmath.org/authors/?q=ai:osswald.horstSummary: It will be shown that all finite-dimensional Lévy processes are completely determined by Borel probability measures on a fixed finite-dimensional Euclidian space in a certain sense. Each Lévy process is infinitely close to a fixed multilinear process, living on that space, depending only on the dimension. Lévy processes can be identified, if they satisfy the same Lévy triplet (Lévy-Khintchine formula). The components of this triplet appear in the Fourier transformation of the current probability measure. \textit{T. Lindstrøm} work [Stochastics Stochastics Rep. 76, No. 6, 517--548 (2004; Zbl 1063.60072)] is used to show that each Lévy triplet is satisfied by an appropriate probability measure on the fixed Euclidian space.
For the entire collection see [Zbl 1470.03011].Duhem's problem revisited: logical versus epistemic formulations and solutionshttps://www.zbmath.org/1475.620722022-01-14T13:23:02.489162Z"Dietrich, Michael"https://www.zbmath.org/authors/?q=ai:dietrich.michael"Honenberger, Phillip"https://www.zbmath.org/authors/?q=ai:honenberger.phillipSummary: When the results of an experiment appears to disconfirm a hypothesis, how does one know whether it's the hypothesis, or rather some auxiliary hypothesis or assumption, that is at fault? Philosophers' answers to this question, now known as ``Duhem's problem,'' have differed widely. Despite these differences, we affirm Duhem's original position that the logical structure of this problem alone does not allow a solution. A survey of philosophical approaches to Duhem's problem indicates that what allows any philosopher, or scientists for that matter, to solve this problem is the addition of epistemic information that guides their assignment of praise and blame after a negative test. We therefore advocate a distinction between the logical and epistemic formulations of Duhem's problem, the latter relying upon additional relevant information about the system being tested. Recognition of the role of this additional information suggests that some proposed solutions to the epistemic form of Duhem's problem are preferable over others.Background beliefs and plausibility thresholds: defending explanationist evidentialismhttps://www.zbmath.org/1475.620762022-01-14T13:23:02.489162Z"Lutz, Matt"https://www.zbmath.org/authors/?q=ai:lutz.mattSummary: In [``Two new objections to explanationism'', ibid. 194, No. 8, 3069--3084 (2017; \url{doi:10.1007/s11229-016-1093-1a})], \textit{B. C. Appley} and \textit{G. Stoutenburg} present two new objections to Explanationist Evidentialism (EE): the Regress Objection and the Threshold Objection. In this paper, I develop a version of EE that is independently plausible and empirically grounded, and show that it can meet Appley and Stoutenburg's objections.Regression to the mean and Judy Benjaminhttps://www.zbmath.org/1475.620772022-01-14T13:23:02.489162Z"McCutcheon, Randall G."https://www.zbmath.org/authors/?q=ai:mccutcheon.randall-gSummary: Van Fraassen's Judy Benjamin problem asks how one ought to update one's credence in \(A\) upon receiving evidence of the sort ``\(A\) may or may not obtain, but \(B\) is \(k\) times likelier than \(C\)'', where \(\{A,B,C\}\) is a partition. Van Fraassen's solution, in the limiting case \(k\rightarrow \infty\), recommends a posterior converging to \(P(A|A\cup B)\) (where \(P\) is one's prior probability function). Grove and Halpern, and more recently Douven and Romeijn, have argued that one ought to leave credence in \(A\) unchanged, i.e. fixed at \(P(A)\). We argue that while the former approach is superior, it brings about a reflection violation due in part to neglect of a ``regression to the mean'' phenomenon, whereby when \(C\) is eliminated by random evidence that leaves \(A\) and \(B\) alive, the ratio \(P(A):P(B)\) ought to drift in the direction of \(1:1\).Automated deduction -- CADE 28. 28th international conference on automated deduction, virtual event, July 12--15, 2021. Proceedingshttps://www.zbmath.org/1475.680262022-01-14T13:23:02.489162ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1428.68018].
Indexed articles:
\textit{Cohen, Liron}, Non-well-founded deduction for induction and coinduction, 3-24 [Zbl 07437069]
\textit{Rabe, Markus N.; Szegedy, Christian}, Towards the automatic mathematician, 25-37 [Zbl 07437070]
\textit{Golińska-Pilarek, Joanna; Huuskonen, Taneli; Zawidzki, Michał}, Tableau-based decision procedure for non-Fregean logic of sentential identity, 41-57 [Zbl 07437071]
\textit{Wernhard, Christoph; Bibel, Wolfgang}, Learning from Łukasiewicz and Meredith: investigations into proof structures, 58-75 [Zbl 07437072]
\textit{Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare}, Efficient local reductions to basic modal logic, 76-92 [Zbl 07437073]
\textit{Nipkow, Tobias; Roßkopf, Simon}, Isabelle's metalogic: formalization and proof checker, 93-110 [Zbl 07437074]
\textit{Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th.}, The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints, 113-130 [Zbl 07437075]
\textit{Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca}, Universal invariant checking of parametric systems with quantifier-free SMT reasoning, 131-147 [Zbl 07437076]
\textit{Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare}, Politeness and stable infiniteness: stronger together, 148-165 [Zbl 07437077]
\textit{Kim, Dohan; Lynch, Christopher}, Equational theorem proving modulo, 166-182 [Zbl 07437078]
\textit{Echenim, Mnacho; Iosif, Radu; Peltier, Nicolas}, Unifying decidable entailments in separation logic with inductive definitions, 183-199 [Zbl 07437079]
\textit{Chaudhuri, Kaustuv}, Subformula linking for intuitionistic logic with application to type theory, 200-216 [Zbl 07437080]
\textit{Fiorentini, Camillo}, Efficient SAT-based proof search in intuitionistic propositional logic, 217-233 [Zbl 07437081]
\textit{Nigam, Vivek; Reis, Giselle; Rahmouni, Samar; Ruess, Harald}, Proof search and certificates for evidential transactions, 234-251 [Zbl 07437082]
\textit{Barnett, Lee A.; Biere, Armin}, Non-clausal redundancy properties, 252-272 [Zbl 07437083]
\textit{Yamada, Akihisa}, Multi-dimensional interpretations for termination of term rewriting, 273-290 [Zbl 07437084]
\textit{Alrabbaa, Christian; Baader, Franz; Borgwardt, Stefan; Koopmann, Patrick; Kovtunova, Alisa}, Finding good proofs for description logic entailments using recursive quality measures, 291-308 [Zbl 07437085]
\textit{Baader, Franz; Koopmann, Patrick; Kriegel, Francesco; Nuradiansyah, Adrian}, Computing optimal repairs of quantified ABoxes w.r.t. static \(\mathcal{EL}\) TBoxes, 309-326 [Zbl 07437086]
\textit{Haifani, Fajar; Tourret, Sophie; Weidenbach, Christoph}, Generalized completeness for SOS resolution and its application to a new notion of relevance, 327-343 [Zbl 07437087]
\textit{Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie}, A unifying splitting framework, 344-360 [Zbl 07437088]
\textit{Hozzová, Petra; Kovács, Laura; Voronkov, Andrei}, Integer induction in saturation, 361-377 [Zbl 07437089]
\textit{Nummelin, Visa; Bentkamp, Alexander; Tourret, Sophie; Vukmirović, Petar}, Superposition with first-class booleans and inprocessing clausification, 378-395 [Zbl 07437090]
\textit{Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar}, Superposition for full higher-order logic, 396-412 [Zbl 07437091]
\textit{Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie}, Making higher-order superposition work, 415-432 [Zbl 07437092]
\textit{Bryant, Randal E.; Heule, Marijn J. H.}, Dual proof generation for quantified Boolean formulas with a BDD-based solver, 433-449 [Zbl 07437093]
\textit{Schurr, Hans-Jörg; Fleury, Mathias; Desharnais, Martin}, Reliable reconstruction of fine-grained proofs in a proof assistant, 450-467 [Zbl 07437094]
\textit{Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H.}, An automated approach to the Collatz conjecture, 468-484 [Zbl 07437095]
\textit{Xu, Runqing; Li, Liming; Zhan, Bohua}, Verified interactive computation of definite integrals, 485-503 [Zbl 07437096]
\textit{Tammet, Tanel; Draheim, Dirk; Järv, Priit}, Confidences for commonsense reasoning, 507-524 [Zbl 07437097]
\textit{Bártek, Filip; Suda, Martin}, Neural precedence recommender, 525-542 [Zbl 07437098]
\textit{Suda, Martin}, Improving ENIGMA-style clause selection while learning from history, 543-561 [Zbl 07437099]
\textit{Neufeld, Emery; Bartocci, Ezio; Ciabattoni, Agata; Governatori, Guido}, A normative supervisor for reinforcement learning agents, 565-576 [Zbl 07437100]
\textit{Krueger, Ryan; Han, Jesse Michael; Selsam, Daniel}, Automatically building diagrams for olympiad geometry problems, 577-588 [Zbl 07437101]
\textit{Baumgartner, Peter}, The Fusemate logic programming system, 589-601 [Zbl 07437102]
\textit{Smallbone, Nicholas}, Twee: an equational theorem prover, 602-613 [Zbl 07437103]
\textit{De Lon, Adrian; Koepke, Peter; Lorenzen, Anton; Marti, Adrian; Schütz, Marcel; Wenzel, Makarius}, The Isabelle/Naproche natural language proof assistant, 614-624 [Zbl 07437104]
\textit{de Moura, Leonardo; Ullrich, Sebastian}, The Lean 4 theorem prover and programming language, 625-635 [Zbl 07437105]
\textit{Errington, Jacob; Jang, Junyoung; Pientka, Brigitte}, Harpoon: mechanizing metatheory interactively, 636-648 [Zbl 07437106]Contextual approximation and higher-order procedureshttps://www.zbmath.org/1475.680482022-01-14T13:23:02.489162Z"Lazić, Ranko"https://www.zbmath.org/authors/?q=ai:lazic.ranko"Murawski, Andrzej S."https://www.zbmath.org/authors/?q=ai:murawski.andrzej-sSummary: We investigate the complexity of deciding contextual approximation (refinement) in finitary Idealized Algol, a prototypical language combining higher-order types with state. Earlier work in the area established the borderline between decidable and undecidable cases, and focussed on the complexity of deciding approximation between terms in normal form.
In contrast, in this paper we set out to quantify the impact of locally declared higher-order procedures on the complexity of establishing contextual approximation in the decidable cases. We show that the obvious decision procedure based on exhaustive \(\beta\)-reduction can be beaten. Further, by classifying redexes by levels, we give tight bounds on the complexity of contextual approximation for terms that may contain redexes up to level \(k\), namely, \((k-1)\)-EXPSPACE-completeness. Interestingly, the bound is obtained by selective \(\beta\)-reduction: redexes from level 3 onwards can be reduced without losing optimality, whereas redexes up to order 2 are handled by a dedicated decision procedure based on game semantics and a variant of pushdown automata.
For the entire collection see [Zbl 1333.68011].Proof relevant corecursive resolutionhttps://www.zbmath.org/1475.680542022-01-14T13:23:02.489162Z"Fu, Peng"https://www.zbmath.org/authors/?q=ai:fu.peng"Komendantskaya, Ekaterina"https://www.zbmath.org/authors/?q=ai:komendantskaya.ekaterina"Schrijvers, Tom"https://www.zbmath.org/authors/?q=ai:schrijvers.tom"Pond, Andrew"https://www.zbmath.org/authors/?q=ai:pond.andrewSummary: Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined inductive meaning, whereas some non-terminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the rôle of coinductive hypothesis.
This paper introduces a heuristic method for obtaining richer coinductive hypotheses in the form of Horn formulas. Our approach subsumes cycle detection and gives coinductive meaning to a larger class of derivations. For this purpose we extend resolution with Horn formula resolvents and corecursive evidence generation. We illustrate our method on non-terminating type class resolution problems.
For the entire collection see [Zbl 1331.68016].Dependent types and fibred computational effectshttps://www.zbmath.org/1475.680572022-01-14T13:23:02.489162Z"Ahman, Danel"https://www.zbmath.org/authors/?q=ai:ahman.danel"Ghani, Neil"https://www.zbmath.org/authors/?q=ai:ghani.neil"Plotkin, Gordon D."https://www.zbmath.org/authors/?q=ai:plotkin.gordon-dSummary: We study the interplay between dependent types and general computational effects. We define a language with both value types and terms, and computation types and terms, where types depend only on value terms. We use computational \(\varSigma\)-types to account for type-dependency in the sequential composition of computations. Our language design is justified by a natural class of categorical models. We account for both algebraic and non-algebraic effects. We also show how to extend the language with general recursion, using continuous families of cpos.
For the entire collection see [Zbl 1333.68011].Guarded dependent type theory with coinductive typeshttps://www.zbmath.org/1475.680602022-01-14T13:23:02.489162Z"Bizjak, Aleš"https://www.zbmath.org/authors/?q=ai:bizjak.ales"Grathwohl, Hans Bugge"https://www.zbmath.org/authors/?q=ai:grathwohl.hans-bugge"Clouston, Ranald"https://www.zbmath.org/authors/?q=ai:clouston.ranald-a"Møgelberg, Rasmus E."https://www.zbmath.org/authors/?q=ai:mogelberg.rasmus-ejlers"Birkedal, Lars"https://www.zbmath.org/authors/?q=ai:birkedal.larsSummary: We present guarded dependent type theory, \(\mathsf {gDTT}\), an extensional dependent type theory with a ``later'' modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of \(\mathsf {gDTT}\) are novel type and term formers involving what we call ``delayed substitutions''. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.
For the entire collection see [Zbl 1333.68011].An interaction net encoding of Gödel's system \(\mathcal {T}\). Declarative pearlhttps://www.zbmath.org/1475.680672022-01-14T13:23:02.489162Z"Mackie, Ian"https://www.zbmath.org/authors/?q=ai:mackie.ian"Sato, Shinya"https://www.zbmath.org/authors/?q=ai:sato.shinyaSummary: The graph rewriting system of interaction nets has been very successful for the implementation of the lambda calculus. In this paper, we show how the ideas can be extended and simplified to encode Gödel's System \(\mathcal {T}\) -- the simply typed \(\lambda \)-calculus extended with numbers. Surprisingly, using some results about System \(\mathcal {T}\), we obtain a very simple system of interaction nets that is significantly more efficient than a direct encoding for the evaluation of programs.
For the entire collection see [Zbl 1331.68016].Compositional coinduction with sized typeshttps://www.zbmath.org/1475.680732022-01-14T13:23:02.489162Z"Abel, Andreas"https://www.zbmath.org/authors/?q=ai:abel.andreas-mSummary: Proofs by induction on some inductively defined structure, e.g., finitely-branching trees, may appeal to the induction hypothesis at any point in the proof, provided the induction hypothesis is only used for immediate substructures, e.g., the subtrees of the node we are currently considering in the proof. The basic principle of structural induction can be relaxed to course-of-value induction, which allows application of the induction hypothesis also to non-immediate substructures, like any proper subtree of the current tree. If course-of-value induction is not sufficient yet, we can resort to define a well-founded relation on the considered structure and use the induction hypothesis for any substructure which is strictly smaller with regard to the constructed relation.
For the entire collection see [Zbl 1337.68011].Complexity optimal decision procedure for a propositional dynamic logic with parallel compositionhttps://www.zbmath.org/1475.680752022-01-14T13:23:02.489162Z"Boudou, Joseph"https://www.zbmath.org/authors/?q=ai:boudou.josephSummary: \(\mathrm{PPDL}^{\mathrm{det}}\) extends propositional dynamic logic (PDL) with parallel composition of programs. This new construct has separation semantics: to execute the parallel program \((\alpha \Vert \beta )\) the initial state is separated into two substates and the programs \(\alpha \) and \(\beta \) are executed on these substates. By adapting the elimination of Hintikka sets procedure, we provide a decision procedure for the satisfiability problem of \(\mathrm{PPDL}^{\mathrm{det}}\). We prove that this decision procedure can be executed in deterministic exponential time, hence that the satisfiability problem of \(\mathrm{PPDL}^{\mathrm{det}}\) is EXPTIME-complete.
For the entire collection see [Zbl 1337.68016].Speeding up the constraint-based method in difference logichttps://www.zbmath.org/1475.680762022-01-14T13:23:02.489162Z"Candeago, Lorenzo"https://www.zbmath.org/authors/?q=ai:candeago.lorenzo"Larraz, Daniel"https://www.zbmath.org/authors/?q=ai:larraz.daniel"Oliveras, Albert"https://www.zbmath.org/authors/?q=ai:oliveras.albert"Rodríguez-Carbonell, Enric"https://www.zbmath.org/authors/?q=ai:rodriguez-carbonell.enric"Rubio, Albert"https://www.zbmath.org/authors/?q=ai:rubio.albertSummary: Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of the program under study as well as the properties to be generated belong to difference logic, i.e., the fragment of linear arithmetic where atoms are inequalities of the form \(u - v \leq k\). However, so far constraint-based techniques have not exploited this fact: in general, Farkas' lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system.
For the entire collection see [Zbl 1337.68009].A program logic for C11 memory fenceshttps://www.zbmath.org/1475.680832022-01-14T13:23:02.489162Z"Doko, Marko"https://www.zbmath.org/authors/?q=ai:doko.marko"Vafeiadis, Viktor"https://www.zbmath.org/authors/?q=ai:vafeiadis.viktorSummary: We describe a simple, but powerful, program logic for reasoning about C11 relaxed accesses used in conjunction with release and acquire memory fences. Our logic, called fenced separation logic (FSL), extends relaxed separation logic with special modalities for describing state that has to be protected by memory fences. Like its precursor, FSL allows ownership transfer over synchronizations and can be used to verify the message-passing idiom and other similar programs. The soundness of FSL has been established in Coq.
For the entire collection see [Zbl 1329.68030].A sound and complete Hoare logic for dynamically-typed, object-oriented programshttps://www.zbmath.org/1475.680852022-01-14T13:23:02.489162Z"Engelmann, Björn"https://www.zbmath.org/authors/?q=ai:engelmann.bjorn"Olderog, Ernst-Rüdiger"https://www.zbmath.org/authors/?q=ai:olderog.ernst-rudigerSummary: A simple dynamically-typed, (purely) object-oriented language is defined. A structural operational semantics as well as a Hoare-style program logic for reasoning about programs in the language in multiple notions of correctness are given. The Hoare logic is proved to be both sound and (relative) complete and is -- to the best of our knowledge -- the first such logic presented for a dynamically-typed language.
For the entire collection see [Zbl 1460.68002].Separation logic-based verification atop a binary-compatible filesystem modelhttps://www.zbmath.org/1475.680942022-01-14T13:23:02.489162Z"Mehta, Mihir Parang"https://www.zbmath.org/authors/?q=ai:mehta.mihir-parang"Cook, William R."https://www.zbmath.org/authors/?q=ai:cook.william-rSummary: Filesystems have held the interest of the formal verification community for a while, with several high-performance filesystems constructed with accompanying proofs of correctness. However, the question of verifying an existing filesystem and incorporating filesystem-specific guarantees remains unexplored, leaving those application developers underserved who need to work with a specific filesystem known to be fit for their purpose. In this work, we present an implementation of a verified filesystem which matches the specification of an existing filesystem, and with our new model AbsFAT tie it to the reasoning framework of separation logic in order to verify properties of programs which use the filesystem. This work is intended to match the target filesystem, FAT32, at a binary level and return the same data and error codes returned by mature FAT32 implementations, considered canonical. We provide a logical framework for reasoning about program behavior when filesystem calls are involved in terms of separation logic, and adapt it to simplify and automate the proof process in ACL2. By providing this framework, we encourage and facilitate greater adoption of software verification by application developers.
For the entire collection see [Zbl 1464.68006].Automating abstract interpretationhttps://www.zbmath.org/1475.680972022-01-14T13:23:02.489162Z"Reps, Thomas"https://www.zbmath.org/authors/?q=ai:reps.thomas-w"Thakur, Aditya"https://www.zbmath.org/authors/?q=ai:thakur.aditya-vSummary: Abstract interpretation has a reputation of being a kind of ``black art'', and consequently difficult to work with. This paper describes a twenty-year quest by the first author to address this issue by raising the level of automation in abstract interpretation. The most recent leg of this journey is the subject of the second author's 2014 Ph.D. dissertation. The paper discusses several different approaches to creating correct-by-construction analyzers. Our research has allowed us to establish connections between this problem and several other areas of computer science, including automated reasoning/decision procedures, concept learning, and constraint programming.
For the entire collection see [Zbl 1329.68030].Relational complexity and higher order logicshttps://www.zbmath.org/1475.681122022-01-14T13:23:02.489162Z"Turull-Torres, José Maria"https://www.zbmath.org/authors/?q=ai:turull-torres.jose-mariaSummary: Relational machines (RM) were introduced as abstract machines that compute queries to relational database instances (dbi's), that are generic (i.e., that preserve isomorphisms). As RM's cannot discern between tuples that are equivalent in first order logic with \(k\) variables, relational complexity was introduced as a complexity theory where the input dbi to a query is measured as its \(size_{k}\), i.e., as the number of classes in the equivalence relation of equality of \(\mathrm {FO}^k\) types of \(k\)-tuples in the dbi. We describe the basic notions of relational complexity, and survey known characterizations of some of its main classes through different fixed point logics and through fragments of second and third order logics.
For the entire collection see [Zbl 1331.68013].Circuit satisfiability and constraint satisfaction around Skolem arithmetichttps://www.zbmath.org/1475.681232022-01-14T13:23:02.489162Z"Glaßer, Christian"https://www.zbmath.org/authors/?q=ai:glasser.christian"Jonsson, Peter"https://www.zbmath.org/authors/?q=ai:jonsson.peter-a"Martin, Barnaby"https://www.zbmath.org/authors/?q=ai:martin.barnaby-dSummary: We study interactions between Skolem arithmetic and certain classes of circuit satisfiability and constraint satisfaction problems (CSPs). We revisit results of
the first author et al. [Discrete Appl. Math. 158, No. 13, 1394--1403 (2010; Zbl 1194.94206)]
in the context of CSPs and settle the major open question from that paper, finding a certain satisfiability problem on circuits -- involving complement, intersection, union and multiplication -- to be decidable. This we prove using the decidability of Skolem arithmetic. Then we solve a second question left open in [loc. cit.] by proving a tight upper bound for the similar circuit satisfiability problem involving just intersection, union and multiplication. We continue by studying first-order expansions of Skolem arithmetic without constants, \((\mathbb {N};\times)\), as CSPs. We find already here a rich landscape of problems with non-trivial instances that are in P as well as those that are NP-complete.
For the entire collection see [Zbl 1337.68005].A logic for non-deterministic parallel abstract state machineshttps://www.zbmath.org/1475.681282022-01-14T13:23:02.489162Z"Ferrarotti, Flavio"https://www.zbmath.org/authors/?q=ai:ferrarotti.flavio-antonio"Schewe, Klaus-Dieter"https://www.zbmath.org/authors/?q=ai:schewe.klaus-dieter"Tec, Loredana"https://www.zbmath.org/authors/?q=ai:tec.loredana"Wang, Qing"https://www.zbmath.org/authors/?q=ai:wang.qing.3Summary: We develop a logic which enables reasoning about single steps of non-deterministic parallel abstract state machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules.
For the entire collection see [Zbl 1331.68013].On the executability of interactive computationhttps://www.zbmath.org/1475.681312022-01-14T13:23:02.489162Z"Luttik, Bas"https://www.zbmath.org/authors/?q=ai:luttik.bas"Yang, Fei"https://www.zbmath.org/authors/?q=ai:yang.fei.5Summary: The model of interactive Turing machines (ITMs) has been proposed to characterise which stream translations are interactively computable; the model of reactive Turing machines (RTMs) has been proposed to characterise which behaviours are reactively executable. In this article we provide a comparison of the two models. We show, on the one hand, that the behaviour exhibited by ITMs is reactively executable, and, on the other hand, that the stream translations naturally associated with RTMs are interactively computable. We conclude from these results that the theory of reactive executability subsumes the theory of interactive computability. Inspired by the existing model of ITMs with advice, which provides a model of evolving computation, we also consider RTMs with advice and we establish that a facility of advice considerably upgrades the behavioural expressiveness of RTMs: every countable transition system can be simulated by some RTM with advice up to a fine notion of behavioural equivalence.
For the entire collection see [Zbl 1337.68005].Unary resolution: characterizing \textsc{Ptime}https://www.zbmath.org/1475.681332022-01-14T13:23:02.489162Z"Aubert, Clément"https://www.zbmath.org/authors/?q=ai:aubert.clement"Bagnol, Marc"https://www.zbmath.org/authors/?q=ai:bagnol.marc"Seiller, Thomas"https://www.zbmath.org/authors/?q=ai:seiller.thomasSummary: We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring, whose elements can be understood as logic programs or sets of rewriting rules over first-order terms. This construction stems from an interactive interpretation of the cut-elimination procedure of linear logic known as the geometry of interaction.
This framework is restricted to terms (logic programs, rewriting rules) using only unary symbols, and this restriction is shown to be complete for polynomial time computation by encoding pushdown automata. Soundness w.r.t. \textsc{Ptime} is proven thanks to a saturation method similar to the one used for pushdown systems and inspired by the memoization technique. A \textsc{Ptime}-completeness result for a class of logic programming queries that uses only unary function symbols comes as a direct consequence.
For the entire collection see [Zbl 1333.68011].Satisfiability via smooth pictureshttps://www.zbmath.org/1475.681372022-01-14T13:23:02.489162Z"de Oliveira Oliveira, Mateus"https://www.zbmath.org/authors/?q=ai:de-oliveira-oliveira.mateusSummary: A picture over a finite alphabet \(\varGamma\) is a matrix whose entries are drawn from \(\varGamma\). Let \(\pi :\varSigma \rightarrow \varGamma\) be a function between finite alphabets \(\varSigma\) and \(\varGamma\), and let \(V,H\subseteq \varSigma \times \varSigma\) be binary relations over \(\varSigma\). Given a picture \(N\) over \(\varGamma\), the picture satisfiability problem consists in determining whether there exists a picture \(M\) over \(\varSigma\) such that \(\pi (M_{ij})=N_{ij}\), and such that the constraints imposed by \(V\) and \(H\) on adjacent vertical and horizontal positions of \(M\) are respectively satisfied. This problem can be easily shown to be NP-complete. In this work we introduce the notion of \(s\)-smooth picture. Our main result states the satisfiability problem for \(s\)-smooth pictures can be solved in time polynomial on \(s\) and on the size of the input picture. With each picture \(N\), one can naturally associate a CNF formula \(F(N)\) which is satisfiable if and only if \(N\) is satisfiable. In our second result, we define an infinite family of unsatisfiable pictures which intuitively encodes the pigeonhole principle. We show that this family of pictures is polynomially smooth. In contrast we show that the formulas which naturally arise from these pictures are hard for bounded-depth Frege proof systems. This shows that there are families of pictures for which our algorithm for the satisfiability for smooth pictures performs exponentially better than certain classical variants of SAT solvers based on the technique of conflict-driven clause-learning (CDCL).
For the entire collection see [Zbl 1337.68009].Tight upper bound on splitting by linear combinations for pigeonhole principlehttps://www.zbmath.org/1475.681382022-01-14T13:23:02.489162Z"Oparin, Vsevolod"https://www.zbmath.org/authors/?q=ai:oparin.vsevolodSummary: The usual DPLL algorithm uses splittings (branchings) on single Boolean variables. We consider an extension to allow splitting on linear combinations mod 2, which yields a search tree called a linear splitting tree. We prove that the pigeonhole principle has linear splitting trees of size \(2^{O(n)}\). This is near-optimal since
\textit{D. Itsykson} and \textit{D. Sokolov} [Lect. Notes Comput. Sci. 8635, 372--383 (2014; Zbl 1427.68123)]
proved a \(2^{\varOmega (n)}\) lower bound. It improves on the size \(2^{\varTheta (n \log n)}\) for splitting on single variables; thus the pigeonhole principle has a gap between linear splitting and the usual splitting on single variables. This is of particular interest since the pigeonhole principle is not based on linear constraints. We further prove that the perfect matching principle has splitting trees of size \(2^{O(n)}\).
For the entire collection see [Zbl 1337.68009].Polynomial interrupt timed automata: verification and expressivenesshttps://www.zbmath.org/1475.681452022-01-14T13:23:02.489162Z"Bérard, B."https://www.zbmath.org/authors/?q=ai:berard.beatrice"Haddad, S."https://www.zbmath.org/authors/?q=ai:haddad.serge"Picaronny, C."https://www.zbmath.org/authors/?q=ai:picaronny.claudine"Safey El Din, M."https://www.zbmath.org/authors/?q=ai:safey-el-din.mohab"Sassolas, M."https://www.zbmath.org/authors/?q=ai:sassolas.mathieuSummary: Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend \textsc{ITA} with polynomial guards and updates, leading to the class of polynomial ITA (\textsc{Pol}ITA). We prove that reachability is decidable in 2EXPTIME on \textsc{Pol}ITA, using an adaptation of the \textit{cylindrical algebraic decomposition} algorithm for the first-order theory of reals. We also obtain decidability for the model checking of a timed version of \textsf{CTL} and for reachability in several extensions of \textsc{Pol}ITA. In particular, compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also study expressiveness questions for \textsc{Pol}ITA and show that \textsc{Pol}ITA are incomparable with stopwatch automata.Decision problems for finite automata over infinite algebraic structureshttps://www.zbmath.org/1475.681582022-01-14T13:23:02.489162Z"Khoussainov, Bakhadyr"https://www.zbmath.org/authors/?q=ai:khoussainov.bakhadyr-m"Liu, Jiamou"https://www.zbmath.org/authors/?q=ai:liu.jiamouSummary: We introduce the concept of finite automata over algebraic structures. We address the classical emptiness problem and its various refinements in our setting. In particular, we prove several decidability and undecidability results. We also explain the way our automata model connects with the existential first order theory of algebraic structures.
For the entire collection see [Zbl 1365.68008].On expressive power of regular expressions over infinite ordershttps://www.zbmath.org/1475.681662022-01-14T13:23:02.489162Z"Rabinovich, Alexander"https://www.zbmath.org/authors/?q=ai:rabinovich.alexanderSummary: Two fundamental results of classical automata theory are the Kleene theorem and the Büchi-Elgot-Trakhtenbrot theorem. Kleene's theorem states that a language of finite words is definable by a regular expression iff it is accepted by a finite state automaton. Büchi-Elgot-Trakhtenbrot's theorem states that a language of finite words is accepted by a finite-state automaton iff it is definable in the weak monadic second-order logic. Hence, the weak monadic logic and regular expressions are expressively equivalent over finite words. We generalize this to words over arbitrary linear orders.
For the entire collection see [Zbl 1337.68014].Derivatives for enhanced regular expressionshttps://www.zbmath.org/1475.681672022-01-14T13:23:02.489162Z"Thiemann, Peter"https://www.zbmath.org/authors/?q=ai:thiemann.peter-jSummary: Regular languages are closed under a wealth of formal language operators. Incorporating such operators in regular expressions leads to concise language specifications, but the transformation of such enhanced regular expressions to finite automata becomes more involved. We present an approach that enables the direct construction of finite automata from regular expressions enhanced with further operators that preserve regularity. Our construction is based on an extension of the theory of derivatives for regular expressions. To retain the standard results about derivatives, we develop a derivability criterion for the compatibility of the extra operators with derivatives.
Some derivable operators do not preserve regularity. Derivatives provide a decision procedure for the word problem of regular expressions enhanced with such operators.
For the entire collection see [Zbl 1365.68008].Comparing trace expressions and linear temporal logic for runtime verificationhttps://www.zbmath.org/1475.681722022-01-14T13:23:02.489162Z"Ancona, Davide"https://www.zbmath.org/authors/?q=ai:ancona.davide"Ferrando, Angelo"https://www.zbmath.org/authors/?q=ai:ferrando.angelo"Mascardi, Viviana"https://www.zbmath.org/authors/?q=ai:mascardi.vivianaSummary: Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime verification of different kinds of properties and systems.
In this paper we formally compare the expressive power of trace expressions with the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification. We show that any LTL formula can be translated into a trace expression which is equivalent from the point of view of runtime verification. Since trace expressions are able to express and verify sets of traces that are not context-free, we can derive that in the context of runtime verification trace expressions are more expressive than LTL.
For the entire collection see [Zbl 1460.68002].Predicate abstraction for linked data structureshttps://www.zbmath.org/1475.681762022-01-14T13:23:02.489162Z"Bakst, Alexander"https://www.zbmath.org/authors/?q=ai:bakst.alexander"Jhala, Ranjit"https://www.zbmath.org/authors/?q=ai:jhala.ranjitSummary: We present alias refinement types (\textsc{Art}), a new approach that uses predicate-abstraction to automate the verification of correctness properties of linked data structures. While there are many techniques for checking that a heap-manipulating program adheres to its specification, they often require that the programmer annotate the behavior of each procedure, for example, in the form of loop invariants and pre- and post-conditions. We introduce a technique that lifts predicate abstraction to the heap by factoring the analysis of data structures into two orthogonal components: (1) alias types, which reason about the physical shape of heap structures, and (2) refinement types, which use simple predicates from an SMT decidable theory to capture the logical or semantic properties of the structures. We evaluate \textsc{Art} by implementing a tool that performs type inference for an imperative language, and empirically show, using a suite of data-structure benchmarks, that \textsc{Art} requires only 21 \% of the annotations needed by other state-of-the-art verification techniques.
For the entire collection see [Zbl 1329.68030].Interval temporal logic model checking: the border between good and bad HS fragmentshttps://www.zbmath.org/1475.681772022-01-14T13:23:02.489162Z"Bozzelli, Laura"https://www.zbmath.org/authors/?q=ai:bozzelli.laura"Molinari, Alberto"https://www.zbmath.org/authors/?q=ai:molinari.alberto"Montanari, Angelo"https://www.zbmath.org/authors/?q=ai:montanari.angelo"Peron, Adriano"https://www.zbmath.org/authors/?q=ai:peron.adriano"Sala, Pietro"https://www.zbmath.org/authors/?q=ai:sala.pietroSummary: The model checking problem has thoroughly been explored in the context of standard point-based temporal logics, such as LTL, CTL, and \({\mathrm{CTL}}^{*}\), whereas model checking for interval temporal logics has been brought to the attention only very recently.
In this paper, we prove that the model checking problem for the logic of Allen's relations started-by and finished-by is highly intractable, as it can be proved to be \({\mathbf {EXPSPACE}}\)-hard. Such a lower bound immediately propagates to the full Halpern and Shoham's modal logic of time intervals (HS). In contrast, we show that other noteworthy HS fragments, namely, propositional neighbourhood logic extended with modalities for the Allen relation starts (resp., finishes) and its inverse started-by (resp., finished-by), turn out to have -- maybe unexpectedly -- the same complexity as LTL (i.e., they are \({\mathbf {PSPACE}}\)-complete), thus joining the group of other already studied, well-behaved albeit less expressive, HS fragments.
For the entire collection see [Zbl 1337.68016].On freeze LTL with ordered attributeshttps://www.zbmath.org/1475.681792022-01-14T13:23:02.489162Z"Decker, Normann"https://www.zbmath.org/authors/?q=ai:decker.normann"Thoma, Daniel"https://www.zbmath.org/authors/?q=ai:thoma.danielSummary: This paper is concerned with freeze LTL, a temporal logic on data words with registers. In a (multi-attributed) data word each position carries a letter from a finite alphabet and assigns a data value to a fixed, finite set of attributes. The satisfiability problem of freeze LTL is undecidable if more than one register is available or tuples of data values can be stored and compared arbitrarily. Starting from the decidable one-register fragment we propose an extension that allows for specifying a dependency relation on attributes. This restricts in a flexible way how collections of attribute values can be stored and compared. This conceptual dimension is orthogonal to the number of registers or the available temporal operators. The extension is strict. Admitting arbitrary dependency relations, satisfiability becomes undecidable. Tree-like relations, however, induce a family of decidable fragments escalating the ordinal-indexed hierarchy of fast-growing complexity classes, a recently introduced framework for non-primitive recursive complexities. This results in completeness for the class \(\mathbf {F}_{\epsilon_0}\). We employ nested counter systems and show that they relate to the hierarchy in terms of the nesting depth.
For the entire collection see [Zbl 1333.68011].A complete decision procedure for linearly compositional separation logic with data constraintshttps://www.zbmath.org/1475.681852022-01-14T13:23:02.489162Z"Gu, Xincai"https://www.zbmath.org/authors/?q=ai:gu.xincai"Chen, Taolue"https://www.zbmath.org/authors/?q=ai:chen.taolue"Wu, Zhilin"https://www.zbmath.org/authors/?q=ai:wu.zhilinSummary: Separation logic is a widely adopted formalism to verify programs manipulating dynamic data structures. Entailment checking of separation logic constitutes a crucial step for the verification of such programs. In general this problem is undecidable, hence only incomplete decision procedures are provided in most state-of-the-art tools. In this paper, we define a linearly compositional fragment of separation logic with inductive definitions, where traditional shape properties for linear data structures, as well as data constraints, e.g., the sortedness property and size constraints, can be specified in a unified framework. We provide complete decision procedures for both the satisfiability and the entailment problem, which are in NP and \({\varPi} ^{P}_{3}\) respectively.
For the entire collection see [Zbl 1337.68016].Model checking and validity in propositional and modal inclusion logicshttps://www.zbmath.org/1475.681872022-01-14T13:23:02.489162Z"Hella, Lauri"https://www.zbmath.org/authors/?q=ai:hella.lauri-t"Kuusisto, Antti"https://www.zbmath.org/authors/?q=ai:kuusisto.antti"Meier, Arne"https://www.zbmath.org/authors/?q=ai:meier.arne"Virtema, Jonni"https://www.zbmath.org/authors/?q=ai:virtema.jonniThe term \textit{team semantics} is used to describe a particular non-standard semantics for standard (first-order, including modal, or propositional) logics in which the interpretation of a formula in a single entity like member of the universe, state of a Kripke structure or propositional variable interpretation is replaced by the interpretation in a set thereof. This gives such logics a kind of second-order flavour whilst retaining the simpler syntax of first-order languages, and it can be used to reason about phenomena arising in settings inherent to sets, like agreeing on truth values, etc. Additional constructs in the syntax are used to formalise statements about such phenomena, and the extension of the basic logic with particular constructs then leads to different logics with team semantics.
The paper at hand studies \textit{inclusion logics}, which arise from the extension by inclusion constructs \(\overrightarrow{p} \subseteq \overrightarrow{q}\), intuitively stating that the tuple of propositions \(\overrightarrow{p}\) is covered by \(\overrightarrow{q}\) in the sense that within the interpreting team, for any team member there is one which assigns the same truth values to \(\overrightarrow{q}\) as the former one assigns to \(\overrightarrow{p}\).
Specifically, the paper contributes further results on the complexity of the model checking and validity checking problems for two types of inclusion logics: those based on propositional respectively modal logic. It presents reductions from related (non-inclusion) logical problems for the lower bounds and upper bounds based on standard algorithmic techniques in this area to obtain complexity results on model checking around the classes P and NP and validity checking involving coNP and coNEXP. (The numbers of the theorems containing such results mostly seem to be broken in tabular overview representations of these results throughout the paper.)
Reviewer: Martin Lange (Kassel)Abstract interpretation with infinitesimals. Towards scalability in nonstandard static analysishttps://www.zbmath.org/1475.681882022-01-14T13:23:02.489162Z"Kido, Kengo"https://www.zbmath.org/authors/?q=ai:kido.kengo"Chaudhuri, Swarat"https://www.zbmath.org/authors/?q=ai:chaudhuri.swarat"Hasuo, Ichiro"https://www.zbmath.org/authors/?q=ai:hasuo.ichiroSummary: We extend abstract interpretation for the purpose of verifying hybrid systems. Abstraction has been playing an important role in many verification methodologies for hybrid systems, but some special care is needed for abstraction of continuous dynamics defined by ODEs. We apply Cousot and Cousot's framework of abstract interpretation to hybrid systems, almost as it is, by regarding continuous dynamics as an infinite iteration of infinitesimal discrete jumps. This extension follows the recent line of work by Suenaga, Hasuo and Sekine, where deductive verification is extended for hybrid systems by (1) introducing a constant \(\mathtt {dt}\) for an infinitesimal value; and (2) employing Robinson's nonstandard analysis (NSA) to define mathematically rigorous semantics. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.
For the entire collection see [Zbl 1329.68030].Deciding bit-vector formulas with mcSAThttps://www.zbmath.org/1475.682262022-01-14T13:23:02.489162Z"Zeljić, Aleksandar"https://www.zbmath.org/authors/?q=ai:zeljic.aleksandar"Wintersteiger, Christoph M."https://www.zbmath.org/authors/?q=ai:wintersteiger.christoph-m"Rümmer, Philipp"https://www.zbmath.org/authors/?q=ai:rummer.philippSummary: The model-constructing satisfiability calculus (mcSAT) is a recently proposed generalization of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry out conflict-driven learning only on the propositional level, mcSAT calculi can also synthesise new theory literals during learning, resulting in a simple yet very flexible framework for designing efficient decision procedures. We present an mcSAT calculus for the theory of fixed-size bit-vectors, based on tailor-made conflict-driven learning that exploits both propositional and arithmetic properties of bit-vector operations. Our procedure avoids unnecessary bit-blasting and performs well on problems from domains like software verification, and on constraints over large bit-vectors.
For the entire collection see [Zbl 1337.68009].Reversal fuzzy switch graphshttps://www.zbmath.org/1475.682332022-01-14T13:23:02.489162Z"Campos, Suene"https://www.zbmath.org/authors/?q=ai:campos.suene"Santiago, Regivan"https://www.zbmath.org/authors/?q=ai:santiago.regivan-h-nunes"Martins, Manuel A."https://www.zbmath.org/authors/?q=ai:martins.manuel-a"Figueiredo, Daniel"https://www.zbmath.org/authors/?q=ai:figueiredo.daniel-rattonSummary: Fuzzy Switch Graphs (FSG) generalize the notion of Fuzzy Graphs by adding high-order arrows and aggregation functions which update the fuzzy values of arrows whenever a zero-order arrow is crossed. In this paper, we propose a more general structure called Reversal Fuzzy Switch Graph (RFSG), which promotes other actions in addition to updating the fuzzy values of the arrows, namely: activation and deactivation of the arrows. RFSGs are able to model dynamical aspects of some systems which generally appear in engineering, computer science and some other fields. The paper also provides a logic to verify properties of the modelled system and closes with an application.
For the entire collection see [Zbl 1464.68006].Modeling imprecise and bipolar algebraic and topological relations using morphological dilationshttps://www.zbmath.org/1475.683792022-01-14T13:23:02.489162Z"Bloch, Isabelle"https://www.zbmath.org/authors/?q=ai:bloch.isabelleSummary: In many domains of information processing, such as knowledge representation, preference modeling, argumentation, multi-criteria decision analysis, spatial reasoning, both vagueness, or imprecision, and bipolarity, encompassing positive and negative parts of information, are core features of the information to be modeled and processed. This led to the development of the concept of bipolar fuzzy sets, and of associated models and tools, such as fusion and aggregation, similarity and distances, mathematical morphology. Here we propose to extend these tools by defining algebraic and topological relations between bipolar fuzzy sets, including intersection, inclusion, adjacency and RCC relations widely used in mereotopology, based on bipolar connectives (in a logical sense) and on mathematical morphology operators. These definitions are shown to have the desired properties and to be consistent with existing definitions on sets and fuzzy sets, while providing an additional bipolar feature. The proposed relations can be used for instance for preference modeling or spatial reasoning. They apply more generally to any type of functions taking values in a poset or a complete lattice, such as L-fuzzy sets.Inclusion and similarity measures for interval-valued fuzzy sets based on aggregation and uncertainty assessmenthttps://www.zbmath.org/1475.683842022-01-14T13:23:02.489162Z"Pękala, Barbara"https://www.zbmath.org/authors/?q=ai:pekala.barbara"Dyczkowski, Krzysztof"https://www.zbmath.org/authors/?q=ai:dyczkowski.krzysztof"Grzegorzewski, Przemysław"https://www.zbmath.org/authors/?q=ai:grzegorzewski.przemyslaw"Bentkowska, Urszula"https://www.zbmath.org/authors/?q=ai:bentkowska.urszulaSummary: We consider the problem of measuring the degree of inclusion and similarity between interval-valued fuzzy sets. We propose a new idea for constructing indicators of inclusion and similarity measures based on the precedence relation, aggregation and uncertainty assessment. Furthermore, we examine selected properties of the suggested measures and their interactions. Finally, we discuss several similarity measures that appear in the literature and compare them with our novel approach.A novel fuzzy rough set model with fuzzy neighborhood operatorshttps://www.zbmath.org/1475.683862022-01-14T13:23:02.489162Z"Ye, Jin"https://www.zbmath.org/authors/?q=ai:ye.jin"Zhan, Jianming"https://www.zbmath.org/authors/?q=ai:zhan.jianming"Ding, Weiping"https://www.zbmath.org/authors/?q=ai:ding.weiping"Fujita, Hamido"https://www.zbmath.org/authors/?q=ai:fujita.hamidoSummary: It is not widely acknowledged that none of existing fuzzy \(\beta\)-neighborhood operators satisfies the reflexivity when \(\beta \neq 1\). To overcome this shortcoming, four types of fuzzy \(\beta\)-neighborhood operators are redefined, which shows that two redefined operators are reflexive. By means of fuzzy logical operators, the \((\mathcal{I}, \mathcal{T})\)-fuzzy rough set (ITFRS) model based on the reflexive fuzzy \(\beta\)-neighborhood operators is constructed in this paper. By combining ITFRS models with the classical TOPSIS method, a new decision-making method is proposed to handle multi-criteria decision-making (MCDM) problems under uncertain and fuzzy environments, where the distance between two intuitionistic fuzzy sets (IFSs) is expressed by an intuitionistic fuzzy number (IFN). Meanwhile, both numerical examples with different types of data are given to explain the feasibility of the proposed method and its effectiveness is also illustrated by a comparative analysis. Finally, the stability of the proposed method is further verified based on an experimental analysis in a real-life MCDM problem.Representing types as neural eventshttps://www.zbmath.org/1475.683982022-01-14T13:23:02.489162Z"Cooper, Robin"https://www.zbmath.org/authors/?q=ai:cooper.robinSummary: One of the claims of Type Theory with Records is that it can be used to model types learned by agents in order to classify objects and events in the world, including speech events. That is, the types can be represented by patterns of neural activation in the brain. This claim would be empty if it turns out that the types are in principle impossible to represent on a finite network of neurons. We will discuss how to represent types in terms of neural events on a network and present a preliminary computational implementation that maps types to events on a network. The kind of networks we will use are closely related to the transparent neural networks discussed by Strannegård.Counting constraints in flat array fragmentshttps://www.zbmath.org/1475.684282022-01-14T13:23:02.489162Z"Alberti, Francesco"https://www.zbmath.org/authors/?q=ai:alberti.francesco"Ghilardi, Silvio"https://www.zbmath.org/authors/?q=ai:ghilardi.silvio"Pagani, Elena"https://www.zbmath.org/authors/?q=ai:pagani.elenaSummary: We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a fragment and we implement our algorithms. The experiments run in discharging proof obligations coming from invariant checking and bounded model-checking benchmarks show the practical feasibility of our decision procedure.
For the entire collection see [Zbl 1337.68016].Lifting QBF resolution calculi to DQBFhttps://www.zbmath.org/1475.684312022-01-14T13:23:02.489162Z"Beyersdorff, Olaf"https://www.zbmath.org/authors/?q=ai:beyersdorff.olaf"Chew, Leroy"https://www.zbmath.org/authors/?q=ai:chew.leroy"Schmidt, Renate A."https://www.zbmath.org/authors/?q=ai:schmidt.renate-a"Suda, Martin"https://www.zbmath.org/authors/?q=ai:suda.martinSummary: We examine existing resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems \(\textsf {Q-Res} < \textsf {IR-calc} < \textsf {IRM-calc} \), the situation is quite different in DQBF. The obvious adaptations of Q-Res and likewise universal resolution are too weak: they are not complete. The obvious adaptation of IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance resolution. Conceptually, we use the relation of DQBF to effectively propositional logic (EPR) and explain our new DQBF calculus based on IR-calc as a subsystem of first-order resolution.
For the entire collection see [Zbl 1337.68009].System description: GAPT 2.0https://www.zbmath.org/1475.684332022-01-14T13:23:02.489162Z"Ebner, Gabriel"https://www.zbmath.org/authors/?q=ai:ebner.gabriel"Hetzl, Stefan"https://www.zbmath.org/authors/?q=ai:hetzl.stefan"Reis, Giselle"https://www.zbmath.org/authors/?q=ai:reis.giselle"Riener, Martin"https://www.zbmath.org/authors/?q=ai:riener.martin"Wolfsteiner, Simon"https://www.zbmath.org/authors/?q=ai:wolfsteiner.simon"Zivota, Sebastian"https://www.zbmath.org/authors/?q=ai:zivota.sebastianSummary: GAPT (General Architecture for Proof Theory) is a proof theory framework containing data structures, algorithms, parsers and other components common in proof theory and automated deduction. In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs. In this paper, we describe the current 2.0 release of GAPT.
For the entire collection see [Zbl 1337.68016].On stronger calculi for QBFshttps://www.zbmath.org/1475.684342022-01-14T13:23:02.489162Z"Egly, Uwe"https://www.zbmath.org/authors/?q=ai:egly.uweSummary: Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations of QBFs into first-order formulas exist. We analyze different translations and show that first-order resolution combined with such translations can polynomially simulate well-known deduction concepts for QBFs. Furthermore, we extend QBF calculi by the possibility to instantiate a universal variable by an existential variable of smaller level. Combining such an enhanced calculus with the propositional extension rule results in a calculus with a universal quantifier rule which essentially introduces propositional formulas for universal variables. In this way, one can mimic a very general quantifier rule known from sequent systems.
For the entire collection see [Zbl 1337.68009].Selecting the selectionhttps://www.zbmath.org/1475.684362022-01-14T13:23:02.489162Z"Hoder, Kryštof"https://www.zbmath.org/authors/?q=ai:hoder.krystof"Reger, Giles"https://www.zbmath.org/authors/?q=ai:reger.giles"Suda, Martin"https://www.zbmath.org/authors/?q=ai:suda.martin"Voronkov, Andrei"https://www.zbmath.org/authors/?q=ai:voronkov.andreiSummary: Modern saturation-based automated theorem provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections and term orderings to tame the growth of the search space and help steer proof search. This paper introduces the notion of lookahead selection that estimates (looks ahead) the effect of selecting a particular literal on the number of immediate children of the given clause and selects to minimize this value. There is also a case made for the use of incomplete selection strategies that attempt to restrict the search space instead of satisfying some completeness criteria. Experimental evaluation in the \textsc{Vampire} theorem prover shows that both lookahead selection and incomplete selection significantly contribute to solving hard problems unsolvable by other methods.
For the entire collection see [Zbl 1337.68016].Q-resolution with generalized axiomshttps://www.zbmath.org/1475.684422022-01-14T13:23:02.489162Z"Lonsing, Florian"https://www.zbmath.org/authors/?q=ai:lonsing.florian"Egly, Uwe"https://www.zbmath.org/authors/?q=ai:egly.uwe"Seidl, Martina"https://www.zbmath.org/authors/?q=ai:seidl.martinaSummary: Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.
For the entire collection see [Zbl 1337.68009].\({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal Khttps://www.zbmath.org/1475.684442022-01-14T13:23:02.489162Z"Nalon, Cláudia"https://www.zbmath.org/authors/?q=ai:nalon.claudia"Hustadt, Ullrich"https://www.zbmath.org/authors/?q=ai:hustadt.ullrich"Dixon, Clare"https://www.zbmath.org/authors/?q=ai:dixon.clareSummary: In this paper, we describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic, \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\). The prover was designed to support experimentation with different combinations of refinements for its basic calculus: it is primarily based on the set of support strategy, which can then be combined with other refinements, simplification techniques and different choices for the underlying normal form and clause selection. The prover allows for both local and global reasoning. We show experimental results for different combinations of strategies and comparison with existing tools.
For the entire collection see [Zbl 1337.68016].nanoCoP: a non-clausal connection proverhttps://www.zbmath.org/1475.684452022-01-14T13:23:02.489162Z"Otten, Jens"https://www.zbmath.org/authors/?q=ai:otten.jensSummary: Most of the popular efficient proof search calculi work on formulae that are in clausal form, i.e. in disjunctive or conjunctive normal form. Hence, most state-of-the-art fully automated theorem provers require a translation of the input formula into clausal form in a preprocessing step. Translating a proof in clausal form back into a more readable non-clausal proof of the original formula is not straightforward. This paper presents a non-clausal theorem prover for classical first-order logic. It is based on a non-clausal connection calculus and implemented with a few lines of Prolog code. By working entirely on the original structure of the input formula, the resulting non-clausal proofs are not only shorter, but can also be more easily translated into, e.g., sequent proofs. Furthermore, a non-clausal proof search is more suitable for some non-classical logics.
For the entire collection see [Zbl 1337.68016].Long distance Q-resolution with dependency schemeshttps://www.zbmath.org/1475.684462022-01-14T13:23:02.489162Z"Peitl, Tomáš"https://www.zbmath.org/authors/?q=ai:peitl.tomas"Slivovsky, Friedrich"https://www.zbmath.org/authors/?q=ai:slivovsky.friedrich"Szeider, Stefan"https://www.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, which use these systems to generate proofs. In this paper, we define a new proof system that combines two such proof systems: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system is sound for the reflexive resolution-path dependency scheme--in fact, we prove that it admits strategy extraction in polynomial time. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q-resolution with universal reduction according to the standard dependency scheme. We report on experiments with a configuration of DepQBF that generates proofs in this system.
For the entire collection see [Zbl 1337.68009].Finding finite models in multi-sorted first-order logichttps://www.zbmath.org/1475.684472022-01-14T13:23:02.489162Z"Reger, Giles"https://www.zbmath.org/authors/?q=ai:reger.giles"Suda, Martin"https://www.zbmath.org/authors/?q=ai:suda.martin"Voronkov, Andrei"https://www.zbmath.org/authors/?q=ai:voronkov.andreiSummary: This work extends the existing MACE-style finite model finding approach to multi-sorted first-order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the multi-sorted setting each sort may have a different domain size, leading to an explosion in the search space. This paper focusses on methods to tame that search space. The key approach adds additional information to the SAT encoding to suggest which domains should be grown. Evaluation of an implementation of techniques in the Vampire theorem prover shows that they dramatically reduce the search space and that this is an effective approach to find finite models in multi-sorted first-order logic.
For the entire collection see [Zbl 1337.68009].Model finding for recursive functions in SMThttps://www.zbmath.org/1475.684482022-01-14T13:23:02.489162Z"Reynolds, Andrew"https://www.zbmath.org/authors/?q=ai:reynolds.andrew"Blanchette, Jasmin Christian"https://www.zbmath.org/authors/?q=ai:blanchette.jasmin-christian"Cruanes, Simon"https://www.zbmath.org/authors/?q=ai:cruanes.simon"Tinelli, Cesare"https://www.zbmath.org/authors/?q=ai:tinelli.cesareSummary: SMT solvers have recently been extended with techniques for finding models of universally quantified formulas in some restricted fragments of first-order logic. This paper introduces a translation that reduces axioms specifying a large class of recursive functions, including terminating functions, to universally quantified formulas for which these techniques are applicable. An evaluation confirms that the approach improves the performance of existing solvers on benchmarks from three sources. The translation is implemented as a preprocessor in the CVC4 solver and in a new higher-order model finder called Nunchaku.
For the entire collection see [Zbl 1337.68016].Congruence closure in intensional type theoryhttps://www.zbmath.org/1475.684522022-01-14T13:23:02.489162Z"Selsam, Daniel"https://www.zbmath.org/authors/?q=ai:selsam.daniel"de Moura, Leonardo"https://www.zbmath.org/authors/?q=ai:de-moura.leonardoSummary: Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT), which form the basis of many interactive theorem provers. The main source of expressiveness in these logics is dependent types, and yet existing congruence closure procedures found in interactive theorem provers based on ITT do not handle dependent types at all and only work on the simply-typed subsets of the logics. Here we present an efficient and proof-producing congruence closure procedure that applies to every function in ITT no matter how many dependencies exist among its arguments, and that only relies on the commonly assumed uniqueness of identity proofs axiom. We demonstrate its usefulness by solving interesting verification problems involving functions with dependent types.
For the entire collection see [Zbl 1337.68016].Effective normalization techniques for HOLhttps://www.zbmath.org/1475.684532022-01-14T13:23:02.489162Z"Wisniewski, Max"https://www.zbmath.org/authors/?q=ai:wisniewski.max"Steen, Alexander"https://www.zbmath.org/authors/?q=ai:steen.alexander"Kern, Kim"https://www.zbmath.org/authors/?q=ai:kern.kim"Benzmüller, Christoph"https://www.zbmath.org/authors/?q=ai:benzmuller.christoph-eSummary: Normalization procedures are an important component of most automated theorem provers. In this work we present an adaption of advanced first-order normalization techniques for higher-order theorem proving which have been bundled in a stand-alone tool. It can be used in conjunction with any higher-order theorem prover, even though the implemented techniques are primarily targeted on resolution-based provers. We evaluated the normalization procedure on selected problems of the TPTP using multiple HO ATPs. The results show a significant performance increase, in both speed and proving capabilities, for some of the tested problem instances.
For the entire collection see [Zbl 1337.68016].Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculihttps://www.zbmath.org/1475.684542022-01-14T13:23:02.489162Z"Zohar, Yoni"https://www.zbmath.org/authors/?q=ai:zohar.yoni"Zamansky, Anna"https://www.zbmath.org/authors/?q=ai:zamansky.annaSummary: Gen2sat is an efficient and generic tool that can decide derivability for a wide variety of propositional non-classical logics given in terms of a sequent calculus. It contributes to the line of research on computer-supported tools for investigation of logics in the spirit of the ``logic engineering'' paradigm. Its generality and efficiency are made possible by a reduction of derivability in analytic pure sequent calculi to SAT. This also makes Gen2sat a ``plug-and-play'' tool so it is compatible with any standard off-the-shelf SAT solver and does not require any additional logic-specific resources. We describe the implementation details of Gen2sat and an evaluation of its performance, as well as a pilot study for using it in a ``hands on'' assignment for teaching the concept of sequent calculi in a logic class for engineering practitioners.
For the entire collection see [Zbl 1337.68016].Kurt Gödels notes on quantum mechanics. Transcriptions and commentshttps://www.zbmath.org/1475.810032022-01-14T13:23:02.489162ZPublisher's description: Kurt Gödel (1906--1978) -- eines der größten mathematischen Genies des 20. Jahrhunderts -- hat unter anderem ein umfangreiches Erbe aus Notizen und Arbeitsbüchern hinterlassen. Dieser Band enthält die bisher unveröffentlichten Arbeitsbücher zur Quantenmechanik aus den Jahren 1935/36. Von Tim Lethen aus der Gabelsberger Kurzschrift übertragen und von Oliver Passon kommentiert, dokumentiert diese Quelle die bisher vollkommen unbekannte, aber intensive Beschäftigung Gödels mit der Quantenmechanik und ihren philosophischen Implikationen. Damit handelt es sich um einen bedeutenden Beitrag zur Forschung über diesen vielseitigen Wissenschaftler, der auch wichtige Impulse zur Geschichte und Philosophie der Quantentheorie liefert.Topos quantum theory with short posetshttps://www.zbmath.org/1475.810072022-01-14T13:23:02.489162Z"Harding, John"https://www.zbmath.org/authors/?q=ai:harding.john"Heunen, Chris"https://www.zbmath.org/authors/?q=ai:heunen.chrisSummary: Topos quantum mechanics, developed in [\textit{A. Döring}, ``Quantum states and measures on the spectral presheaf'', Adv. Sci. Lett. 2, No. 2, 291--301 (2009; \url{doi:10.1166/asl.2009.1037}); with \textit{J. Harding}, Houston J. Math. 42, No. 2, 559--568 (2016; Zbl 1360.46052); with \textit{C. Isham}, Lect. Notes Phys. 813, 753--937 (2011; Zbl 1253.81011); \textit{C. Flori}, A first course in topos quantum theory. Berlin: Springer (2013; Zbl 1280.81001); A second course in topos quantum theory. Cham: Springer (2018; Zbl 1398.81002); \textit{C. J. Isham} and \textit{J. Butterfield}, Int. J. Theor. Phys. 37, No. 11, 2669--2733 (1998; Zbl 0979.81018); ibid. 38, No. 3, 827--859 (1999; Zbl 1007.81009); ibid. 41, No. 4, 613--639 (2002; Zbl 1021.81002); \textit{J. Hamilton} et al., ibid. 39, No. 6, 1413--1436 (2000; Zbl 1055.81004)], creates a topos of presheaves over the poset \(\mathcal{V}(\mathcal{N})\) of abelian von Neumann subalgebras of the von Neumann algebra \(\mathcal{N}\) of bounded operators associated to a physical system, and established several results, including: (a) a connection between the Kochen-Specker theorem and the non-existence of a global section of the spectral presheaf; (b) a version of the spectral theorem for self-adjoint operators; (c) a connection between states of \(\mathcal{N}\) and measures on the spectral presheaf; and (d) a model of dynamics in terms of \(\mathcal{V}(\mathcal{N})\). We consider a modification to this approach using not the whole of the poset \(\mathcal{V}(\mathcal{N})\), but only its elements \(\mathcal{V}(\mathcal{N})^*\) of height at most two. This produces a different topos with different internal logic. However, the core results (a)-(d) established using the full poset \(\mathcal{V}(\mathcal{N})\) are also established for the topos over the smaller poset, and some aspects simplify considerably. Additionally, this smaller poset has appealing aspects reminiscent of projective geometry.What can (mathematical) categories tell us about spacetime?https://www.zbmath.org/1475.830412022-01-14T13:23:02.489162Z"Sanders, Ko"https://www.zbmath.org/authors/?q=ai:sanders.koSummary: It is widely believed that in quantum theories of gravity, the classical description of spacetime as a manifold is no longer viable as a fundamental concept. Instead, spacetime emerges as an approximation in appropriate regimes. In order to understand what is required to explain this emergence, it is necessary to have a good understanding of the classical structure of spacetime. I focus on the concept of spacetime as it appears in locally covariant quantum field theory (LCQFT), an axiomatic framework for describing quantum field theories in the presence of gravitational background fields. A key aspect of LCQFT is the way in which it formulates locality and general covariance, using the language of category theory. I argue that the use of category theory gives a precise and explicit statement of how spacetime acts as an organizing principle in a certain systems view of the world. Along the way I indicate how physical theories give rise to categories that act as a kind of model for modal logic, and how the categorical view of spacetime shifts the emphasis away from the manifold structure. The latter point suggests that the view of spacetime as an organizing principle may persist, perhaps in a generalized way, even in a quantum theory of gravity. I mention some new questions, which this shift in emphasis raises.
For the entire collection see [Zbl 1460.81001].The solution of generalized stable sets and its refinementhttps://www.zbmath.org/1475.910612022-01-14T13:23:02.489162Z"Han, Weibin"https://www.zbmath.org/authors/?q=ai:han.weibin"van Deemen, Adrian"https://www.zbmath.org/authors/?q=ai:van-deemen.adrianThe authors review results on the solution of generalized stable sets for abstract decision problems, in the case of irreflexive but not necessarily asymmetric or complete dominance relations. Although the fundamental properties of this solution are preserved for this kind of dominance relations, they may contain Pareto-suboptimal alternatives when the dominance relation is derived from pairwise majority comparison, and may fail to discriminate among the alternatives under consideration when the dominance relation is a Hamilton cycle, i.e., a cycle that includes all alternatives. A refinement of generalized stable sets is proposed in order to address these shortcomings, in which case the undisturbed generalized stable sets are Pareto optimal and have discriminating power in the case of Hamilton cycles. Moreover, this refinement is always a subset of the solutions of the uncovered set and of the unsurpassed set. This implies that undisturbed generalized stable set also may be seen as a refinement of both the uncovered set and the unsurpassed set
Reviewer: George Stoica (Saint John)Diversity and rights: a social choice-theoretic analysis of the possibility of public reasonhttps://www.zbmath.org/1475.910822022-01-14T13:23:02.489162Z"Chung, Hun"https://www.zbmath.org/authors/?q=ai:chung.hun"Kogelmann, Brian"https://www.zbmath.org/authors/?q=ai:kogelmann.brianSummary: Public reason liberalism takes as its starting point the deep and irreconcilable diversity we find characterizing liberal societies. This deep and irreconcilable diversity creates problems for social order. One method for adjudicating these conflicts is through the use of rights. This paper is about the ability of such rights to adjudicate disputes when \textit{perspectival disagreements} -- or disagreements over how to categorize objects in the world -- obtain. We present both formal possibility and impossibility results for rights structures under varying degrees of perspectival diversity. We show that though perspectival diversity appears to be a troubling problem for the prospect of stable social order, if rights are defined properly then disagreements can likely be resolved in a consistent manner, achieving social cooperation rather than conflict.Application of rough set theory to analyze primary parameters causing death in COVID-19 patientshttps://www.zbmath.org/1475.920892022-01-14T13:23:02.489162Z"Sharma, Leena"https://www.zbmath.org/authors/?q=ai:sharma.leenaSummary: Big data perpetually contains some information that is either structured or unstructured. Also, it is challenging to discover prediction from big data because of its volume, variety, and velocity. Its analysis is vital in intelligent information systems. Rough set theory (RST) provides the best tools to deal with big data analysis as it is the best method for the illustration of uncertainty. Using RST, information can be extracted from raw data in terms of decision rules. RST works on ideas of core, reduct, and information discovered within the types of rules. It is an easy and feasible methodology in getting and minimizing rules from data. Attribute reduction is a vital side of RST. A reduct is a set of minimum attributes that predict a similar description or classification as the whole set of attributes. In this chapter, RST is used to predict the main causes of death in COVID-19 disease at local and global levels. Parameters such as age, sex, pneumonia, and hypertension, were taken to analyze the condition of COVID-19 patients. Using relative reduction, the main parameters that are responsible for death were identified. By identifying the pattern for illness included in COVID-19, precautionary measures can be taken to keep safe from this disease.
For the entire collection see [Zbl 1472.92003].On type-2 fuzzy sets and type-2 fuzzy systemshttps://www.zbmath.org/1475.930672022-01-14T13:23:02.489162Z"Shvedov, A. S."https://www.zbmath.org/authors/?q=ai:shvedov.a-sSummary: One of the advantages of systems based on fuzzy logic (fuzzy systems) is the possibility of a soft switch from one set of values of input parameters of the system to another, when different conclusions are drawn for different sets of these values. A fuzzy set of type 2 is a direct generalization of an ordinary fuzzy set. In this paper, we review some branches of the theory of type-2 fuzzy sets and the theory of type-2 fuzzy systems. We discuss operations on type-2 fuzzy sets, type-2 fuzzy relations, and the centroids of type-2 fuzzy sets and describe type-2 functional fuzzy systems and type-2 relational fuzzy systems.Proceedings of the 51st IEEE international symposium on multiple-valued logic, ISMVL 2021, online event, May 25--27, 2021https://www.zbmath.org/1475.940022022-01-14T13:23:02.489162ZThe articles of this volume will not be indexed individually. For the preceding symposium see [Zbl 1475.94003].Proceedings of the 50th IEEE international symposium on multiple-valued logic, ISMVL 2020, Miyazaki, Japan, November 9--11, 2020https://www.zbmath.org/1475.940032022-01-14T13:23:02.489162ZThe articles of this volume will not be indexed individually. For the preceding symposium see [Zbl 1429.94005].