A history of logic -- Patterns of reasoning -- A language and its meaning -- A symbolic language -- 1850-1950 mathematical logic -- Modern symbolic logic -- Elements of set theory -- Sets, functions, relations -- Induction -- Turning machines -- Computability and decidability -- Propositional logic -- Syntax and proof systems -- Semantics of PL -- Soundness and completeness -- First order logic -- Syntax and proof systems of FOL -- Semantics of (...) FOL -- More semantics -- Soundness and completeness -- Why is first order logic "First Order"? (shrink)

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set (...) that is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED. We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them. (shrink)

From 1929 through 1944, Wittgenstein endeavors to clarify mathematical meaningfulness by showing how (algorithmically decidable) mathematical propositions, which lack contingent "sense," have mathematical sense in contrast to all infinitistic "mathematical" expressions. In the middle period (1929-34), Wittgenstein adopts strong formalism and argues that mathematical calculi are formal inventions in which meaningfulness and "truth" are entirely intrasystemic and epistemological affairs. In his later period (1937-44), Wittgenstein resolves the conflict between his intermediate strong formalism and his criticism (...) of set theory by requiring that a mathematical calculus (vs. a "sign-game") must have an extrasystemic, real world application, thereby returning to the weak formalism of the Tractatus. (shrink)

This somewhat unusual introductory logic text has been clearly designed to bring the student into contact with the mathematical aspects and problems of logical systems as quickly and naturally as possible, at the expense of "fundamental" discussions of logical theory, language and philosophy. In the introductory chapter, the student is introduced to elementary logical technique via Gentzen-type rules of inference, given the requisite set-theoretical background, given a preliminary orientation with respect to the concept of an axiomatic theory, and (...) then shown the full first-order language of the basic predicate calculus. The following chapter develops an axiomatic version of first-order logic with identity, and exhibits proofs of the deduction theorem, completeness theorem, and various applications of equivalence and replacement theorems and other materials to formal number theory. Finally, in what is undoubtably the most valuable part of the book, a good treatment of first-order mathematical theories is given in the third chapter. This includes an extensive discussion of Tarski's semantical theory of truth and a detailed version of Henkin's completeness theorem. Sections on decidability and Gödel's theorem complete this fine introduction to basic mathematical logic. There are numerous exercises throughout the book.—H. P. K. (shrink)

This is a very high quality book with a slightly misleading title. It is difficult to see how it could serve as an introduction for anyone except the mathematically mature or, at least, a student who has already been introduced to formal logic through the lower predicate calculus. Not that these topics are not covered in the book—they comprise the first 92 pages; but the discussion quickly moves into intellectual high gear with sophisticated treatments of the independence of systems (...) of propositional logic, first-order theories, isomorphism of interpretations, and completeness and decidability. With this caveat, Mendelson's book is one of the best of the "second generation" of books on mathematical logic. It is lucid and rigorous, and contains no "frills." It does, however, contain numerous exercises in which the student will have the pleasure of developing for himself some of the more important theorems in the various subjects treated. Among these are chapters on formal number theory, including Gödel's incompleteness theorem, recursive undecidability, Tarski's theorem; a chapter on axiomatic set theory with Hartog's theorem, the axiom of choice, and the axiom of restriction ; and a truly excellent chapter on effective computability which takes off from the notion of an algorithm, and then uses this as a basis upon which to develop the theories of Markov algorithms, Turing algorithms, the theories of Herbrand and Gödel, recursively enumerable sets and undecidable problems. An appendix contains a version of K. Schütte's consistency proof for formal number theory.—H. P. K. (shrink)

The paper proposes a new definition of the conception of effectiveness . A good name for this version of effectiveness is discernibility. The definition is based on the fact that every computation may be reduced to the operation of discerning the fundamental symbols and concatenation of formulas. This approach to effectiveness allows us to formulate the proof of undecidability in such a way that arithmetization of the syntax may be replaced by the use of concatenation in metalogic.

The philosophy of mathematics plays a vital role in the mature philosophy of Charles S. Peirce. Peirce received rigorous mathematical training from his father and his philosophy carries on in decidedly mathematical and symbolic veins. For Peirce, math was a philosophical tool and many of his most productive ideas rest firmly on the foundation of mathematical principles. This volume collects Peirce’s most important writings on the subject, many appearing in print for the first time. Peirce’s determination to (...) understand matter, the cosmos, and "the grand design" of the universe remain relevant for contemporary students of science, technology, and symbolic logic. (shrink)

Inquisitive logic is an extension of classical logic which can express questions. To enable this expressiveness, a possible world semantics is used. So, it is natural to combine inquisitive and modal logic, thus obtaining the inquisitive modal logic $$\textrm{InqML}$$. This paper contributes to the model theory of $$\textrm{InqML}$$. We show that the filtration technique can be adapted to the inquisitive logic semantics. Using filtrations, we prove that $$\textrm{InqML}$$ has the finite model property, i.e., every satisfiable (...) formula is satisfiable in a finite model. As a consequence, we obtain that $$\textrm{InqML}$$ is decidable. Finally, we study filtrations over particular model classes and we prove that some extensions of $$\textrm{InqML}$$ are also decidable. (shrink)

This book offers a comprehensive treatment of the classical decision problem of mathematical logic and of the role of the classical decision problem in modern computer science. The text presents a revealing analysis of the natural order of decidable and undecidable cases and includes a number of simple proofs and exercises.

We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete.

This much-needed book provides a thorough account of temporal logic, one of the most important areas of logic in computer science today. The book begins with a solid introduction to semantical and axiomatic approaches to temporal logic. It goes on to cover predicate temporal logic, meta-languages, general theories of axiomatization, many dimensional systems, propositional quantifiers, expressive power, Henkin dimension, temporalization of other logics, and decidability results. With its inclusion of cutting-edge results and unifying methodologies, this (...) book is an indispensable reference for both the pure logician and the theoretical computer scientist. (shrink)

The optimal balance between decidability and expressiveness is a big problem of logical systems, in particular, of quantified epistemic logics (QELs). On the one hand, decidability is a very significant characteristic of logics that allows us to use such logics in the framework of artificial intelligence. On the other hand, QELs have important expressive capabilities that should not be lost when we construct decidable fragments of these logics. QELs are known to be much more expressive than first-order logics. (...) One important example of their extra expressive power is that they allow us to distinguish between de dicto and de re readings of epistemic sentences. It is clear that such capabilities should be preserved as much as possible in decidable fragments. In this paper, we consider extensions of QELs that include quantification over modalities. Denote this extensions by $$\hbox {Q}_{\Box }$$ Ls. $$\hbox {Q}_{\Box }$$ Ls allows us to make more subtle distinctions between de dicto and de re readings of epistemic sentences, and we also should keep these new features as much as possible in decidable fragments. It is known that there are not much interesting decidable QELs. The situation with $$\hbox {Q}_{\Box }$$ Ls is the same. But in recent years (after 2018), we have obtained a variety of decidable $$\hbox {Q}_{\Box }$$ Ls constructed in different ways. We distinguish between (1) the approach in which for every undecidable $$\hbox {Q}_{\Box }$$ L and for every variant of its decidable fragment, a specific proof is constructed, and (2) the approach in which a class of decidable $$\hbox {Q}_{\Box }$$ Ls is obtained using general tools and a uniform method for all $$\hbox {Q}_{\Box }$$ Ls of this class. In this paper, we compare the results of these approaches. (shrink)

The IOth International Congress of Logic, Methodology and Philosophy of Science, which took place in Florence in August 1995, offered a vivid and comprehensive picture of the present state of research in all directions of Logic and Philosophy of Science. The final program counted 51 invited lectures and around 700 contributed papers, distributed in 15 sections. Following the tradition of previous LMPS-meetings, some authors, whose papers aroused particular interest, were invited to submit their works for publication in a (...) collection of selected contributed papers. Due to the large number of interesting contributions, it was decided to split the collection into two distinct volumes: one covering the areas of Logic, Foundations of Mathematics and Computer Science, the other focusing on the general Philosophy of Science and the Foundations of Physics. As a leading choice criterion for the present volume, we tried to combine papers containing relevant technical results in pure and applied logic with papers devoted to conceptual analyses, deeply rooted in advanced present-day research. After all, we believe this is part of the genuine spirit underlying the whole enterprise of LMPS studies. (shrink)

Ishihara's problem of decidable variables asks which class of decidable propositional variables is sufficient to warrant classical theorems in intuitionistic logic. We present several refinements to the class proposed by Ishii for this problem, which also allows the class to cover Glivenko's logic. We also treat the extension of the problem to minimal logic, suggesting a couple of new classes.

The main result of the paper states that there is a finitely presented group _G_ with decidable word problem where detection of finite subsets of _G_ which generate amenable subgroups is not decidable.

We provide an alternative proof of the decidability of the equational theory of lattices. The proof presented here is quite short and elementary.

In this paper, the positive fragment of the logic math formula of contraction-less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four-valued logic math formula. This extended relevant logic is called math formula, and it has the property of constructible falsity which is known to be a characteristic property of math formula. A Gentzen-type sequent calculus math formula for math formula is introduced, and the (...) cut-elimination and decidability theorems for math formula are proved. Two extended Routley-Meyer semantics are introduced for math formula, and the completeness theorems with respect to these semantics are proved. (shrink)

The uniform continuity theorem states that every pointwise continuous real‐valued function on the unit interval is uniformly continuous. In constructive mathematics, is strictly stronger than the decidable fan theorem, but Loeb [17] has shown that the two principles become equivalent by encoding continuous real‐valued functions as type‐one functions. However, the precise relation between such type‐one functions and continuous real‐valued functions (usually described as type‐two objects) has been unknown. In this paper, we introduce an appropriate notion of continuity for a modulus (...) of a continuous real‐valued function on [0, 1], and show that real‐valued functions with continuous moduli are exactly those functions induced by Loeb's codes. Our characterisation relies on two assumptions: (1) real numbers are represented by regular sequences (equivalently Cauchy sequences with explicitly given moduli); (2) the continuity of a modulus is defined with respect to the product metric on the regular sequences inherited from the Baire space. Our result implies that is equivalent to the statement that every pointwise continuous real‐valued function on [0, 1] with a continuous modulus is uniformly continuous. We also show that is equivalent to a similar principle for real‐valued functions on the Cantor space. These results extend Berger's [2] characterisation of for integer‐valued functions on and unify some characterisations of in terms of functions having continuous moduli. (shrink)

We study concepts of decidability for subsets of Euclidean spaces ℝk within the framework of approximate computability . A new notion of approximate decidability is proposed and discussed in some detail. It is an effective variant of F. Hausdorff's concept of resolvable sets, and it modifies and generalizes notions of recursivity known from computable analysis, formerly used for open or closed sets only, to more general types of sets. Approximate decidability of sets can equivalently be expressed by (...) computability of the characteristic functions by means of appropriately working oracle Turing machines. The notion fulfills some natural requirements and is hereditary under canonical embeddings of sets into spaces of higher dimensions. However, it is not closed under binary union or intersection of sets. We also show how the framework of resolvability and approximate decidability can be applied to investigate concepts of reducibility for subsets of Euclidean spaces. (shrink)

In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B prop [x : A], i. e. to require that the predicate ∨ ¬ B) is provable, is equivalent, when working within the framework of Martin-Löf's Intuitionistic Type Theory, to require that there exists a decision function ψ: A → Boole such that = Booletrue) ↔ B). Since we will also show that the proposition x = Booletrue [x: Boole] is decidable, we (...) can alternatively say that the main result of this paper is a proof that the decidability of the predicate Bprop [x : A] can be effectively reduced by a function ψ A → Boole to the decidability of the predicate ψ = Booletrue [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function ψ, together with a proof of its correctness, is effectively constructed as a function of the proof of ∨ ¬ B). (shrink)

We show that various fragments of the intuitionistic/constructive theory of the reals are decidable.

We prove that if an n-element algebra generates the variety \ which is actively structurally complete, then the cardinality of the carrier of each subdirectly irreducible algebra in \ is at most \\cdot n^{2\cdot n}}\). As a consequence, with the use of known results, we show that there exist algorithms deciding whether a given finite algebra \ generates the structurally complete variety \\) in the cases when \\) is congruence modular or \\) is congruence meet-semidistributive or \ is a semigroup.

We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square}$$\end{document}-free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\phi}$$\end{document} and a sublanguage L of the language of the formula, we can decide whether \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} (...) \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\phi}$$\end{document} has a uniform interpolant with respect to L in K4. The \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square}$$\end{document}-free case is proved using a reduction to the Gödel Löb Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the μ-calculus. (shrink)

The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the ∀*∀ class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.

In this paper we investigate those extensions of the bimodal provability logic ${\vec CSM}_{0}$ (alias ${\vec PRL}_{1}$ or ${\vec F}^{-})$ which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing ${\vec CSM}_{0}$ are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not (...) even complete with respect to Kripke semantics. (shrink)

We discuss several ontological properties of explicit mathematics and operational set theory: global choice, decidable classes, totality and extensionality of operations, function spaces, class and set formation via formulas that contain the definedness predicate and applications.

In first order logic without equality, but with arbitrary relations and functions the ∃*∀∃* class is the unique maximal solvable prefix class. We show that the satisfiability problem for this class is decidable in deterministic exponential time The result is established by a structural analysis of a particular infinite subset of the Herbrand universe and by a polynomial space bounded alternating procedure.

We consider the decision problem for modules over a group ring ℤ[G], where G is a cyclic group of prime order. We show that it reduces to the same problem for a class of certain abelian structures, and we obtain some partial decidability results for this class.

We extend the analysis of the decision problem for modules over a group ring ℤ[G] to the case when G is a cyclic group of squarefree order. We show that separated ℤ[G]-modules have a decidable theory, and we discuss the model theoretic role of these modules within the class of all ℤ[G]-modules. The paper includes a short analysis of the decision problem for the theories of modules over ℤ[ζm], where m is a positive integer and ζm is a primitive mth (...) root of 1. (shrink)

An AE-sentence is a sentence in prenex normal form with all universal quantifiers preceding all existential quantifiers, and the AE-theory of a structure is the set of all AE-sentences true in the structure. We show that the AE-theory of \, \cap, \cup, 0, 1)\) is decidable by giving a procedure which, for any AE-sentence in the language, determines the truth or falsity of the sentence in our structure.

The implication relationship between subsystems in Reverse Mathematics has an underlying logic, which can be used to deduce certain new Reverse Mathematics results from existing ones in a routine way. We use techniques of modal logic to formalize the logic of Reverse Mathematics into a system that we name s-logic. We argue that s-logic captures precisely the “logical” content of the implication and nonimplication relations between subsystems in Reverse Mathematics. We present a sound, complete, decidable, (...) and compact tableau-style deductive system for s-logic, and explore in detail two fragments that are particularly relevant to Reverse Mathematics practice and automated theorem proving of Reverse Mathematics results. (shrink)

We prove decidability of satisfiability of sentences of the monodic packed fragment of first-order temporal logic with equality and connectives Until and Since, in models with various flows of time and domains of arbitrary cardinality. We also prove decidability over models with finite domains, over flows of time including the real order.

Let G be the direct sum of the noncyclic groupof order four and a cyclic groupwhoseorderisthe power pn of some prime p. We show that ℤ2G-lattices have a decidable theory when the cyclotomic polynomia equation image is irreducible modulo 2ℤ for every j ≤ n. More generally we discuss the decision problem for ℤ2G-lattices when G is a finite group whose Sylow 2-subgroups are isomorphic to the noncyclic group of order four.

SUMMARY Every case of knowing that S is, was or will be P involves, when analysed, some decision or the acceptance of some decision. This applies equally when you are discussing the so-called tautological propositions of logic and pure mathematics; for you can only claim to “know” that some logical or mathematical proposition is true because you have previously decided to accept that certain meanings shall be attached to certain words, or that certain symbols shall function in a (...) certain way. When we examine what philosophers are doing who demand that we prefix “we know” to this or that part of their analyses of perceptual situations, we find that they are often using “know” in a question-begging manner in order to buttress some particular, and usually contentious, analysis. Nor is any philosopher in a position to lay down rigid and precise rules for the proper use of “know” in ordinary conversation; although he can usefully debate the nature and cogency of the grounds on which decisions, issuing in “know”-statements, are generally made. Lastly, Austin is quite right in claiming that when I say “I know” I give my authority and pledge my word, which I do not do when I merely say “I believe”; but I give my authority and pledge my word only because I have decided, or accepted a decision, that so and so is the case. (shrink)

This article focuses on defective conditionals ? namely indicative conditionals whose antecedents are false and whose truth-values therefore cannot be determined. The problem is to decide which formal connective can adequately represent this usage. Classical logic renders defective conditionals true whereas traditional mathematics dismisses them as irrelevant. This difference in treatment entails that, at the propositional level, classical logic validates some sentences that are intuitively false in plane geometry. With two proofs, I show that the same flaw is (...) shared by a family of trivalent logics. I go on to examine the strict conditional and its derivatives. This family is the only one to avoid the faulty inference but it does so without addressing the status of the truth-value assigned to defective conditionals. (shrink)

In this paper we prove, modulo Schanuel's Conjecture, that there are algorithms which decide if two exponential polynomials in π are equal in ℝ and if two exponential polynomials in π and i coincide in ℂ.