WWW.ABSTRACT.XLIBX.INFO FREE ELECTRONIC LIBRARY - Abstract, dissertation, book

<< HOME
CONTACTS

Pages:     | 1 |   ...   | 2 | 3 || 5 |

# «COMPACTNESS AND ¨ LOWENHEIM–SKOLEM PROPERTIES IN CATEGORIES OF PRE-INSTITUTIONS ANTONINO SALIBRA University of Pisa, Dip. Informatica Corso Italia ...»

-- [ Page 4 ] --

Full adequacy of R follows from Proposition 3.7 and Lemma 6.6.5.

Expansion-adequacy of R is shown as follows: ∀τ : Σ1 → Σ2 ∈ SigL, ∀M2 ∈

ModI (Σ2R ), ∀M1 ∈ ModL (Σ1 ):

ˆ M2 τR ∈ M1R ⇒ M1 ∈ (M2 τR )T (by Deﬁnition 6.6.2(i)) ⇒ M1 ∈ M2T τ (naturality of model transformation in T and Deﬁnition 6.6.1) ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2T ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2R (by Deﬁnition 6.6.2(i)).

Finitarity of R is an immediate consequence of Lemma 6.6.15 and of the construction of the mapping of presentations as in Lemma 6.6.7.

As we mentioned above, Theorem 6.6 does not generalize the recalled lemma from [6] because it only applies to abstract pre-institutions. A proper generalization of the recalled lemma does exist, however, and is as follows.

In the ﬁrst place, the hypothesis that L is abstract plays no rˆle in the proof o of Theorem 6.6, thus it can be removed.

ˆ In the second place, we note that the only place where the abstractness of I is made use of in the proof of Theorem 6.6 is Lemma 6.6.18, which shows the naturality of presentation transformation by R.

ˆ Now, consider the variant of Theorem 6.6 that is obtained by replacing I with ILI, the ﬁrst-order pre-institution with only renamings as signature morphisms— according to Example 2.9, and by relaxing ﬁnitarity of R to quasi-ﬁnitarity. This variant of Theorem 6.6 holds as well, as we are going to argue by a simple proof adaptation, and it is easy to see that it properly generalizes the recalled lemma from [6].

The required proof adaptation is as follows.

Starting from Lemma 6.6.15, the abstract ﬁrst-order sentence ψR is now to be seen as a ﬁrst-order presentation. Then the deﬁnition of ER in Lemma 6.6.17 becomes ER = ψ∈E ψR, which clearly makes R meet quasi-ﬁnitarity. Finally, consider Lemma 6.6.18. ψR is now a ﬁrst-order presentation; more precisely, it is the elementary equivalence class of a ﬁrst-order sentence. So is τR ψR, since τR is a ﬁrst-order signature isomorphism. And obviously, so is (τ ψ)R as well. Since the presentations τR ψR and (τ ψ)R have exactly the same models, by a proof analogous to that of Lemma 6.6.18, and since both presentations are elementary equivalence classes of a ﬁrst-order sentence, they must consist of the same sentences, i.e. they coincide. The identity τR ER = (τ E )R then follows from the elementwise construction of ER.

## PRE-INSTITUTIONS

7. Cardinal pre-institutions and L¨wenheim–Skolem properties. To o begin with, we note that the properties expressed in the L¨wenheim–Skolem theoo rems (both Downward and Upward, see e.g. [4]) refer to the cardinality of models;

moreover, the cardinality of symbol sets (generalized by signatures, in our context) play a rˆle in generalizations of these theorems, such as the L¨wenheim–Skolem– o o Tarski theorem.

In pre-institutions, models as well as signatures are viewed as “points” in the general case, that is, abstraction is made from any internal structure they may have. The treatment of (general forms of) the L¨wenheim–Skolem properties thus o requires the following concept.

Definition 7.1. A pre-institution with cardinal numbers, K = (I, #), or cardinal pre-institution for short, is a pre-institution I as in Deﬁnition 2.1 together with a function # that assigns a cardinal number #Σ to each signature Σ, as well as a cardinal number #M to each model M, also called the power of Σ or M respectively, and that meets the following conditions, for all signature morphisms

τ : Σ1 → Σ2 and Σ2 -models M :

1. if τ is monic then #Σ1 ≤ #Σ2,

2. if τ is epic then #Σ1 ≥ #Σ2, 3. #M ≥ #M τ.

In abstract model theory, L¨wenheim numbers tell the strength of downward o L¨wenheim–Skolem theorems. The transfer of their deﬁnition to pre-institutions o is straightforward (cf. Def. 6.2.1 in [5]).

Definition 7.2. Let K be a cardinal pre-institution and κ a cardinal. lκ (K) is the least cardinal µ such that every satisﬁable set of sentences of power ≤ κ has a model of power ≤ µ, provided there is such a cardinal; otherwise, lκ (K) = ∞.

def l(K) = l1 (K) is called the L¨wenheim number of K.

o The L¨wenheim number of a cardinal pre-institution is thus the least cardinal o µ such that every satisﬁable sentence has a model of power at most µ, provided such a cardinal exists. Then, not unlike an abstract logic, a cardinal pre-institution K has the L¨wenheim–Skolem property down to λ iﬀ l(K) ≤ λ.

o Hanf numbers are the upward counterpart of L¨wenheim numbers.

o Definition 7.3. Let K be a cardinal pre-institution and κ a cardinal. hκ (K) is the least cardinal µ such that every set of sentences of power ≤ κ has models of arbitrarily large cardinality if it has a model of power ≥ µ, provided there is such a cardinal; otherwise, hκ (K) = ∞.

def h(K) = h1 (K) is called the Hanf number of K.

The Hanf number of a cardinal pre-institution is thus the least cardinal µ such that every sentence satisﬁable by a model of power at least µ has models of arbitrarily larger power, provided such a cardinal exists.

90 A. SALIBRA AND G. SCOLLO A classical result in abstract model theory, viz. the Hanf theorem (1960) (see e.g. Thm. 6.1.4 in [5]), guarantees existence of Hanf numbers for abstract logics under certain “smallness” conditions. The same conditions guarantee existence of L¨wenheim numbers as well, by a similar argument (see e.g. Prop. 2.5.2 in [4]).

o The formulation of analogous conditions for pre-institutions requires the following notion.

Definition 7.4. Let I be a pre-institution as in Deﬁnition 2.1. A renaming in I is an isomorphism : Σ1 Σ2 in Sig. Moreover, we say that any two signatures Σ1, Σ2 ∈ Sig are renaming-equivalent in I, written Σ1 Σ2, iﬀ there exists a Σ2 in Sig. As a matter of notation, if Σ ∈ Sig, [Σ] denotes renaming : Σ1 the renaming-equivalence class that contains Σ.

For cardinal pre-institutions, the following is hardly surprising.

Lemma 7.5.

If : Σ1 Σ2 is a renaming in a cardinal pre-institution K as in Deﬁnition 7.1, then #Σ1 = #Σ2, #M2 = #M2, and #M1 = #M1 −1, for all M1 ∈ Mod(Σ1 ) and M2 ∈ Mod(Σ2 ).

P r o o f. Immediate consequence of Deﬁnitions 7.1 and 7.4.

We are now ready to formulate smallness conditions for pre-institutions, that will permit us to lift the Hanf theorem to our framework.

Definition 7.6 (small pre-institution). A pre-institution I is small iﬀ it meets

the following conditions:

(i) the renaming equivalence of signatures in I has a small set of equivalence classes, (ii) for every signature Σ in I the set of Σ-sentences is small.

Smallness of a cardinal pre-institution K = (I, #) is just smallness of the underlying pre-institution I, thus independent of the size of signatures or of models that is deﬁned by #.

Finally, the following property is a weaker form of the ps property (see Deﬁnition 2.2), since it requires satisfaction invariance only for renamings; this closely reﬂects the renaming property of general logics, in the sense of [5].

Definition 7.7. Let I be a pre-institution as in Deﬁnition 2.1; I has the

renaming property iﬀ it meets the following requirement:

∀ : Σ1 Σ2 ∈ Sig : ∀ϕ ∈ Sen(Σ1 ), ∀M ∈ Mod(Σ2 ) : M ϕ⇔M ϕ.

The lifting of the Hanf theorem to pre-institutions now follows. The set-theoretic axiom of replacement plays a key rˆle, as in the proof of the classical Hanf o theorem.

Proposition 7.8. Let K be a cardinal pre-institution as in Deﬁnition 7.1. If K has the renaming property and is small, then both its L¨wenheim number and o its Hanf number exist.

## PRE-INSTITUTIONS

P r o o f. Let K be a cardinal pre-institution as in the hypothesis. By the axiom

of choice, a small set H of signatures exists such that ∀Σ ∈ Sig: [Σ] ∩ H is a singleton. We note that the renaming property of K has the following consequence:

Σ1, then a renaming : Σ → Σ1 exists, and by Lemma 7.5 and Deﬁniif Σ tion 7.7 a power-preserving bijection between the models of ϕ and those of ϕ exists, for every ϕ ∈ Sen(Σ). Now, for each Σ ∈ H and ϕ ∈ Sen(Σ), let αϕ be ∞ if ϕ has no model, or otherwise the least cardinal µ such that µ = #M for some model M of ϕ. By the axiom of replacement, the set {αϕ | ϕ ∈ Sen(Σ), Σ ∈ H} is small, thus its least upper bound exists, and this is the L¨wenheim number of o K thanks to the aforementioned consequence of the renaming property of K.

The existence of the Hanf number of K has a similar proof.

For the applicability of our form of the “reduction scheme” to L¨wenheim– o Skolem properties along pre-institution transformations, these need the following property. We say that a transformation on cardinal pre-institutions preserves

model power if model power never decreases along the transformation. More precisely:

Definition 7.9. Let T : K → K be a transformation on cardinal pre-institutions K = (I, #), K = (I, # ), with T : I → I as in Deﬁnition 2.3. We say that

T : K → K preserves model power iﬀ ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀M ∈ MT :

#M ≤ # M.

–  –  –

Theorem 7.10.

Let K, K be cardinal pre-institutions as in Deﬁnition 7.9. If there exists an adequate transformation T : K → K that preserves model power

and meets the following condition for cardinals µ, ν: ∀Σ ∈ Sig, ∀E ∈ Pre(Σ):

|E| ≤ µ ⇒ |(ET − TautT (Σ))/≡I | ≤ ν, then lν (K) ≤ lν (K ).

P r o o f. Let Σ ∈ Sig, E ∈ Pre(Σ), with |E| ≤ µ, E satisﬁable. If M E, then MT ET by the satisfaction invariant, and MT is non-empty. Thus ET is satisﬁable, and |(ET − Taut T (Σ))/≡I | ≤ ν by the hypothesis. Now, let E consist of one sentence for each equivalence class in (ET − TautT (Σ))/ ≡I, thus |E | ≤ ν. Clearly, E is satisﬁable iﬀ so is ET −TautT (Σ); moreover, the adequacy of T entails that ET TautT (Σ), by Proposition 3.4. Therefore E is satisﬁable because so is ET ; the fact that |E | ≤ ν further entails that E has a model M with # M ≤ lν (K ). Then, by the construction of E and since ET TautT (Σ), M is a model of ET as well, hence the adequacy of T entails the existence of a model N of E such that M ∈ NT. Since T preserves model power, we infer #N ≤ # M ≤ lν (K ). Thus every satisﬁable E of power at most µ has a model of power at most lν (K ), which is what we had to prove.

92 A. SALIBRA AND G. SCOLLO

8. Related work (9 ). This work shares with [2] the motivation for focussing on the morphisms of institution categories more than on their objects.

Clearly, a reason for this is the interest that institution-independent speciﬁcation [19] and general logics [5, 15] naturally ﬁnd in computer science. It may be source of some surprise, thus, that so far no general agreement has been reached on the most convenient notion of institution morphism. A careful analysis and comparison of several, quite distinct such notions can be found in [2]. To that, we wish to add the following, necessarily quick and preliminary considerations.

In comparison with the notions of institution morphism proposed in [9, 15, 2], our notion is the only one where the three arrows (respectively relating to signatures, sentences, models) are all covariant. Of those three notions, the one which seems closest to ours is that of basic simulation [2], which essentially diﬀers from ours in two respects: 1) it sends sentences to sentences, whereas ours sends presentations to presentations, and 2) model transformation is contravariant, but by a surjective, partial natural transformation. The latter could thus be turned into a covariant, total natural transformation, sending models to sets of models, like in our case. Of course, the model sets ought to be disjoint; this condition, arising from well-deﬁnedness of the model transformation as deﬁned for basic simulations, closely corresponds to the suﬃcient condition for full adequacy given in Lemma 2.6 above—modulo some equivalence of models in the source institution, however.

Although we are more interested in the morphisms than in the objects, the less restrictive deﬁnition of the objects in our framework also contributes to widening the applicability of abstract model-theoretic tools in algebraic speciﬁcation.

Most of the speciﬁcation frameworks studied so far ﬁt the institutions scheme, yet not all of them do. Cases where (at least the eps half of) the satisfaction condition is known to fail include equational type logic with non-standard reduction (as exempliﬁed in Section 5 of [18]) and, most notably, behavioural semantics [3, 16, 17]. These frameworks ﬁt the pre-institutions scheme, as well as the drastically general scheme proposed in [7]—where hardly anything of the abstract model-theoretic approach underlying the theory of institutions can be recognized, however.

9. Future work. We conclude with a list of topics that currently attract our interest, and which seem to deserve further investigation along, and as a test of, the approach presented in this paper.

• Generalization of compactness notions and results to (κ, λ)-compactness [11], which is of interest in the study of inﬁnitary logics.

(9 ) In this paper, we conﬁne ourselves to the comparison proposed in Section 6 of [18].

In future work of ours we intend to oﬀer a more extensive comparison with related work [1], together with an exploration of connections with other topics in the ﬁeld of algebraic logic.

## PRE-INSTITUTIONS

• Investigation of the applicability of the reduction scheme, as generalized here, to other properties such as: Beth deﬁnability, Craig interpolation, Robinson property, Karp property, freeness, initiality, etc.

• Lindstr¨m theorems.

o

• Expressiveness applications.

–  –  –

[1] H. A n d r´ k a, I. N´ m e t i and I. S a i n, Abstract model theoretic approach to algebraic logic, e e manuscript, Mathematical Institute, Budapest, 1984.

Pages:     | 1 |   ...   | 2 | 3 || 5 |

Similar works:

«Fontes Slavia Orthodoxa I Научная серия под редакцией Елены Потехиной и Александра Кравецкого Publikacje Centrum Badań Europy Wschodniej Uniwersytetu Warmińsko-Mazurskiego w Olsztynie Fontes Slavia Orthodoxa I Православие в славянском мире: история, культура, язык Научная редакция Елены Потехиной, Александра Кравецкого Olsztyn 2014 Recenzent:...»

«V. Sumathi et.al / International Journal of Engineering and Technology (IJET) ENERGY EFFICIENT AUTOMATED CAR PARKING SYSTEM V. Sumathi1, N.V. Pradeep Varma1 and M. Sasank1 1 School of Electrical Engineering, VIT University, Vellore, India Abstract— Due to a rapid increase in the number of vehicles, the need for parking spaces is on rise. It is important to park the cars in close proximity to avoid traffic congestion and use a parking area efficiently. Current car parking management systems...»

«Deutscher Bundestag 13/2130 Drucksache 13. Wahlperiode 10. 08. 95 Antwort der Bundesregierung auf die Kleine Anfrage des Abgeordneten Albert Schmidt (Hitzhofen) und der Fraktion BÜNDNIS 90/DIE GRÜNEN — Drucksache 13/1675 — Einsparungsmöglichkeiten durch neuartige Trassierung von Schienenwegen für den Hochgeschwindigkeitsverkehr unter Berücksichtigung der Neigezugtechnik Entscheidendes Kriterium für die Kosten von Neubaustrecken für den Schienenverkehr ist insbesondere im...»

«Finding Jung Frank N Mc Millan Jr A Life In Quest Of The Lion Extremely it will foremost do you to move the conversations constantly. How they lead the CCJs C-store Regional, it are operating also because point whom is to see their approach change about identify you if banking. How it have to do for project for competitive and innovative if March Online Quota, them are this anything which is Finding Jung: Frank N. McMillan Jr., a Life in Quest of the Lion in their phone. Popular Facebook India...»

«IUTAM Symposium on Complexity of Nonlinear Waves 8–12 September, Tallinn, 2014 Book of Abstracts Editors: Andrus Salupere Gérard A. Maugin Ins tute of Cyberne cs at Tallinn University of Technology IUTAM Symposium on Complexity of Nonlinear Waves, 8 – 12 September, Tallinn, Estonia, 2014. Book of Abstracts Editors: Andrus Salupere Gérard A. Maugin Available online at: http://www.ioc.ee/iutam2014/files/BOOK_OF_ABSTRACTS_GA12-08.pdf Organiser of the Symposium: Centre for Nonlinear Studies...»

«WestminsterResearch http://www.wmin.ac.uk/westminsterresearch The transferability of the low-cost model to long-haul airline operations. Graham Francis1 Nigel Dennis2 Stephen Ison3 Ian Humphreys3 Waikato Management School, Waikato University Transport Studies Group, School of Architecture and the Built Environment, University of Westminster Transport Studies Group, Department of Civil and Building Engineering, Loughborough University This is an author-produced electronic version of an article...»

«scudo fiat scudo fiat FIAT Händlersuche Fiat.de Sie suchen einen neuen FIAT Wir helfen bei der Händlersuche! Fiat Scudo Kombi Such Fiat Scudo Kombi. Such Fiat Scudo Kombi. Ergebnisse von 6 Suchmaschinen! Sixt Leasing Angebote Jetzt sparen: Top Konditionen. Jetzt sparen: Top Konditionen. Ihren Neuwagen finden Sie hier! Scudo Fiat NeuGebrauchtwagen im Angebot! NeuGebrauchtwagen im Angebot! Preis vergleichen, Geld sparen. FIAT Scudo Transporter (2007 heute) Fahrberichte FIAT Scudo Transporter...»

«The French Quarter Salon & Day Spa 910 West Jefferson, Effingham IL 217.342.3435 Hair services Hair enhancement Services Women’s haircut from \$20 Deep conditioning masque \$12 Men’s haircut from \$18 Deep fuel treatment \$12 Children’s haircut from \$15 Purifying treatment \$12 Shampoo, Blow-dry & Weak hair strengthener 3/\$25 Style from \$25 Shades color rinse w/ Perm \$20 Long hair from \$30 Price break for cut and style Hair color services Hand & Foot Services Semipermanent shades \$40 Lunchtime...»

«National Animal United Identification States Department of System (NAIS) Agriculture A User Guide And Additional Information Resources Archive Draft Version November 2006 A State Federal Industry Partnership The NAIS is a Voluntary Program The November 2006 User Guide is the most current plan for NAIS and replaces all previously published program documents, including the 2005 Draft Strategic Plan and Draft Program Standards and the 2006 Implementation Strategies. Archive TABLE OF CONTENTS...»

«mons belgien mons belgien Roompot Belgien Sonne, Strand und Natur pur! Sonne, Strand und Natur pur! Zum besten Preis zusammen genießen 10 Hotels in Mons Hotels zum halben Preis. Hotels zum halben Preis. Hotels in Mons reservieren. Mons Belgien Hotel | izito.com Ergebnisse von 6 Suchmaschinen für Mons Belgien Hotel Mons Belgien Mons Hotels: Jetzt richtig sparen! Mons Hotels: Jetzt richtig sparen! 8 Hotels in Mons. 635 Bewertungen Mons Belgien Interrail Eurail Reisen mit [DE] Mons (Belgien)...»

«m or the us [rn Umm h Dr. Israr Jhmad a Markazi Anjuman Khuddam-ul-Quf an Lahore Three-Point Action Agenda for the Muslim Ummah Dr. Israr Ahmad English Translation Dr. Absar Ahmad Lahore Markazi Anjuman Khuddam-ul-Qufan J'jflj~,L~J4.,I Original Title i Urdu n First Printing December 1997 I 1 ol) Second Printing December 2001 2200 Printed at: Shirkat Printing Press, Lahore Published by: Markazi Anjuman Khuddam-ul-Qur'an Lahore 36-K, Model Town Lahore 54700 (Pakistan) Phone: 5869501-03 Fax:...»

«LIMITATION OF THE FINE AGGREGATE ANGULARITY (FAA) TEST TO PREDICT THE BEHAVIOR OF ASPHALT MIXTURES Jose Leomar Fernandes Jr. * Department of Transportation, University of Sao Paulo, Brazil. * Av. Trabalhador Saocarlense, 400, CEP 13566-590, Sao Carlos, Sao Paulo, Brazil, leomar@sc.usp.br Lilian Tais de Gouveia Ph.D. Student, University of Sao Paulo (EESC-USP), liliantg@sc.usp.br ABSTRACT: The performance of dense asphalt mixtures is influenced by the shape, angularity and surface texture of...»

<<  HOME   |    CONTACTS
2016 www.abstract.xlibx.info - Free e-library - Abstract, dissertation, book

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.