Rubio etal - An axiom system for Incidence Spatial Geometry.pdf

(203 KB) Pobierz
An Axiom System for Incidence Spatial Geometry
RACSAM
Rev. R. Acad. Cien. Serie A. Mat.
V OL . 102 (2), 2008, pp. 237 – 249
Ciencias de la Computaci on / Computational Sciences
An Axiom System for Incidence Spatial Geometry
R. Rubio and A. Rıder
Abstract. Incidence spatial geometry is based on three-sorted structures consisting of points, lines
and planes together with three intersort binary relations between points and lines, lines and planes and
points and planes. We introduce an equivalent one-sorted geometrical structure, called incidence spatial
frame, which is suitable for modal considerations. We are going to prove completeness by SD-Theorem.
Extensions to projective, affine and hyperbolic geometries are also considered.
Un sistema axiom atico para la geometrıa espacial de incidencia
Resumen. La geometrıa espacial de incidencia esta construida por medio de estructuras trisurtidas
formadas por puntos, rectas y planos con relaciones binarias de interconexi on, para cada dos de estos
elementos. En este trabajo introducimos una estructura monosurtida, que denominamos marco espacial
de incidencia y que resulta adecuada para un tratamiento modal. Probaremos la completitud del sis-
tema por medio del SD-teorema. Las extensiones a los casos proyectivo, afın e hiperb olico son tambien
considerados.
Deductive logic systems are useful tools for knowledge engineering and computer sciences. This de-
velopment has turned into a master research line in mathematical logic. In particular, the systems based on
modal languages are especially adequate for computation sciences. Under this approach, several systems
have been studied which model temporal relations in their different interpretations and aspects of use, so
that the logic of time is a well-established branch of modal logic, whereas the same cannot be said of the
logic of space. The reason is probably in the more simple mathematical structure of time: a set of moments
together with a precedence relation between moments [ 9 ]. Such one-sorted relational structures are very
suitable for a modal treatment. It is quite apparent that incidence spatial relations are more complex than
temporal ones. Therefore, these structures are composed of different objects (i.e., they are many-sorted
structures): points, lines, planes, etc. Also, these objects are linked by several relations: collinearity, par-
allelism, orthogonality, incidence, etc. However, the study of geometrical models and their logical theories
is justified from an applied perspective since these logical systems can be used to formalize various aspect
and modes of practical spatial reasoning, such as reasoning on geographic charts, robotics, etc.
Several authors have been progressively working on geometrical properties and relations from the point
of view of these modal languages. Von Wright [ 19 ] has introduced a modal logic of space whose modalities
were “near” and “somewhere”. Van Benthem [ 5 ] and Goldblatt [ 10 ] independently advocated the use
of modal logic to describe relations between events but were not able to propose any intensional model
of space. Recently, Balbiani and co-authors have been working on geometrical properties and relations
concerning to the plane geometry, from the point of view of new multimodal and many-sorted languages [ 2 ,
3 , 4 ].
Presentado por / Submitted by Luis Laita de la Rica.
Recibido / Received: 20 de noviembre 2007 Aceptado / Accepted: 6 de febrero de 2008.
Palabras clave / Keywords: Modal Logic, Incidence Spatial Geometry.
Mathematics Subject Classifications: 03B45, 03B70, 68Q17
c ° 2008 Real Academia de Ciencias, Espa na.
237
R. Rubio and A. Rıder
In this work, following [ 16 , 14 , 15 ], we build a one-sorted structure (with only one class of objects)
which will be adequate for classical modal considerations and able to capture in an equivalent way the
models of incidence spatial geometry (dimension three) and we build a classical axiomatic multimodal
system suitable to be valuated on these one-sorted structures. This idea of an abstract frame for repre-
senting knowledge about different types of data has its origin in the modal theory of arrows developed by
Vakarelov [ 16 ].
We also prove correctness and completeness for our systems and extensions to affine, projective and
hyperbolic geometries are also considered. On the other hand, decidibility is still an open problem.
1 Incidence Spatial Geometry
In this section we introduce the incidence spatial geometries and incidence spatial frame, which will be
later needed when we assign the semantic to an axiomatic system. As incidence spatial frames are defined
by simply encoding the information concerning points, lines and planes in a different way, let us remember
the structure of incidence spatial geometry. Finally, we show that these categories are equivalent.
1.1 The category of incidence spatial geometries
By an incidence spatial geometry we will mean any three-sorted structureS=(P,L,¦,in 1 ,in 2 ,in 3 ),
which satisfies:
1.Pis a non-empty set, whose elements are called points, denoted by lower case lettersx,y,z, etc. . . ,
2.Lis a non-empty set, whose elements are called lines, denoted by capital lettersX,Y,Z, etc. . . ,
3.¦is a non-empty set, whose elements are called planes, denoted by lower bold lettersx,y,z, etc. . .
4. in 1 is an intersort relation between points and lines (in 1 ½P×L),
5. in 2 is an intersort relation between points and planes (in 2 ½Pצ),
6. in 3 is an intersort relation between lines and planes (in 3 ½Lצ).
Moreover we have the following axioms:
I0P\L=;,P\¦=;,L\¦=;.
I1(8x,y2P)(9Z2L)((xin 1 Z)^(yin 1 Z)), two points are together incident with at least
one line.
I2(8x,y2P)(8Z,T2L)(((xin 1 Z)^(yin 1 Z)^(xin 1 T)^(yin 1 T))!((x=
y)_(Z=T))), two different points are together incident with at most one line.
I3(8Z2L)(9x,y2P)((x6=y)^(xin 1 Z)^(yin 1 Z)), each line contains at least two
different points.
I4(8x2P)(9Z,T2L)((Z6=T)^(xin 1 Z)^(xin 1 T)), each point belongs to at least two
different lines.
I5(8x2P)(8Y2L)(9z2¦)((xin 2 z)^(Yin 3 z)), one point and one line are together
incident with at least one plane.
I6(8x2P)(8Y2L)(8z,t2¦)(((xin 2 z)^(Yin 3 z)^(xin 2 t)^(Yin 3 t))!((xin 1 Y)_
(z=t))), one point and one line, which aren’t incident, are incident with at most one plane.
I7(8z2¦)(9X,Y2L)((X6=Y)^(Xin 3 z)^(Yin 3 z)), each plane contains at least two
different lines.
238
An Axiom System for Incidence Spatial Geometry
I8(8x,y2P)(8Z2L)(8t2¦)(((xin 1 Z)^(yin 1 Z)^(xin 2 t)^(yin 2 t))!((Zin 3 t))),
if two points are together incident with one line and one plane, then the line will be incident
with the plane.
I9(8x2P)(8z,t2¦)(9y,z2P)(((xin 2 z)^(xin 2 t))!((y6=z)^(yin 2 z)^(yin 2 t)^
(zin 2 z)^(zin 2 t))), if one point is incident with two planes, then the planes contain at least
two common points.
I10(8X2L)(9y,z2¦)((z 6=t)^(Xin 3 y)^(Xin 3 z)), each line belongs to at least two
different planes.
This geometry is known as absolute or neutral geometry and is presented in many textbooks on geom-
etry, for example in [ 11 , 12 ]. The class of all incidence spatial geometries is denoted by§. We consider§as
a category where the objects are the incidence spatial geometries and the homomorphism are defined as fol-
lows: LetS=(P,L,¦,in 1 ,in 2 ,in 3 )andS 0 =(P 0 ,L 0 ,¦ 0 ,in 0 1 ,in 0 2 ,in 0 3 )be incidence spatial geometries.
A mapffromP[L[¦ontoP 0 [L 0 [¦ 0 is called a homomorphism fromSintoS 0 if:
•for any(x,Y,z)2Swe have(f(x),f(Y),f(z))2S 0 ,
•for any(x,Y,z)2S,
– ifxin 1 Ythenf(x)in 0 1 f(Y),
– ifxin 2 zthenf(x)in 0 2 f(z),
– ifYin 3 zthenf(Y)in 0 3 f(z).
An homomorphismfwhich admits an inverse homomorphism is called an isomorphism.
Incidence spatial geometries are in a sense minimal geometrical structures, which can be extended with
new axioms. Three natural extensions are projective, affine and hyperbolic geometries.
An incidence spatial geometryS=(P,L,¦,in 1 ,in 2 ,in 3 )is called projective if it satisfies the follow-
ing additional axioms:
P1(8Z,T2L)(8z2¦)(9x2P)(((Zin 3 z)^(Tin 3 z))!((xin 1 Z)^(xin 1 T))), two lines
(on a plane) contain at least one point in common.
P2(8T2L)(8x,y2P)(9z2P)(((xin 1 Z)^(yin 1 Z))!((zin 1 T)^(z6=x)^(z6=y))), if
a line contains two pointsxandythen it contains at least one pointzdifferent fromxandy.
These axioms are presented in [ 7 ].
To introduce the notion of affine spatial geometry we first define the relation of parallelism between
lines. Two linesZandTthat lie in a plane are parallel (ZkT) ifZ=Tor they do not intersect. We
denote parallelism byZkT.
ZkT iff (9z2¦)(Zin 3 z^Tin 3 z)^(8x2P)(xin 1 Z^xin 1 T!Z=T).
An incidence spatial geometryS=(P,L,¦,in 1 ,in 2 ,in 3 )is called affine if it satisfies the following addi-
tional axioms:
A1(8x2P)(8Y2L)(9Z2L)(((YkZ)^(xin 1 Z))_(xin 1 Y)), for every lineYand every
pointxthat does not lie onYthere is at least one lineZthroughxthat is parallel toY.
A2(8X,Y,Z2L)(((XkY)^(YkZ))!((XkZ))), the relationkis transitive.
239
R. Rubio and A. Rıder
From these axioms and the definition ofk, we can prove that there is at most one line both incident
with a given point and parallel to a given line. Thus, this axiomatic is equivalent to that considered by
Hilbert [ 12 ].
An incidence spatial geometryS=(P,L,¦,in 1 ,in 2 ,in 3 )is called hyperbolic if it satisfies the follow-
ing additional axiom:
H1(8x2P)(8Y2L)(9Z,T2L)(((Z6=T)^(YkZ)^(YkT)^(xin 1 Z)^(xin 1 T))_
(xin 1 Y)), for every lineYand every pointxnot onYthere exists at least two lines throughx
parallel toY.
This axiomatic are presented in [ 11 ].
1.2 The category of incidence spatial frames
The notion of incidence spatial geometry as a three-sorted relational structure with three intersort binary
relations is not suitable as a semantical basis of some modal logic. That is why we introduce new structures,
called incidence spatial frames, which are one-sorted and can be used for modal semantics.
LetS=(P,L,¦,in 1 ,in 2 ,in 3 )be an incidence spatial geometry. The relational structureW(S)=
(W,´ 1 ,´ 2 ,´ 3 )is called an incidence spatial frame overSif the following conditions are satisfied:
1.W={(x,Y,z):x2P,Y2L,z2¦,xin 1 Y,xin 2 z,Yin 3 z},
2.(x 1 ,Y 1 ,z 1 )´ 1 (x 2 ,Y 2 ,z 2 )iffx 1 =x 2 ,
3.(x 1 ,Y 1 ,z 1 )´ 2 (x 2 ,Y 2 ,z 2 )iffY 1 =Y 2 ,
4.(x 1 ,Y 1 ,z 1 )´ 3 (x 2 ,Y 2 ,z 2 )iffz 1 =z 2 .
The elementt=(x,Y,z)ofWcan be considered as point, line or plane according to the context in
whichtoccurs. For instance in the expressiont´ 1 v, the elementstandvare meant as points and the
relation´ 1 can be understood as the equality of points. In the structureW(S)we can define three relations
on 1 ,on 2 andon 3 in the following way:
(x 1 ,Y 1 ,z 1 )on 1 (x 2 ,Y 2 ,z 2 ) iff x 1 in 1 Y 2 ,
(x 1 ,Y 1 ,z 1 )on 2 (x 2 ,Y 2 ,z 2 ) iff x 1 in 2 z 2 ,
(x 1 ,Y 1 ,z 1 )on 3 (x 2 ,Y 2 ,z 2 ) iff Y 1 in 3 z 2 .
The relations converse ofon i is denoted byon −1
i fori2{1,2,3}.
The following shows thaton i andon −1
i , fori={1,2,3}are definable as compositions of the three
relations´ 1 ,´ 2 and´ 3 .
Lemma 1 LetSbe one incidence spatial geometry andW(S)be the incidence spatial frame overS. Then
for anyx,y2W, we have:
(i)xon 1 y iff (9z2W)((x´ 1 z)^(z´ 2 y)) iff (on 1 =´ 1 ±´ 2 ),
(ii)xon 2 y iff (9z2W)((x´ 1 z)^(z´ 3 y)) iff (on 2 =´ 1 ±´ 3 ),
(iii)xon 3 y iff (9z2W)((x´ 2 z)^(z´ 3 y)) iff (on 3 =´ 2 ±´ 3 ),
(iv)xon −1
1 y iff (9z2W)((x´ 2 z)^(z´ 1 y)) iff (on −1
1 =´ 2 ±´ 1 ),
(v)xon −1
2 y iff (9z2W)((x´ 3 z)^(z´ 1 y)) iff (on −1
1 =´ 3 ±´ 1 ),
(vi)xon −1
3 y iff (9z2W)((x´ 3 z)^(z´ 2 y)) iff (on −1
3 =´ 3 ±´ 2 ).
240
An Axiom System for Incidence Spatial Geometry
P ROOF . Straightforward. ¥
Lemma 2 LetSbe an incidence spatial geometry andW(S)be the incidence spatial frame overS. Then
the following conditions are satisfied:
SF0´ 1 ,´ 2 and´ 3 are equivalence relations such that
(8x,y2W)(((x´ 1 y)^(x´ 2 y)^(x´ 3 y))!((x=y))),
SF1(8x,y2W)(9z2W)((xon 1 z)^(yon 1 z)),
SF2(8x,y,z,t2W)(((xon 1 z)^(yon 1 z)^(xon 1 t)^(yon 1 t))!((x´ 1 y)_(z´ 2 t))),
SF3(8z2W)(9x,y2W)((x6´ 1 y)^(xon 1 z)^(yon 1 z)),
SF4(8x2W)(9z,t2W)((z6´ 2 t)^(xon 1 z)^(xon 1 t)),
SF5(8x,y2W)(9z2W)((xon 2 z)^(yon 3 z)),
SF6(8x,y,z,t2W)(((xon 2 z)^(yon 3 z)^(xon 2 t)^(yon 3 t))!((xon 1 y)_(z´ 3 t))),
SF7(8z2W)(9x,y2W)((x6´ 2 y)^(xon 3 z)^(yon 3 z)),
SF8(8x,y,z,t2W)(((xon 1 z)^(yon 1 z)^(xon 2 t)^(yon 2 t))!((zon 3 t))),
SF9(8x,z,t2W)(9y,v2W)(((xon 2 z)^(xon 2 t))!
((y6´ 1 v)^(yon 2 z)^(yon 2 t)^(von 2 z)^(von 2 t))),
SF10(8x2W)(9y,z2W)((z6´ 3 t)^(xon 3 y)^(xon 3 z)).
IfSbe an incidence spatial projective geometry then we have:
SPF1(8y,z,t2W)(9x2W)(((yon 3 t)^(zon 3 t))!((xon 1 y)^(xon 1 z))),
SPF2(8x,y,z2W)(9t2W)(((xon 1 z)^(yon 1 z))!((ton 1 z)^(t6=x)^(t6=y))).
IfSbe an incidence spatial affine geometry then we have:
SAF1(8x,y2W)(9z2W)((ykz)^(xon 1 z)_(xon 1 y)),
SAF2(8x,y,z2W)(((xky)^(ykz))!((xkz))).
IfSbe an incidence spatial hyperbolic geometry then we have:
SHF1(8x,y2W)(9z,t2W)((z6=t)^(ykz)^(ykt)^(xon 1 z)^(xon 1 t)_(xon 1 y)).
P ROOF . Straightforward. ¥
We define incidence spatial frame as any relational structureW f =(W,´ 1 ,´ 2 ,´ 3 )withW6=;and
satisfying the axioms SF0. . . SF10 from lemma 2 . By an incidence spatial projective frame we will mean
any incidence spatial frame, satisfying the axioms SPF1 and SPF2 from lemma 2 . We define incidence
spatial affine frame as any incidence spatial frame, satisfying the axioms SAF1 and SAF2 from lemma 2 .
In the same way we define incidence spatial hyperbolic frame as any incidence spatial frame, satisfying
the axiom SHF1 from lemma 2 . The class of all incidence spatial frames is denoted by©. We consider©
as a category where morphisms are the usual homomorphisms between one-sorted relational structure. If
W f =(W,´ 1 ,´ 2 ,´ 3 )andW 0 f =(W 0 ,´ 0 1 ,´ 0 2 ,´ 0 3 )are incidence spatial frames, then the mapfis called
homomorphism fromW f toW 0 f if it satisfies: for anyx,y2W, ifx´ i ythenf(x)´ 0 i f(y), i=1,2,3.
An homomorphismffromW f ontoW 0 f is called isomorphism if it satisfies:
(i)fis a bijective map fromW f ontoW 0 f ,
(ii) for anyx,y2W, iff(x)´ 0 i f(y)thenx´ i y,i=1,2,3.
241

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin