Logic programming as classical inference

We propose a denotational semantics for logic programming based on a classical notion of logical consequence which is apt to capture the main proposed semantics of logic programs. In other words, we show that any of those semantics can be viewed as a relation of the form $T{\models }^{\star }X$ where T is a theory which naturally represents the logic program under consideration together with a set of formulas playing the role of “hypotheses”, in a way which is dictated by that semantics, ${\models }^{\star }$ is a notion of logical consequence which is classical because negation, disjunction and existential quantification receive their classical meaning, and X represents what can be inferred from the logic program, or an intended interpretation of that logic program (such as an answer-set, its well-founded model, etc.). The logical setting we propose extends the language of classical modal logic as it deals with modal operators indexed by ordinals. We make use of two kinds of basic modal formulas: ${\square }_{\alpha }\phi$ which intuitively means that the logical program can generate φ by stage α of the generation process, and ${◇}_{\alpha }{\square }_{\beta }\phi$ with $\alpha >\beta$, which intuitively means that φ can be used as a hypothesis from stage β of the generation process onwards, possibly expecting to confirm φ by stage α (so expecting ${\square }_{\alpha }\phi$ to be generated). This allows us to capture Rondogiannis and Wadge's version of the well-founded semantics [27] where a member of the well-founded model is a closed atom which receives an ordinal truth value of ${\mathtt{true}}_{\alpha }$ or ${\mathtt{false}}_{\alpha }$ for some ordinal α: in our framework, this corresponds to having $T{\models }^{\star }{\square }_{\alpha }\phi$ or $T{\models }^{\star }{\square }_{\alpha }\neg \phi$, respectively, with T being the natural representation of the logic program under consideration and the right set of “hypotheses” as dictated by the well-founded semantics. The framework we present goes much beyond the proposed traditional semantics for logic programming, as it can for instance let us investigate under which conditions a set of hypotheses can be minimal, with each hypothesis being activated as late as possible and confirmed as soon as possible, setting the theoretical foundation to sophisticated ways of making local use of hypotheses in knowledge-based systems, while still being theoretically grounded in a classical notion of logical consequence.     

Informative Aboutness

Pretheoretically, (B) ‘all believers are immortal’ is about all believers, but (1) B is not about any unbeliever. Similarly, (M) ‘all mortals are unbelievers’ is not about any immortal, but (2) M is about all mortals. But B and M are logically equivalent universal generalizations, so arguably they are about exactly the same objects; by (2), they are about those mortals who are unbelievers, contradicting (1). If one responds by giving up (1), is there still a sense in which B treats unbelievers differently from believers? I argue that there is. B is uninformative about unbelievers but informative about believers, in the following sense: for any object o, the information that B provides only about o—namely, ‘o is a believer only if o is immortal’—is entailed (and thus rendered redundant) by ‘o is an unbeliever’ but not by ‘o is a believer’.     

Bridging Curry and Church's typing style

There are two versions of type assignment in the λ-calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called “domain free”), in which it is not. As an example, in Church-style typing, ${\lambda }_{x:A}.x$ is the identity function on type A, and it has type $A\to A$ but not $B\to B$ for a type B different from A. In Curry-style typing, ${\lambda }_x.x$ is a general identity function with type $C\to C$ for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.     

When ignorance excuses

An ingenious argument – we may call it the Argument from Excuse – purports to show that the Standard View of Ignorance is false and the New View of Ignorance is true. On the former, ignorance is lack of knowledge; on the latter, ignorance is lack of true belief. I defend the Standard View by arguing that the Argument from Excuse is unsound. I also argue that an implication of my case is that Factual Ignorance Thesis (FIT) is false. According to FIT, whenever an agent A acts from factual ignorance, A is morally blameworthy (culpable) for the act only if A is morally blameworthy (culpable) for the ignorance from which A acts.     

Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system $\mathsf{TK}$ for verification of validity in modal logic $\mathsf{K}$. The system $\mathsf{TK}$ is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. $\mathsf{TK}$ is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of $\mathsf{TK}$ and can be used for the global assumptions problem.     

论"观物"与"观无"——儒学与现象学的一种融通

In traditional Chinese expressions, guannian 观念 (ideas) are results of guan 观 (viewing). However, viewing can be understood to have two different levels of meanings: one is “viewing things,” that is, viewing with something to view; another is “viewing nothing,” that is, viewing with nothing to view. What are viewed in “viewing things” are either physical beings—all existing things and phenomena—or the metaphysical being (for example, the “Dao as a thing”). In both cases, something is being viewed. What is viewed in “viewing nothing” is the being itself, or “nothing,” in which there is nothing to view. According to Confucianism, the existence of “nothing” manifests itself as life sentiments, especially the sentiment of love, which is the very root and source of benevolence; moreover “viewing nothing” is, in essence, a perception of life. Life sentiments or the perception of life is “the thing itself ” prior to any being or any thing. Translated by Liu Huawei from Sichuan Daxue Xuebao 四川大学学报 (Journal of Sichuan University), 2006, (4): 67–74     

A family of Gödel hybrid logics

In this paper, we define a family of fuzzy hybrid logics that are based on Gödel logic. It is composed of two infinite-valued versions called ${\mathsf{GH}}_{\infty }$ and ${\mathsf{WGH}}_{\infty }$, and a sequence of finitary valued versions ${({\mathsf{GH}}_n)}_{0<n<\infty }$. We define decision procedures for both ${\mathsf{WGH}}_{\infty }$ and ${({\mathsf{GH}}_n)}_{0<n<\infty }$ that are based on particular sequents and on a set of proof rules dealing with such sequents. As these rules are strongly invertible the procedures naturally allow one to generate countermodels. Therefore we prove the decidability and the finite model property for these logics. Finally, from the decision procedure of ${\mathsf{WGH}}_{\infty }$, we design a sound and complete sequent calculus for this logic.     

Entailment with Near Surety of Scaled Assertions of High Conditional Probability

An assertion of high conditional probability or, more briefly, an HCP assertion is a statement of the type: The conditional probability of B given A is close to one. The goal of this paper is to construct logics of HCP assertions whose conclusions are highly likely to be correct rather than certain to be correct. Such logics would allow useful conclusions to be drawn when the premises are not strong enough to allow conclusions to be reached with certainty. This goal is achieved by taking Adams" (1966) logic, changing its intended application from conditionals to HCP assertions, and then weakening its criterion for entailment. According to the weakened entailment criterion, called the Criterion of Near Surety and which may be loosely interpreted as a Bayesian criterion, a conclusion is entailed if and only if nearly every model of the premises is a model of the conclusion. The resulting logic, called NSL, is nonmonotonic. Entailment in this logic, although not as strict as entailment in Adams" logic, is more strict than entailment in the propositional logic of material conditionals. Next, NSL was modified by requiring that each HCP assertion be scaled; this means that to each HCP assertion was associated a bound on the deviation from 1 of the conditional probability that is the subject of the assertion. Scaling of HCP assertions is useful for breaking entailment deadlocks. For example, it it is known that the conditional probabilities of C given A and of ¬ C given B are both close to one but the bound on the former"s deviation from 1 is much smaller than the latter"s, then it may be concluded that in all likelihood the conditional probability of C given A B is close to one. The resulting logic, called NSL-S, is also nonmonotonic. Despite great differences in their definitions of entailment, entailment in NSL is equivalent to Lehmann and Magidor"s rational closure and, disregarding minor differences concerning which premise sets are considered consistent, entailment in NSL-S is equivalent to entailment in Goldszmidt and Pearl"s System-Z ⁺. Bacchus, Grove, Halpern, and Koller proposed two methods of developing a predicate calculus based on the Criterion of Near Surety. In their random-structures method, which assumed a prior distribution similar to that of NSL, it appears possible to define an entailment relation equivalent to that of NSL. In their random-worlds method, which assumed a prior distribution dramatically different from that of NSL, it is known that the entailment relation is different from that of NSL.     

Moral supervenience

Abstract

It is widely held, even among nonnaturalists, that the moral supervenes on the natural. This is to say that for any two metaphysically possible worlds w and w′, and for any entities x in w and y in w′, any isomorphism between x and y that preserves the natural properties preserves the moral properties. In this paper, I put forward a conceivability argument against moral supervenience, assuming non-naturalism. First, I argue that though utilitarianism may be true, and the trolley driver is permitted to kill the one to save the five, there is a conceivable scenario that is just like our world in all natural respects, yet at which deontology is true, and the trolly driver is not permitted to kill the one to save the five. I then argue that in the special case of morality, it is possible to infer from the conceivability of such a scenario to its possibility. It follows that supervenience is false.