Generalised Geometric Logic

This paper introduces a notion of generalised geometric logic. Connections of generalised geometric logic with L-topological system and L-topological space are established.

THE ANALYSIS OF ELEMENTS GEOMETRY POSITION IN THE IRANIAN GARDEN STRUCTURE

Iranian garden has been known as a specific architecture in the whole world. Among all its special features, the geometrical structure of Iranian garden has always attracted the attention of architects and researchers. Nowadays, despite numerous studies on the Iranian gardens, the lack of geometrical studies and the extension of some old concepts have led to recognize the Iranian gardens based on a unique pattern in terms of geometry. This pattern has been known as an archetype and typifies the Iranian Garden Geometry as a quarter pattern. That it could not be a true hypothesis, because the impact of garden components on its structure has been neglected. Investigating geometric position of garden elements and their relationship with the general form of garden would provide more accurate theoretical basis for Iranian garden design. In addition, this approach could help experts to retrieve the ruined part of historical gardens. So far, extensive garden studies have been carried out more on the symbolic concepts, components introduction and typology according to times and locations. This article is the first attempt to study each common element’s geometry to realize how the spatial structures could be effective in the garden formation. This paper aims to recognize the architectural geometric logic of gardens based on library studies and field recordings.

Some Applications

This chapter describes some applications of the theory developed in the previous chapters in a variety of different mathematical contexts. The main methodology used to generate such applications is the ‘bridge technique’ presented in Chapter 2. The discussed topics include restrictions of Morita equivalences to quotients of the two theories involved, give a solution to a prozblem of Lawvere concerning the boundary operator on subtoposes, establish syntax-semantics ‘bridges’ for quotients of theories of presheaf type, present topos-theoretic interpretations and generalizations of Fraïssé’s theorem in model theory on countably categorical theories and of topological Galois theory, develop a notion of maximal spectrum of a commutative ring with unit and investigate compactness conditions for geometric theories allowing one to identify theories lying in smaller fragments of geometric logic.

A duality theorem

This chapter presents a duality theorem providing, for each geometric theory, a natural bijection between its geometric theory extensions (also called ‘quotients’) and the subtoposes of its classifying topos. Two different proofs of this theorem are provided, one relying on the theory of classifying toposes and the other, of purely syntactic nature, based on a proof-theoretic interpretation of the notion of Grothendieck topology. Via this interpretation the theorem can be reformulated as a proof-theoretic equivalence between the classical system of geometric logic over a given geometric theory and a suitable proof system whose rules correspond to the axioms defining the notion of Grothendieck topology. The role of this duality as a means for shedding light on axiomatization problems for geometric theories is thoroughly discussed, and a deduction theorem for geometric logic is derived from it.

Lattices of theories

In this chapter, by using the duality theorem established in Chapter 3, many ideas and concepts of elementary topos theory are transferred into the context of geometric logic; these notions notably include the coHeyting algebra structure on the lattice of subtoposes of a given topos, open, closed, quasi-closed subtoposes, the dense-closed factorization of a geometric inclusion, coherent subtoposes, subtoposes with enough points, the surjection-inclusion factorization of a geometric morphism, skeletal inclusions, atoms in the lattice of subtoposes of a given topos, the Booleanization and DeMorganization of a topos. An explicit description of the Heyting operation between Grothendieck topologies on a given category and of the Grothendieck topology generated by a given collection of sieves is also obtained, as well as a number of results about the problem of ‘relativizing’ a local operator with respect to a given subtopos.

Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic

We introduce a theorem proving strategy for Partial Classical Logic (PCL) thatis based on geometric logic. The strategy first translates PCL theories into sets of Kleene formulas. After that, the Kleene formulas are translated into 3-valued geometric logic. The resulting formulas can be refuted by an adaptation ofgeometric resolution.The translation to Kleene logic does not only open the way to theorem proving, butit also sheds light on the relation between PCL, Kleene Logic, and classical logic.