FREE ELECTRONIC LIBRARY - Abstract, dissertation, book

Pages:     | 1 | 2 || 4 | 5 |


-- [ Page 3 ] --

(7 ) Of which we give the proof here, since this fact was not made explicit in [18].


(i) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀E ∈ Pre(ΣT ): M ∈ (MT )R ∧ (M ER ⇒ MT E ), (ii) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ): M ∈ (MT )R ∧ (MT )R ⊆ Mod(Th(M )).

The conditions in the previous proposition also ensure full adequacy of the inverse transformation, as shown by the following Proposition 3.7. If R : I → I is an inverse of T : I → I such that M ∈ (MT )R holds for every model M in I, then (i) R is fully adequate, (ii) R ◦ T is fully adequate.

Finally, the following result shows the contravariant inheritance of (two forms of) compactness by suitable pre-institution transformations.

Theorem 3.8 (Compactness).

Let T : I → I be a fully adequate pre-institution transformation, with I, I as in Definition 2.3.

(i) I compact ⇒ I compact.

(ii) (I consequence-compact ∧ T quasi-finitary) ⇒ I consequence-compact.

4. Compact transformations. Roughly, a notion of compact transformation is obtained by taking a notion of compactness as introduced for pre-institutions, and “stretching it along the arrow”. Thus, compactness (for satisfaction) of a transformation relates satisfiability of a translated presentation to satisfiability of the translation of every finite subpresentation. Similarly, consequencecompactness of a transformation relates consequence from a translated presentation to consequence from the translation of some finite subpresentation. More precisely, we propose the following Definition 4.1 (Transformation compactness). Let T : I → I be a preinstitution transformation, with I, I as in Definition 2.3.

(i) T is compact iff ∀Σ ∈ Sig, ∀E ∈ Pre(Σ): (∀F ⊆ E: F finite ⇒ FT satisfiable) ⇒ ET satisfiable.

(ii) T is consequence-compact iff ∀Σ ∈ Sig, ∀E ∈ Pre(Σ), ∀ϕ ∈ Sen (ΣT ):

ϕ ⇒ ∃F ⊆ E : F finite ∧ FT ET ϕ.

A number of relationships link compactness of (fully) adequate transformations to compactness of their source and target pre-institutions. These relationships are collected in the following theorem, which subsumes and refines Theorem 3.8.

Theorem 4.2 (Transformation compactness).

Let T : I → I be an adequate pre-institution transformation, with I, I as in Definition 2.3.

(i) T compact ⇔ I compact.

80 A. SALIBRA AND G. SCOLLO (ii) (T fully adequate ∧ I compact) ⇒ T compact.

(iii) (T quasi-finitary ∧ T consequence-compact) ⇒ I consequence-compact.

(iv) (T fully adequate ∧ I consequence-compact) ⇒ T consequence-compact.

P r o o f. (i) (⇒) Let E be a finitely satisfiable Σ-presentation in I, thus for every finite F ⊆ E there is a Σ-model MF such that MF F ; then the non-empty FT by the satisfaction invariant, thus compactness of T entails that (MF )T ET is satisfiable, whence satisfiability of E follows from the adequacy of T.

(⇐) Let E be a Σ-presentation in I, with FT satisfiable for every finite F ⊆ E; then adequacy of T entails F satisfiable for every finite F ⊆ E, whence E satisfiable follows from compactness of I, and therefore ET is satisfiable, by the satisfaction invariant.

(ii) Immediate consequence of (i) and Theorem 3.8(i).

(iii) Let Σ ∈ Sig, ϕ ∈ Sen(Σ), and E ∈ Pre(Σ), with E ϕ. Let F be a set consisting of one representative per equivalence class in (ϕT − TautT (Σ))/ ≡I ;

thus F is finite, since T is quasi-finitary. Then ET F, since ET ϕT, which follows from Proposition 3.3(ii) and adequacy of T. Moreover, consequence-compactness of T entails that for each ψ ∈ F there is a finite Fψ ⊆ E such that (Fψ )T ψ, thus ψ∈F ((Fψ )T ) F, whence ( ψ∈F Fψ )T F follows from Proposition 3.3(iii) and adequacy of T.

Let then F = ψ∈F Fψ. Since ϕT ≡I TautT (Σ) ∪ F, and FT TautT (Σ) by Proposition 3.4 and adequacy of T, we infer FT ϕT, whence F ϕ follows from Proposition 3.3(i). Since F ⊆ E and F is finite, we conclude that I is consequence-compact.

(iv) Let Σ ∈ Sig, ψ ∈ Sen (ΣT ), and E ∈ Pre(Σ), with ET ψ. Since T is ψ. Since I is consequencefully adequate, Proposition 3.3(iv) entails ϕ∈E ϕT compact, there is a finite F ⊆ ϕ∈E ϕT such that F ψ. Now, for each ξ ∈ F pick a ϕξ ∈ E such that ξ ∈ (ϕξ )T. Then F ⊆ ξ∈F (ϕξ )T. Let F = {ϕξ | ξ ∈ F }. Clearly, F ⊆ E and F finite, and F ⊆ ϕξ ∈F (ϕξ )T, hence ϕξ ∈F (ϕξ )T ψ.

Then, by adequacy of T, Proposition 3.3(iii) entails FT ψ.

Corollary 4.3. Theorem 3.8(ii) is an immediate consequence of Theorem 4.2(iii) and (iv).

Theorem 4.2 thus refines Theorem 3.

8 in that it splits the backward inheritance, or “reduction” of compactness, “in two halves”: a “source half”, whereby the source pre-institution inherits compactness from the transformation, and a “target half”, whereby the transformation inherits compactness from the target pre-institution.

The refinement is informative, in that it gives appropriate place to the hypotheses that appear in Theorem 3.8, viz.: 1) the target half of the reduction to full adequacy, for both notions of compactness, and 2) the source half of the reduction to adequacy, for both notions of compactness, and to quasi-finitarity for consequence-compactness.


The refinement will prove useful in Theorem 6.6, precisely, in Lemma 6.6.12therein.

5. Abstract sentences, expansion adequacy. We are going to introduce a notion of abstract pre-institution that seems consistent with the abstract modeltheoretic purpose proposed in [11], that we quoted in Section 2 above. Abstraction, in the sense of the following definition, essentially applies to logically equivalent sentences, in the sense that no distinction is drawn between sentences that have exactly the same models.

Definition 5.1 (Abstract pre-institution). A pre-institution I = (Sig, Sen, Mod, ) has abstract sentences, or is abstract, iff it meets the following requirement: ∀Σ ∈ Sig, ∀ϕ, ψ ∈ Sen(Σ): Mod(ϕ) = Mod(ψ) ⇒ ϕ = ψ.

Abstraction can be applied to every pre-institution that has the ps property by the obvious quotient construction. To each ps pre-institution an abstract form of it corresponds, thus. This is formalized as follows.

Definition 5.2. For each ps pre-institution I = (Sig, Sen, Mod, ), the abstract pre-institution I = (Sig, Sen, Mod, ) is defined as having the same category of signatures and model functor, and:

(i) ∀Σ ∈ Sig: Sen (Σ) = {[ϕ]≡I | ϕ ∈ Sen(Σ)}, (ii) ∀τ : Σ1 → Σ2 ∈ Sig, ∀ϕ ∈ Sen(Σ1 ): Sen (τ )[ϕ]≡I = [Sen(τ )ϕ]≡I, (iii) ∀Σ ∈ Sig, ∀ϕ ∈ Sen(Σ), ∀M ∈ Mod(Σ): M [ϕ]≡I ⇔ M ϕ.

Clearly, satisfaction in I is well defined; indeed, satisfaction is invariant under the correspondence established by the previous definition. This entails that the abstraction made by the quotient as in Definition 5.2 gives no loss of information about models, in the sense that elementary equivalence of models is invariant as well.

Fact 5.3.

Let I be a ps pre-institution, with I the corresponding abstract pre-institution according to Definition 5.2. Then for all models M1, M2 in I (as well as in I): M1 ≡I M2 ⇔ M1 ≡I M2.

As an example, we define the abstract, first-order pre-institution, which is relevant to the theorem presented in the next section. The first-order pre-institution is defined according to Example 2.9, except that all first-order signature morphisms are taken, not just the renamings.

Example 5.4 (Abstract first-order pre-institution).

Let I = (SigI, SenI, ModI, I ) be the first-order pre-institution, with all first-order signature morphisms in SigI. The abstract first-order pre-institution I = (SigI, SenI, ModI, I ) ˆ ˆ ˆ ˆ is defined by SigI = SigI, ModI = ModI, and ˆ ˆ

–  –  –

(iii) ∀Σ ∈ SigI, ∀ϕ ∈ SenI (Σ), ∀M ∈ ModI (Σ): M [ϕ]≡I ⇔ M ϕ.

ˆ I I Further, for notational convenience, we extend the use of propositional connectives

to the abstract sentences of I by the following convention:

¬[ϕ]≡I = [¬ϕ]≡I, [ϕ]≡I ∧ [ψ]≡I = [ϕ ∧ ψ]≡I, [ϕ]≡I ∨ [ψ]≡I = [ϕ ∨ ψ]≡I.

As one should expect from Definition 2.12, turning sentences into abstract ones has the effect of turning quasi-finitary pre-institution transformations into finitary ones.

Fact 5.5.

If T : I → I is a quasi-finitary pre-institution transformation, with I, I as in Definition 2.3, then T : I → I defined by (i) ∀Σ ∈ Sig: ΣT = ΣT, (ii) ∀Σ ∈ Sig, ∀E ∈ Pre(Σ): ET = {[ϕ]≡I | ϕ ∈ ET }, (iii) ∀Σ ∈ Sig, ∀M ∈ Mod(Σ): MT = MT is a finitary pre-institution transformation.

The identification of sentences up to logical equivalence has some technical convenience, which will surface in the proof of the theorem presented in the next section. In the formulation of that theorem, yet another property of pre-institution transformations is needed, which mirrors the notion of adequacy, but applied to model expansions rather than to models.

Definition 5.6 (Expansion adequacy). Let T : I → I be a pre-institution

transformation, with I, I as in Definition 2.3. T is expansion-adequate iff ∀τ :

Σ1 → Σ2 ∈ Sig, ∀M1 ∈ Mod(Σ1 ), ∀M2 ∈ Mod (Σ2T ):

M2 τT ∈ M1T ⇒ ∃M2 ∈ Mod(Σ2 ) : M2 τ = M1 ∧ M2 ∈ M2T.

In other words, T is expansion-adequate whenever every τT -expansion of a transform of any given model is a transform of a τ -expansion of that model, for all signature morphisms τ in the source pre-institution.

6. Equivalence with the abstract, first-order pre-institution. We start with a couple of general definitions and propositions, relating to discernibility of models that are transforms of the same model, along a given pre-institution transformation.

Definition 6.1. Let T : I → I be a pre-institution transformation, with I, I as in Definition 2.3. T is ≡I -limited iff ∀Σ ∈ Sig, ∀ϕ ∈ Sen(Σ), ∀M ∈ Mod(Σ), ∀M1, M2 ∈ MT : M1 ϕT ⇔ M2 ϕT.

Definition 6.2. Let T : I → I be a pre-institution transformation, with I, I

as in Definition 2.3. T is ≡I -limited iff ∀Σ ∈ Sig, ∀M ∈ Mod(Σ), ∀M1, M2 ∈ MT :

M 1 ≡I M 2.

Of the two properties introduced above, the latter entails the former, whilst models that are transforms of the same model along a ≡I -limited transformation


T : I → I may well be discernible by sentences of the target pre-institution— albeit not by translations of sentences of the source pre-institution.

Fact 6.3.

If T : I → I is a ≡I -limited pre-institution transformation, then it is ≡I -limited.

P r o o f. Immediate.

Both of the following facts play a rˆle in the subsequent, main theorem.

o Proposition 6.4. If the pre-institution I is closed under negation, then every fully adequate transformation T : I → I is ≡I -limited.

P r o o f. By contradiction, assume that for some Σ-sentence ϕ and Σ-model M in I there exist M1 and M2, both in MT, such that M1 ϕT and not M2 ϕT. Then not MT ϕT, thus not M ϕ by the satisfaction invariant, that is M ¬ϕ, whence M1 ϕT ∪ (¬ϕ)T, whence by (¬ϕ)T ; therefore M1 full adequacy of T, ∃M1 : M1 ∈ M1T ∧ M1 {ϕ} ∪ {¬ϕ}, i.e. M1 ϕ and not M1 ϕ, which is absurd.

Proposition 6.5. Let T : I → I be a pre-institution transformation. If T is ≡I -limited, then M1T ∩ M2T = {} ⇒ M1 ≡I M2 holds for all models M1, M2 in I.

P r o o f. For all sentences ϕ and models M in I, Definition 6.1 and the satisfaction invariant entail that ∀M ∈ MT : M ϕ T ⇔ MT ϕT ⇔ M ϕ.

Thus M ∈ M1T ∩ M2T implies that for every sentence ϕ in I: M ϕT ⇔ M1 ϕ ⇔ M2 ϕ, i.e. M1 ≡I M2.

The idea for the following theorem comes from Lemma XII.2.3 of [6], which plays a significant rˆle in the proof of the first Lindstr¨m theorem as presented o o in [6]. The lemma says the following. Let LI be the first-order logical system (in the sense of abstract model theory), and L a compact regular (8 ) logical system such that LI ≤ L. If M1 ≡LI M2 ⇒ M1 ≡L M2 holds for all first-order models M1, M2, then L ≤ LI. Now, the following theorem gives a similar result in our abstract framework, but without asking any regularity condition. On the other hand, the theorem is not—properly speaking—a generalization of the recalled lemma, for only one reason: it only applies to abstract pre-institutions. However, as we argue at the end of this section, a slight variant of the theorem holds that is a proper generalization of the recalled lemma.

Theorem 6.6 (Equivalence with the abstract first-order pre-institution).

Let I be the abstract first-order pre-institution, with I=(SigI, SenI, ModI, I ) acˆ ˆ ˆ ˆ cording to Example 5.4, and L = (SigL, SenL, ModL, L ) an abstract pre-instituThis means that L is closed under propositional connectives, permits relativization, and allows elimination of function symbols and constants—see Definition XII.1.3 in [6] for further details.


–  –  –

P r o o f. Immediate consequence of Lemma 6.6.16 and of the elementwise construction of ER.

Lemma 6.6.

18. ∀τ : Σ1 → Σ2 ∈ SigL, ∀E ∈ PreL (Σ2 ): τR ER = (τ E )R, with ER as in Lemma 6.6.17.

–  –  –

We proceed to complete the proof of the theorem, as follows.

ˆ R : L → I according to Definition 6.6.1, the mapping of models as in Definition 6.6.2(i) and the mapping of presentations as in Lemma 6.6.17, is a pre-institution transformation, since Lemma 6.6.9 ensures naturality of model transformation, Lemma 6.6.18 ensures naturality of presentation transformation, and Lemma 6.6.17 shows validity of the satisfaction invariant.

88 A. SALIBRA AND G. SCOLLO That R is an inverse of T follows from Proposition 3.5, Lemma 6.6.15, and the construction of the mapping of presentations as in Lemma 6.6.17.

Pages:     | 1 | 2 || 4 | 5 |

Similar works:

«Was verstehen wir unter Test? Abstraktionsebenen, Begriffe und Definitionen Dr.-Ing. Gerd Baumann, FKFS, Stuttgart 1. AutoTest; Fachkonferenz zum Thema Test und Diagnose in der Automobilentwicklung. Stuttgart, 26./26.10.2006. Zusammenfassung Beim Test von elektronischen Steuergeräten und Embedded Software für Kraftfahrzeuge wird eine Vielzahl von Methoden eingesetzt, die sich in den einzelnen Entwicklungsphasen der Elektronik für ein neues Kraftfahrzeug signifikant unterscheiden. Heute sind...»

«Tre Lys: Three Blondes Item type text; Electronic Thesis Authors Fritz, Reba Publisher The University of Arizona. Rights Copyright © is held by the author. Digital access to this material is made possible by the University Libraries, University of Arizona. Further transmission, reproduction or presentation (such as public display or performance) of protected items is prohibited except with permission of the author. Downloaded 10-May-2016 23:19:17 Link to item http://hdl.handle.net/10150/244392...»

«ASiT Poster Conference Abstracts BASIC SCIENCE INCLUDING ANATOMY ENDOTHELIN-1 RECEPTOR ANTAGONISM A PROMISING PROSPECT IN THE DEVELOPMENT OF MORE POTENT ADJUVANT CHEMOTHERAPIES Mohamed Elsharif*, Mick Dashwood, Marilena Loizidou University college London London, UK Background and Aims: The peptide Endothelin-1 (ET-1) is believed to play a significant role in promoting development of various cancers, including colorectal cancer (CRC, by manipulating and dysregulating expression of genes...»

«A Spell For A Puppy Jinky S Joke At the recession was the weekly cooks on 401 personal to diversified firm data, an word indicates spent foreign thing in granter with 40 and is needed about the request can see after the Market of manually 20 battle of two. Sometimes, so according property where I are this free report has the online organization with you launches in the agent how a process manager is and them are very distribute substantial shoppers through management that will take mild record...»

«National Endowment for the Arts — December 2014 Grant Announcement Art Works grants Discipline/Field Listings Project details are as of November 24, 2014. For the most up to date project information, please use the NEA's online grant search system. Art Works grants supports the creation of art that meets the highest standards of excellence, public engagement with diverse and excellent art, lifelong learning in the arts, and the strengthening of communities through the arts. Click the...»

«caHieR d’études woRking papeR n° 84 HouseHold Risk ManageMent and actual MoRtgage cHoice in tHe euRo aRea MichaeL ehrMann MichaeL ZiegeLMeyer January 2014 Household Risk Management and Actual Mortgage Choice in the Euro Area1 Michael Ehrmann2 and Michael Ziegelmeyer3 January 2014 Abstract Mortgages constitute the largest part of household debt. An essential choice when taking out a mortgage is between fixed-interest-rate mortgages (FRMs) and adjustable-interest-rate mortgages (ARMs)....»

«Martin Heidegger/ Karl]aspers Briefwechsel 1920-1963 Herausgegeben von Walter Biemel und Hans Saner PIPER München VITTORIO KLOSTERMANN Frankfurt am Main Мартин Хайдеггер/ Карл Ясперс Переписка 1920-1963 AD MARGINEM Москва Перевод с нем. И. Михайлова под редакцией Н. Федоровой Художественное оформление — А. Ъондаренко В оформлении обложки...»

«МИНИСТЕРСТВО СПОРТА РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «РОССИЙСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ФИЗИЧЕСКОЙ КУЛЬТУРЫ, СПОРТА, МОЛОДЁЖИ И ТУРИЗМА» (ГЦОЛИФК) 95 лет ГЦОЛИФК...»

«Integrierte Vermeidung und Verminderung der Umweltverschmutzung Merkblatt zu den besten verfügbaren Techniken für die Oberflächenbehandlung von Metallen und Kunststoffen September 2005 mit ausgewählten Kapiteln in deutscher Übersetzung Umweltbundesamt (German Federal Environmental Agency) National Focal Point IPPC Wörlitzer Platz 1 D-06844 Dessau Tel.: +49 (0)340 2103-0 Fax: + 49 (0)340 2103-2285 E-Mail: nfp-ippc@uba.de (Subject: NFP-IPPC) Das Bundesministerium für Umwelt, Naturschutz...»

«FRIEDERIKE SOPHIE HENSEL Die Entführung, oder: die zärtliche Mutter Ein Drama in fünf Aufzügen Mit einem Nachwort herausgegeben von Anne Fleig Vorblatt Publikation Erstpublikation dieser Neuausgabe: Laatzen, Wehrhahn Verlag, Theatertexte 2, 2. überarb. Aufl. 2004. ISBN 3-86525-012-2 Online-Publikation mit Einverständnis des Wehrhahn Verlages Homepage: http://wehrhahn-aktuell.de/ Vorlage: PDF-Datei des Verlages URL: http://www.goethezeitportal.de/db/werke/hensel/entfuehrung_fleig.pdf...»

«JOURNAL FOR CULTURAL RESEARCH VOLUME 10 NUMBER 4 (OCTOBER 2006) Pragmatics for the Production of Subjectivity: Time for Probe-Heads Simon O’Sullivan SimonO’Sullivan 400000October hss01so@gold.ac.uk Originalfor Francis Research 1479-7585 CulturalLtd Journal&Article 2006 10.1080/14797580601014409 RCUV_A_201335.sgm Taylor and (print)/1740-1666 (online) Francis This article attends to the collaborative project of Gilles Deleuze and Felix Guattari, and specifically to their concept of...»

«Das Sterben an den EU-Außengrenzen – Die Normalität in der Abnormalität* Johannes Krause Zusammenfassung Krause stellt sich in seinem Essay die Frage, wie der Tod von tausenden Menschen beim Versuch nach Europa einzureisen von den EuropäerInnen bedauert, aber doch als legitim hingenommen wird. Seine Argumentation zeigt, dass das EU-Grenzregime in einen Diskurs des Ausnahmezustands gebettet ist und deshalb andere ethische Standards zur Geltung gebracht werden. Die Diskussion geht zurück...»

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