Universal Completeness

We prove that Substitutivity is sound with respect to all models. Let M be a Σ-model such that M|= (∀χ)ρ. Assume a substitutionθ:χ→ϕsuch that(∀ϕ)ρ∈Sen(Σ), and let M2be any ϕ-expansion of M. Because M_2θis aχ-expansion of M (since(M_2θ)χ=M₂ϕ) which by hypothesis satisfies(∀χ)ρ, we have that M₂θ|=ρ. By the satisfaction condition, we obtain that M2|=θ(ρ). Since M2 was an arbitrary expansion of M, we have thus proved M|= (∀ϕ)θ(ρ). (Q.E.D.)

Theorem 8.3.2 (Reachable universal completeness). The RUWES of

I

is complete with respect to all(

D

^c,

D

^l)-reachable models if

1. the WES of

I

2is complete with respect to all(

D

^c,

D

^l)-reachable models (and compact), and

2. for each set of sentences E ⊆ Sen2(Σ) and each sentence e∈Sen2(Σ), we have E |= e iff M|= (E⇒e)for all(

D

^c,

D

^l)-reachable models M.

Proof. Assume that for all(

D

^c,

D

^l)-reachable models M we have M|= (Γ⇒(∀χ)e), where Σ→^χ Σ∈

D

^{c. We want}Γ(∀χ)e. Suppose towards a contradiction thatΓ(∀χ)e. Then there exists a signature morphismΣ→^ϕ Σin

D

^l and a substitutionθ:χ→ϕsuch thatΓ(∀ϕ)θ(e).

We define the set ofΣ-sentencesΓ2={ρ∈Sen₂(Σ)|Γρ}.

We show that Γ2 ²(∀ϕ)θ(e). Assume that Γ2²(∀ϕ)θ(e). For the infinitary case take Γ=Γ2. For the finitary case, since the WES of

I

2is compact, there exists a finiteΓ⊆Γ2such thatΓ²(∀ϕ)θ(e)which impliesΓ(∀ϕ)θ(e). SinceΓρfor allρ∈Γ we haveΓΓ. Hence,Γ(∀ϕ)θ(e)which is a contradiction with our assumption.

We haveΓ2²(∀ϕ)θ(e), and by completeness of

I

2we obtainΓ2|= (∀ϕ)θ(e). There exists a(

D

^c,

D

^l)-reachable model such that M |=Γ2 and M|= (∀ϕ)θ(e). Note that M|= (∀ϕ)θ(e) implies M |= (∀χ)e. If we have proved that M |=Γ we have reached a contradiction with A|= (Γ⇒(∀χ)e)for all(

D

^c,

D

^l)-reachable models A.

Let (∀χ1)e₁ ∈Γ, where Σ→^χ1 Σ1∈

D

^c, and let N be anyχ1-expansion of M. Since M is (

D

^c,

D

^l)-reachable there exists a signature morphismΣ→^ϕ1 Σ₁in

D

^l, a substitutionψ:χ1→ϕ1, and aϕ1-expansion Nof M such that Nθ=N. By Substitutivity(∀ϕ1)ψ(e₁)∈Γ2which im-plies M|= (∀ϕ1)ψ(e1). Since Nisϕ1-expansion of M we have N|=ψ(e1)and by satisfaction

condition Nψ=N|=e₁. (Q.E.D.)

Generic universal weak entailment systems (GUWES). Let us assume a

D

^l-universal

institution I= (Sig,Sen,Mod,|=)over

I

1withSen₁the sub-functor ofSen.

Given a compact WES

E

1= (Sig,Sen1,¹) for

I

1, the GUWES of

I

consists of the least WES with universal quantifications over

E

1, closed under Substitutivity. This is the finitary version of the GUWES, and is applicable to the restriction of GHCL to the sentences quantified over finite sets of variables of loose sorts. Its infinitary variant is obtained by dropping the compactness condition, and by considering the infinitary WES of

I

; it is applicable to the restriction of GHCL_∞ to the sentences quantified over sets (possible infinite) of variables of loose sorts.

Proposition 8.3.3. The GUWES of

I

is sound (and compact) whenever the WES of

I

1is sound (and compact).

Proof. By Proposition 8.2.3and Corollary3.3.11it is suffices to prove the soundness of Sub-stitutivity which may be found in the proof of Proposition8.3.1.

For the compactness of the GUWES of

I

consider the compact sub-WES

E

^c= (Sig,Sen, ^c)of

E

= (Sig,Sen,). It contains

E

1 because

E

1 is compact. Note that

E

^c satisfies Substi-tutivity because the rules of SubstiSubsti-tutivity are finitely generated. If we prove that

E

^{c satisfies}

Generalization then because

E

is the least WES over

E

1 satisfying the rules of Substitutivity and Generalization we obtain

E

^c=

E

^.

If Γ ^c (∀ϕ)e then there exists Γ ⊆Γ finite such that Γ (∀ϕ)e. By Generalization ϕ(Γ)e which means ϕ(Γ)^c e. Now if ϕ(Γ)^c e then there is Γ⊆Γ finite such that ϕ(Γ)e. Using the Generalization again we get Γ (∀ϕ)e which means Γ^c (∀ϕ)e. (Q.E.D.)

Theorem 8.3.4 (Generic universal completeness). Let

D

be a broad subcategory of signature morphisms such that

D

^l⊆

D

. Assume that

1. the WES of

I

1is complete, and

2. for each set of sentences E ⊆Sen1(Σ)and each sentence e ∈Sen1(Σ), we have E |=Σ

e iff M|=Σ(E⇒e)for all

D

-reachable models M.

Then we have

1. the GUWES of

I

is complete (and compact), and

2. Γ|=Σ(∀ϕ)e, where Σ→^ϕ Σ∈

D

^{l, iff M}|=_Σ (ϕ(Γ)⇒e)for all

D

-reachable models M.

Proof. 1. Assume thatΓ|=Σ(∀ϕ)e where Σ→^ϕ Σ∈

D

^{. We want} ΓΣ (∀ϕ)e. Suppose towards a contradiction thatΓΣ(∀ϕ)e.

We define the set ofΣ-sentencesΓ^ϕ₁ ={ρ∈Sen₁(Σ)|ΓΣ(∀ϕ)ρ}.

SupposeΓ^ϕ₁¹_Σe. For the infinitary case we takeΓ=Γ^ϕ₁. For the finitary case, since the WES of

I

1is compact, there exists a finiteΓ⊆Γ^ϕ₁ such thatΓ¹e. By Generalization ϕ(Γ)_Σρ for allρ∈Γ, which impliesϕ(Γ)_ΣΓ. SinceΓ^ϕ₁ ¹_Σ eimpliesΓ^ϕ_{1 Σ}e, we obtain ϕ(Γ)_Σ e and again by Generalization ΓΣ (∀ϕ)e, which contradicts our assumption. Hence,Γ^ϕ₁ ¹_Σe.

By completeness of

I

1 Γ^ϕ₁ |=e. There exists a

D

-reachable model M such that M|=Γ^ϕ₁ but M |= e. This implies M ϕ|= (∀ϕ)e. If we proved that M ϕ|= Γ we reached a contradiction withΓ|= (∀ϕ)e. We will therefore focus on proving that Mϕ|=Γ.

Let(∀ϕ1)e₁∈Γ, whereΣ→^ϕ1 Σ1∈

D

, and let N be anyϕ1-expansion of Mϕ. We show that N |=e₁. Since M is

D

-reachable there exists a substitution θ :ϕ1 →ϕ such that Mθ=N. By Substitutivity we obtain Γ(∀ϕ)θ(e₁) which impliesθ(e₁)∈Γ^ϕ₁. Since M|=Γ^ϕ₁ we have M|=θ(ρ)and by the satisfaction condition Mθ=N|=e₁.

2. The non-trivial implication is from right to left. Assume thatΓ|=Σ(∀ϕ)e, where Σ→^ϕ Σ∈

D

^l, then by soundness of the WES of

I

^{we have} Γ(∀ϕ)e. Using the first part of the proof we get a

D

^-reachableΣ-model M such that M|=ϕ(Γ)and M|=e. Therefore there exists a

D

-reachable model M such that M|= (ϕ(Γ)⇒e).

(Q.E.D.) The following remark addresses the second condition of Theorem 8.3.2.

Remark 8.3.5. Under the assumption of Theorem 8.3.4, for any subcategory

D

^c⊆

D

^of

sig-nature morphisms, we haveΓ|=Σ (∀ϕ)e iff M|=Σ(Γ⇒(∀ϕ)e) for all(

D

^c,

D

^l)-reachable models M.

Weak entailment systems with implications (IWES). Assume an institution

I

= (Sig, Sen,Mod,|=), a sub-functorSen₀:Sig→Set ofSen such that

• (H ⇒C)∈Sen(Σ), for all (finite) sets of sentences H ⊆Sen₀(Σ) and any sentence C∈Sen0(Σ), and

• any sentence in

I

is of the form(H⇒C)as above.

We denote the institution(Sig,Sen0,Mod,|=)by

I

0.

Given a compact WES

E

0= (Sig,Sen₀,⁰)for

I

0, the IWES of

I

consists of the least WES over

E

0, closed under the rules of Implications. This is the finitary version of the IWES for

I

, and is applicable to the restriction of GHCL to the quantifier-free sentences. Its infinitary variant is obtained by dropping the compactness condition and by considering the infinitary WES for

I

; it is applicable to the restriction of GHCL_∞to the quantifier-free sentences.

Proposition 8.3.6. The WES of

I

is sound (and compact) whenever the WES of

I

0is sound (and compact).

Proof. The soundness of the WES of

I

0is lifted to the soundness of

I

using Corollary 3.3.9.

In the finitary case the WES of

I

0 is compact. By Proposition 3.3.8 the IWES of

I

^is

compact. (Q.E.D.)

Theorem 8.3.7. Let us assume that 1. the WES of

I

0is complete,

2. every set of sentences in

I

0is basic, and

3. there exits a broad subcategory

D

⊆Sig such that for each set B⊆Sen₀(Σ)there is a

D

-reachable model MBdefining B as basic set of sentences.

Then we have

1. the IWES of

I

is sound, complete (and compact), and 2. Γ|=ρiff M|= (Γ⇒ρ)for all

D

-reachable models M.

Proof. 1. Because the entailment system of I has Implications it is enough to prove that Γ|=ρimpliesΓρ

for eachΓ⊆Sen₁(Σ) and eachρ∈Sen₀(Σ). Let M_Γ0 be the model defining the set of sentencesΓ0={e∈Sen₀(Γ)|Γe}as basic. We use the following couple of lemmas.

Lemma 8.3.8. M_Γ0 |=e iffΓe for all sentences e∈Sen₀(Σ). Lemma 8.3.9. M_Γ0 |=Γ.

IfΓ|=ρthen by Lemma8.3.9we have that M_Γ0 |=ρ. Now by Lemma8.3.8we obtain Γρ. By Proposition3.3.8the WES of

I

is compact.

Lemma8.3.8. The implication from right to left holds by the definition of Γ0. For the other implication let us consider a sentence e such that M_Γ0 |=e. For any model M such that M|=Γ0, because Γ0is basic there exists a model homomorphism M_Γ0 →M. Since M_Γ0 |=e and e is basic, there exists another model homomorphism M_e→M_Γ0. These give a model homomorphism Me →M which means M |=e. We have thus shown that Γ0|=e.

By the completeness of I₀we obtain thatΓ0e. For the infinitary case let us takeΓ₀=Γ0. For the finitary case, since the WES of I₀is compact, there existsΓ₀⊆Γ0finite such that Γ₀e. By the definition ofΓ0we obtain thatΓΓ₀henceΓe. (Q.E.D.) Lemma8.3.9. Let us consider that we have a

I

^-sentenceH⇒C∈Γand let us assume that M_Γ0 |=H. By Lemma 8.3.8 we have that Γ|=H and because H ⇒C∈Γ and the WES of

I

has Implications we obtain thatΓC. By Lemma8.3.8again we deduce

M_Γ0 |=C. (Q.E.D.)

2. Letρ= (H ⇒C) with H ⊆Sen₀(Σ) and C∈Sen₀(Σ). Consider the model M_(Γ∪H)0 defining(Γ∪H)0={e∈Sen₀(Σ)|Γ∪H|=e}as basic set of sentences. By Lemma8.3.9 we have that M_(Γ∪H)0 |=Γ∪H. By the hypothesis this implies M_(Γ∪H)0 |=H ⇒C.

Because M_(Γ∪H)0 |=H too, it follows that M_(Γ∪H)0 |=C. Since C is basic there exists a homomorphism M_C→M_(E∪H)0.

Now let M be any model such that M|=Γ∪H. By Lemma 8.3.8 we obtain that M|= (Γ∪H)0. Because (Γ∪H)0 is basic, there exists a homomorphism M_(Γ∪H)0 →M. We obtain thus a homomorphism M_C→M, which means M|=C.

(Q.E.D.) The following is a consequence of Theorems8.3.2,8.3.4and8.3.7.

Theorem 8.3.10. Consider an institution

I

= (Sig,Sen,Mod,|=) with three broad subcate-gories

D

^,

D

^{c and}

D

^lof signatures morphisms, where

D

^c⊆

D

^and

D

^l⊆

D

, and a sub-functor Sen₀ofSen (

I

0= (Sig,Sen₀,Mod,|=)) such that

• (∀χ)(∀ϕ)(H⇒C)∈Sen(Σ)for all signature morphismsΣ→^χ Σ∈

D

^c,Σ→^ϕ Σ∈

D

^l,

all (finite) sets H⊆Sen₀(Σ)and any sentence C∈Sen₀(Σ), and

• all sentences are of the form(∀χ)(∀ϕ)H⇒C as in the item above.

If

E

0= (Sig,Sen0,⁰)is a WES for

I

0 then the free WES of

I

^over

E

0 with Implications and universal quantifications, and satisfying Case splitting and Substitutivity is sound and complete with respect to all(

D

^c,

D

^l)-reachable models whenever

1. the WES of

I

0is sound, complete (and compact), 2. every set of sentences in

I

0is basic, and

3. for each set B⊆Sen₀(Σ) there is a

D

-reachable model M_B defining B as basic set of sentences.

Atomic weak entailment systems (AWES). In order to develop concrete sound and com-plete universal WES we need to define sound and comcom-plete WES for the “atomic” layer of the institutions.

GFOL :

Proposition 8.3.11. Let GHCL₀ be the restriction of GHCL to the atomic sentences.

The WES of GHCL₀generated by the rules bellow is sound, complete and compact.

(Re f lexivity) /0t=t, where t is a term.

(Symmetry)t=tt=t , where t,tare terms.

(Transitivity){t=t,t=t} t=t, where t,t,tare terms.

(Congruence){ti=t_i|1≤i≤n} σ(t1,...,tn) =σ(t₁,...,t_n), where ti,t_i∈TF are terms andσis an operation symbol.

(PCongruence){t_i=t_i|1≤i≤n}∪{π(t₁,...,t_n)} π(t₁,...,t_n), where t_i,t_iare terms and πis a predicate symbol.

Proof. Soundness follows by simple routine check and compactness by applying Propo-sition3.2.6after noting that all the rules are finitely generated. For proving the complete-ness, for any set E of atoms for a signature(S,F,P)we define

≡E={(t,t)|Et=t}

By Reflexivity, Symmetry, Transitivity and Congruence this is a congruence on TF. Then we define a model M_E as follows:

– the(S,F)-algebra part of M_E is defined as the quotient of the initial algebra (term algebra) TF by≡E, and

– for each relation symbolπ∈P, we define(M_E)π={x/≡E|Eπ(x)}

The definition of (M_E)π is correct because of the rule PCongruence. Now we note that for each(S,F,P)-atomρwe have E ρiff ME |=ρ. Now if E |=ρthen ME |=ρwhich

means Eρ. (Q.E.D.)

GOSA:

Definition 8.3.12. A congruence relation≡on a(S,≤,F)-model M is a(S,F)-congruence relation≡= (≡s)s∈Ssuch that if s≤sin(S,≤)and a,a∈Msthen a≡saiff a≡s a. Proposition 8.3.13. Let GOSA₀be the restriction of GOSA to the atomic sentences. The WES of GOSA0 generated by the rules bellow is sound, complete and compact.

(Re f lexivity) /0t=t, where t is a term.

(Symmetry)t=tt=t , where t,tare terms.

(Transitivity){t=t,t=t} t=t, where t,t,tare terms.

(Congruence){t_i=t_i|1≤i≤n} σ(t₁,...,t_n) =σ(t₁,...,t_n), where t_i,t_i∈T_F are terms andσis an operation symbol.

Proof. Soundness follows by simple routine check and compactness by applying Propo-sition3.2.6after noting that all the rules are finitely generated. For proving the complete-ness, for any set E of equations for a signature(S,≤,F)we define

≡E={(t,t)|Et=t}

Since the signature(S,≤,F)is regular the term algebra T_F is the initial(S,≤,F)-algebra inMod(S,≤,F). By (Reflexivity), (Symmetry), (Transitivity) and (Congruence) this is an F-congruence on T_F. ≡E is also an order-sorted congruence on T_F, because the definition of≡E does not depend upon a sort. Since the signature(S,≤,F)is locally filtered we may define a model ME as the quotient of the initial algebra (term algebra) TF by order-sorted congruence≡E.

Notice that for each(S,≤,F)-equation t=t, Et=tiff M_E |=t=t. Now if E|=t=t

then M_E |=t=twhich means E t=t. (Q.E.D.)

GPOA:

Definition 8.3.14. A (preorder) congruence relation on a(S,F)-preorder algebra M is a pair(≡,)where≡is a(S,F)-congruence relation andis a preorder on M which

– preserve the preorder structure of M, i.e. m≤m implies mm for all elements m,m∈M,

– is compatible with operations in F, i.e. m≤m implies M_σ(m)≤M_σ(m) for all operationsσ∈F_w,s and all elements m,m∈M_w, and

– is compatible with the congruence≡, i.e. m₁≡m₂, m₂m₃and m₃≡m₄ implies m₁m₄for all elements m₁,m₂,m₃,m₄∈M.

Proposition 8.3.15. Let GPOA₀be the restriction of GPOA to the atomic sentences. The WES of GPOA₀generated by the rules bellow is sound, complete and compact.

(Re f lexivity) /0t=t for each term t (Symmetry)t=tt=t for any terms t,t

(Transitivity){t=t,t=t} t=t for any terms t,t,t

(Congruence){t_i=t_i|1≤i≤n} σ(t₁,...,t_n) =σ(t₁,...,t_n)for anyσ∈F (Re f lexivity)/0t≤t for each term t

(Transitivity){t≤t,t≤t} t≤t for any terms t,t,t

(Congruence){t_i≤t_i|1≤i≤n} σ(t₁,...,t_n)≤σ(t₁,...,t_n)for anyσ∈F (ET){t₁=t₂, t₂≤t₃, t₃=t₄} t₁≤t₄for any terms t₁,t₂,t₃,t₄

Proof. Soundness follows by simple routine check and compactness by applying Propo-sition3.2.6after noting that all the rules are finitely generated. For proving the complete-ness, for any set E of atoms for a signature(S,P)we define the congruence(≡E,E)

– ≡E={(t,t)|Et=t} – E={(t,t)|Et≤t}

By the above rules of GPOA0 the pair(≡E,E) is a preorder congruence on the term algebra T_F. Then we define the preorder algebra M_E as the quotient of the term algebra by(≡E,E). We note that for each equational or transitional(S,F)-atomρ

E ρif and only if ME |=ρ

Now if E|=ρthen M_E |=ρwhich means E ρ. (Q.E.D.) GPA:

Definition 8.3.16. A congruence relation≡ on a (S,F)-model M is a S-sorted equiva-lence relation≡= (≡s)s∈S such that for every operation symbolσ∈F and elements m, m∈M with m≡mif both M_σ(m)and M_σ(m)are defined then M_σ(m)≡M_σ(m). Proposition 8.3.17. Let GPA0 be the restriction of GPA to the atomic sentences. The WES of GPA₀generated by the rules bellow is sound, complete and compact.

(Symmetry)t=^e tt=^e t for any terms t,t

(Transitivity){t =^e t, t=^e t} t=^e tfor any terms t,t,t (Congruence){t_i=^e t_i, de f(σ(t₁,...,t_n)), de f(σ(t₁,...,t_n))}

σ(t₁,...,t_n)=^e σ(t₁,...,t_n)for anyσ∈F

(Subterm)de f(σ(t1,...,tn)) {de f(ti)|i∈1,n}for anyσ∈F

Proof. Soundness follows by simple routine check and compactness by applying Propo-sition3.2.6after noting that all the rules are finitely generated. For proving the complete-ness, for any set E of atoms for a signature(S,T F,PF)we define

≡E={(t,t)|Et=^e t}

Note that For every set of existence equations E ⊆Sen(S,F)we have that E de f(t)if and only if t∈TE, where TE is the partial algebra having the carrier the set of all sub-terms appearing in E.

Firstly we prove that≡E is a congruence relation on T_E. The reflexivity of ≡E is given by the above remark. The first two rules ensure the symmetry and the transitivity of≡E. By the rule(C)we have that≡E is a congruence relation on TE.

For each existence equation t=^e twe have Et=^e t ⇐⇒ t≡E t ⇐⇒ T_E/≡E |=t=^e t. If E |=t=^e tthen T_E/≡E |=t =^e twhich implies E t =^e t. (Q.E.D.) The following is a corollary of Theorem8.3.10.

Corollary 8.3.18. [Completeness of the GHCL] The RUWES of GHCL generated by the rules of Case splitting, Substitutivity, Generalization, Implications, Reflexivity, Symmetry, Tran-sitivity, Congruence and PCongruence is sound and complete with respect to all reachable models.

Similar completeness results hold for GHOSA, GHPOA, GHPA and also their infinitary variants GHCL_∞, GHOSA_∞, GHPOA_∞, GHPA_∞.

ドキュメント内 JAIST Repository: Theorem Proving and Institutions (ページ 69-76)