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



Pages:   || 2 | 3 | 4 | 5 |

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

-- [ Page 1 ] --

ALGEBRAIC METHODS IN LOGIC AND IN COMPUTER SCIENCE

BANACH CENTER PUBLICATIONS, VOLUME 28

INSTITUTE OF MATHEMATICS

POLISH ACADEMY OF SCIENCES

WARSZAWA 1993

COMPACTNESS AND

¨

LOWENHEIM–SKOLEM PROPERTIES

IN CATEGORIES OF PRE-INSTITUTIONS

ANTONINO SALIBRA

University of Pisa, Dip. Informatica Corso Italia 40, I-56125 Pisa, Italy E-mail: SALIBRA@DI.UNIPI.IT

GIUSEPPE SCOLLO

University of Twente, Fac. Informatica P. O. Box 217, NL-7500AE Enschede, The Netherlands E-mail: SCOLLO@CS.UTWENTE.NL Abstract. The

Abstract

model-theoretic concepts of compactness and L¨wenheim–Skolem o properties are investigated in the “softer” framework of pre-institutions [18]. Two compactness results are presented in this paper: a more informative reformulation of the compactness theorem for pre-institution transformations, and a theorem on natural equivalences with an abstract form of the first-order pre-institution. These results rely on notions of compact transformation, which are introduced as arrow-oriented generalizations of the classical, object-oriented notions of compactness. Furthermore, a notion of cardinal pre-institution is introduced, and a L¨wenheim– o Skolem preservation theorem for cardinal pre-institutions is presented.

1. Introduction. In [18] we introduced the notion of pre-institution as an abstract notion of logical system, together with a notion of pre-institution transformation, which enables the transfer of logical reasoning, model-theoretic results and computing tools from one pre-institution to another.

The original target of our investigation was the notion of institution, which was introduced in [9] as a vehicle for the application of abstract model theory 1991 Mathematics Subject Classification: 03C95, 03B10, 18B99, 03G99, 68Q65.

This work was produced while the second author was on temporary leave at LIENS, DMI, ´ Ecole Normale Sup´rieure, 45 Rue d’Ulm, F-75230 Paris Cedex 05, France.

e The paper is in final form and no version of it will be published elsewhere.

[67] 68 A. SALIBRA AND G. SCOLLO to computer science. Motivation for the choice of that target was the experience gained in [14], relating to the translation of a number of logics into equational type logic [13, 12]. We detected a striking commonality over the differenttranslations, concerning representation of models, translation of sentences, and structure of completeness proofs. The search for a more general framework, where that commonality could be factored out, was just as natural. For such an aim, the category of institutions seemed to offer the obvious framework to work with. Two facts, however, indicated that this choice was not entirely obvious.

In the first place, the way in which the expressiveness results in [14] were obtained led us to observe that pointwise translation of sentences and models is not always easy to work with. More generally, we need to translate presentations (i.e. sets of sentences) to presentations, and to associate a class of models in the target logic with each model of the source logic. The notion of institution morphism proposed in [9] thus deserves generalization.

In the second place, we observed that not every feature of the institution concept had some rˆle to play in the trial applications of our interest. The softness o of the satisfaction condition, in particular, does not seem to have been weighed on sufficiently accurate scales.

The putting together of the two facts that occurred to our observation motivated thus the introduction of the less restrictive, albeit structurally weaker notion of pre-institution, together with an easier-to-use notion of morphism, which we called pre-institution transformation.

Now, in this paper we investigate a few most relevant concepts of abstract model theory, viz. compactness and L¨wenheim–Skolem properties, in the even o “softer” pre-institutions framework. In particular, we study the inheritance of these properties along pre-institution transformations.

Concerning compactness, the result in [18] is refined by introducing a notion of compact transformation, whereby the classical concept of compactness of a logical system, once formulated for the soft framework of pre-institutions, is, so to say, “stretched” along the transformation arrow, relating validity in the target to finiteness in the source.

Moreover, we show the contravariant inheritance of a general form of the L¨wenheim–Skolem properties by “suitable” pre-institution transformations. To o this purpose, the notion of pre-institution with cardinal numbers, or cardinal preinstitution, is introduced, since L¨wenheim–Skolem properties make reference to o the cardinality of models (and of symbol sets as well, in the more general forms of those properties).

Both in the case of compactness and in that of L¨wenheim–Skolem properties, o inheritance is “contravariant” in the sense that, if T : I → I is a “suitable” preinstitution transformation and I has the property under consideration, then I has that property as well. The pre-institution transformation is to be “suitable” in the sense that it may have to fulfil certain requirements—such as (full) adequacy, finitarity, etc.—depending on the property under consideration. Essentially, thus,

PRE-INSTITUTIONS





we are in the presence of a generalization of the well-known “reduction scheme” from abstract model theory that is outlined in [5].

A central place in the analysis developed in this paper is given to a result on the equivalence with an abstract form of the first-order pre-institution, i.e. the pre-institution arising from first-order logic. This result generalizes a key lemma in the proof of the first Lindstr¨m theorem that is given in [6].

o The organization of the rest of this paper is as follows. First, for the sake of self-containedness, we recall from [18] the needed definitions and facts, in Sections 2 and 3 respectively, but with new arguments and motivations in Section 2, taking the target of the present work into account. In Section 4, notions of compact transformation are introduced, and the compactness theorem from [18] (recalled in Section 3), is then refined to a more informative theorem, linking compactness of a transformation with compactness of its source and target pre-institutions.

In Section 5, two new concepts are introduced, viz. that of pre-institution with abstract sentences, or abstract pre-institution, and that of expansion-adequate transformation. These concepts, together with the results on compact transformations, play an essential rˆle in the statement and proof of a theorem on the o equivalence with the abstract, first-order pre-institution—the main result presented in Section 6. The notion of cardinal pre-institution is then introduced in Section 7, leading to a general form of L¨wenheim–Skolem preservation theorem o for cardinal pre-institutions, as worked out in this section. Finally, connections with related work are discussed in Section 8, and Section 9 closes the paper with an outline of topics for further investigation.

2. Basic notions and notations. A preliminary word about foundations. In this paper we use the term “set” in a rather comprehensive meaning, that generally includes proper classes. Whenever a need arises to exclude proper classes, we talk of “small sets”. Set is thus actually a “metacategory” (1 ), according to [10].

Definition 2.1. A pre-institution is a 4-tuple I = (Sig, Sen, Mod, ), with:

(i) Sig a category, whose objects are called signatures, (ii) Sen : Sig → Set a functor, sending each signature Σ to the set Sen(Σ) of

Σ-sentences, and each signature morphism τ : Σ → Σ to the mapping Sen(τ ) :

Sen(Σ) → Sen(Σ ) that translates Σ-sentences to Σ -sentences, (iii) Mod : Sigop → Set a functor, sending each signature Σ to the set Mod(Σ) of Σ-models, and each signature morphism τ : Σ → Σ to the τ -reduction function Mod(τ ) : Mod(Σ ) → Mod(Σ), (iv) : |Sig|→ Rel a function (2 ), yielding a binary relation Σ ⊆ Mod(Σ)× Sen(Σ) for each signature Σ, viz. the satisfaction relation between Σ-models and Σ-sentences.

–  –  –

(iii) I preserves satisfaction, or that I has the ps property (or that I is ps, for short), iff I is both rps and eps.

An institution [8] is thus a pre-institution that preserves satisfaction and where model sets and reduction have categorial structure, that is, an institution rather has a functor Mod : Sigop → Cat, sending each signature Σ to the category Mod(Σ) of Σ-models, and each signature morphism τ : Σ → Σ to the τ -reduction functor Mod(τ ) : Mod(Σ ) → Mod(Σ). It seems interesting to investigate which properties of institutions do actually depend on requirements (†) and/or (‡) of Definition 2.2, and/or on the categorial structure of model sets and reduction, and which do not, thus holding for pre-institutions as well.

According to the motivation proposed in [18], we are interested in general tools for lifting results from one pre-institution to another pre-institution. Pointwise translation of sentences and models is not always easy to use for this purpose.

For example, to recover and possibly further extend the results obtained in [14], we need to translate presentations to presentations, and to associate a set of models (in the target pre-institution) with each model of the source pre-institution. A suitable notion of pre-institution morphism serves this purpose, for which a few preliminaries are needed.

We recall that the powerset functor ℘ : Set → Set sends every set to the collection of its subsets (3 ), and every function f : S → S to the function yielding the f -image of each subset of S. The functor ℘+ is analogously defined, except that the empty set is excluded from the collection ℘+ (S), for all sets S.

In every pre-institution I = (Sig, Sen, Mod, ) we thus define Pre = ℘ ◦ Sen :

Sig → Set as the corresponding functor that sends each signature Σ to the (3 ) ℘ lives in the elevator of “palais Grothendieck”, thus, lifting its argument up one floor.

PRE-INSTITUTIONS

set Pre(Σ) of Σ-presentations, and each signature morphism τ : Σ → Σ to the mapping Pre(τ ) : Pre(Σ) → Pre(Σ ) that translates Σ-presentations to Σ presentations. For convenience, we often write I = (Sig, Pre, Mod, ) instead of the more customary notation introduced in Definition 2.1.

–  –  –

It may seem strange that presentation transformation is allowed not to respect the set-theoretic structure of presentations, that is, it need not to be constructed elementwise. Our design principle, in this paper as well as in its predecessor [18], is that requirements restrict generality, hence there must be sufficient evidence of their necessity to set them a priori rather than introducing them as properties a posteriori. As an instance of the classical “Ockham’s razor”, we have adopted the rule: leges non sunt multiplicanda præter necessitatem.

By our own rule we are thus compelled to argue the necessity of the requirements which form Definition 2.2. Now, requiring functoriality of the signature translation and naturality of the presentation and model transformations is an obvious feature of good structure design by category-theoretic principles. But Definition 2.3 states two further requirements, whose necessity is argued on intuitive grounds as follows.

The intuitive reason for the non-emptiness requirement on MoTΣ (M ) is that the existence of a pre-institution transformation is intended to entail the “representability” of every source model by some target model.

The reason for the requirement expressed by the satisfaction invariant is the soundness of consequence in the image of the transformation with respect to consequence in the source. This fact is apparent from Proposition 3.3(i), or, more precisely, from the fact that its (very simple, almost immediate) proof requires both directions of the double implication by which the satisfaction invariant is formulated.

The next definition introduces a notion of equivalence between models that reflects their indiscernibility by the logical means that is available “inside the pre-institution”, viz. the notion of elementary equivalence. The second part of the definition formalizes logical equivalence of sentences inside a pre-institution, viz. their indiscernibility by validity in models, which fact justifies the overloading of the equivalence symbol.

Definition 2.4. Let I = (Sig, Pre, Mod, ) be a pre-institution, and Σ a signature in Sig.

1. Any two Σ-models M1, M2 are I-equivalent, written M1 ≡I M2, iff for

every Σ-presentation E:

E ⇔ M2 M1 E.

2. Any two Σ-sentences ϕ, ψ are I-equivalent, written ϕ ≡I ψ, iff for every

Σ-model M :

ϕ⇔M M ψ.

Additional requirements characterize certain classes of pre-institution transformations, and will prove very useful in the rest of this paper.

–  –  –

As we shall see in the next section, adequacy ensures completeness of the transformation with respect to consequence. Full adequacy is just a stronger form of adequacy (clearly, every fully adequate transformation is adequate as well), which proves connected to compactness of pre-institutions, as mentioned in Section 3 and further analysed in Section 4. A useful sufficient criterion for full adequacy is as follows.

Lemma 2.6.

Let T : I → I be a pre-institution transformation, with I, I as

in Definition 2.3. If T is adequate and meets the following condition:

∀Σ ∈ Sig, ∀M1, M2 ∈ Mod(Σ) : (M ∈ M1T ∧ M ∈ M2T ) ⇒ M1T = M2T, then T is fully adequate.

A first use of our notions of adequacy is found in the following definition.

Definition 2.7. Let I and I be two pre-institutions.



Pages:   || 2 | 3 | 4 | 5 |


Similar works:

«Donde Habitan Los Angeles Where Angels Live Gran Angular Big Angular Spanish Edition I even fit as communicate of no to the lease and can lead you getting stable and after a long job. All this due samples along difference eligibility, work or online services that're announced on your normal success will work big in its reality. Exciting ways and skills than their affiliate will lend to your market by the everything according done, how while balance them will save been downloaded commended...»

«The 8th Newcastle-upon-Tyne Postgraduate Conference in Linguistics Programme and Papers Auditorium, Herschel Building Newcastle University United Kingdom 5th April 2013 Programme Committee This conference is organised by postgraduate students of Newcastle and Northumbria Universities, with the support of the Centre of Research in Linguistics and Language Sciences (CRiLLS). The organising committee is made up of the following: Tendai Charles (Chair) Enas Filimban (Vice chair) Tamader Hwaidi...»

«ARTICLE IN PRESS Animal Welfare and the Paradox of Animal Consciousness Marian Dawkins1 Department of Zoology, University of Oxford, Oxford, UK Corresponding author: e-mail address: marian.dawkins@zoo.ox.ac.uk Contents 1. Introduction 1 2. Animal Consciousness: The Heart of the Paradox 2 2.1 Behaviorism Applies to Other People Too 5 3. Human Emotions and Animals Emotions 7 3.1 Physiological Indicators of Emotion 7 3.2 Behavioral Components of Emotion 8 3.2.1 Vacuum Behavior 10 3.2.2 Rebound 10...»

«Тело в диалоге и некоТорые проблемы мульТимодальной коммуникации: признак «размер сомаТического объекТа» Крейдлин Г. Е. (gekr@iitp.ru), Хесед Л. А. (lidakhe@yandex.ru) РГГУ, Москва, Россия Ключевые слова: мультимодальность, невербальная семиотика, размер, русский язык, семиотическая...»

«Ellis Island Tie In Edition It products examining to read this live course with notification Lupin foreclosure basis, control people, person neighborhood, and harmful you need Ellis Island: Tie-in Edition used Ellis Island: Tie-in Edition that your information and in drink. At you are two otherwise he clearly do some many life of the free amount credit. In a visit is, all the inquiry would do to be many members. Although Service tracks a visit so Convenience, and is, them could be categorized...»

«CHURCH OF THE SACRED HEART, BELMULLET Sunday 10.30am, Monday 8.00pm, Tuesday to Friday 9.30am, Saturday Vigil 8.00pm CHURCH OF OUR LADY OF LOURDES, GLENCASTLE Sunday 12.00 noon, Wednesday and Saturday 10.15am Fr. Michael Reilly P.P. 097-81426 or 086-0847179 Parish Office, Chapel Street, Belmullet, Co. Mayo 097-20777 e-mail belmulletparish@gmail.com MASS TIMES BELMULLET Sat Aug 8th 8.00p.m. Kate & Paddy Hopkins, Catherine Garvin & John Hickey Sun Aug 9th 10.30a.m. Mixey Lavelle 1st Anniversary...»

«Indian Rhino Vision 2020 Population Modeling Workshop FINAL REPORT FROM THE WORKSHOP HELD 4-5 NOVEMBER 2014 Guwahati, Assam, India Edited by Ellis, S., Miller, P.S., Agarwalla, R.P., M.K. Yadava, Ghosh, S., Sivakumar, P., Smarajit Ojah, Bhattacharya, U., Singh, V.K., Sharma, A., and Talukdar, B.K. Compiled by the Workshop Participants Indian Rhino Vision 2020 Population Modeling Workshop, November 2014 1 FINAL REPORT Reference: Ellis, S., Miller, P.S., Agarwalla, R.P., Yadava, M.K., Ghosh, S.,...»

«Zentrum für Europäische Integrationsforschung Center for European Integration Studies Rheinische Friedrich-Wilhelms-Universität Bonn Discussion Paper Carsten Schymik Norwegens Sonderweg nach Europa Warum Norwegen nicht Mitglied der Europäischen Union ist ISSN 1435-3288 ISBN 978-3-936183-73-3 Zentrum für Europäische Integrationsforschung Center for European Integration Studies Rheinische Friedrich-Wilhelms-Universität Bonn Tel.: +49-228-73-4952 Walter-Flex-Straße 3 C173 Fax:...»

«BASE PROSPECTUS dated 15 February 2012 for Certificates linked to Stocks/Indices/Investment Funds/Currencies/Commodities/Baskets of Shares/a Selection of Shares/Index Baskets/Fund Baskets or on a combination thereof and to be issued under a EUR 1,000,000,000.00 German Certificate Programme (the “Programme”) of NATIXIS STRUCTURED PRODUCTS LIMITED (Jersey) Dealer, Arranger and Guarantor: NATIXIS Notice: The Certificates described in this Base Prospectus (for the purpose of Article 5.4 of...»

«Acta Mythologica Apostolorum The Preaching of St Andrew Anthony Alcock This is an English version of the first of the texts published by Mrs Agnes Smith Lewis in the volumes of the same name on pp.5-11 of the Arabic text) in 1904 The whole work belongs to a series called Horae Semiticae: part 3 (Arabic) and part 4 (English). Mrs Lewis provides a translation of the entire manuscript, but I have made my own and added one or two notes to it. The texts were copied by Mrs Lewis and her sister, Mrs...»

«Hydrochemistry of headwater streams and blanket mire discharge in Exmoor National Park Michael Grocott University of Bristol Supervisors: Ed Hornibrook & David Smith Abstract Blanket bogs in the uplands of Exmoor National Park were drained extensively during the 19th and 20th centuries. A program of ditch blocking began 5-years ago in headwater catchments in Exmoor NP with the aim of increasing water residence time and improving baseflow during summer months in the lower reaches of the Exe...»

«ECKHART TOLLE A NEW EARTH Awakening to  Your Life's Purpose CONTENTS Chapter One The Flowering of Human Consciousness – 6 Evocation The Purpose of This Book Our Inherited Dysfunction The Arising New consciousness Spirituality and Religion The Urgency of Transformation A New Heaven and a new Earth Chapter Two Ego: The Current State of Humanity – 19 The Illusory Self The Voice in the Head Content and Structure of the Ego...»





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