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)

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)

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)

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 purpose of this paper is to try to set the record a little straighter about the idea of a verifiability criterion.

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)

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)

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.

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)

AI systems, which receive vast amounts of information including privacy information, are emerging. Protecting the privacy of the general public is an important issue for democracies. In this study, “Public space watched by AI- connected cameras” is taken as an example of an AI-system that is expected to be used for public purposes and has a relatively high privacy violation risk. It is defined as a wide public area where every point is monitored by multiple AI-connected street cameras. The following (...) four socially acceptable applications of “Public space watched by AI- connected cameras” are discussed: (1) Human/vehicle tracking, (2) Watching over children, (3) Detection of abnormal situations, (4) Criminal and terrorist behavior pattern analysis. As for privacy protection measures for AI systems, in addition to reliable protection itself, reliable recording and auditing to deter misuse and abuse is considered a prerequisite to ensure that the general public can feel secure. In this paper, the concept of “Verifiable record of AI output”, which is a verifiable and tamper-proof record and disclosure of AI output is proposed. “Verifiable record of AI output” is based on the idea that it may be more realistic to apply a simple exit control only for AI output to confirm rule conformance, rather than anonymizing huge AI inputs such as Big Data or controlling internal AI processes that are black-boxed. A concrete example of implementing “Verifiable record of AI output” in “Public space watched by AI-connected cameras” is proposed. In the “Verifiable record of AI output”, the AI system is enclosed in an outbound firewall, and only AI outputs that are confirmed to be in line with “the purpose of use approved in advance through social discussion” are allowed to be transmitted. The process from application to permission of transmission is anonymized and disclosed in a verifiable and tamper-proof manner. This public record can be verified by the general public or an auditing organization to ensure that any misuse or abuse of the AI system will be exposed. The “Verifiable record of AI output” proposed in this paper is characterized by reliable measurement and recording of AI output, and its disclosure for auditing purposes. The possibility of using this as a template to apply to other AI systems that receive Big Data input, including the privacy of the general public, is considered. (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)

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)

The aim of this paper is to argue for a revised and precisified version of the infamous Verifiability Criterion for the meaningfulness of declarative sentences. The argument is based on independently plausible premises concerning probabilistic confirmation and meaning as context-change potential, it is shown to be logically valid, and its ramifications for potential applications of the criterion are being discussed. Although the paper is not historical but systematic, the criterion thus vindicated will resemble the original one(s) in some important (...) ways. At the same time, it will also be more modest insofar as meaningfulness will turn out to be relativized linguistically and probabilistically, and different choices of the linguistic and probabilistic parameters may lead to different verdicts on meaningfulness. (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.

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)

It is a widely held doctrine at the moment that metaphysical propositions are meaningless, are, in fact, not genuine propositions at all. This doctrine is supported by the contention that only propositions which are verifiable are significant: and it is held that metaphysical propositions do not fulfil this condition, and are consequently pseudo-propositions. Those who hold this view divide propositions into three classes: Tautologies; which are analytic, certain, and are guaranteed by the principle of contradiction. Factually significant propositions; which are (...) synthetic, hypothetical, and are capable of empirical verification. Pseudopropositions, which only appear to be propositions and are, in reality, meaningless nonsense. (shrink)

In the field of logics of formal inconsistency, the notion of “consistency” is frequently too broad to draw decisive conclusions with respect to the validity of many theses involving the consistency connective. In this paper, we consider the matter of the axiom 0—i.e., the schema ◦ ◦ϕ—by considering its interpretation in contexts in which “consistency” is understood as a type of verifiability. This paper suggests that such an interpretation is implicit in two extracanonical LFIs—Sören Halldén’s nonsense-logic C and Graham (...) Priest’s cointuitionistic logic daC—drawing some interesting conclusions concerning the status of 0. Initially, we discuss Halldén’s skepticism of this axiom and provide a plausible counterexample to its validity. We then discuss the interpretation of the operator in Priest’s daC and show the equivalence of 0 to the intuitionistic principle of testability. These observations suggest that it may be fruitful for members of the LFI community to look outside the canon for evidence concerning the adoption of principles like 0. (shrink)

I agree with Dr Eyal that the ‘trust-promotion argument for informed consent’ fails to account for common sense intuitions about informed consent.1 Appealing to ‘social trust, especially trust in caretakers and medical institutions’ cannot, by itself, justify informed consent requirements. And stipulating, in the trust-promoting argument's first clause, that such trust is necessary is an invitation to abuse, in healthcare systems as much as in political systems. Those who are asked to give their informed consent to medical procedures have every (...) reason for healthy scepticism, given the well-documented inadequacies of existing healthcare systems. ‘Trust but verify’—the Russian folk saying that President Ronald Reagan invoked in negotiating with Soviet leaders—has relevance in a great many circumstances, not least for individuals before agreeing to undergo medical procedures or to participate in clinical studies.While it is in no way necessary for these individuals to trust health professionals, much less medical institutions more generally, what is necessary is for the health professionals …. (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)

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)

One of the primary, if not most critical, difficulties in the design and implementation of autonomous systems is the black-boxed nature of the decision-making structures and logical pathways. How human values are embodied and actualised in situ may ultimately prove to be harmful if not outright recalcitrant. For this reason, the values of stakeholders become of particular significance given the risks posed by opaque structures of intelligent agents (IAs). This paper explores how decision matrix algorithms, via the belief-desire-intention model for (...) autonomous vehicles, can be designed to minimize the risks of opaque architectures. Primarily through an explicit orientation towards designing for the values of explainability and verifiability. In doing so, this research adopts the Value Sensitive Design (VSD) approach as a principled framework for the incorporation of such values within design. VSD is recognized as a potential starting point that offers a systematic way for engineering teams to formally incorporate existing technical solutions within ethical design, while simultaneously remaining pliable to emerging issues and needs. It is concluded that the VSD methodology offers at least a strong enough foundation from which designers can begin to anticipate design needs and formulate salient design flows that can be adapted to the changing ethical landscapes required for utilisation in autonomous vehicles. (shrink)