Abstract Context Logic as Modal Logic Completeness and Param(5)

时间：2026-01-18

similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret the

Deﬁnition17(AX-Proof Theory).Given a ML-signatureΣand a set of axioms AX⊆PΣ,the ML-proof theory3generated by AX consists of the following axioms and rules:

P⇒Q P P∈AX P tautology

P[P /p]

:(S1,...,S n)→S

n S P()= (p1,...,,...,p n)

P(p i∨p i)⇔P(p i)∨P(p i)

We sometimes write AX to emphasise the set AX.

There is a well-known general completeness result for ML due to Sahlqvist,which relates the AX-satisfaction relation and the AX-proof theory as long as the axioms have a certain form.We state the result here,since we use it to show completeness for CL.

Deﬁnition18(Very Simple Sahlqvist Formulae).Given ML-signatureΣ=(S,O,ρ),a very simple Sahlqvist antecedent A is a formula given by the grammar:

A::=true S|false

|p S|A∧A| (A1,...,A n)

for p S∈V S and :(S1,...,S n)→S.A very simple Sahlqvist formula is an implication of the form A⇒P+,where P+is a positive formula,in that every propositional letter p S appears under an even number of negations.

Theorem19(Sahlqvist(see[2])).For every axiom set AX con-sisting of very simple Sahlqvist formulae,the ML-proof theory gen-erated by AX is complete with respect to the class of AX-models.

3.1Context Logic as ML

We have shown that a CL-model can be viewed as a ML-model over signatureΣCL(example12),and that the corresponding sat-isfaction relations agree(example15).Now we identify an axiom set AX CL over signatureΣCL,such that the AX CL-models cor-respond exactly to the CL-models and the proof theories coincide. Since the AX CL-axioms are Sahlqvist axioms,the general com-pleteness result for ML(Theorem19)implies completeness for CL. Deﬁnition20(CL-Axioms).Given ML-signatureΣCL,the axiom set AX CL overΣCL consists of the following formulae,where p,q∈V D and k∈V C:

1.I(p)⇒p

2.p⇒I(p)

3.q∧k(p)⇒True(p∧(k q))

4.q∧k(p)⇒(k∧(p q))(true)

5.p∧(k q)⇒True (q∧k(p))

6.k∧(p q)⇒true (q∧k(p))

The axioms in AX CL are very simple Sahlqvist formulae.The ﬁrst two axioms correspond directly to the identity axiom of CL. The other axioms capture the relationship between M ap,M ,and M ,which simply permutes elements(Example12).For example, the third axiom species that,if the given data satisﬁes q and can be split into a context satisfying k and subdata satisfying p,then there exists subdata satisfying p and k q(think of the same subdata).This axiom shifts the emphasis from the given data to the subdata.Theﬁfth axiom is a sort of converse.It states that,if the given data satisﬁes p and k q,then it is possible to enclose it in a context(actually one satisfying k),such that q and k(p) are satisﬁed.The third andﬁfth axiom together describe the exact connection between M ap and M .Similarly,the fourth and sixth axiom describe the exact connection between M ap and M .

3This is called the normal modal proof theory in[2].

We have already illustrated how a CL-model can be interpreted as a ML-model(Example12).This ML-model is indeed a AXΣ

-model.Conversely,every AXΣ

-model gives rise to a CL-model. Lemma21.

1.Every CL-Model M gives rise to an AX CL-model MΣ

. 2.Every AX CL-model M gives rise to a CL-model M AX

. 3.The CL-model M equals the CL-model(MΣ

)AX

4.The AX CL-model M equals the AX CL-model(M AX

)Σ

5.The satisfaction relations agree.

Proof.Part1follows from Example12by observing that the AX-axioms are satisﬁed by MΣ

.The construction of M AX

and the proof of part2is given below.Parts3and4follow from the constructions of the models.Part5is stated in more detail and proved in Example15.For part2,let M be a AX CL-model,with sets M D and M C,and interpretations M ap,M I,M and M . The tuple M AX

=(M D,M C,M ap,M I)is a CL-model.In particular,axioms1and2give the condition that M I is a left unit of M ap.Axioms3to6give the condition(c,d,d )∈M ap⇔(c,d ,d)∈M ⇔(d,d ,c)∈M ,which captures exactly the relationship between connectives ap, , .

Finally,we connect the proof theory of CL and AX CL.

Lemma22.Given arbitrary P1,P2∈P and K1,K2∈K,

P1 CL P2iff AX

|P1|⇒|P2|

K1 CL K2iff AX

|K1|⇒|K2|

Proof.For simplicity of notation we omit the explicit conversion |P|.The proof consists of two parts:

1.the rules of CL are derivable in AX

;

2.the axioms in AX CL are derivable in CL.

For each part we give one case in detail,the other cases follow similarly.For theﬁrst part,we show that the following is derivable

K(P1)⇒P2