亚洲免费av电影一区二区三区,日韩爱爱视频,51精品视频一区二区三区,91视频爱爱,日韩欧美在线播放视频,中文字幕少妇AV,亚洲电影中文字幕,久久久久亚洲av成人网址,久久综合视频网站,国产在线不卡免费播放

        ?

        含例鄰域邏輯的薩奎斯特對應理論

        2021-09-29 06:54:30趙之光
        邏輯學研究 2021年3期
        關鍵詞:理論

        趙之光

        1 Introduction

        The notion ofcontingencygoes back to Aristotle,who develops a logic of statements about contingency.([1]) From modal logic point of view,[5] firstly defines the contingent statement aspossibly trueandpossibly false.The contingency logic,in which“contingency”is considered as a modal operator,has been well studied in[3,4],etc.In this paper,we focus oncontingencyin classical propositional logic.Here,a statementφiscontingent,if there is an assignmentvand an assignmentu,s.t.v(φ)tandu(φ)f.In other words,a statement iscontingentif it is neither a tautology nor a contradiction.The logic of truth-functional contingency,is to capture all these contingent statements.

        There are many works on the complementary sentential logics,such as [2,7,9],etc.,all of which introduce different systems to capture non-tautologies in classical propositional logic.The first proper system for truth-functional contingency was introduced in [6].Using this system,in order to obtain a contingent formula,we can translate a formula into its perfect disjunctive normal form by transformation rules,and then remove all redundant variables occurring in it.T.Tiomkin introduced a sound,complete and cut-free calculus for contingent sequent in classical propositional logic.([8]) However,the cut rules and extension rules in [8] mix classical sequents with contingent sequents together.The standard Hilbert style calculus for this logic is still missing.In this paper,we are going to introduce a Hilbert calculus for the logic of truth-functional contingency,where every formula introduced in a deduction is a contingent formula,and it is introduced only if it is a contingent axiom,or it follows by one of the contingent rules of inference from contingent formulas introduced earlier in the deduction.

        The paper is organized as follows.In the next section,we present syntax and semantics of truth-functional contingency.In Section 3,we introduce a Hilbert calculus for the logic of truth-functional contingency.In Section 4,we prove the soundness and completeness of the calculus.Finally,we present some directions for future research.

        2 Preliminaries

        In this section,we present syntax and semantics of truth-functional contingency which will be used in the following sections.

        Fix a denumerable setVof atomic propositions.The language is defined recursively as follows:

        wherep ∈V.In what follows,we will usep,q,r,...(with or without subscripts)to denote any atomic proposition,andφ,ψ,χ,...(with or without subscripts)to denote any formula inF.The outmost parenthesis of formulas will be omitted.

        An assignmentv:V →{t,f}is defined as the same as in classical logic,and it can be uniquely extended to:F →{t,f}.

        Definition 1(Truth-functionally contingent formula) For any formulaφ ∈F,we sayφis atruth-functionally contingent formula,abbreviated as contingent formula,if there is an assignmentvand an assignmentu,s.t.(φ)tand(φ)f.

        In what follows,we use|c φifφis a contingent formula.The logicLCof truth-functional contingency is the set of all contingent formulas.

        3 A Hilbert Calculus for LC

        In this section,we will introduce a sound and complete Hilbert calculus HLC forLC,which is inspired by[2].

        Before giving the calculus,we first introduce some notations which will be used in this section.For any formulaφ,we let Var(φ){p | poccurs inφ}.Let the formula be the form of ΔΔ1or ΔΔ1?(Δ2?...(Δn?1?Δn)...),where Δipior Δi?pi,andpipjforij.

        Definition 2(Hilbert calculus HLC) The Hilbert calculus HLC is defined as follows:

        Adeductionin HLC is a finite sequenceφ1,...,φn,s.t.φi(i ∈{1,...,n})is either an axiom or a formula which is derived by applying rule(s) to its previous formula(s) occuring in the sequence.A formulaφis atheoremin HLC if there is a dedutionφ1,...,φn,s.t.φφn.In what follows,we use?c φto meanφis a theorem in HLC.

        We first show some theorems in HLC,which will be used in the subsequent sections.

        Corollary 1The following formulas are theorems in HLC.For any Δ defined as above:

        (1)?c p ??p;

        (2)?c ?p ?p;

        (3)?cΔ;

        (4)?cΔi ?Δ fori

        (5)?c ?Δn ?Δ;

        (6)?c ?Δ?Δ.

        ProofWe use proof tree to show above formulas are theorems in HLC.(1)can be shown as follows:

        (4)can be shown by the following proof tree:

        (5) can be proven as follows:If Δnpn,then ΔΔ1?(...?(Δi?1?(Δi ?(Δi+1?...?(Δn?1?pn)))...)).

        4 The Soundness and Completeness of HLC

        In this section,we are going to show that HLC is sound and complete,that is,?c φiff|c φfor anyφ ∈F.We call HLC issound,if every axiom in HLC is a contingent formula,and every rule is contingency-preserving,that is,if the premise(s)of a rule is(are) (a) contingent formula(s) then the conclusion of the rule is also a contingent formula.We call HLC iscompleteif every contingent formula is deducible in HLC.

        Lemma 1|cΔ.

        ProofIt suffices to show that there exist assignmentsvandu,s.t.(Δ)tand

        Ifn1,then ΔΔ1por?p.It is obvious that there exist assignmentsvandu,s.t.(Δ)tand(Δ)f.Ifn>1,then ΔΔ1?(...?(Δn?1?Δn)...).For any 1≤i ≤n,there always existvianduis.t.(Δi)tand(Δi)fby the construction of Δ(Definition 2).Since Var(Δi)Var(Δj)whenij,we can defineandas follows:

        Theorem 1(Soundness).HLCis sound.

        ProofThat is to show that every theorem in HLC is a contingent formula.It is clear that the two axioms are contingent formulas,we only need to prove that all rules are contingency-preserving.

        As to (R1a),suppose that|c φ,then there existv′andu′,s.t.(φ)tand(φ)f.It is clear that|c p,that is,there existv′′andu′′s.t.(p)tand(p)f.Sincep/∈Var(φ),we can defineand ˉuas follows:

        As to (R9),it suffices to show that if|c φ ?(ψ ?χ),then there exist assignmentsvandu,s.t.((φ ∧ψ)?χ)tand((φ ∧ψ)?χ)f.Hence|c φ ?(ψ ? χ),then there existands.t.(φ ?(ψ ? χ))tand(φ ?(ψ ?χ))f.We can defineandas follows:

        Lemma 2Let Var(φ)?Var(Δ)and ΔΔ1?(Δ2?...?(Δn?1?Δn)...)withpipjforij,and Δipior Δi?pi.Then,|c φ ?Δ implies?c φ ?Δ.

        ProofBy induction on the complexity of the formulaφ.Ifφpj,there are two subcases.

        Subcase 1:whenj

        Subcase 2:whenjn.If Δnpn,thenpn ?Δ is a tautology,so that Δnmust be?pn,by Corollary 1(1),we have the proof as follows:

        Ifφ?ψ.By subinduction on the complexity ofψ:

        Ifψpj,the proof of it is omitted since it is quite analogous to the proof above.

        Ifψ?χ,i.e.|c ??χ ?Δ,it is clear that|c χ ?Δ,then by induction hypothesis,?c χ ?Δ,then by(R6),we have?c ??χ ?Δ.

        Ifψχ ∧δ,i.e.|c ?(χ ∧δ)?Δ,then by Lemma 1,there existsvsuch that(Δ)t,which makes(?χ ?Δ)(?δ ?Δ)t.And there existsusuch that(?(χ ∧δ)?Δ)f,hence(Δ)f,and(χ)or(δ)is false,which makes(?χ ?Δ)for(?δ ?Δ)f.Now it is clear in this case we have|c ?χ ?Δ or|c ?δ ?Δ.By induction hypothesis,?c ?χ ?Δ or?c ?δ ?Δ.Corollary 1(3) and?c ?χ ?Δ imply that?c ?(χ ∧δ)?Δ by (R5) and (R11a),Corollary 1(3)and?c ?δ ?Δ imply that?c ?(χ ∧δ)?Δ by(R4)and(R11a).

        Theorem 2(Completeness).HLCis complete.

        ProofThat is to show that every contingent formula is a theorem in HLC.The proof strategy is as follows:we first show that|c φ ?Δ and|c ?φ ?Δ′by the assumption|c φ,and then use Lemma 2 to show that?c φ.Since|c φ,there existuandw,such that(φ)tand(φ)f.Assume that Var(φ){p1,...,pn},defineqi:

        Defineri:

        Corollary 2?c φiff?c ?φ.

        ProofFrom left to right direction,assume that?c φ,then by Theorem 1,we have|c φ,which means there existsvsuch that(φ)t,i.e.(?φ)f,and there existsusuch that(φ)f,i.e.(?φ)t,therefore,|c ?φ.By Theorem 2,we have?c ?φ.If?c ?φ,by Theorem 1,we have|c ?φ,which means there existsvsuch that(?φ)t,i.e.(φ)fand there existsusuch that(?φ)f,i.e.(φ)t,therefore|c φ.By Theorem 2,we have?c φ. □

        5 Future work

        In this paper,we introduced a complete and sound Hilbert calculus for the logic of truth-functional contingency,which captures all contingent formulas in classical logic.The quantificational extension of the logicLCwill be our next work.Inspired by[8],to develop a pure sequent calculus for contingent sequent without using classical sequent will be a challenge work in future.Another interesting topic is to study the relation between contingency logic([4]),as we introduced in Section 1,andLCin this paper.

        猜你喜歡
        理論
        堅持理論創(chuàng)新
        當代陜西(2022年5期)2022-04-19 12:10:18
        神秘的混沌理論
        理論創(chuàng)新 引領百年
        相關于撓理論的Baer模
        多項式理論在矩陣求逆中的應用
        基于Popov超穩(wěn)定理論的PMSM轉速辨識
        大電機技術(2017年3期)2017-06-05 09:36:02
        十八大以來黨關于反腐倡廉的理論創(chuàng)新
        “3T”理論與“3S”理論的比較研究
        理論宣講如何答疑解惑
        學習月刊(2015年21期)2015-07-11 01:51:44
        婦女解放——從理論到實踐
        国产精品免费久久久久影院| 亚洲三区二区一区视频| 亚洲αv在线精品糸列| 国产一区二区三区中出| 日韩精品人成在线播放| 77777_亚洲午夜久久多人| 无码精品a∨在线观看| 久久人人做人人妻人人玩精| 一区二区三区国产美女在线播放| 手机av男人天堂免费网址| 成年女人18毛片观看| 久久精品国产91精品亚洲| 日韩欧美人妻一区二区三区| 99热免费观看| 国产在线不卡免费播放| av在线不卡一区二区三区| 精品中文字幕在线不卡| 97人妻精品一区二区三区男同| 国内露脸少妇精品视频| 男女一级毛片免费视频看| 手机在线看片在线日韩av| 亚洲av午夜福利精品一区不卡| 免费亚洲一区二区三区av| 亚洲国色天香卡2卡3卡4| 亚洲a∨天堂男人无码| 99热高清亚洲无码| 中文字幕高清不卡视频二区| 亚洲精品成人片在线观看精品字幕| 色狠狠色狠狠综合一区| 亚洲另类激情综合偷自拍图| 亚洲va精品va国产va| 亚洲国产成人va在线观看天堂| 国产乱对白刺激视频| 精品人妻va出轨中文字幕| 岛国av无码免费无禁网站下载| 午夜日韩视频在线观看| 男女交射视频免费观看网站 | 成人午夜福利视频| 亚洲男同志gay 片可播放| 国产chinese在线视频| 久久深夜中文字幕高清中文|