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. (shrink)

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. (shrink)

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). (shrink)

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. (shrink)

A conjectural inference is proposed, aimed at producing conjectural theorems from formal conjectures assumed as axioms, as well as admitting contradictory statements as conjectural theorems. To this end, we employ Paraconsistent Informational Logic, which provides a formal setting where the notion of conjecture formulated by an epistemic agent can be defined. The paraconsistent systems on which conjectural deduction is based are sequent formulations of the C-systems presented in Carnielli-Marcos [CAR 02b]. Thus, conjectural deduction may also be considered to be a (...) tool for investigating the properties of paraconsistency in general. (shrink)

In this paper are studied the properties of the proofs in PRA of provability logic sentences, i.e. of formulas which are Boolean combinations of formulas of the form PIPRA, where h is the Gödel-number of a sentence in PRA. The main result is a Normal Form Theorem on the proof-trees of provability logic sequents, which states that it is possible to split the proof into an arithmetical part, which contains only atomic formulas and has an essentially intuitionistic character, and into (...) a logical part, which is merely instrumental. Moreover, the induction rules which occur in the arithmetical part are implicit. Some applications of the Normal Form Theorem are shown in order to obtain some syntactical results on the PRA-completeness of modal logic. In particular a completeness theorem for Boolean combinations of modalities is given. (shrink)