
\subsection {Systèmes formels}
Pour construire une langue (par exemple le français), on a besoin de 4 choses : 
\begin{itemize}
\item   un alphabet (a, b, ..., z, blanc, virgule, parenthèse ouvrante, ...),
\item   un procédé de formation des mots, qui est la concaténation,
\item  un dictionnaire, qui permet de savoir que "chat" est français, alors que "cat"   ne l'est pas,
\item des règles de grammaire, qui permettent de savoir que "chattes" est français,   alors qu'il n'est pas dans le dictionnaire. 
\end{itemize}

\subsubsection{Définition}
Pour construire un système formel, nous aurons besoin de 4 choses analogues :
\begin{itemize}
  \item un alphabet, ensemble de symboles pas nécessairement réduit à des caratères, 
  \item un procédé de formation des expressions, pas nécessairement la concaténation, 
  \item un ensemble d'axiomes, c'est-à-dire d'expressions obéissant aux deux premiers  points ci-dessus, et dont on décide arbitrairement qu'ils appartiennent au   système, 
 \item des règles de dérivation qui, à partir des axiomes, permettent de produire des  théorèmes (c'est-à-dire des expressions appartenant au système), et peuvent  ensuite s'appliquer aux théorèmes pour en produire d'autres. 
\end{itemize}

\subsubsection { Exemple}

Considérons le système "peu" : 
 \begin{itemize}
 \item  alphabet = l'ensemble des trois symboles "p" , "e" , et "u" 
 \item   p.f.e. = concaténation 
 \item   axiome = upueuu 
 \item   règles : 
   \begin{itemize}
   \item     R1 : si une expression de la forme AeB est un théorème (où "A" désigne     n'importe quelle suite de "u", de "p", et de "e", et B de même), alors     l'expression uAeBu est aussi un théorème.
   \item     R2 : si une expression de la forme AeB est un théorème, alors l'expression  AueuB est aussi un théorème. 
     \end{itemize}
\end{itemize}

Questions : 
\begin{itemize}
\item   Q1 = uupuueuuuu est-il un théorème?
\item   Q2 = upuueuuuu ? 
\item   Q3 = upupueuuu ?
\end{itemize}
 
Réponses : 
\begin{itemize}
\item   Q1, oui.
\item   Q2, non : il y a un nombre impair de "u", ce qui n'est pas possible.
\item   Q3, non : il y a deux "p".
\end{itemize}

 

\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/par-logique-fig1.eps}}
}
  \caption{Preuve? On développe l'arbre}
  \label{preuve}
\end{figure}


 
\subsubsection{Deuxième exemple}

Considérons le système : 
\begin{itemize}
\item   alphabet = l'ensemble des trois symboles "plus " , "egal " , et "un ",
\item   p.f.e. = concaténation,
\item   axiome = un plus un egal un un.
\item   règles : 
  \begin{itemize}
  \item     R1 : si une expression de la forme A egal B est un théorème (où "A" désigne     n'importe quelle suite de "un ", de "plus ", et de "egal ", et B de même),  alors l'expression un A egal B un est aussi un théorème.
  \item     R2 : si une expression de la forme A egal B est un théorème, alors 
    l'expression A un egal un B est aussi un théorème. 
  \end{itemize}
\end{itemize}

Questions : 
\begin{itemize}
\item   Q1 = un un plus un un egal un un un un est-il un théorème ? 
\item   Q2 = un plus un un egal un un un un ? 
\item   Q3 = un plus un plus un egal un un un ? 
\end{itemize}

Réponses : oui, non, et non, car les deux systèmes sont isomorphes.

Si nous remplaçons "plus " par "+", "egal " par "=", et "un " par "1", l'axiome s'écrit : $1+1=2$ , en base 1 (en chiffres romains, concaténation = addition).

R1 se lit : si $A=B$, alors $1+A=B+1$

R2 : si $A=B$, alors $A+1=1+B$

Q1 : $2+2=4$ est un théorème 

Q2 : $1+2=4$ est un non-théorème

Q3 : $1+1+1 ...$ est-un non-théorème ! 

\subsubsection{ Moralité}
Pour démontrer qu'une expression est un théorème, nous avons une procédure 
(développer l'arbre comme illustré en figure \ref{preuve}) infaillible, qui répond en $2n/2$, $n$ étant la longueur de la chaîne, donc en temps fini.

Par contre, pour démontrer qu'une expression est un non-théorème, il nous faut 
"tricher". Dans les deux exemples ci-dessus, nous avons fait de l'arithmétique, que faudrait-il faire sur un autre exemple ?

Donc les notions de "être un théorème" et de "être un non-théorème" ne sont pas symétriques. Notre système "peu" est semi-décidable : nous avons une procédure qui répond "oui" en temps fini, mais pas de procédure pour répondre "non".

\subsubsection{Interprétation}
Ce que nous venons de manipuler n'est pas un système formel : le symbole "2" ne fait pas partie de l'alphabet. Ce que nous venons de manipuler est 
l'interprétation du système formel. "1+1+1=3", dont l'interprétation est << vrai >>, bien que ce soit un non-théorème.

Une interprétation d'un S.F. n'est en général pas équivalente au S.F., 
c'est-à-dire que les notions de "être un théorème" et "être un non-théorème" 
d'une part, et de "être vrai" et "être faux" d'autre part, peuvent ne pas se 
recouvrir.

Cependant, il ne faut pas rejeter l'interprétation : souvenez-vous, si vous avez étudié un peu de Géométrie, la première fois qu'on vous a demandé "démontrer que le triangle ABC est isocèle". Vous avez soigneusement mesuré les deux cotés, et vous avez dit : "Oui, les deux cotés sont égaux". Et l'enseignant vous a répondu : "NON! Ce n'est pas parce que c'est vrai sur la figure que c'est un théorème". 

Mais vous n'avez pas pour autant cessé de faire des figures pour résoudre les 
problèmes, parce qu'elles guident le raisonnement. Nous y reviendrons. 

\subsubsection{Synthèse}
Considérons un système formel quelconque, et l'ensemble (qui peut être infini) 
des expressions qu'on peut engendrer dans ce système en appliquant le procédé de formation des expressions.

 Nous pouvons partitionner (voir figure \ref{TNT}) cet ensemble en :
 \begin{itemize}
 \item les expressions qui sont des théorèmes,
 \item  et celles qui sont des non-théorèmes.
 \end{itemize}


\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/par-logique-fig2.eps}}
}
  \caption{Partition Théorème/Non Théorème}
  \label{TNT}
\end{figure}
 
Nous pouvons également partitionner (voir figure \ref{TNTDND}) cet ensemble en :
\begin{itemize}
\item ce qu'une procédure peut démontrer en temps fini,
\item  et ce qu'elle ne peut pas.
\end{itemize}

\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/par-logique-fig3.eps}}
}
  \caption{Partition Théorème/Non Théorème - Décidable/Non Décidable}
  \label{TNTDND}
\end{figure} 

Si la partie ND est vide, le système est dit décidable. Si la partie TND est 
vide, il est semi-décidable. Si aucune partie n'est vide, il est indécidable.

Nous pouvons par ailleurs partitionner (voir figure \ref{TNTVF}) l'ensemble en :
\begin{itemize}
\item  les expressions dont l'interprétation est "vrai",
\item  et celles dont l'interprétation est "faux".
\end{itemize}

\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/par-logique-fig4.eps}}
}
  \caption{Partition Théroème/Non Théorème - Vrai/Faux}
  \label{TNTVF}
\end{figure}

Si la partie TF n'est pas vide, nous dirons que notre interprétation est sans 
intérêt. On montre en revanche que la partie NTV n'est, en général, pas vide.

Lorsqu'une proposition "manifestement vraie" ne peut être démontrée, on est donc en droit de se demander dans laquelle de ces zones on se trouve. Un cas célèbre était la conjecture de Fermat, qui a tenu les mathématiciens en échec pendant trois siècles : il n'existe pas d'entiers positifs x, y et z, et d'entier n 
supérieur à 2, tels que $x^n+y^n=z^n$ .


La partie suivante revient plus précisément sur les bases de la logique formelle qui est utilisée pour exprimer les mécanismes d'inférence ou encore de raisonnement qui caractériseraient un processus << intelligent >>.
