[Prev][Next][Index][Thread]
On the meaning of logical rules II
The paper "On the meaning of logical rules II : : multiplicatives and
additives"
is available at
ftp://iml.univ-mrs.fr/pub/girard/meaning1.[dvi.Z,ps.Z,ps.gz]
\begin{abstract}
El m\'etodo inicial que imagino era relativamente sencillo. Conocer
bien el espa\~nol, recuperar la fe cat\'olica, guerrear contra los
moros o contro el turco, olvidar la historia de Europa entre los
a\~nos de 1602 y de 1918, {\em ser} Miguel de Cervantes. Pierre
M\'enard estudi\'o ese procedimiento (s\'e que logr\'o un manejo
bastante fiel del espa\~nol del siglo diecisiete), pero lo descart\'o
por f\'acil. [\ldots]
Mi complaciente precursor no rehus\'o la colaboraci\'on del azar~:
iba componiendo la obra inmortal un poco {\em \`a la diable}, llevado
por inercias del lenguaje y de la invenci\'on. Yo he contra\'{\i} el
misterioso deber de reconstruir literalmente su obra espont\'anea. Mi
solitario juego est\'a gobernado por dos leyes polares. La primera me
permite ensayar variantes de tipo formal o psicol\'ogico~; la secunda
me obliga a sacrificarlas al texto \Guill{original} y a razonar de
un modo irrefutabile esa aniquilaci\'on.\\
J.-L. Borges {\em Pierre M\'enard autor del Quijote}, 1939.
\end{abstract}
The paper expounds the solution to our search for meaning
\cite{meaning1} in a particular case~: the fragment of logic built
from the neutral elements $\bot,\top$,${\bf 1},\bf 0$ by means of the
connectives $\Par,\Avec,\Tenseur,\Plus$.
\\
As explained in the previous paper and summarized in the abstract,
the task is to produce a trivial meet between syntax and semantics,
but in a non-trivial way. Typically, we cannot content ourselves with
a plain game-theoretic paraphrases of logic~; we have to deconstruct
familiar syntax and to reconstruct it in another way. But, as in the
case of M\'enard reconstructing the {\em Quijote}, the synthesis is
absolutely prior to the analysis\ldots\ in particular the
presentation analysis/synthesis that we follow is completely alien to
the very spirit of the work.
\\
We shall organize a sort of tunnel between syntax and semantics, with
a meet in between~: the analysis will replace syntax with a
game-theoretic variant, and synthesis will elaborate an abstract
notion of game, which can be specialized to our fragment and yield
exactly the analytic games.
\begin{description}
\item[Analysis] We shall modify the extant sequent calculus into a
{\em hypersequentialized} version {\bf HC}, which has internalized
the alternation positive/negative to the extent that even negative
formulas disappear\ldots\ the usual connectives being replaced with
{\em synthetic connectives}. The configurations of {\bf HC} can be
fully analyzed by means of various game-theoretic artefacts.
Moreover, {\bf HC} admits wrong logical rules ({\em
paralogisms}\footnote{To avoid misunderstandings~: the mistakes are
{\em volontary}, nothing to do with ---say--- \Guill{abduction}.}),
which are essential to prove the basic equivalences between usual
logic and the game version in {\bf HC}. These paralogisms have a
heavy price~: who uses them loses, and we end with a complete
equivalence between usual logic and {\em winning strategies} in a
sort of analytic game.
\item[Synthesis] We can, starting with the geometrical idea of
iterated division of space, build a universal game. The {\em
disputes} (i.e. the plays) of this game are equipped with a (sort of)
structure of coherent space. Then cliques in this coherent space may
be seen as {\em designs} (i.e. a very specific sort of strategy), and
when a design is {\em orthogonal} to a counterdesign, the unique
dispute they share has at most one winner. If we define a {\em
behavior} as a set of designs equal to its biorthogonal, then logical
formulas are interpreted as behaviors. Then it is a matter of care to
translate a design within a logical behavior into a paraproof of the
corresponding formula, and a winning design into a real proof. By the
way, losing corresponds to giving up or making a deliberate mistake
to annoy the enemy, what is called here a {\em dog's move}, whose
basic meaning (besides the fact that it might also make your opponent
lose) is that of an artificial obstruction~: this is the geometrical
meaning of paralogisms.
\end{description}
Eventually, the paper ends into a trivial equivalence, what was
sought\ldots\ But this quest for triviality was highly difficult~: if
the rest of the connectives is not yet available, there is a reason
for that~: there is still a lot to do before reaching a state of
highly non-trivial triviality.
---
Jean-Yves GIRARD
Directeur de Recherche
CNRS, Institut de Mathematiques de Luminy
163 Avenue de Luminy, case 907
13288 Marseille cedex 9
<girard@iml.univ-mrs.fr>
(33) (0)4 91 26 96 58
(33) (0)4 91 26 96 32 (Mme Bodin, secretariat)
(33) (0)4 91 26 96 55 (Fax)