Mystical religious experiences typically purport to engage with the transcendent and often claim to involve encounters with spiritual entities or a detachment from the material world. Daoism diverges from this paradigm. This paper examines Daoist mystical experiences of bodily transformations and explores their epistemological implications. Specifically, we defend the justificatory power of Daoist somatic experiences against the disanalogy objection. The disanalogy objection posits that mystical experiences, in contrast to sense perceptions, are not socially verifiable and thereby lack prima facie epistemic (...) value. We argue that some Daoist mystical bodily states, being essentially spatiotemporal, are exempt from this challenge. This leads to a broader understanding of mysticism and offers a partial resolution to the disanalogy objection. (shrink)

This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

Abstract In slogan form, the thesis of this paper is that beliefs are self-verifying fictions: We make them up, but in so doing, they come to exist, and so the fiction of belief is in fact true. This picture of belief emerges from a combination of three independently motivated views: (1) a phenomenal intentionalist picture of intentionality, on which phenomenal consciousness is the basis of intentionality; (2) what I will call a “self-ascriptivist” picture of derived representation, on which non-fundamental representational (...) features are a matter of our ascribing contents to ourselves or our mental states or contents; and (3) a representationalist picture of the attitudes, on which the attitude components of mental states (e.g., the “belief” bit of a belief that P) are represented contents. This paper outlines and motivates the view of beliefs as self-verifying fictions, compares the view to alternative views of belief, and contrasts beliefs on the resulting picture to other belief-like mental states. (shrink)

We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive (...) proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the "Tangibility Reflection Principle". We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further. (shrink)

This paper is intended to provide a rather brief, suggestive, though not very precise, analysis of the significance of “contextualism” for “meaning”, and more specifically of the significance of “systematic simplicity” in relation to “meaningful operations” in the language of natural science. The notion of “equivalent theories” is examined in conjunction with the question of simplicity, and finally, these ideas are brought to bear upon “realism” and “semantic realism” in particular. The pragmatic-aesthetic question of the role of simplicity in scientific (...) theories is of some concern to philosophers of science. Henry Margenau has pointed out that, among the metaphysical requirements of scientific theories, the “most embarrassing … is one which is often called the postulate of simplicity….” When a topic is embarrassing, the best way to help remove such embarrassment is to indulge further in frank and open discussion of the topic. This I have tried to do in what follows. (shrink)

Mystical religious experiences typically purport to engage with the transcendent and often claim to involve encounters with spiritual entities or a detachment from the material world. Daoism diverges from this paradigm. This paper examines Daoist mystical experiences of bodily transformations and explores their epistemological implications. Specifically, we defend the justificatory power of Daoist somatic experiences against the disanalogy objection. The disanalogy objection posits that mystical experiences, in contrast to sense perceptions, are not socially verifiable and thereby lack prima facie epistemic (...) value. We argue that some Daoist mystical bodily states, being essentially spatiotemporal, are exempt from this challenge. This leads to a broader understanding of mysticism and offers a partial resolution to the disanalogy objection. (shrink)

How can one verify the accuracy of recorded information (e.g., information found in books, newspapers, and on Web sites)? In this paper, I argue that work in the epistemology of testimony (especially that of philosophers David Hume and Alvin Goldman) can help with this important practical problem in library and information science. This work suggests that there are four important areas to consider when verifying the accuracy of information: (i) authority, (ii) independent corroboration, (iii) plausibility and support, and (iv) presentation. (...) I show how philosophical research in these areas can improve how information professionals go about teaching people how to evaluate information. Finally, I discuss several further techniques that information professionals can and should use to make it easier for people to verify the accuracy of information. (shrink)

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its (...) available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL-CTL , which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatise a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL-CTL in the description language of the Mocha model checker (Alur et al., Proceedings of the tenth international conference on computer-aided verification (CAV) , 1998), and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources. (shrink)

This is a case-study in knowledge representation and dynamic epistemic protocol verification. We analyze the ‘one hundred prisoners and a lightbulb’ puzzle. In this puzzle it is relevant what the agents know, how their knowledge changes due to observations, and how they affect the state of the world by changing facts, i.e., by their actions. These actions depend on the history of previous actions and observations. Part of its interest is that all actions are local, i.e. not publicly observable, and (...) part of the problem is therefore how to disseminate local results to other agents, and make them global. The various solutions to the puzzle are presented as protocols. The paper consists of three parts. First, we present different versions of the puzzle, and their solutions. This includes a probabilistic version, and a version assuming synchronicity. The latter is very informative for the prisoners, and allows different protocols. Then, we model the puzzle in an epistemic logic incorporating dynamic operators for the effects of information changing events. Such events include both informative actions, where agents become more informed about the non-changing state of the world, and factual changes, wherein the world and the facts describing it change themselves as well. Finally, we verify the basic protocol to solve the problem. Novel contributions in this paper are: Firstly, Protocol 2 and Protocol 4. Secondly, the modelling in dynamic epistemic logic in its entirety — we do not know of a case study that combines factual and informational dynamics in a setting of non-public events, or of a similar proposal to handle asynchronous behaviour in a dynamic epistemic logic. Thirdly, our method to verify dynamic epistemic protocols by reasoning over possibly infinite execution sequences of these protocols. A precursor of the present paper, entitled ‘One hundred prisoners and a lightbulb – logic and computation’, was presented at KR 2010, Toronto. The differences with the present contribution are as follows: the former contains a section with computational results, whereas the focus of the present paper is the verification of one of the presented protocols in the former. (shrink)

The effective reasoning capability of an agent can be defined as its capability to infer, within a given space and time bound, facts that are logical consequences of its knowledge base. In this paper we show how to determine the effective reasoning capability of an agent with limited memory by encoding the agent as a transition system and automatically verifying whether a state where the agent believes a certain conclusion is reachable from the start state. We present experimental results using (...) the Model Based Planner (MBP) which illustrates how the length of the deduction varies for different memory sizes. (shrink)

The contentions of this paper are essentially two. One is that truth does not consist of verifiability—and still less of verification—in the sense in which this has been maintained by some pragmatists, operationalists, and positivists. The other is that in a certain other sense of “verifiability”, which will be described, truth is the same thing as verifiability. The paper, it should be understood, attempts only to make clear what is and what is not the relation between truth (...) and verifiability. It does not attempt in addition to carry the analysis of verification itself to the point where it would, by implication, furnish a terminal answer to the question, what is truth. The latter task, because of space limitations, must be reserved for some future occasion. (shrink)

For some time there have been appearing in the philosophical literature hints and suggestions that the so-called “problem of the external world” should be abandoned, not primarily because it is of little pragmatic significance, but rather because there is really no such problem to be solved. The publication of Reichenbach's Experience and Prediction has now stimulated a resurgence of these suggestions. In the course of his discussion of the book in the April Philosophy of Science Professor Ernest Nagel has taken (...) occasion to argue briefly that this problem, which Reichenbach attempts to solve, cannot even be stated unless one assumes its solution. And in a similar vein more recently Dr. William Barrett has also criticized Reichenbach and has then gone on to present certain fundamental logical considerations which, it is alleged, guarantee that the expression “Is there an external world?” cannot designate a legitimate philosophical problem. The situation, as he describes it, is as follows. The sentence “There is an external world” or the equivalent sentence “There is a physical object” can be confirmed in a physicalistic language only if one assumes the existence of certain physical objects. This procedure is of course circular. These sentences cannot therefore be confirmed, and, since the verifiability theory of meaning is accepted, the questions derived by transferring them into the interrogative mood cannot be meaningfully asked. A similar result is asserted to follow if one employs a perception language for science in place of a physicalistic language, since there is a parallelism between these two languages such that for every expression in the one there will be a corresponding expression in the other. (shrink)

The pervasive contrast in modern life between the certainties of science and technology, on the one hand, and the uncertainties of human goals and policies, on the other, is the objective source of a fundamental conflict in theory. It is now widely held that facts are rather definitely verifiable, but that values are unverifiable; though other students assume that values are also verifiable in some significant sense and degree.

A common dictum or assumption in contemporary scientific and philosophical circles is that, if values are at all verifiable in any significant sense, they are less verified and less verifiable than facts. Esthetic and moral values in particular are regarded as less verifiable than scientific facts. It is frequently said that esthetic and moral “facts” and values are essentially and finally a matter of private preference or arbitrary social agreement whereas scientific facts are in the last analysis determined and underwritten (...) by the actual nature of events and relations themselves. Yet in opposition to what may thus appear to be the chief current of contemporary opinion, some thinkers follow mainly in the tradition of Kant, Lotze, and Ritschel. They claim for values, including moral and esthetic values, a unique objectivity and validity. (shrink)

Epistemic protocols are communication protocols aiming at transfer of knowledge in a controlled way. Typically, the preconditions or goals for protocol actions depend on the knowledge of agents, often in nested form. Informal epistemic protocol descriptions for muddy children, coordinated attack, dining cryptographers, Russian cards, secret key exchange are well known. The contribution of this paper is a formal study of a natural requirement on epistemic protocols, that the contents of the protocol can be assumed to be common knowledge. By (...) formalizing this requirement we can prove that there can be no unbiased deterministic protocol for the Russian cards problem. For purposes of our formal analysis we introduce an epistemic protocol language, and we show that its model checking problem is decidable. (shrink)

Shows the failure of an attempt, which appears to have been the last in a series of increasingly complex efforts following Ayer, to define the notion of verifiability in purely deductive terms.