FREE ELECTRONIC LIBRARY - Abstract, dissertation, book

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


-- [ 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 Definition 6.6.2(i)) ⇒ M1 ∈ M2T τ (naturality of model transformation in T and Definition 6.6.1) ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2T ⇒ ∃M2 ∈ ModL (Σ2 ) : M1 = M2 τ ∧ M2 ∈ M2R (by Definition 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 first 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 first-order pre-institution with only renamings as signature morphisms— according to Example 2.9, and by relaxing finitarity of R to quasi-finitarity. 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 first-order sentence ψR is now to be seen as a first-order presentation. Then the definition of ER in Lemma 6.6.17 becomes ER = ψ∈E ψR, which clearly makes R meet quasi-finitarity. Finally, consider Lemma 6.6.18. ψR is now a first-order presentation; more precisely, it is the elementary equivalence class of a first-order sentence. So is τR ψR, since τR is a first-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 first-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.


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 Definition 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 definition 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 satisfiable 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 satisfiable 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 λ iff 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 satisfiable 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 Definition 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, iff 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 Definition 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 Definitions 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 iff 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 defined by #.

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

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

renaming property iff 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 Definition 7.1. If K has the renaming property and is small, then both its L¨wenheim number and o its Hanf number exist.


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 Definiif Σ 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 Definition 2.3. We say that

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

#M ≤ # M.

–  –  –

Theorem 7.10.

Let K, K be cardinal pre-institutions as in Definition 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 satisfiable. If M E, then MT ET by the satisfaction invariant, and MT is non-empty. Thus ET is satisfiable, 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 satisfiable iff so is ET −TautT (Σ); moreover, the adequacy of T entails that ET TautT (Σ), by Proposition 3.4. Therefore E is satisfiable 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 satisfiable E of power at most µ has a model of power at most lν (K ), which is what we had to prove.


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 specification [19] and general logics [5, 15] naturally find 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 differs 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-definedness of the model transformation as defined for basic simulations, closely corresponds to the sufficient 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 definition of the objects in our framework also contributes to widening the applicability of abstract model-theoretic tools in algebraic specification.

Most of the specification frameworks studied so far fit 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 exemplified in Section 5 of [18]) and, most notably, behavioural semantics [3, 16, 17]. These frameworks fit 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 infinitary logics.

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

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


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

• Lindstr¨m theorems.


• 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.