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.     

A Kripke Semantics for the Logic of Gelfand Quantales

Gelfand quantales are complete unital quantales with an involution, *, satisfying the property that for any element a, if a b a for all b, then a a* a = a. A Hilbert-style axiom system is given for a propositional logic, called Gelfand Logic, which is sound and complete with respect to Gelfand quantales. A Kripke semantics is presented for which the soundness and completeness of Gelfand logic is shown. The completeness theorem relies on a Stone style representation theorem for complete lattices. A Rasiowa/Sikorski style semantic tableau system is also presented with the property that if all branches of a tableau are closed, then the formula in question is a theorem of Gelfand Logic. An open branch in a completed tableaux guarantees the existence of an Kripke model in which the formula is not valid; hence it is not a theorem of Gelfand Logic.     

Theory matrices (for modal logics) using alphabetical monotonicity

In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system is only correct if a new condition I call alphabetical monotonicity holds. I sketch how the result can be applied to a wide range of logics such as first order variants of many standard modal logics, including non-serial modal logics.     

Analytic Tableaux for all of <Emphasis Type="Italic">SIXTEEN</Emphasis><Subscript>3</Subscript>

In this paper we give an analytic tableau calculus P L _{1 6} for a functionally complete extension of Shramko and Wansing’s logic. The calculus is based on signed formulas and a single set of tableau rules is involved in axiomatising each of the four entailment relations ? _t , ? _f , ? _i , and ? under consideration—the differences only residing in initial assignments of signs to formulas. Proving that two sets of formulas are in one of the first three entailment relations will in general require developing four tableaux, while proving that they are in the ? relation may require six.     

ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse

Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse (REG ^c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG ^c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG ^c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in REG ^c logics is coNP-complete.     

Cut-free sequent and tableau systems for propositional Diodorean modal logics

We present sound, (weakly) complete and cut-free tableau systems for the propositional normal modal logicsS4.3, S4.3.1 andS4.14. When the modality is given a temporal interpretation, these logics respectively model time as a linear dense sequence of points; as a linear discrete sequence of points; and as a branching tree where each branch is a linear discrete sequence of points.Although cut-free, the last two systems do not possess the subformula property. But for any given finite set of formulaeX the superformulae involved are always bounded by a finite set of formulaeX* _L depending only onX and the logicL. Thus each system gives a nondeterministic decision procedure for the logic in question. The completeness proofs yield deterministic decision procedures for each logic because each proof is constructive.Each tableau system has a cut-free sequent analogue proving that Gentzen's cut-elimination theorem holds for these latter systems. The techniques are due to Hintikka and Rautenberg.Presented byDov M. Gabbay     

Tableaux for Łukasiewicz Infinite-valued Logic

In this work we propose a labelled tableau method for ukasiewicz infinite-valued logic L . The method is based on the Kripke semantics of this logic developed by Urquhart [25] and Scott [24]. On the one hand, our method falls under the general paradigm of labelled deduction [8] and it is rather close to the tableau systems for sub-structural logics proposed in [4]. On the other hand, it provides a CoNP decision procedure for L validity by reducing the check of branch closure to linear programming     

A Sound and Complete Tableau Calculus for Reasoning about only Knowing and Knowing at Most

We define a tableau calculus for the logic of only knowing and knowing at most ON, which is an extension of Levesque's logic of only knowing O. The method is based on the possible-world semantics of the logic ON, and can be considered as an extension of known tableau calculi for modal logic K45. From the technical viewpoint, the main features of such an extension are the explicit representation of "unreachable" worlds in the tableau, and an additional branch closure condition implementing the property that each world must be either reachable or unreachable. The calculus allows for establishing the computational complexity of reasoning about only knowing and knowing at most. Moreover, we prove that the method matches the worst-case complexity lower bound of the satisfiability problem for both ON and O. With respect to [22], in which the tableau calculus was originally presented, in this paper we both provide a formal proof of soundness and completeness of the calculus, and prove the complexity results for the logic ON.     

Relevant analytic tableaux

Tableau formulations are given for the relevance logics E (Entailment), R (Relevant implication) and RM (Mingle). Proofs of equivalence to modus-ponens-based formulations are vialeft-handed Gentzen sequenzen-kalküle. The tableau formulations depend on a detailed analysis of the structure of tableau rules, leading to certain global requirements. Relevance is caught by the requirement that each node must be used; modality is caught by the requirement that only certain rules can cross a barrier. Open problems are discussed.     

Pure Modal Logic of Names and Tableau Systems

By a pure modal logic of names (PMLN) we mean a quantifier-free formulation of such a logic which includes not only traditional categorical, but also modal categorical sentences with modalities de re and which is an extension of Propositional Logic. For categorical sentences we use two interpretations: a “natural” one; and Johnson and Thomason’s interpretation, which is suitable for some reconstructions of Aristotelian modal syllogistic (Johnson in Notre Dame J Form Logic 30(2):271–284, 1989; Thomason in J Philos Logic 22(2):111–128, 1993 and J Philos Logic 26:129–141, 1997. In both cases we use Johnson-like models (1989). We also analyze different kinds of versions of PMLN, for both general and singular names. We present complete tableau systems for the different versions of PMLN. These systems enable us to present some decidability methods. It yields “strong decidability” in the following sense: for every inference starting with a finite set of premises (resp. every syllogism, every formula) we can specify a finite number of steps to check whether it is logically valid. This method gives the upper bound of the cardinality of models needed for the examination of the validity of a given inference (resp. syllogism, formula).     

Two Kinds of Consequential Implication

The first section of the paper establishes the minimal properties of so-called consequential implication and shows that they are satisfied by at least two different operators of decreasing strength (symbolized by \(\rightarrow \) and \(\Rightarrow \)). Only the former has been analyzed in recent literature, so the paper focuses essentially on the latter. Both operators may be axiomatized in systems which are shown to be translatable into standard systems of normal modal logic. The central result of the paper is that the minimal consequential system for \(\Rightarrow \), CI\(\Rightarrow \), is definitionally equivalent to the deontic system KD and is intertranslatable with the minimal consequential system for \(\rightarrow \), CI. The main drawback ot the weaker operator \(\Rightarrow \) is that it lacks unrestricted contraposition, but the final section of the paper argues that \(\Rightarrow \) has some properties which make it a valuable alternative to \(\rightarrow \), turning out especially plausible as a basis for the definition of operators representing synthetic (i.e. context-dependent) conditionals.     

On the limits of statistical learning: Intertrial contextual cueing is confined to temporally close contingencies

Since the seminal study by Chun and Jiang (Cognitive Psychology, 36, 28–71, 1998), a large body of research based on the contextual-cueing paradigm has shown that the cognitive system is capable of extracting statistical contingencies from visual environments. Most of these studies have focused on how individuals learn regularities found within an intratrial temporal window: A context predicts the target position within a given trial. However, Ono, Jiang, and Kawahara (Journal of Experimental Psychology, 31, 703–712, 2005) provided evidence of an intertrial implicit-learning effect when a distractor configuration in preceding trials N ? 1 predicted the target location in trials N. The aim of the present study was to gain further insight into this effect by examining whether it occurs when predictive relationships are impeded by interfering task-relevant noise (Experiments 2 and 3) or by a long delay (Experiments 1, 4, and 5). Our results replicated the intertrial contextual-cueing effect, which occurred in the condition of temporally close contingencies. However, there was no evidence of integration across long-range spatiotemporal contingencies, suggesting a temporal limitation of statistical learning.     

The Church–Fitch knowability paradox in the light of structural proof theory

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$ , by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$ (KP). The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$ (OP). A Gentzen-style reconstruction of the Church–Fitch paradox is presented following a labelled approach to sequent calculi. First, a cut-free system for classical (resp. intuitionistic) bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism.     

Distinct neuronal patterns of positive and negative moral processing in psychopathy

Psychopathy is a disorder characterized by severe and frequent moral violations in multiple domains of life. Numerous studies have shown psychopathy-related limbic brain abnormalities during moral processing; however, these studies only examined negatively valenced moral stimuli. Here, we aimed to replicate prior psychopathy research on negative moral judgments and to extend this work by examining psychopathy-related abnormalities in the processing of controversial moral stimuli and positive moral processing. Incarcerated adult males (N = 245) completed a functional magnetic resonance imaging protocol on a mobile imaging system stationed at the prison. Psychopathy was assessed using the Hare Psychopathy Checklist–Revised (PCL-R). Participants were then shown words describing three types of moral stimuli: wrong (e.g., stealing), not wrong (e.g., charity), and controversial (e.g., euthanasia). Participants rated each stimulus as either wrong or not wrong. PCL-R total scores were correlated with not wrong behavioral responses to wrong moral stimuli, and were inversely related to hemodynamic activity in the anterior cingulate cortex in the contrast of wrong > not wrong. In the controversial > noncontroversial comparison, psychopathy was inversely associated with activity in the temporal parietal junction and dorsolateral prefrontal cortex. These results indicate that psychopathy-related abnormalities are observed during the processing of complex, negative, and positive moral stimuli.     

Dynamics of lying

We propose a dynamic logic of lying, wherein a ‘lie that $\varphi $ ’ (where $\varphi $ is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula $\varphi $ . The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of other agents or the belief consequences of the lies of other agents. We distinguish two speaker perspectives: (Obs) an outside observer who is lying to an agent that is modelled in the system, and (Ag) an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: (Cred) the credulous agent who believes everything that it is told (even at the price of inconsistency), (Skep) the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and (Rev) the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or in the extension of that logic to belief revision.