Proof-Theoretic Modal PA-Completeness III: The Syntactic Proof

This paper is the final part of the syntactic demonstration of the Arithmetical Completeness of the modal system G; in the preceding parts [9] and [10] the tools for the proof were defined, in particular the notion of syntactic countermodel. Our strategy is: PA-completeness of G as a search for interpretations which force the distance between G and a GL-LIN-theorem to zero. If the GL-LIN-theorem S is not a G-theorem, we construct a formula H expressing the non G-provability of S, so that ⊢_GL-LIN ∼ H and so that a canonical proof T of ∼ H in GL-LIN is a syntactic countermodel for S with respect to G, which has the height θ(T) equal to the distance d(S, G) of S from G. Then we define the interpretation ξ of S which represents the proof-tree T in PA. By induction on θ(T), we prove that ⊢_PA S^ξ and d(S, G) > 0 imply the inconsistency of PA. This revised version was published online in June 2006 with corrections to the Cover Date.     

Proof theory and mathematical meaning of paraconsistent C-systems

A proof-theoretic analysis and new arithmetical semantics are proposed for some paraconsistent C-systems, which are a relevant sub-class of Logics of Formal Inconsistency (LFIs) introduced by W.A. Carnielli et al. (2002, 2005) [8] and [9]. The sequent versions BC, CI, CIL of the systems bC, Ci, Cil presented in Carnielli et al. (2002, 2005) [8] and [9] are introduced and examined. BC, CI, CIL admit the cut-elimination property and, in general, a weakened sub-formula property. Moreover, a formal notion of constructive paraconsistent system is given, and the constructivity of CI is proven. Further possible developments of proof theory and provability logic of CI-based arithmetical systems are sketched, and a possible weakened Hilbert?s program is discussed. As to the semantical aspects, arithmetical semantics interprets C-system formulas into Provability Logic sentences of classical Arithmetic PA (Artemov and Beklemishev (2004) [2], Japaridze and de Jongh (1998) [19], Gentilini (1999) [15], Smorynski (1991) [22]): thus, it links the notion of truth to the notion of provability inside a classical environment. It makes true infinitely many contradictions B∧¬B and falsifies many arbitrarily complex instances of non-contradiction principle ¬(A∧¬A). Moreover, arithmetical models falsify both classical logic LK and intuitionistic logic LJ, so that a kind of metalogical completeness property of LFI-paraconsistent logic w.r.t. arithmetical semantics is proven. As a work in progress, the possibility to interpret CI-based paraconsistent Arithmetic PACI into Provability Logic of classical Arithmetic PA is discussed, showing the role that PACIarithmetical models could have in establishing new meta-mathematical properties, e.g. in breaking classical equivalences between consistency statements and reflection principles.     

Proof-Theoretic Modal PA-Completeness I: A System-Sequent Metric

This paper is the first of a series of three articles that present the syntactic proof of the PA-completeness of the modal system G, by introducing suitable proof-theoretic objects, which also have an independent interest. We start from the syntactic PA-completeness of modal system GL-LIN, previously obtained in [7], [8], and so we assume to be working on modal sequents S which are GL-LIN-theorems. If S is not a G-theorem we define here a notion of syntactic metric d(S, G): we calculate a canonical characteristic fomula H of S (char(S)) so that _G H (S) and _GL-LIN H, and the complexity of H gives the distance d(S, G) of S from G. Then, in order to produce the whole completeness proof as an induction on this d(S, G), we introduce the tree-interpretation of a modal sequent Q into PA, that sends the letters of Q into PA-formulas describing the properties of a GL-LIN-proof P of Q: It is also a d(*, G)-metric linked interpretation, since it will be applied to a proof-tree T of H with H = char(S) and ( H) = d(S, G).     

Cognitive variables related to suicidal contemplation in adolescents with implications for long-range prevention

In a series of studies with college and high school students (Total N=808) consistent and strong relationships were found between suicidal contemplation and the irrational beliefs considered by Rational-Emotive Theory & Therapy (RET) to underlie emotional distress. Suicidal contemplation was measured first by an item from the Beck Depression Inventory and subsequently by the Suicide Probability Scale. Irrational beliefs were measured by the Jones Irrational Beliefs Test and, in the third study, by the new Attitudes & Belief Scale-II as well. Groups formed on the basis of increasing indices of suicidal contemplation were found to be consistently, increasingly more irrational on both measures. Also groups created according to low, medium, and high levels of irrational beliefs (the B in RET) were found to be markedly different on C variables such as anxiety, depression, hopelessness, anger, psychosomoatic symptoms and suicidal contemplation. The findings were interpreted as strongly inferring a causational relationship from attitudes and beliefs to emotional distress and the contemplation of suicide. The implications of the findings for RET theory and for therapeutic and preventive strategies related to emotional distress and suicidal contemplation are clear. Other approaches to the explanation of suicide are cited and reference is made to a previous critical summary of them (Woods & Muller, 1988).Paul J. Woods, Ph.D., Co-Editor of this Journal, is a Fellow of the Institute for Rational-Emotive Therapy in New York City, a Professor of Psychology at Hollins College, and a Licensed Psychologist in independent practice in Roanoke, Virginia.Ellen S. Silverman, R. N., C. & M.A. collaborated in Study III for a Master's thesis at Hollins College. She is currently in a Ph.D. program in psychology at Virginia Polytechnic Institute & State University.Julia M. Gentilini, B. A. collaborated on Study I for an Honors' thesis in psychology at Hollins College.Deborah K. Cunningham, M. A. collaborated on Study II for a Master's thesis at Hollins College. She is currently in a Ph.D. program in psychology at the University of Memphis.Russell M. Grieger, Ph.D., Co-Editor of this Journal, is a Licensed Clinical Psychologist in independent practice in Charlottesville, Virginia, and a Fellow of the Institute for Rational-Emotive Therapy in New York City.     

Syntactical results on the arithmetical completeness of modal logic

In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations of formulas of the form p _i,m _i=0, 1, 2, ... The paper is the preliminary step for a forthcoming global syntactical resolution of the PA-completeness problem for modal logic.     

Proof-Theoretic Modal PA-Completeness II: The Syntactic Countermodel

This paper is the second part of the syntactic demonstration of the Arithmetical Completeness of the modal system G, the first part of which is presented in [9]. Given a sequent S so that ⊢_GL-LIN S, ⊬_G S, and given its characteristic formula H = char(S), which expresses the non G-provability of S, we construct a canonical proof-tree T of ~ H in GL-LIN, the height of which is the distance d(S, G) of S from G. T is the syntactic countermodel of S with respect to Gand is a tool of general interest in Provability Logic, that allows some classification in the set of the arithmetical interpretations. This revised version was published online in June 2006 with corrections to the Cover Date.     

Paraconsistent Informational Logic

We introduce a Paraconsistent Informational Logic that formalizes the idea of conjectures which are acceptable as to the quality and the variety of the information that they convey with respect to a given theory T, even if they are classically inconsistent with T. The work constitutes an extension of a previously developed Informational Logic for classical frameworks, where a new notion of logical entropy measure H on formulas and on proofs plays a central role.