排序方式: 共有39条查询结果,搜索用时 0 毫秒
1.
2.
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. 相似文献
3.
Norihiro Kamide 《Studia Logica》2009,91(2):217-238
New propositional and first-order paraconsistent logics (called L
ω
and FL
ω
, respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding
theorems of L
ω
and FL
ω
into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple
semantics for L
ω
and FL
ω
are proved. The cut-elimination theorems for L
ω
and FL
ω
are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems.
Presented by Yaroslav Shramko and Heinrich Wansing 相似文献
4.
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). 相似文献
5.
Reiner Hähnle 《Studia Logica》1998,61(1):101-121
We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers. 相似文献
6.
7.
We cast aspects of consciousness in axiomatic mathematical terms, using the graphical calculus of general process theories (a.k.a symmetric monoidal categories and Frobenius algebras therein). This calculus exploits the ontological neutrality of process theories. A toy example using the axiomatic calculus is given to show the power of this approach, recovering other aspects of conscious experience, such as external and internal subjective distinction, privacy or unreadability of personal subjective experience, and phenomenal unity, one of the main issues for scientific studies of consciousness. In fact, these features naturally arise from the compositional nature of axiomatic calculus. 相似文献
8.
We discuss recent work generalising the basic hybrid logic with the difference modality to any reasonable notion of transition. This applies equally to both subrelational transitions such as monotone neighbourhood frames or selection function models as well as those with more structure such as Markov chains and alternating temporal frames. We provide a generic canonical cut-free sequent system and a terminating proof-search strategy for the fragment without the difference modality but including the global modality. 相似文献
9.
In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is
described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent
its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics.
We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then
we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions
of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations
in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness”
operator. 相似文献
10.
We introduce various sequent systems for propositional logicshaving strict implication, and prove the completeness theoremsand the finite model properties of these systems.The cut-eliminationtheorems or the (modified) subformula properties are provedsemantically. 相似文献