Received: from chenas.inria.fr by moose.cs.indiana.edu
	(8.7.1/IUCS.1.49) id GAA17327; Fri, 15 Mar 1996 06:21:22 -0500 (EST)
From: <balbiani@ura1507.univ-paris13.fr>
Received: from d.univ-paris13.fr by chenas.inria.fr (5.65c8d/92.02.29)
	via EUnet-France id AA09768; Fri, 15 Mar 1996 12:20:56 +0100 (MET)
Received: from univ-paris13.fr (ura1507.univ-paris13.fr) by d.univ-paris13.fr; Fri, 15 Mar 96 12:21:57 +0100 (MET)
Received: from [193.105.152.221] by univ-paris13.fr (SMI-8.6/SMI-SVR4)
	id MAA05191; Fri, 15 Mar 1996 12:19:40 GMT
Message-Id: <199603151219.MAA05191@univ-paris13.fr>
Mime-Version: 1.0
Content-Type: multipart/mixed; boundary="========================_3484184==_"
Date: Fri, 15 Mar 1996 12:34:35 +0000
To: lsm@cs.indiana.edu
Subject: ITALLC96
Status: R



--========================_3484184==_
Content-Type: text/plain; charset="us-ascii"


   Dear Larry Moss

Please find attached our contribution to ITALLC96. Note that our paper
will be presented at the international conference on formal and applied
practical reasoning, next june, in Bonn, Germany. Luis Farinas del Cerro
and I are currently extending the results of itallc96.tex and hope to be
able to present the new results at ITALLC96.

   With my best wishes

   Philippe Balbiani

   balbiani@ura1507.univ-paris13.fr

   Laboratoire d'informatique de Paris-Nord
   Institut Galilee
   Universite Paris-Nord
   Avenue Jean-Baptiste Clement
   F-93430 Villetaneuse



--========================_3484184==_
Content-Type: text/plain; name="itallc96.tex"; charset="us-ascii"
Content-Disposition: attachment; filename="itallc96.tex"

%
%
\documentstyle{article}
%
%
\hyphenation{Va-ka-re-lov}
%
%
\title{Geometrical structures and modal logic}
%
%
\author{Philippe {\sc Balbiani}, Luis {\sc Fari\~{n}as del Cerro},\\
        Tinko {\sc Tinchev} and Dimiter {\sc Vakarelov}}
%
%
\date{Laboratoire d'informatique de Paris-Nord\footnote{Philippe Balbiani,
      balbiani@ura1507.univ-paris13.fr, Laboratoire d'informatique de
Paris-Nord,
      Institut Galil\'{e}e, Universit\'{e} Paris-Nord, Avenue Jean-Baptiste
      Cl\'{e}ment, F-93430 Villetaneuse.}\\
      Institut de recherche en informatique de Toulouse\footnote{Luis
      Fari\~{n}as del Cerro, farinas@irit.fr, Institut de recherche en
      informatique de Toulouse, Universit\'{e} Paul Sabatier, 118 route de
      Narbonne, F-31062 Toulouse Cedex.}\\
      Department of Mathematical Logic, Sofia University\footnote{Tinko
      Tinchev and Dimiter Vakarelov, dvak@ipx.fmi.uni-sofia.bg, Department of
      Mathematical Logic with
      Laboratory for Applied Logic, Faculty of Mathematics and Informatics,
      Sofia University, Boul. James Bouchier 5, 1126 Sofia, Bulgaria.}}
%
%
\newtheorem{montheoreme}{Theorem}
\newtheorem{monlemme}{Lemma}
\newtheorem{moncorollaire}{Corollary}
\newtheorem{monexemple}{Example}
\newenvironment{mapreuve}{{\bf Proof}}{$\dashv$}
%
%
\begin{document}
%
%
\maketitle
%
%
\abstract{Although, in natural language, space modalities are used as frequently
as time modalities, 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
relation of precedence. Such a relational structure is suited to a modal
treatment.
The structure of space is more complex: several sorts of geometrical beings as
points and lines together with binary relations as incidence or orthogonality,
or only one sort of geometrical beings as points but ternary relations as
collinearity or betweeness. In this paper, we define a general framework for
axiomatizing modal logics which Kripke semantics is based on geometrical
structures:
structures of collinearity, projective structures, orthogonal structures.}
%
%
%\abstract{A structure of collinearity consists of a set of points together
%with a ternary relation of collinearity between points. Therefore, a
%structure of collinearity cannot constitute the standard semantics of a modal
%logic. To overcome this problem, a frame of collinearity consisting of a set of
%tips together with a family of binary relations between tips is associated to
%every structure of collinearity in such a way that the set of all structures of
%collinearity is categorically equivalent to the set of all frames of
%collinearity. Therefore, a frame of collinearity can constitute the standard
%semantics of the modal logic of collinearity. Extensions to projective geometry
%and orthogonal geometry are also considered.}
%
%
\section{Introduction}
%
Although, in natural language, space modalities are used as frequently as time
modalities, the logic of time is a well-established branch of modal logic
\cite{GabHodRey} 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 relation of precedence. Such a relational structure is
suited to a modal treatment. The structure of space is more complex: several
sorts of geometrical beings as points and lines together with binary relations
as incidence \cite{Heyting} \cite{Hilbert} or orthogonality \cite{Goldblatt},
or only one sort of geometrical beings as points but ternary relations as
collinearity or betweeness \cite{SzczerbaTarski}. Such relational structures
are not suited to a modal treatment. \par
%
Structures of collinearity, first example, consist of a set of points together
with a ternary relation of collinearity between points. They cannot constitute
the standard semantics of the modal logic of collinearity. To overcome this
problem, a frame of collinearity is associated to every structure of
collinearity in the following way. Let ${\underline S}=(P,C)$ be a structure
of collinearity, with $P$ the set of points and $C$ the ternary relation of
collinearity between points. Let $W$ be the graph of the relation $C$. For
every $i,j\in\{1,2,3\}$, let $\equiv_{ij}$ be the binary relation on $W$
defined by $(X_{1},X_{2},X_{3})\equiv_{ij}(Y_{1},Y_{2},Y_{3})$ iff $X_{i}=
Y_{j}$. Intuitively, each element $(X,Y,Z)$ of $W$ can be considered either as
$X$, $Y$ or $Z$. Let $u=(X_{1},X_{2},X_{3})$, $v=(Y_{1},Y_{2},Y_{3})$ and
$w=(Z_{1},Z_{2},Z_{3})$. The expression $(\exists x\in W)(u\equiv_{i1}x\wedge
v\equiv_{j2}x\wedge w\equiv_{k3}x)$ is equivalent to $C(X_{i},Y_{j},Z_{k})$.
Therefore, $W({\underline S})=(W,\equiv_{ij})$ contains in some sense the whole
information of ${\underline S}$. $W({\underline S})$ is the frame of
collinearity over ${\underline S}$. It satisfies the properties detailed in
section $4.2$. A frame of collinearity is a relational structure of the form
$(W,\equiv_{ij})$ that satisfies the same properties. It can be proved that
any frame of collinearity is isomorphic to a frame of collinearity over some
structure of collinearity and that the set of all structures of collinearity
is categorically equivalent to the set of all frames of collinearity.
Therefore, frames of collinearity can constitute the standard semantics of
the modal logic of collinearity. \par
%
Projective structures, second example, consist of a set of points and a set of
lines together with a binary relation of incidence between points and lines.
They cannot constitute the standard semantics of the modal logic of projective
geometry. To overcome this problem, a projective frame is associated to every
projective structure in the following way. Let ${\underline S}=(P,L,in)$ be a
projective structure, with $P$ the set of points, $L$ the set of lines and $in$
the binary relation of incidence between points and lines. Let $W$ be the graph
of the relation $in$. Let $\equiv_{11}$ and $\equiv_{22}$ be the binary
relations on $W$ defined by $(X,x)\equiv_{11}(Y,y)$ iff $X=Y$ and $(X,x)
\equiv_{22}(Y,y)$ iff $x=y$. Intuitively, each element $(X,x)$ of $W$ can be
considered either as $X$ or $x$. Let $u=(X,x)$ and $v=(Y,y)$. The expression
$u\equiv_{11}\circ\equiv_{22}v$ is equivalent to $X$ $in$ $y$. Therefore,
$W({\underline S})=(W,\equiv_{11},\equiv_{22})$ contains in some sense the
whole information of ${\underline S}$. $W({\underline S})$ is the projective
frame over ${\underline S}$. It satisfies the properties detailed in section
$7.1.2$. A projective frame is a relational structure of the form $(W,
\equiv_{11},\equiv_{22})$ that satisfies the same properties. It can be proved
that any projective frame is isomorphic to a projective frame over some
projective structure and that the set of all projective structures is
categorically equivalent to the set of all projective frames. Therefore,
projective frames can constitute the standard semantics of the modal logic of
projective geometry. \par
%
Section $2$ introduces point $n$-frames and $n$-arrow frames and gives the
proof of their categorial equivalence. Section $3$ extends Vakarelov's basic
arrow logic \cite{Vakarelov1} \cite{Vakarelov2}. Its standard semantics is the
set of all $n$-arrow frames. Section $4$ describes an example of point
$3$-frames: the structures of collinearity, proves its categorial equivalence
with the associated example of $3$-arrow frames: frames of collinearity, and
identifies the modal logic with standard semantics in the set of all frames of
collinearity. Sections $5$ and $6$ extend the results of sections $2$ and $3$
to sorted point $n$-frames and sorted $n$-arrow frames. Section $7.1$ describes
an example of sorted point $2$-frames: the projective structures, proves its
categorial equivalence with the associated example of sorted $2$-arrow frames:
projective frames, and identifies the modal logic with standard semantics in
the set of all projective frames. Section $7.2$ describes an example of sorted
point $3$-frames: the orthogonal structures, proves its categorial equivalence
with the associated example of sorted $3$-arrow frames: orthogonal frames, and
identifies the modal logic with standard semantics in the set of all
orthogonal frames.
%
%
\section{Point $n$-frames and $n$-arrow frames}
%
Let $n\ge 2$ and $(n)=\{1,\ldots,n\}$. This section is devoted to the
proof of the categorial equivalence between point $n$-frames and $n$-arrow
frames.
%
\subsection{Point $n$-frames}
%
A {\em point $n$-frame} consists of a non-empty set $S$
together with a $n$-ary relation $R$ on $S$ such that, for every $X\in S$,
there exists $X_{1},\ldots,X_{n}\in S$ and there exists $i\in(n)$ such that
$R(X_{1},\ldots,X_{n})$ and $X_{i}=X$. The class of all point $n$-frames
is denoted by $\Sigma_{n}$ and is considered as a category with
morphisms the usual homomorphisms between relational structures. Namely,
let ${\underline S}=(S,R)$ and ${\underline S}'=(S',R')$ be point $n$-frames.
Then $f$ is called a {\em homomorphism} from ${\underline S}$
into ${\underline S}'$ if, for every $X_{1},\ldots,X_{n}\in S$, $R(X_{1},
\ldots,X_{n})$ only if $R'(f(X_{1}),\ldots,f(X_{n}))$. A one-to-one $f$ is
called an {\em isomorphism} from ${\underline S}$ into ${\underline S}'$ if,
for every $X_{1},\ldots,X_{n}\in S$, $R'(f(X_{1}),\ldots,f(X_{n}))$ only if
$R(X_{1},\ldots,X_{n})$.
%
\subsection{$n$-arrow frames}
%
A {\em $n$-arrow frame} consists of a non-empty set $W$ of {\em tips} together
with $n^{2}$ binary relations $\equiv_{ij}$ on $W$ such that, for every $i,j,
k\in(n)$:
%
\begin{itemize}
   \item for every $u\in W$, $u\equiv_{ii}u$,
   \item for every $u,v\in W$, $u\equiv_{ij}v$ only if $v\equiv_{ji}u$,
   \item for every $u,v,w\in W$, $u\equiv_{ij}v$ and $v\equiv_{jk}w$ only if
         $u\equiv_{ik}w$.
\end{itemize}
%
The $n$-arrow frame ${\underline W}=(W,\equiv_{ij})$ is {\em normal}
if:
%
\begin{itemize}
   \item for every $u,v\in W$, $u\equiv_{ii}v$, for every $i\in(n)$,
         only if $u=v$.
\end{itemize}
%
The class of all normal $n$-arrow frames is denoted by $\Phi_{n}$ and
is considered as a category with morphisms the usual homomorphisms between
relational structures.
%
\subsection{From point $n$-frames to $n$-arrow frames}
%
Let ${\underline S}=(S,R)$ be a point $n$-frame. Let $W=\{(X_{1},
\ldots,X_{n})$: $X_{1},\ldots,X_{n}\in S$ and $R(X_{1},\ldots,X_{n})\}$.
For every $i,j\in(n)$, let $\equiv_{ij}$ be the binary relation on $W$
defined by $(X_{1},\ldots,X_{n})\equiv_{ij}(Y_{1},\ldots,Y_{n})$ iff $X_{i}=
Y_{j}$.
%
\begin{monlemme}
$W({\underline S})=(W,\equiv_{ij})$ is a normal $n$-arrow frame.
\end{monlemme}
%
\begin{monexemple}
Suppose $n=3$. It can be proved that if, for every $X,Y\in S$, $R(X,Y,X)$
then, for every $i,j\in(3)$ and for every $x,y\in W$, there exists $u\in W$
such that $x\equiv_{i1}u$, $y\equiv_{j2}u$ and $x\equiv_{i3}u$.
\end{monexemple}
%
\subsection{From $n$-arrow frames to point $n$-frames}
%
Let ${\underline W}=(W,\equiv_{ij})$ be a normal $n$-arrow frame. For
every $\alpha_{1},\ldots,\alpha_{n}\in{\cal P}(W)$, if:
%
\begin{itemize}
   \item for every $i,j\in(n)$ and for every $u,v\in W$, $u\in\alpha_{i}$ and
         $v\in\alpha_{j}$ only if $u\equiv_{ij}v$,
   \item for every $i,j\in(n)$ and for every $u,v\in W$, $u\in\alpha_{i}$ and
         $u\equiv_{ij}v$ only if $v\in\alpha_{j}$,
   \item $\alpha_{1}\cup\ldots\cup\alpha_{n}\not=\emptyset$
\end{itemize}
%
then $(\alpha_{1},\ldots,\alpha_{n})$ is a {\em generalized point} of
${\underline W}$. For every $u\in W$ and for every $i\in(n)$, let
$i(u)=(\equiv_{i1}(u),\ldots,\equiv_{in}(u))$. Direct calculations would lead
to the conclusion that:
%
\begin{monlemme}
For every $u,v\in W$ and for every $i,j\in(n)$, $i(u)=j(v)$ iff $u\equiv_{ij}
v$.
\end{monlemme}
%
\begin{monlemme}
For every generalized point $(\alpha_{1},\ldots,\alpha_{n})$ of ${\underline
W}$, there exists $u\in W$ and $i\in(n)$ such that $i(u)=(\alpha_{1},\ldots,
\alpha_{n})$.
\end{monlemme}
%
Let $S$ be the set of the generalized points of ${\underline W}$. Let $R$ be
the $n$-ary relation on $S$ defined by $R(X_{1},\ldots,X_{n})$ iff there
exists $u\in W$ such that, for every $i\in(n)$, $X_{i}=i(u)$.
%
\begin{monlemme}
$S({\underline W})=(S,R)$ is a point $n$-frame.
\end{monlemme}
%
\begin{monexemple}
Suppose $n=3$. It can be proved that if, for every $i,j\in(3)$ and for every
$x,y\in W$, there exists $u\in W$ such that $x\equiv_{i1}u$, $y\equiv_{j2}u$
and $x\equiv_{i3}u$ then, for every $X,Y\in S$, $R(X,Y,X)$.
\end{monexemple}
%
\subsection{Representation theorems}
%
Let ${\underline W}=(W,\equiv_{ij})$ be a normal $n$-arrow frame and
${\underline W}'=W(S({\underline W}))$. For every $u\in W$,
let $g(u)=(1(u),\ldots,n(u))$. Direct calculations would lead to the
conclusion that $g$ is an isomorphism from ${\underline W}$ into ${\underline
W}'$. Therefore:
%
\begin{monlemme}
${\underline W}$ and ${\underline W}'$ are isomorphic.
\end{monlemme}
%
Let ${\underline S}=(S,R)$ be a point $n$-frame and
${\underline S}'=S(W({\underline S}))$. For every $X\in S$, let
$f(X)=(1(X),\ldots,n(X))$ where $i(X)=\{(X_{1},\ldots,X_{n})$: $X_{1},
\ldots,X_{n}\in S$, $R(X_{1},\ldots,X_{n})$ and $X_{i}=X\}$. Direct
calculations would lead to the conclusion that $f$ is an isomorphism from
${\underline S}$ into ${\underline S}'$. Consequently:
%
\begin{monlemme}
${\underline S}$ and ${\underline S}'$ are isomorphic.
\end{monlemme}
%
Direct calculations would lead to the conclusion that the mapping $S$:
${\underline W}\rightarrow S({\underline W})$ is a functor from $\Phi_{n}$
into $\Sigma_{n}$ and that the mapping $W$: ${\underline S}\rightarrow
W({\underline S})$ is a functor from $\Sigma_{n}$ into $\Phi_{n}$. Therefore:
%
\begin{montheoreme}
The categories $\Sigma_{n}$ and $\Phi_{n}$ are equivalent.
\end{montheoreme}
%
%
\section{Basic arrow logic}
%
Let $n\ge 2$. This section introduces a modal logic with standard semantics
in the class of all normal $n$-arrow frames.
%
\subsection{Language}
%
The linguistic basis of basic arrow logic is the propositional
calculus. Let $VAR$ be the set of its {\em atomic formulas}. For every
$i,j\in(n)$, the modal operator $[\equiv_{ij}]$ is added to the standard
propositional formalism and, for every $i\in(n)$, the modal operator
$[\not\equiv_{ii}]$ is added to the standard propositional formalism. Let
$[\not=]A=[\not\equiv_{11}]A\wedge\ldots\wedge[\not\equiv_{nn}]A$ and
$[U]A=A\wedge[\not=]A$.
%
\subsection{Semantics}
%
A {\em general $n$-arrow frame} consists of a non-empty set $W$
together with, for every $i,j\in(n)$, a binary relation $\equiv_{ij}$ on
$W$ such that $(W,\equiv_{ij})$ is a $n$-arrow frame and, for every
$i\in(n)$, a binary relation $\not\equiv_{ii}$ on $W$. A general $n$-arrow
frame ${\underline W}=(W,\equiv_{ij},\not\equiv_{ii})$ is {\em
$\not=$-standard} if, for every $u,v\in W$, $u\not=v$ iff there exists
$i\in(n)$ such that $u\not\equiv_{ii}v$. A $\not=$-standard frame
${\underline W}=(W,\equiv_{ij},\not\equiv_{ii})$ is {\em quasi-standard}
if, for every $i\in(n)$, $\not\equiv_{ii}$ is the complement of $\equiv_{ii}$.
%
\begin{monlemme}
If the general $n$-arrow frame ${\underline W}=(W,\equiv_{ij},\not\equiv
_{ii})$ is quasi-standard then the $n$-arrow frame $(W,\equiv_{ij})$ is
normal.
\end{monlemme}
%
Let ${\underline W}=(W,\equiv_{ij},\not\equiv_{ii})$ be a general $n$-arrow
frame. A {\em valuation} on ${\underline W}$ is a mapping which assigns a
subset of $W$ to every atomic formula. A {\em ($\not=$-standard,
quasi-standard) general $n$-arrow model} is a structure of the form ${\cal
M}=(W,\equiv_{ij},\not\equiv_{ii},m)$ where ${\underline W}=(W,\equiv_{ij},
\not\equiv_{ii})$ is a ($\not=$-standard, quasi-standard) general $n$-arrow
frame and $m$ is a valuation on ${\underline W}$. The satisfiability relation
in ${\cal M}$ between a formula $A$ and a possible world $u\in W$ is defined
in the following way:
%
\begin{itemize}
   \item $u\models_{{\cal M}}A$ iff $u\in m(A)$, $A$ atomic formula,
   \item $u\models_{{\cal M}}\neg A$ iff $u\not\models_{{\cal M}}A$,
   \item $u\models_{{\cal M}}A\wedge B$ iff $u\models_{{\cal M}}A$
         and $u\models_{{\cal M}}B$,
   \item for every $i,j\in(n)$, $u\models_{{\cal M}}[\equiv_{ij}]A$ iff,
         for every possible world $v\in W$, $u\equiv_{ij}v$ only if
         $v\models_{{\cal M}}A$,
   \item for every $i\in(n)$, $u\models_{{\cal M}}[\not\equiv_{ii}]A$ iff,
         for every possible world $v\in W$, $u\not\equiv_{ii}v$ only if
         $v\models_{{\cal M}}A$.
\end{itemize}
%
If ${\cal M}$ is $\not=$-standard then:
%
\begin{monlemme}
For every formula $A$ and for every possible world $u\in W$:
%
\begin{itemize}
   \item $u\models_{{\cal M}}[\not=]A$ iff,
         for every possible world $v\in W$, $u\not=v$ only if
         $v\models_{{\cal M}}A$,
   \item $u\models_{{\cal M}}[U]A$ iff,
         for every possible world $v\in W$, $v\models_{{\cal M}}A$.
\end{itemize}
%
\end{monlemme}
%
A formula is {\em valid} in a general $n$-arrow model when it is
satisfied in every possible world of this model. A schema is {\em valid} in
a general $n$-arrow frame if every instance of the schema is valid in
every model on this frame. A schema is {\em valid} in a class of
general $n$-arrow frames if it is valid in every frame of this class.
Let $\Sigma$ and $\Sigma'$ be two classes of general $n$-arrow frames.
$\Sigma$ is {\em modally definable} in $\Sigma'$ by a schema $A$ if, for
every frame ${\underline W}\in\Sigma'$, $A$ is valid in ${\underline W}$
iff ${\underline W}\in\Sigma$.
%
\begin{monlemme}
The quasi-standard $n$-arrow frames are modally definable
in the class of all $\not=$-standard $n$-arrow frames by the conjunction
of the following schemata:
%
\begin{itemize}
   \item for every $i\in(n)$, $[\equiv_{ii}]A\wedge[\not\equiv_{ii}]A
         \rightarrow[U]A$,
   \item for every $i\in(n)$, $<\equiv_{ii}>[\not=]A
         \rightarrow[\not\equiv_{ii}]A$.
\end{itemize}
%
\end{monlemme}
%
\subsection{Axiomatics}
%
Together with the classical tautologies, all the instances of the following
schemata are axioms of $BAL_{n}$:
%
\begin{itemize}
   \item for every $i,j\in(n)$,
         $[\equiv_{ij}](A\rightarrow B)\rightarrow([\equiv_{ij}]A
         \rightarrow[\equiv_{ij}]B)$,
   \item for every $i\in(n)$,
         $[\not\equiv_{ii}](A\rightarrow B)\rightarrow([\not\equiv_{ii}]A
         \rightarrow[\not\equiv_{ii}]B)$,
   \item $A\rightarrow[\not=]<\not=>A$,
   \item $[U]A\rightarrow[\not=][\not=]A$,
   \item for every $i,j\in(n)$, $[U]A\rightarrow[\equiv_{ij}]A$,
   \item for every $i\in(n)$,
         $[\equiv_{ii}]A\wedge[\not\equiv_{ii}]A\rightarrow[U]A$,
   \item for every $i\in(n)$,
         $<\equiv_{ii}>[\not=]A\rightarrow[\not\equiv_{ii}]A$,
   \item for every $i\in(n)$, $[\equiv_{ii}]A\rightarrow A$,
   \item for every $i,j\in(n)$, $A\rightarrow[\equiv_{ij}]<\equiv_{ji}>A$,
   \item for every $i,j,k\in(n)$,
         $[\equiv_{ik}]A\rightarrow[\equiv_{ij}][\equiv_{jk}]A$.
\end{itemize}
%
Together with the {\em modus ponens}, the following schemata are inference
rules of $BAL_{n}$:
%
\begin{itemize}
   \item for every $i,j\in(n)$, the $[\equiv_{ij}]$-necessitation rule is:
         if $\vdash_{BAL_{n}}A$ then $\vdash_{BAL_{n}}[\equiv_{ij}]A$,
   \item for every $i\in(n)$, the $[\not\equiv_{ii}]$-necessitation rule is:
         if $\vdash_{BAL_{n}}A$ then $\vdash_{BAL_{n}}[\not\equiv_{ii}]A$,
   \item the irreflexivity rule is: if $B$ is an atomic formula not in $A$
         and $\vdash_{BAL_{n}} ([\not=]B\rightarrow B)\vee A$ then
         $\vdash_{BAL_{n}}A$.
\end{itemize}
%
\begin{montheoreme}
The theorems of $BAL_{n}$ are valid in every quasi-standard $n$-arrow model.
\end{montheoreme}
%
The $\not=$-standard $n$-arrow frames are not modally definable in
the class of all general $n$-arrow frames. Nevertheless, $\not=$-standard
$n$-arrow frames can be characterized by an inference rule: the irreflexivity
rule. The irreflexivity rule have been introduced by Gabbay \cite{Gabbay} and
studied by de Rijke \cite{deRijke}. Usually, the axiomatization of modal logic
does not contain any rule of this kind \cite{HughesCresswell}.
If the accessibility relation associated to a modal operator is required to be
irreflexive then the irreflexivity rule makes the completeness proof easier.
%
\subsection{Completeness}
%
This section is devoted to the proof of the completeness of $BAL_{n}$
for the class of all quasi-standard $n$-arrow models.
A formula $A$ is {\em consistent} when $\not\vdash_{BAL_{n}}\neg A$. A finite
set $\{A_{1},\ldots,A_{n}\}$ of formulas is {\em consistent} when the formula
$A_{1}\wedge\ldots\wedge A_{n}$ is consistent. An infinite set of formulas is
{\em consistent} when every of its finite subset is consistent. A set of
formulas is {\em maximal} when, for every formula $A$, either $A$ or $\neg A$
belongs to the set. A set of formulas is a {\em $\not=$-theory} if there
exists an atomic formula $B$ such that the formula $\neg([\not=]B\rightarrow
B)$ belongs to the set. Complicated calculations would lead to the conclusion
that every consistent set of formulas is a subset of a maximal consistent
$\not=$-theory (see \cite{BaFaTiVa} for details). Let $W$ be the set of all
the maximal consistent
$\not=$-theories. For every $i,j\in(n)$, let $\equiv_{ij}$ be the binary
relation on $W$ defined by $\Gamma\equiv_{ij}\Delta$ iff $\{A$: $[\equiv
_{ij}]A\in\Gamma\}\subseteq\Delta$. Direct calculations would lead to the
conclusion that, for every $i,j,k\in(n)$:
%
\begin{itemize}
   \item for every $\Gamma\in W$, $\Gamma\equiv_{ii}\Gamma$,
   \item for every $\Gamma,\Delta\in W$, $\Gamma\equiv_{ij}\Delta$ only if
         $\Delta\equiv_{ji}\Gamma$,
   \item for every $\Gamma,\Delta,\Phi\in W$, $\Gamma\equiv_{ij}\Delta$ and
         $\Delta\equiv_{jk}\Phi$ only if $\Gamma\equiv_{ik}\Phi$.
\end{itemize}
%
Consequently, $(W,\equiv_{ij})$ is a $n$-arrow frame. For every $i\in(n)$,
let $\not\equiv_{ii}$ be the binary relation on $W$ defined by $\Gamma\not
\equiv_{ii}\Delta$ iff $\{A$: $[\not\equiv_{ii}]A\in\Gamma\}\subseteq\Delta$.
The following three lemmas imply that, for every $\Gamma,\Delta,\Phi\in W$ and
for every sequence $(R_{1},\ldots,R_{k}),(S_{1},\ldots,S_{l})$ of elements of
$\{\equiv_{ij},\not\equiv_{ii}\}$, if $\Gamma R_{1}\circ\ldots\circ
R_{k}\Delta$ and $\Gamma S_{1}\circ\ldots\circ S_{l}\Phi$ then either
$\Delta=\Phi$ or there exists $m\in(n)$ such that $\Delta\not\equiv_{mm}\Phi$.
%
\begin{monlemme}
For every $\Gamma,\Delta,\Phi\in W$ and for every $i,j\in(n)$, if $\Gamma
\not\equiv_{ii}\Delta\not\equiv_{jj}\Phi$ then either $\Gamma=\Phi$ or there
exists $k\in(n)$ such that $\Gamma\not\equiv_{kk}\Phi$.
\end{monlemme}
%
\begin{monlemme}
For every $\Gamma,\Delta\in W$ and for every $i,j\in(n)$, if $\Gamma
\equiv_{ij}\Delta$ then either $\Gamma=\Delta$ or there exists $k\in(n)$
such that $\Gamma\not\equiv_{kk}\Delta$.
\end{monlemme}
%
\begin{monlemme}
For every $\Gamma,\Delta\in W$ and for every $i\in(n)$, if $\Gamma\not
\equiv_{ii}\Delta$ then there exists $j\in(n)$ such that $\Delta\not\equiv
_{jj}\Gamma$.
\end{monlemme}
%
Let ${\underline W}=(W,\equiv_{ij},\not\equiv_{ii})$. Let $m$ be the
valuation on ${\underline W}$ defined by $m(A)=\{\Gamma$: $\Gamma\in W$
and $A\in\Gamma\}$, $A$ atomic formula. Let ${\cal M}=({\underline W},m)$.
Direct
calculations would lead to the conclusion that, for every $\Gamma\in W$ and
for every formula $A$, $\Gamma\models_{{\cal M}}A$ iff $A\in\Gamma$.
${\cal M}$ is the {\em canonical model} of $BAL_{n}$.
Let $A$ be a consistent formula. There exists $\Gamma\in W$ such that $A\in
\Gamma$ and $\Gamma\models_{{\cal M}}A$. Let $W^{\circ}=\{\Delta$: $\Delta
\in W$ and there exists a sequence $(R_{1},\ldots,R_{k})$ of elements of
$\{\equiv_{ij},\not\equiv_{ii}\}$ such that $\Gamma R_{1}\circ\ldots\circ
R_{k}\Delta\}$. Let $\equiv_{ij}^{\circ},\not\equiv_{ii}^{\circ}$ be the
restrictions of $\equiv_{ij},\not\equiv_{ii}$ to $W^{\circ}$. Direct
calculations would lead to the conclusion that ${\underline W}^{\circ}=
(W^{\circ},\equiv_{ij}^{\circ},\not\equiv_{ii}^{\circ})$ is a general
$n$-arrow frame. Let $m^{\circ}$ be the restriction of $m$ to $W^{\circ}$.
Let ${\cal M}^{\circ}=({\underline W}^{\circ},m^{\circ})$. Direct
calculations would lead to the conclusion that $\Gamma\models_{{\cal
M}^{\circ}}A$. Moreover, for every $\Delta,\Phi\in W^{\circ}$, either
$\Delta=\Phi$ or there exists $i\in(n)$ such that $\Delta\not\equiv_{ii}\Phi$.
Let $\Delta\in W^{\circ}$. Since $\Delta$ is a $\not=$-theory, then there
exists an atomic formula $B$ such that $\neg([\not=]B\rightarrow B)\in\Delta$.
Therefore, $[\not=]B,\neg B\in\Delta$. Consequently, for every $\Phi\in
W^{\circ}$, if there exists $i\in(n)$ such that $\Delta\not\equiv_{ii}\Phi$
then $B\in\Phi$, $\neg B\not\in\Phi$ and $\Delta\not=\Phi$. Therefore, for
every $\Delta,\Phi\in W^{\circ}$, $\Delta\not=\Phi$ iff there exists $i
\in(n)$ such that $\Delta\not\equiv_{ii}\Phi$. Consequently,
${\underline W}^{\circ}$ is $\not=$-standard. Let it be proved that, for
every $\Delta,\Phi\in W^{\circ}$ and for every $i\in(n)$, either $\Delta
\equiv_{ii}\Phi$ or $\Delta\not\equiv_{ii}\Phi$. If neither $\Delta
\equiv_{ii}\Phi$ nor $\Delta\not\equiv_{ii}\Phi$ then there exists a formula
$[\equiv_{ii}]A\in\Delta$ such that $A\not\in\Phi$ and there exists a formula
$[\not\equiv_{ii}]B\in\Delta$ such that $B\not\in\Phi$. Consequently,
$[\equiv_{ii}](A\vee B)\wedge[\not\equiv_{ii}](A\vee B)\in\Delta$ and
$\neg(A\vee B)\in\Phi$. Therefore, $[U](A\vee B)\in\Delta$ and $A\vee B\in\Phi$,
a contradiction. Similarly, direct calculations would lead to the conclusion
that, for every $\Delta,\Phi\in W^{\circ}$ and for every $i\in(n)$, either
$\neg\Delta\equiv_{ii}\Phi$ or $\neg\Delta\not\equiv_{ii}\Phi$. Consequently,
${\underline W}^{\circ}$ is quasi-standard. Therefore:
%
\begin{montheoreme}
$BAL_{n}$ is complete for the class of all quasi-standard $n$-arrow
models, that is to say: the formulas valid in every quasi-standard
$n$-arrow model are theorems of $BAL_{n}$.
\end{montheoreme}
%
%
\section{Collinearity}
%
Let $n=3$. Collinearity is one of the basic ternary relations between the
points of a geometrical structure.
%
\subsection{Structures of collinearity}
%
A {\em structure of collinearity} is a point $3$-frame ${\underline
S}=(P,C)$ such that:
%
\begin{itemize}
   \item for every $X,Y\in P$, $C(X,Y,X)$,
   \item for every $X,Y,Z\in P$, $C(X,Y,Z)$ only if $C(Y,X,Z)$,
   \item for every $X,Y,Z,T\in P$, $C(X,Y,Z)$ and $C(X,Y,T)$ only if
         $X=Y$ or $C(X,Z,T)$.
\end{itemize}
%
The class of all structures of collinearity is denoted by $\Sigma_{3}^{C}$.
The elements of $P$ are called {\em points} and are denoted by capital letters.
$C$ is the relation of {\em collinearity} between the points of the relational
structure.
%
\begin{monexemple}
The affine geometries axiomatized by Szczerba and Tarski \cite{SzczerbaTarski}
are structures of collinearity.
\end{monexemple}
%
\subsection{Frames of collinearity}
%
A {\em frame of collinearity} is a $3$-arrow frame ${\underline W}=
(W,\equiv_{ij})$ such that, for every $i,j,k,l\in(3)$:
%
\begin{itemize}
   \item for every $x,y\in W$, there exists $u\in W$ such that
         $x\equiv_{i1}u$, $y\equiv_{j2}u$ and $x\equiv_{i3}u$,
   \item for every $x,y,z\in W$, there exists $u\in W$ such that
         $x\equiv_{i1}u$, $y\equiv_{j2}u$ and $z\equiv_{k3}u$ only if
         there exists $v\in W$ such that $y\equiv_{j1}v$, $x\equiv_{i2}v$
         and $z\equiv_{k3}v$,
   \item for every $x,y,z,t\in W$, there exists $u\in W$ such that
         $x\equiv_{i1}u$, $y\equiv_{j2}u$ and $z\equiv_{k3}u$ and
         there exists $v\in W$ such that
         $x\equiv_{i1}v$, $y\equiv_{j2}v$ and $t\equiv_{l3}v$ only if either
         $x\equiv_{ij}y$ or there exists $w\in W$ such that
         $x\equiv_{i1}w$, $z\equiv_{k2}w$ and $t\equiv_{l3}w$.
\end{itemize}
%
The class of all normal frames of collinearity is denoted by $\Phi_{3}^{C}$.
%
\subsection{Structures and frames of collinearity}
%
Direct calculations would lead to the conclusion that:
%
\begin{monlemme}
Let ${\underline S}$ be a structure of collinearity. Then $W({\underline S})$
is a normal frame of collinearity.
\end{monlemme}
%
\begin{monlemme}
Let ${\underline W}$ be a normal frame of collinearity. Then $S({\underline
W})$ is a structure of collinearity.
\end{monlemme}
%
Therefore:
%
\begin{montheoreme}
The categories $\Sigma_{3}^{C}$ and $\Phi_{3}^{C}$ are equivalent.
\end{montheoreme}
%
\subsection{Modal logic of collinearity}
%
This section introduces a modal logic with standard semantics in the class
of all normal frames of collinearity.
A {\em general frame of collinearity} consists of a non-empty set $W$
together with, for every $i,j\in(3)$, a binary relation $\equiv_{ij}$ on
$W$ such that $(W,\equiv_{ij})$ is a frame of collinearity and, for every
$i\in(3)$, a binary relation $\not\equiv_{ii}$ on $W$.
%
\begin{monlemme}
The quasi-standard frames of collinearity are modally definable
in the class of all quasi-standard $3$-arrow frames by the conjunction of
the following schemata:
%
\begin{itemize}
   \item for every $i,j\in(3)$, $<U>A\wedge B\rightarrow<\equiv_{i1}>
         (<\equiv_{2j}>A\wedge<\equiv_{3i}>B)$,
   \item for every $i,j,k\in(3)$, $<\equiv_{i1}>
         (<\equiv_{2j}>A\wedge<\equiv_{3k}>B)\rightarrow$
         \\
         $<\equiv_{i2}>(<\equiv_{1j}>A\wedge<\equiv_{3k}>B)$,
   \item for every $i,j,k,l\in(3)$, $<\equiv_{i1}>(<\equiv_{2j}>(A\wedge$
         \\
         $<\equiv_{j2}>(<\equiv_{1i}>B\wedge<\equiv_{3k}>C))\wedge
         <\equiv_{3l}>D)$
         \\
         $\rightarrow<\equiv_{ij}>A\vee<\not=>B\vee
         <\equiv_{i1}>(<\equiv_{2k}>C\wedge<\equiv_{3l}>D)$.
\end{itemize}
%
\end{monlemme}
%
Together with the axioms of $BAL_{3}$, all the instances of the previous
schemata are axioms of $BAL_{3}^{C}$.
%
\begin{montheoreme}
$BAL_{3}^{C}$ is complete for the class of all quasi-standard models of
collinearity.
\end{montheoreme}
%
%
\section{Sorted point $n$-frames and sorted $n$-arrow frames}
%
Let $n\ge 2$. This section is devoted to the proof of the categorial
equivalence between sorted point $n$-frames and sorted $n$-arrow frames.
%
\subsection{Sorted point $n$-frames}
%
A {\em sorted point $n$-frame} consists, for every $i\in(n)$, of a non-empty
set $S_{i}$ together with, for every $i,j\in(n)$ such that $i\not=j$, a binary
relation $R_{ij}$ between $S_{i}$ and $S_{j}$ such that:
%
\begin{itemize}
   \item for every $i,j\in(n)$ such that $i\not=j$ and for every $X\in S_{i}$,
         there exists $Y\in S_{j}$ such that $X$ $R_{ij}$ $Y$,
   \item for every $i,j\in(n)$ such that $i\not=j$ and for every $X\in S_{i},
         Y\in S_{j}$, if $X$ $R_{ij}$ $Y$ then there exists $Z_{1}
         \in S_{1},\ldots,Z_{n}\in S_{n}$ such that $X=Z_{i}$, $Y=Z_{j}$
         and, for every $k,l\in(n)$ such that $k\not=l$, $X_{k}$ $R_{kl}$
         $X_{l}$.
\end{itemize}
%
\begin{monlemme}
For every $i,j\in(n)$ such that $i\not=j$ and for every $X\in S_{i},Y\in
S_{j}$, if $X$ $R_{ij}$ $Y$ then $Y$ $R_{ji}$ $X$.
\end{monlemme}
%
The class of all sorted point $n$-frames is denoted by $\Sigma^{n}$ and is
considered as a category with morphisms the usual homomorphisms between
relational structures.
%
\subsection{Sorted $n$-arrow frames}
%
The $n$-arrow frame ${\underline W}=(W,\equiv_{ij})$ is {\em sorted} if:
%
\begin{itemize}
   \item for every $u_{1},\ldots,u_{n}\in W$, if, for every $i,j\in(n)$ such
         that $i\not=j$, $u_{i}\equiv_{ii}\circ\equiv_{jj}u_{j}$ then there
         exists $u\in W$ such that, for every $i\in(n)$, $u_{i}\equiv_{ii}u$.
\end{itemize}
%
The class of all normal sorted $n$-arrow frames is denoted by $\Phi^{n}$.
%
\subsection{From sorted point $n$-frames to sorted $n$-arrow frames}
%
Let ${\underline S}=(S_{i},R_{ij})$ be a sorted point $n$-frame. Let
$W=\{(X_{1},\ldots,X_{n})$: $X_{1}\in S_{1},\ldots,X_{n}\in S_{n}$ and, for
every $i,j\in(n)$ such that $i\not=j$, $X_{i}$ $R_{ij}$ $X_{j}\}$. For every
$i,j\in(n)$, let $\equiv_{ij}$ be the binary relation on $W$ defined by
$(X_{1},\ldots,X_{n})\equiv_{ij}(Y_{1},\ldots,Y_{n})$ iff $X_{i}=Y_{j}$.
%
\begin{monlemme}
$W({\underline S})=(W,\equiv_{ij})$ is a normal sorted $n$-arrow frame.
\end{monlemme}
%
\begin{monexemple}
It can be proved, for every $i,j\in(n)$ such that $i\not=j$, that if $S_{i}
\cap S_{j}=\emptyset$ then $\equiv_{ij}=\emptyset$ and that if $S_{i}\subseteq
S_{j}$ then $\equiv_{ij}$ is serial.
\end{monexemple}
%
\subsection{From sorted $n$-arrow frames to sorted point $n$-frames}
%
Let ${\underline W}=(W,\equiv_{ij})$ be a normal sorted $n$-arrow frame.
For every $i\in(n)$, let $S_{i}=\{i(u)$: $u\in W\}$. For
every $i,j\in(n)$ such that $i\not=j$, let $R_{ij}$ be the binary relation
between $S_{i}$ and $S_{j}$ defined by $i(u)$ $R_{ij}$ $j(v)$ iff $u\equiv
_{ii}\circ\equiv_{jj}v$. Direct calculations would lead to the conclusion
that:
%
\begin{monlemme}
$S({\underline W})=(S_{i},R_{ij})$ is a sorted point $n$-frame.
\end{monlemme}
%
\begin{monexemple}
It can be proved, for every $i,j\in(n)$ such that $i\not=j$, that if
$\equiv_{ij}=\emptyset$ then $S_{i}\cap S_{j}=\emptyset$ and that if
$\equiv_{ij}$ is serial then $S_{i}\subseteq S_{j}$.
\end{monexemple}
%
%
\subsection{Representation theorems}
%
Let ${\underline W}=(W,\equiv_{ij})$ be a normal sorted $n$-arrow frame and
${\underline W}'=W(S({\underline W}))$. For every $u\in W$, let $g(u)=(1(u),
\ldots,n(u))$. Direct calculations would lead to the conclusion that $g$ is
an isomorphism from ${\underline W}$ into ${\underline
W}'$. Therefore:
%
\begin{monlemme}
${\underline W}$ and ${\underline W}'$ are isomorphic.
\end{monlemme}
%
Let ${\underline S}=(S_{i},R_{ij})$ be a sorted point $n$-frame and
${\underline S}'=S(W({\underline S}))$. For every $X\in S_{i}$, let
$f(X)=\{(X_{1},\ldots,X_{n})$: $X_{1}\in S_{1},\ldots,X_{n}\in S_{n}$,
$X=X_{i}$ and, for every $j,k\in(n)$ such that $j\not=k$, $X_{j}$ $R_{jk}$
$X_{k}\}$. Direct calculations would lead to the conclusion that $f$ is an
isomorphism from ${\underline S}$ into ${\underline S}'$. Consequently:
%
\begin{monlemme}
${\underline S}$ and ${\underline S}'$ are isomorphic.
\end{monlemme}
%
Therefore:
%
\begin{montheoreme}
The categories $\Sigma^{n}$ and $\Phi^{n}$ are equivalent.
\end{montheoreme}
%
%
\section{Sorted arrow logic}
%
This section introduces a modal logic with standard semantics in the class
of all normal sorted $n$-arrow frames.
%
\subsection{Semantics}
%
Let $A_{1},\ldots,A_{n}$ be formulas. Let $B_{1}=true$ and, for every $k
\ge 1$, $B_{k+1}=$ $<\equiv_{(k+1)(k+1)}><\equiv_{kk}>([\not=]A_{k}\wedge
B_{k})\wedge\bigwedge_{i\in(k)}<\equiv_{(k+1)(k+1)}><\equiv_{ii}>\neg A_{i}$.
Let ${\cal M}=(W,\equiv_{ij},\not\equiv_{ii},m)$ be a quasi-standard
$n$-arrow model. Direct calculations would lead to the conclusion that, for
every $k\in(n)$ and for every $x\in W$, $x\models_{{\cal M}}B_{k}$ iff there
exists $x_{1},\ldots,x_{k}\in W$ such that $x_{k}=x$, $x_{i}\models_{{\cal
M}}[\not=]A_{i}\wedge B_{i}$, for every $i\in(k-1)$ and $x_{i}\equiv_{ii}\circ
\equiv_{jj}x_{j}$, for every $i,j\in(k)$ such that $i\not=j$. Consequently:
%
\begin{monlemme}
The quasi-standard sorted $n$-arrow frames are modally definable in the class
of all quasi-standard $n$-arrow frames by the following schema:
%
\begin{itemize}
   \item $C_{n}=B_{n}\rightarrow<\equiv_{nn}>\bigwedge_{i\in(n-1)}
         <\equiv_{ii}>\neg A_{i}$.
\end{itemize}
%
\end{monlemme}
%
\begin{monexemple}
$B_{2}$ is logically equivalent to the schema $<\equiv_{22}><\equiv_{11}>
[\not=]A_{1}\wedge<\equiv_{22}><\equiv_{11}>\neg A_{1}$. The schema $B_{3}$
is equivalent to $<\equiv_{33}><\equiv_{22}>([\not=]A_{2}\wedge B_{2})\wedge
<\equiv_{33}><\equiv_{11}>\neg A_{1}$ $\wedge<\equiv_{33}><\equiv_{22}>
\neg A_{2}$.
\end{monexemple}
%
Together with the axioms of $BAL_{n}$, all the instances of the previous
schema are axioms of $BAL^{n}$.
%
\begin{montheoreme}
$BAL^{n}$ is complete for the class of all quasi-standard sorted $n$-arrow
models.
\end{montheoreme}
%
%
\section{Geometrical sorted point $n$-frames}
%
Projective structures and orthogonal structures are examples of sorted point
$n$-frames.
%
\subsection{Projective geometry}
%
Incidence is one of the basic binary relations between the points and the
lines of a geometrical structure.
%
\subsubsection{Projective structures}
%
A {\em projective structure} is a relational structure
${\underline S}=(P,L,in)$ such that:
%
\begin{itemize}
   \item $P\cap L=\emptyset$,
   \item for every $X,Y\in P$, there exists $x\in L$ such that
         $X$ $in$ $x$ and $Y$ $in$ $x$,
   \item for every $x,y\in L$, there exists $X\in P$ such that
         $X$ $in$ $x$ and $X$ $in$ $y$,
   \item for every $X,Y\in P$ and for every $x,y\in L$,
         $X$ $in$ $x$, $Y$ $in$ $x$, $X$ $in$ $y$ and
         $Y$ $in$ $y$ only if $X=Y$ or $x=y$.
\end{itemize}
%
The elements of $L$ are called {\em lines} and are denoted by
lower case letters. $in$ is the relation of incidence between the
points and the lines of the relational structure. The class of all
projective structures is denoted by $\Sigma^{2}_{P}$.
%
\begin{monexemple}
The projective geometries axiomatized by Heyting \cite{Heyting} are
projective structures.
\end{monexemple}
%
A projective structure $(P,L,in)$ is considered as
a sorted point $2$-frame $(S_{1},S_{2},R_{12},R_{21})$ where $S_{1}=P$,
$S_{2}=L$, $R_{12}=in$ and $R_{21}=in^{-1}$.
%
\subsubsection{Projective frames}
%
A {\em projective frame} is a sorted $2$-arrow frame ${\underline W}=
(W,\equiv_{ij})$ such that:
%
\begin{itemize}
   \item $\equiv_{12}=\emptyset$,
   \item for every $x,y\in W$, $x\equiv_{11}\circ\equiv_{22}\circ\equiv_{11}y$,
   \item for every $x,y\in W$, $x\equiv_{22}\circ\equiv_{11}\circ\equiv_{22}y$,
   \item for every $x,y,z,t\in W$, $x\equiv_{11}\circ\equiv_{22}z$,
         $y\equiv_{11}\circ\equiv_{22}z$, $x\equiv_{11}\circ\equiv_{22}t$ and
         $y\equiv_{11}\circ\equiv_{22}t$ only if $x\equiv_{11}y$ or $z
         \equiv_{22}t$.
\end{itemize}
%
The class of all normal projective frames is denoted by $\Phi^{2}_{P}$.
%
\subsubsection{Projective structures and projective frames}
%
Direct calculations would lead to the conclusion that:
%
\begin{monlemme}
Let ${\underline S}$ be a projective structure. Then $W({\underline S})$
is a normal projective frame.
\end{monlemme}
%
\begin{monlemme}
Let ${\underline W}$ be a normal projective frame. Then $S({\underline W})$
is a projective structure.
\end{monlemme}
%
Therefore:
%
\begin{montheoreme}
The categories $\Sigma^{2}_{P}$ and $\Phi^{2}_{P}$ are equivalent.
\end{montheoreme}
%
\subsubsection{Projective modal logic}
%
This section introduces a modal logic with standard semantics in the class
of all normal projective frames. A {\em general projective frame} consists of
a non-empty set $W$ together with, for every $i,j\in(2)$, a binary relation
$\equiv_{ij}$ on $W$ such that $(W,\equiv_{ij})$ is a projective frame and,
for every $i\in(2)$, a binary relation $\not\equiv_{ii}$ on $W$.
%
\begin{monlemme}
The quasi-standard projective frames are modally definable in the
class of all quasi-standard sorted $2$-arrow frames by the conjunction of the
following schemata:
%
\begin{itemize}
   \item $[\equiv_{12}]false$,
   \item $[\equiv_{11}][\equiv_{22}][\equiv_{11}]A\rightarrow[U]A$,
   \item $[\equiv_{22}][\equiv_{11}][\equiv_{22}]A\rightarrow[U]A$,
   \item $<\equiv_{11}><\equiv_{22}>(A\wedge<\equiv_{22}><\equiv_{11}>
         ([\not=]B\wedge C))\rightarrow$
         \\
         $[\equiv_{11}][\equiv_{22}](<\equiv_{22}>A\vee
         [\equiv_{22}][\equiv_{11}]B)\vee<\equiv_{11}>C$.
\end{itemize}
%
\end{monlemme}
%
Together with the axioms of $BAL^{2}$, all the instances of the previous
schemata are axioms of $BAL^{2}_{P}$.
%
\begin{montheoreme}
$BAL^{2}_{P}$ is complete for the class of all quasi-standard projective
models.
\end{montheoreme}
%
\subsection{Orthogonal geometry}
%
Orthogonality is one of the basic binary relations between the lines of a
geometrical structure.
%
\subsubsection{Orthogonal structures}
%
An {\em orthogonal structure} is a relational structure
${\underline S}=(P,L,in,\perp)$ such that:
%
\begin{itemize}
   \item $P\cap L=\emptyset$,
   \item for every $X,Y\in P$, there exists $x\in L$ such that
         $X$ $in$ $x$ and $Y$ $in$ $x$,
   \item for every $X,Y\in P$ and for every $x,y\in L$,
         $X$ $in$ $x$, $Y$ $in$ $x$, $X$ $in$ $y$ and
         $Y$ $in$ $y$ only if $X=Y$ or $x=y$,
   \item for every $X\in P$ and for every $x\in L$, there exists $y\in L$
         such that $X$ $in$ $y$ and $x\perp y$,
   \item for every $X\in P$ and for every $x,y,z\in L$,
         $X$ $in$ $y$, $x\perp y$, $X$ $in$ $z$ and
         $x\perp z$ only if $y=z$,
   \item for every $x,y\in L$, $x\perp y$ only if $y\perp x$.
\end{itemize}
%
$\perp$ is the relation of orthogonality between the lines of the
relational structure. The class of all orthogonal structures is denoted by
$\Sigma^{3}_{O}$.
%
\begin{monexemple}
The orthogonal geometries axiomatized by Goldblatt \cite{Goldblatt} are
orthogonal structures.
\end{monexemple}
%
An orthogonal structure $(P,L,in,\perp)$ is considered as a sorted point
$3$-frame $(S_{1},S_{2},S_{3},R_{12},R_{13},R_{21},R_{23},R_{31},R_{32})$
where $S_{1}=P$, $S_{2}=L$, $S_{3}=L$, $R_{12}=in$, $R_{13}=in$,
$R_{21}=in^{-1}$, $R_{23}=\perp$, $R_{31}=in^{-1}$ and $R_{32}=\perp^{-1}$.
%
\subsubsection{Orthogonal frames}
%
An {\em orthogonal frame} is a sorted $3$-arrow frame ${\underline W}=
(W,\equiv_{ij})$ such that, for every $i,j,k\in\{2,3\}$:
%
\begin{itemize}
   \item $\equiv_{12}=\emptyset$,
   \item $\equiv_{23}$ is serial,
   \item $\equiv_{32}$ is serial,
   \item for every $x,y\in W$, $x\equiv_{11}\circ\equiv_{23}y$ iff
         $x\equiv_{11}\circ\equiv_{33}y$,
   \item for every $x,y\in W$, $x\equiv_{11}\circ\equiv_{32}y$ iff
         $x\equiv_{11}\circ\equiv_{22}y$,
   \item for every $x,y\in W$, $x\equiv_{11}\circ\equiv_{ij}\circ\equiv_{11}y$,
   \item for every $x,y,z,t\in W$, $x\equiv_{11}\circ\equiv_{ii}z$,
         $y\equiv_{11}\circ\equiv_{ii}z$, $x\equiv_{11}\circ\equiv_{jj}t$ and
         $y\equiv_{11}\circ\equiv_{jj}t$ only if $x\equiv_{11}y$ or $z
         \equiv_{ij}t$,
   \item for every $x,y\in W$, $x\equiv_{11}\circ\equiv_{i2}\circ
         \equiv_{3j}y$,
   \item for every $x,y,z,t\in W$, $x\equiv_{11}\circ\equiv_{jj}z$,
         $y\equiv_{i2}\circ\equiv_{3j}z$, $x\equiv_{11}\circ\equiv_{kk}t$ and
         $y\equiv_{i2}\circ\equiv_{3k}t$ only if $z\equiv_{jk}t$,
   \item for every $x,y\in W$, $x\equiv_{i2}\circ\equiv_{3j}y$ only if
         $x\equiv_{i3}\circ\equiv_{2j}y$.
\end{itemize}
%
The class of all normal orthogonal frames is denoted by $\Phi^{3}_{O}$.
%
\subsubsection{Orthogonal structures and orthogonal frames}
%
Direct calculations would lead to the conclusion that:
%
\begin{monlemme}
Let ${\underline S}$ be an orthogonal structure. Then $W({\underline S})$
is a normal orthogonal frame.
\end{monlemme}
%
\begin{monlemme}
Let ${\underline W}$ be a normal orthogonal frame. Then $S({\underline W})$
is an orthogonal structure.
\end{monlemme}
%
Therefore:
%
\begin{montheoreme}
The categories $\Sigma^{3}_{O}$ and $\Phi^{3}_{O}$ are equivalent.
\end{montheoreme}
%
\subsubsection{Orthogonal modal logic}
%
A {\em general orthogonal frame} consists of a non-empty set $W$ together
with, for every $i,j\in\{1,2,3\}$, a binary relation $\equiv_{ij}$ on $W$
such that $(W,\equiv_{ij})$ is an orthogonal frame and, for every $i\in(3)$,
a binary relation $\not\equiv_{ii}$ on $W$.
%
\begin{monlemme}
The quasi-standard orthogonal frames are modally definable in the
class of all quasi-standard sorted $3$-arrow frames by the conjunction of the
following schemata:
%
\begin{itemize}
   \item $[\equiv_{12}]false$,
   \item $<\equiv_{23}>true$,
   \item $<\equiv_{32}>true$,
   \item $[\equiv_{11}][\equiv_{33}]A\leftrightarrow
         [\equiv_{11}][\equiv_{23}]A$,
   \item $[\equiv_{11}][\equiv_{22}]A\leftrightarrow
         [\equiv_{11}][\equiv_{32}]A$,
   \item $[\equiv_{11}][\equiv_{ij}][\equiv_{11}]A\rightarrow[U]A$,
   \item $<\equiv_{11}><\equiv_{ii}>(A\wedge<\equiv_{ii}><\equiv_{11}>
         ([\not=]B\wedge C))\rightarrow[\equiv_{11}][\equiv_{jj}]
         (<\equiv_{ji}>A\vee[\equiv_{jj}][\equiv_{11}]B)\vee<\equiv_{11}>C$,
   \item $[\equiv_{11}][\equiv_{i2}][\equiv_{3j}]A\rightarrow[U]A$,
   \item $<\equiv_{11}><\equiv_{jj}>(A\wedge<\equiv_{j3}><\equiv_{2i}>
         [\not=]B)\rightarrow[\equiv_{11}][\equiv_{kk}]
         (<\equiv_{kj}>A\vee[\equiv_{k3}][\equiv_{2i}]B)$,
   \item $[\equiv_{i3}][\equiv_{2j}]A\rightarrow[\equiv_{i2}][\equiv_{3j}]A$.
\end{itemize}
%
\end{monlemme}
%
Together with the axioms of $BAL^{3}$, all the instances of the previous
schemata are axioms of $BAL^{3}_{O}$:
%
\begin{montheoreme}
$BAL^{3}_{O}$ is complete for the class of all quasi-standard orthogonal
models.
\end{montheoreme}
%
%
\section{Conclusion}
%
The methodology presented in this paper for a modal treatment of structures
of collinearity, projective structures and orthogonal structures can be
applied to other geometrical structures as well:
%
\begin{itemize}
   \item Structures of betweeness consist of a set of points together with
         a ternary relation of betweeness between points \cite{SzczerbaTarski}.
   \item Projective structures of space consist of a set of points, a set of
         lines and a set of planes together with three binary relations of
         incidence between points, lines and planes.
\end{itemize}
%
However, many questions remain unsolved:
%
\begin{itemize}
   \item Proof of the completeness or the incompleteness of $BAL_{3}^{C}$,
         $BAL^{2}_{P}$ and $BAL^{3}_{O}$ without the irreflexivity rule.
   \item Proof of the decidability or the undecidability of $BAL_{3}^{C}$,
         $BAL^{2}_{P}$ and $BAL^{3}_{O}$.
\end{itemize}
%
%
\begin{thebibliography}{11}
   \bibitem{BaDuFaLo}
      {\bf P. Balbiani}, {\bf V. Dugat}, {\bf L. Fari\~{n}as del Cerro}
      and {\bf A. Lopez.}
      {\em El\'{e}ments de g\'{e}om\'{e}trie m\'{e}canique}.
      Herm\`{e}s,
      1994.
   \bibitem{BaFaTiVa}
      {\bf P. Balbiani}, {\bf L. Fari\~{n}as del Cerro}, {\bf T. Tinchev}
      and {\bf D. Vakarelov.}
      {\em Modal logics for incidence geometries}.
      Journal of Logic and Computation,
      to appear.
   \bibitem{vanBenthemTime}
      {\bf J. van Benthem.}
      {\em The Logic of Time}.
      Reidel,
      1983.
   \bibitem{Gabbay}
      {\bf D. Gabbay.}
      {\em An irreflexivity lemma with applications to axiomatizations
      of conditions on tense frames}.
      U. M\"{o}nnich (editor),
      Aspects of Philosophical Logic.
      67-89,
      Reidel,
      1981.
   \bibitem{GabHodRey}
      {\bf D. Gabbay}, {\bf I. Hodkinson} and {\bf M. Reynolds.}
      {\em  Temporal Logic: Mathematical Foundations and
      Computational Aspects}.
      Volume I,
      Oxford University Press,
      1994.
   \bibitem{Goldblatt}
      {\bf R. Goldblatt.}
      {\em Orthogonality and Spacetime Geometry}.
      Springer-Verlag,
      1987.
   \bibitem{Heyting}
      {\bf Heyting.}
      {\em Axiomatic Projective Geometries}.
      North-Holland,
      1963.
   \bibitem{Hilbert}
      {\bf D. Hilbert.}
      {\em Foundations of Geometry}.
      Second english edition,
      Open Court,
      1971.
   \bibitem{HughesCresswell}
      {\bf G. Hughes} and {\bf M. Cresswell.}
      {\em A Companion to Modal Logic}.
      Methuen,
      1984.
   \bibitem{deRijke}
      {\bf M. de Rijke.}
      {\em The modal logic of inequality}.
      Journal of Symbolic Logic,
      Volume 57,
      Number 2,
      566-584,
      1992.
   \bibitem{SzczerbaTarski}
      {\bf L. Szczerba} and {\bf A. Tarski.}
      {\em Metamathematical properties of some affine geometries}.
      Y. Bar-Hillel (editor),
      Logic, Methodology and Philosophy of Science.
      166-178,
      North-Holland,
      1972.
   \bibitem{Vakarelov1}
      {\bf D. Vakarelov.}
      {\em A modal theory of arrows. Arrow logics I}.
      D. Pearce and G. Wagner (editors),
      Logics in AI, European Workshop JELIA '92, Berlin, Germany,
      September 1992, Proceedings.
      Lecture Notes in Artificial Intelligence 633,
      1-24,
      Springer-Verlag,
      1992.
   \bibitem{Vakarelov2}
      {\bf D. Vakarelov.}
      {\em Many-dimensional arrow structures. Arrow logics II}.
      Journal of Applied Non-Classical Logics,
      to appear.
\end{thebibliography}
%
%
\end{document}



--========================_3484184==_--
