On the meaning of logical rules II

The paper "On the meaning of logical rules II : : multiplicatives and  

is available at  


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.

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. 

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

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

(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)