共查询到9条相似文献,搜索用时 4 毫秒
1.
2.
The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi. 相似文献
3.
We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb rules are given. 相似文献
4.
In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. 相似文献
5.
6.
Grigori Mints 《Studia Logica》2006,82(1):121-132
S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and
new kinds of reductions 相似文献
7.
Paolo Gentilini 《Studia Logica》1999,63(2):245-268
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. 相似文献
8.
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). 相似文献
9.
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. 相似文献