‘First. That on October 23, in the city of New York, your relator was arrested by divers persons claiming to be acting by authority of the government of the United States, and was by said persons conveyed to the United States immigration station at Ellis island, in the harbor of New York, and is now there imprisoned by the commissioner of immigration of the port of New York.

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)

Common-sense folk psychology and mainstream philosophy of action agree about decisions: these are under an agent's direct control, and are thus intentional actions for which agents can be held responsible. I begin this paper by presenting a problem for this view. In short, since the content of the motivational attitudes that drive deliberation and decision remains open-ended until the moment of decision, it is unclear how agents can be thought to exercise control over what they decide at the moment of (...) deciding. I note that this problem might motivate a non-actional view of deciding?a view that decisions are not actions, but are instead passive events of intention acquisition. For without an understanding of how an agent might exercise control over what is decided at the moment of deciding, we lack a good reason for maintaining commitment to an actional view of deciding. However, I then offer the required account of how agents exercise control over decisions at the moment of deciding. Crucial to this account is an understanding of the relation of practical deliberation to deciding, an understanding of skilled deliberative activity, and the role of attention in the mental action of deciding. (shrink)

To decide to A, as I conceive of it, is to perform a momentary mental action of forming an intention to A. I argue that ordinary instances of practical deciding, so conceived, falsify the following...

This book is the most comprehensive treatment available of one of the most urgent - and yet in some respects most neglected - problems in bioethics: decision-making for incompetents. Part I develops a general theory for making treatment and care decisions for patients who are not competent to decide for themselves. It provides an in-depth analysis of competence, articulates and defends a coherent set of principles to specify suitable surrogate decisionmakers and to guide their choices, examines the value of advance (...) directives, and investigates the role that considerations of cost ought to play in decisions concerning incompetents. Part II applies this theoretical framework to the distinctive problems of three important classes of individuals, many of whom are incompetent: minors, the elderly and psychiatric patients. The authors' approach combines a probing analysis of fundamental issues in ethical theory with a sensitive awareness of the concrete realities of health care institutions and the highly personal and individual character of difficult practical problems. Its broad scope will appeal to health professionals, moral philosophers and lawyers alike. (shrink)

Can we decide to trust? Sometimes, yes. And when we do, we need not believe that our trust will be vindicated. This paper is motivated by the need to incorporate these facts into an account of trust. Trust involves reliance; and in addition it requires the taking of a reactive attitude to that reliance. I explain how the states involved here differ from belief. And I explore the limits of our ability to trust. I then turn to the idea of (...) trusting what others say. I suggest that we sometimes decide to trust people to be sincere and knowledgeable; and that having taken this attitude towards them, we come to believe what they say. I spell out some consequences that this has for an account of testimony, and for van Fraassen's decision theoretic principle of Reflection. (shrink)

The purpose of this paper is to prove the decidability ofstit theory (a logic of seeing to it that) with a single agent andRefref Equivalence. This result is obtained through an axiomatization of the theory and a proof that it has thefinite model property. A notion ofcompanions to stit formulas is introduced and extensively used in the proof.

Mereological theories are theories based on a binary predicate ‘being a part of’. It is believed that such a predicate must at least define a partial ordering. A mereological theory can be obtained by adding on top of the basic axioms of partial orderings some of the other axioms posited based on pertinent philosophical insights. Though mereological theories have aroused quite a few philosophers’ interest recently, not much has been said about their meta-logical properties. In this paper, I will look (...) into whether those theories are decidable or not. Besides, since theories of Boolean algebras are in some sense upper bounds of mereological theories which can be found in the literature, I shall also make some observations about the possibility of getting mereological theories beyond Boolean algebras. (shrink)

The signature of the formal language of mereology contains only one binary predicate P which stands for the relation “being a part of”. Traditionally, P must be a partial ordering, that is, ${\forall{x}Pxx, \forall{x}\forall{y}((Pxy\land Pyx)\to x=y)}$ and ${\forall{x}\forall{y}\forall{z}((Pxy\land Pyz)\to Pxz))}$ are three basic mereological axioms. The best-known mereological theory is “general extensional mereology”, which is axiomatized by the three basic axioms plus the following axiom and axiom schema: (Strong Supplementation) ${\forall{x}\forall{y}(\neg Pyx\to \exists z(Pzy\land \neg Ozx))}$ , where Oxy means ${\exists (...) z(Pzx\land Pzy)}$ , and (Fusion) ${\exists x\alpha \to \exists z\forall y(Oyz\leftrightarrow \exists x(\alpha \land Oyx))}$ , for any formula α where z and y do not occur free. In this paper, I will show that general extensional mereology is decidable, and will also point out that the decidability of the first-order approximation of the theory of complete Boolean algebras can be shown in the same way. (shrink)

Policy-makers must sometimes choose between an alternative which has somewhat lower expected value for each person, but which will substantially improve the outcomes of the worst off, or an alternative which has somewhat higher expected value for each person, but which will leave those who end up worst off substantially less well off. The popular ex ante Pareto principle requires the choice of the alternative with higher expected utility for each. We argue that ex ante Pareto ought to be rejected (...) because it conflicts with the requirement that, when possible, one ought to decide as one would with full information. We apply our argument in an analysis of US policy on screening for breast cancer. -/- . (shrink)

A sequent calculus S for the variety tqBa of all topological quasi-Boolean algebras is established. Using a construction of syntactic finite algebraic model, the finite model property of S is shown, and thus the decidability of S is obtained. We also introduce two non-distributive variants of topological quasi-Boolean algebras. For the variety TDM5 of all topological De Morgan lattices with the axiom 5, we establish a sequent calculus S5 and prove that the cut elimination holds for it. Consequently the (...) decidability of S5 is established. Furthermore, this proof-theoretic method is applied to some subvarieties of TDM5. (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)

The ways in which we exercise intentional agency are varied. I take the domain of intentional agency to include all that we intentionally do versus what merely happens to us. So the scope of our intentional agency is not limited to intentional action. One can also exercise some intentional agency in omitting to act and, importantly, in producing the intentional outcome of an intentional action. So, for instance, when an agent is dieting, there is an exercise of agency both with (...) respect to the agent’s actions and omissions that constitute her dieting behavior and in achieving the intended outcome of losing weight. In our mental lives we exercise intentional agency both in performing mental actions and when we intentionally produce certain outcomes at which our mental actions are aimed. The nature and scope of our intentional agency in our mental lives with respect to controlling the acquisition of mental states such as belief, desire, and intention is a topic that is of interest in its own right. In this essay, I will focus solely on our control over coming to believe. Understanding what sort of control we have our beliefs has far-reaching implications. For instance, theorizing about self-deception and wishful thinking is aided by theorizing about what if any intentional agency we can exercise with respect to acquiring beliefs. Another often mentioned concern that motivates thinking about doxastic agency comes from religion (when conversion requires a change of belief). We also hold persons morally and epistemically responsible for beliefs they have or fail to have. Finally, some deontological theories of epistemic justification require that agents be able to exercise a robust form of doxastic control. Fruitful work on any of these problems requires that we have an account of our intentional agency in acquiring beliefs. There are at least three loci of doxastic control. The first is over acquiring beliefs. The second is over maintaining beliefs. The third is over how we use our beliefs. I am chiefly concerned with the first locus of doxastic control in this essay, but I will say something about the second locus along the way. Also, I will only consider one way we might exercise control over acquiring beliefs. Specifically, I will present an argument against direct doxastic voluntarism (DDV). By “DDV” I mean to refer to the thesis that it is conceptually possible for agents to consciously exercise the same sort of direct voluntary control over coming to acquire a doxastic attitude—such as belief, suspension of belief, and disbelief—that they exercise over uncontroversial basic actions. If DDV is correct, then coming to believe can be a basic action-type. DDV, or something very close to it, was Bernard Williams’ target in his 1973 paper, “Deciding to Believe.” Williams’s argument is widely regarded as having been a failure. But I think that Williams was on to something in his paper. Hence, in this paper, while I do not attempt to resurrect Williams’s argument, I develop and defend a revised argument for a thesis that is quite close to Williams’s. I will proceed as follows. First, I will discuss Bernard Williams’ (1973) failed attempt at showing that DDV is conceptually impossible. This will be followed by a discussion of some constraints on our belief-forming activities. I will then clarify my target a bit more than Williams does in his original paper. Finally, I will present my own argument against the conceptual possibility of DDV. (shrink)

As this passage from a recent book on the psychology of decision-making indicates, deciding seems to be part of our daily lives. But what is it to decide to do something? It may be true, as some philosophers have claimed, that to decide to A is to perform a mental action of a certain kind – specifically, an action of forming an intention to A. (Henceforth, the verb ‘form’ in this context is to be understood as an action verb.) Even (...) if this is so, we are faced with pressing questions. Do we form all of our intentions? If not, how does forming an intention differ from other ways of acquiring one? Do we ever, in fact, form intentions, or do we rather merely acquire them in something like the way we acquire beliefs or desires? These are some of the questions that will occupy me here. My aim is to clarify the nature of deciding to act and to make a case for the occurrence of genuine acts of intention formation. (shrink)

The species of indeterminist tense logic called Peircean by A. N. Prior is proved to be recursively decidable.

We formally introduce a novel, yet ubiquitous, category of norms: norms of instrumentality. Norms of this category describe which actions are obligatory, or prohibited, as instruments for certain purposes. We propose the Logic of Agency and Norms (LAN) that enables reasoning about actions, instrumentality, and normative principles in a multi-agent setting. Leveraging LAN , we formalize norms of instrumentality and compare them to two prevalent norm categories: norms to be and norms to do. Last, we pose principles relating the three (...) categories and evaluate their validity vis-à-vis notions of deliberative acting. On a technical note, the logic will be shown decidable via the finite model property. (shrink)

This article contends that the intellectual history of developing British imperial policy towards indigenous peoples' property rights to land in the mid-nineteenth century is best approached through seeing policy as made in the context of two intellectual vocabularies that were conjoined: the stadial theory of history and the law of nations. New Zealand provides an example of these languages in contestable play between the 1830s and 1853 at a time when the expanding British Empire as a whole vied with issues (...) such as 'native title' and the placement and control of settler populations. (shrink)

Presented here is a new result concerning the computational power of so-called SADn computers, a class of Turing-machine-based computers that can perform some non-Turing computable feats by utilising the geometry of a particular kind of general relativistic spacetime. It is shown that SADn can decide n-quantifier arithmetic but not (n+1)-quantifier arithmetic, a result that reveals how neatly the SADn family maps into the Kleene arithmetical hierarchy. Introduction Axiomatising computers The power of SAD computers Remarks regarding the concept of computability.

We give a decision procedure for the ∀∃-theory of the weak truth-table (wtt) degrees of the recursively enumerable sets. The key to this decision procedure is a characterization of the finite lattices which can be embedded into the r.e. wtt-degrees by a map which preserves the least and greatest elements: a finite lattice has such an embedding if and only if it is distributive and the ideal generated by its cappable elements and the filter generated by its cuppable elements are (...) disjoint. We formulate general criteria that allow one to conclude that a distributive upper semi-lattice has a decidable two-quantifier theory. These criteria are applied not only to the weak truth-table degrees of the recursively enumerable sets but also to various substructures of the polynomial many-one (pm) degrees of the recursive sets. These applications to the pm degrees require no new complexity-theoretic results. The fact that the pm-degrees of the recursive sets have a decidable two-quantifier theory answers a question raised by Shore and Slaman in [21]. (shrink)

During the first wave of the COVID-19 pandemic in Italy, practitioners had to make tragic decisions regarding the allocation of scarce resources in the ICU. The Italian debate has paid a lot of attention to identifying the specific regulatory criteria for the allocation of resources in the ICU; in this paper, however, we argue that deciding such criteria is not enough for the implementation of fair and transparent allocative decisions. In this respect, we discuss three ethical issues: (a) in the (...) Italian context, the treating physician, rather than a separate committee, was generally the one responsible for the allocation decision; (b) although many allocative guidelines have supported moral equivalence between withholding and withdrawing treatments, some health professionals have continued to consider it a morally problematic aspect; and (c) the health workers who have had to make the aforementioned decisions or even only worked in ICU during the pandemic often experienced moral distress. We conclude by arguing that, even if these problems are not directly related to the above-mentioned issues of distributive justice, they can nevertheless directly affect the quality and ethics of the implementation of allocative criteria, regardless of those chosen. (shrink)

In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted (...) first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps. (shrink)

Book reviewed in this article: The Concept of Moral Consensus: The Case of Technological Interventions into Human Reproduction. Edited by Kurt Bayertz. Deciding Together: Bioethics and Moral Consensus. By Jonathan D. Moreno.

Let HF be the collection of the hereditarily finite well-founded sets and let the primitive language of set theory be the first-order language which contains binary symbols for equality and membership only. As announced in a previous paper by the authors, "Truth in V for ∃*∀∀-sentences is decidable," truth in HF for ∃*∀∀-sentences of the primitive language is decidable. The paper provides the proof of that claim.

This paper extends the investigations into logical properties of the quantified argument calculus (Quarc) by suggesting a series of proper subsystems which, although retaining the entire vocabulary of Quarc, restrict quantification in such a way as to make the result decidable. The proof of decidability is via a procedure that prunes the infinite branches of a derivation tree in what is a syntactic counterpart of semantic filtration. We demonstrate an application of one of these systems by showing that Aristotle’s (...) assertoric syllogistic is embeddable within, thus also providing another method of showing its decidability. (shrink)

The present paper has three objectives: Presenting an actualization of a proof of the decidability of monadic predicates logic in the contemporary model theory context; Show examples of decidable and undecidable fragments inside First order logic, offering an original proof of the following theorem: Any formula of First of order logic is decidable if its prenex normal form is in the following form: ∀x1,…,∀xn∃y1,…,∃ymφ; Presenting a theorem that characterizes the validity of First order logic by the tautologicity of Propositional (...) logic, said result is interesting since immediately arises the doubt of how to conciliate said characterization with Alonzo Church’s Undecidability Theorem for First Order Logic. (shrink)

For $\Bbb {F}$ the field of real or complex numbers, let $CG(\Bbb {F})$ be the continuous geometry constructed by von Neumann as a limit of finite dimensional projective geometries over $\Bbb {F}$ . Our purpose here is to show the equational theory of $CG(\Bbb {F})$ is decidable.

Mele's chapter addresses two primary aims. The first is to develop an experimentally useful conception of conscious deciding. The second is to challenge a certain source of skepticism about free will: the belief that conscious decisions and intentions are never involved in producing corresponding overt actions. The challenge Mele develops has a positive dimension that accords with the aims of this volume: It sheds light on a way in which some conscious decisions and intentions do seem to be efficacious.

Qualitative Reasoning (QR) is an area of research within Artificial Intelligence that automates reasoning and problem solving about the physical world. QR research aims to deal with representation and reasoning about continuous aspects of entities without the kind of precise quantitative information needed by conventional numerical analysis techniques. Order-of-magnitude Reasoning (OMR) is an approach in QR concerned with the analysis of physical systems in terms of relative magnitudes. In this paper we consider the logic OMR_N for order-of-magnitude reasoning with the (...) bidirectional negligibility relation. It is a multi-modal logic given by a Hilbert-style axiomatization that reflects properties and interactions of two basic accessibility relations (strict linear order and bidirectional negligibility). Although the logic was studied in many papers, nothing was known about its decidability. In the paper we prove decidability of OMR N by showing that the logic has the strong finite model property. (shrink)

This paper presents proofs of completeness and decidability of a non-temporal fragment of an Xstit logic. This shows a distinction between the non-temporal fragments of Xstit logic and regular stit logic since the latter is undecidable. The proof of decidability is via the finite model property. The finite model property is shown to hold by constructing a filtration. However, the set that is used to filter the models isn’t simply closed under subformulas, it has more complex closure conditions. (...) The filtration set is akin to the Fischer–Ladner closure of a set used to show completeness and decidability of propositional dynamic logic. (shrink)

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

A definition is given for formulae $A_1,\ldots,A_n$ in some theory $T$ which is formalized in a propositional calculus $S$ to be (in)dependent with respect to $S$. It is shown that, for intuitionistic propositional logic $\mathbf{IPC}$, dependency (with respect to $\mathbf{IPC}$ itself) is decidable. This is an almost immediate consequence of Pitts' uniform interpolation theorem for $\mathbf{IPC}$. A reasonably simple infinite sequence of $\mathbf{IPC}$-formulae $F_n(p, q)$ is given such that $\mathbf{IPC}$-formulae $A$ and $B$ are dependent if and only if at least (...) on the $F_n(A, B)$ is provable. (shrink)

In this paper we shall introduce a simple temporal logic suitable for reasoning about the temporal aspects of parallel universes, parallel processes, distributed systems, or multiple agents. We will use a variant of the mosaic method to prove decidability of this logic. We also show that the logic does not have the finite model property. This shows that the mosaic method is sometimes a stronger way of establishing decidability.

Justification logics are modal logics that include justifications for the agent's knowledge. So far, there are no decidability results available for justification logics with negative introspection. In this paper, we develop a novel model construction for such logics and show that justification logics with negative introspection are decidable for finite constant specifications.

A subspace V of an infinite dimensional fully effective vector space V ∞ is called decidable if V is r.e. and there exists an r.e. W such that $V \oplus W = V_\infty$ . These subspaces of V ∞ are natural analogues of recursive subsets of ω. The set of r.e. subspaces forms a lattice L(V ∞ ) and the set of decidable subspaces forms a lower semilattice S(V ∞ ). We analyse S(V ∞ ) and its relationship with L(V (...) ∞ ). We show: Proposition. Let U, V, W ∈ L(V ∞ ) where U is infinite dimensional and $U \oplus V = W$ . Then there exists a decidable subspace D such that U |oplus D = W. Corollary. Any r.e. subspace can be expressed as the direct sum of two decidable subspaces. These results allow us to show: Proposition. The first order theory of the lower semilattice of decidable subspaces, Th(S(V ∞ )), is undecidable. This contrasts sharply with the result for recursive sets. Finally we examine various generalizations of our results. In particular we analyse S * (V ∞ ), that is, S(V ∞ ) modulo finite dimensional subspaces. We show S * (V ∞ ) is not a lattice. (shrink)

ABSTRACT The question of axiomatizability of first-order temporal logics is studied w.r.t. different semantics and several restrictions on the language. The validity problem for logics admitting flexible interpretations of the predicate symbols or allowing at least binary predicate symbols is shown to be ?1 1-complete. In contrast, it is decidable for temporal logics with rigid monadic predicate symbols but without function symbols and identity.

In this paper, John Tillson defends an approach to deciding the aims and content of public schooling from the critique of Public Reason Liberalism. The approach that he defends is an unrestricted pairing of the Epistemic Criterion and of the Momentousness Criterion. On the Epistemic Criterion, public schooling should align students' credence with credibility. On the Momentousness Criterion, public schooling ought to include content that it is costly for children to lack the correct view about, where they are otherwise unlikely (...) to have it. Public Reason Liberals seek to restrict both the Epistemic and Momentousness Criteria to within a range that is acceptable to politically reasonable citizens. In response, Tillson argues, first, that the considerations that encourage Public Reason Liberalism instead motivate unrestricted versions of the Epistemic and Momentousness Criteria; and, second, that Public Reason Liberalism faces a dilemma, that it either entails absurd consequences or must undermine itself in addressing these. (shrink)

Discussions about assisted suicide have hitherto been based on accounts of dignity conceived only as an inherent value or as a status; accounts of dignity in which it appears as a (contingent) attitude, by contrast, have been neglected. Yet there are two good reasons to consider dignity to be an attitude. First, this concept of dignity best allows us to grasp a crucial aspect of everyday language: people often express fears of losing their dignity—and it is not possible to explain (...) this with an account in which dignity is inherent. Second, such a concept allows us to adduce new argumentation where the argument based on status ends. Dignity considered as a status provides grounds to argue for the moral permissibility of assisted suicide, in the sense that in such an account individuals possess the normative power to waive their right to life. But the question then remains of how to decide what counts as a good reason for assisted suicide—and this is where an argument based on dignity as an attitude can provide illumination. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

The implicational fragment of the logic of relevant implication, $R_\to$ is known to be decidable. We show that the implicational fragment of the logic of ticket entailment, $T_\to$ is decidable. Our proof is based on the consecution calculus that we introduced specifically to solve this 50-year old open problem. We reduce the decidability problem of $T_\to$ to the decidability problem of $R_\to$. The decidability of $T_\to$ is equivalent to the decidability of the inhabitation problem of implicational (...) types by combinators over the base $\{\textsf{B},\textsf{B}',\textsf{I},\textsf{W}\}$. (shrink)