(* Ce travail a pour but d'exhiber la proposition indémontrable dans
 * l'arithmétique de Peano, suivant la méthode de Tarski. Il montre que cette
 * arithmétique (que l'on abrègera P.A.) est incomplète pour peu qu'on la
 * suppose correcte. Pour cela, on va suivre la méthode décrite dans l'ouvrage
 * "Les théorèmes d'incomplétude de Gödel", écrit par Raymond Smullyan et publié
 * aux éditions Dunod. 
 *
 * On utilisera un alphabet à 13 symboles : "0", "'", "(", ")", "f", ",", "v",
 * "~", "=>", "\/", "=", "<=", et "#".
 * - Les expressions "0", "0'", "0''", … sont les noms formels des entiers
 *     naturels 0, 1, 2, … On les abrègera en écrivant l'entier naturel
 *     correspondant.
 * - Le symbole "'" sert de nom à la fonction successeur.
 * - Les expressions "f,", "f,," et "f,,," sont les noms formels des opérations
 *     d'addition, de multiplication et d'exponentiation, que l'on abrègera
 *     respectivement par les symboles "+", "." et "e".
 * - Le symbole "~" représente la négation, le "=>" l'implication.
 * - Le symbole "\/" est le quantificateur universel (le "pour tout", impossible
 *     à décrire sur un clavier classique).
 * - Le symbole "=" désigne la relation d'égalité et le "<=" la relation
 *     "inférieur ou égal".
 * - Les expressions de la forme "(v,)", "(v,,)", "(v,,,)", … seront nos
 *     variables, que l'on abrègera en utilisant les entiers -1, -2, -3, …
 *     (qui ne servent pas, en effet l'arithmétique de Peano ne travaille
 *     qu'avec des entiers naturels).
 *
 * Pour cela, on va créer un type qui va contenir nos termes (expressions
 * mathématiques) et un autre qui va contenir nos formules. *)

type variable = int ;;
type nombre = int ;;

type terme =
  | Variable of variable (* Une variable *)
  | Nombre of nombre (* Un nombre *)
  | Addition of terme * terme (* L'addition *)
  | Multiplication of terme * terme (* La multiplication *)
  | Exponentiation of terme * terme (* L'exponentiation *)
  | Successeur of terme (* La fonction successeur *)
;;

type formule = 
  | Egal of terme * terme (* Égalité entre deux termes *)
  | InferieurOuEgal of terme * terme (* Relation "<=" *)
  | Negation of formule (* La négation d'une expression *)
  | Implication of formule * formule (* L'implication entre deux expressions *)
  | PourTout of variable * formule (* Le quantificateur universel *) 
;; 

(* On crée des fonctions d'affichange de formules *)

let rec imprimeTerme = function
  | Variable v ->
      Printf.printf "v{%d}" (-v);
  | Nombre a ->
      Printf.printf "%d" a;
  | Addition (a,b) ->  (
      Printf.printf "(";
      imprimeTerme a;
      Printf.printf "+";
      imprimeTerme b;
      Printf.printf ")";
    )
  | Multiplication(a,b) -> (
      Printf.printf "(";
      imprimeTerme a;
      Printf.printf ".";
      imprimeTerme b;
      Printf.printf ")";
    )
  | Exponentiation(a,b) -> (
      Printf.printf "(";
      imprimeTerme a;
      Printf.printf "^";
      imprimeTerme b;
      Printf.printf ")";
    )
  | Successeur a ->   (
      imprimeTerme a;
      Printf.printf "'";
    )
;; 

let rec imprimeFormule = function
  | Negation (Negation f) -> 
      imprimeFormule f;
  | Implication (Negation (f1),f2) -> (
      Printf.printf "(";
      imprimeFormule f1;
      Printf.printf " V ";
      imprimeFormule f2;
      Printf.printf ")";
    )
  | Negation (Implication (f1,Negation (f2))) -> (
      Printf.printf "(";
      imprimeFormule f1;
      Printf.printf " * ";
      imprimeFormule f2;
      Printf.printf ")";
    )
  | Negation (PourTout (v,Negation(f))) -> (
      Printf.printf "Ev{%d}" (-v);
      imprimeFormule f;
    )
  | Egal (t1,t2) ->       (
      Printf.printf "(";
      imprimeTerme t1;
      Printf.printf " = ";
      imprimeTerme t2;
      Printf.printf ")";
    )
  | InferieurOuEgal (t1,t2) ->    (
      Printf.printf "(";
      imprimeTerme t1;
      Printf.printf " <= ";
      imprimeTerme t2;
      Printf.printf ")";
    )
  | Negation f ->         (
      Printf.printf "~";
      imprimeFormule f;
    )
  | Implication (f1,f2) ->    (
      Printf.printf "(";
      imprimeFormule f1;
      Printf.printf " => ";
      imprimeFormule f2;
      Printf.printf ")";
    )
  | PourTout (v,f) ->         (
      Printf.printf "Av{%d}" (-v);
      imprimeFormule f;
    )
;;

(* On définit maintenant les abréviations classiques : le "et", le "ou", etc. *)

let ou f1 f2 =
  Implication (Negation (f1),f2)
;;

let et f1 f2 =
  Negation (Implication (f1,Negation (f2)))
;;

let equivalent f1 f2 =
  et (Implication (f1,f2)) (Implication (f2,f1))
;;

let ilExiste v f =
  Negation (PourTout (v,Negation(f)))
;;

let different t1 t2 =
  Negation (Egal (t1,t2))
;;

let strictementInferieur t1 t2 =
  et (InferieurOuEgal (t1,t2)) (Negation (Egal (t1,t2)))
;;

let pourToutBorne v t f =
  PourTout (v,Implication (InferieurOuEgal (Variable v,t),f))
;;

let ilExisteBorne v t f =
  Negation (pourToutBorne v t (Negation f))
;;

(* Les deux dernières fonctions signifient respectivement: "Pour toute variable
 * v inférieure au terme t, f est vérifiée" et "Il existe une variable v
 * inférieure au terme t telle que f soit vérifiée". Bien qu'elles paraissent
 * pour l'instant assez dénuées d'intérêt, elles seront très utiles par la
 * suite. *)

(* La notion de vérité de l'arithmétique de Peano est définie par récurrence :
 *  - Si un énoncé est de la forme "t1 = t2" où t1 et t2 sont des termes, il est
 *      vrai ssi t1 = t2.
 *  - Si un énoncé est de la forme "t1 <= t2" où t1 et t2 sont des termes, il
 *      est vrai ssi t1 <= t2.
 *  - Si un énoncé est de la forme "~f" où f est une formule, il est vrai ssi f
 *      est faux.
 *  - Si un énoncé est de la forme "f1 => f2" où f1 et f2 sont des formules, il
 *      est vrai ssi f1 est faux ou f2 est vrai.
 *  - Si un énoncé est de la forme "A(v)F", il est vrai ssi pour tout nombre n,
 *      l'énoncé F(n) est vrai.
 * Et on dira qu'un énoncé est faux si et seulement si il n'est pas vrai.
 * On rappelle que supposer P.A. correct revient à dire "Toute formule prouvable
 * est vraie et tout formule réfutable est fausse". On définira plus tard la
 * notion de prouvabilité et de réfutabilité. *)

(* On va maintenant créer des fonctions chargées d'aller chercher à l'intérieur
 * d'une formule (ou d'un terme) la variable ayant l'indice le plus grand (ceci
 * pour être capable d'éviter les collisions entre variables) *)

(* Cette fonction renvoie la variable ayant l'indice le plus grand dans un terme t *)
let rec plusGrandeVariableDansTerme t = match t with
  | Variable (v) ->
      v
  | Nombre (n) ->
      0
  | Addition (t1,t2) ->
      min (plusGrandeVariableDansTerme t1) (plusGrandeVariableDansTerme t2)
  | Multiplication (t1,t2) ->
      min (plusGrandeVariableDansTerme t1) (plusGrandeVariableDansTerme t2)
  | Exponentiation (t1,t2) ->
      min (plusGrandeVariableDansTerme t1) (plusGrandeVariableDansTerme t2)
  | Successeur (t1) ->
      plusGrandeVariableDansTerme t1
;; 

(* Cette fonction recherche la variable ayant l'indice le plus grand dans une formule f *)
let rec plusGrandeVariableDansFormule f = match f with
  | Egal (t1,t2) ->
      min (plusGrandeVariableDansTerme t1) (plusGrandeVariableDansTerme t2)
  | InferieurOuEgal (t1,t2) ->
      min (plusGrandeVariableDansTerme t1) (plusGrandeVariableDansTerme t2)
  | Negation (f1) ->
      plusGrandeVariableDansFormule f1
  | Implication (f1,f2) ->
      min (plusGrandeVariableDansFormule f1) (plusGrandeVariableDansFormule f2)
  | PourTout (v,f1) ->
      min v (plusGrandeVariableDansFormule f1)
;; 

(* Pour simplifier les formules à suivre, on va faire des alias *)

let pgvdt = plusGrandeVariableDansTerme ;;
let pgvdf = plusGrandeVariableDansFormule ;;

let (++) x y = Addition (x,y) ;;
let ( ** ) x y = Multiplication (x,y) ;;
let (^^) x y = Exponentiation (x,y) ;;
let succ x = Successeur x ;;

let (===) x y = Egal (x,y) ;;
let (<<=) x y = InferieurOuEgal (x,y) ;;
let (=/=) x y = different x y ;;
let (<<<) x y = strictementInferieur x y ;;

let (==>) x y = Implication (x,y) ;;
let pt x y = PourTout (x,y) ;;
let ie x y = ilExiste x y ;;
let (~~~) x = Negation x ;;
let (^^^) x y = et x y ;;
let (|/) x y = ou x y ;;
let (<=>) x y = equivalent x y ;;
let ptb (x,y) z = pourToutBorne x y z ;;
let ieb (x,y) z = ilExisteBorne x y z ;;

let var x = Variable x ;;
let nb x = Nombre x ;;
let v1 = var (-1) ;;

(* On va maintenant définir les formules exprimant la concaténation de deux
 * formules en base 13 *)

(* La formule "puiss13 x" est vraie ssi x est une puissance de 13 *)
let puiss13 x =
  (* On calcule la variable qu'on va utiliser pour éviter les collisions *)
  let v = (pgvdt x) - 1 in 
  ie v (x === (nb 13) ^^ (var v))
;; 

(* La formule "s x y" est vraie ssi y est la plus plus petite
 * puissance de b plus grande que x *)
let s x y =
  let v = (min (pgvdt x) (pgvdt y)) - 1 in
  (puiss13 y) 
    ^^^ (x <<< y)
    ^^^ (pt v ((puiss13 (var v)) ^^^ (x <<< (var v))) ==> (y <<= (var v)))
;; 

(* La formule "puissl13 x y" est vraie ssi 13^(l13(x))=y, où l13(x) est la
 * longueur de x écrit en base 13 *)
let puissl13 x y =
  ((x === (nb 0)) ^^^ (y === (nb 13))) |/ ((x =/= (nb 0)) ^^^ (s x y))
;; 

(* La formule concat13 x y z est vraie ssi x*y=z en base 13, où * est
 * l'opérateur de concaténation *)
let concat13 x y z =
  let v1 = (min (min (pgvdt x) (pgvdt y)) (pgvdt z)) - 1 in
  let v2 = v1 - 1 in
  ie v1 (ie v2 ((puissl13 y (var v1)) 
                  ^^^ ((x ** (var v1)) === (var v2)) 
                  ^^^ (((var v2) ++ y) === z)))
;; 

(* Le formule grosseConcat [|x1,x2,…,xn|] y est vraie ssi x1*x2*…*xn=y en
 * base 13 *)
let rec grosseConcat tableau y = 
  let taille = Array.length tableau in
  let vrairenvoi = ref (Egal (nb 17,nb 42)) in
  if taille > 2 then
    (
      let variableMin = ref 0 in
      for i = 0 to (taille - 1) do
        variableMin := min !variableMin (pgvdt tableau.(i))
      done;
      let v = Array.make (taille-2) (-1) in
      for i = 0 to (taille - 3) do
        v.(i) <- (!variableMin - (i+1))
      done;
      let renvoi = ref (concat13 tableau.(0) tableau.(1) (var v.(0))) in
      for i = 1 to (taille-3) do
        renvoi := !renvoi ^^^ (concat13 (var v.(i-1)) tableau.(i+1) (var v.(i)));
      done;
      renvoi := !renvoi ^^^ (concat13 (var v.(taille-3)) tableau.(taille-1) y);
      for i = 0 to (taille-3) do
        renvoi := ie v.(i) !renvoi;
      done;
      vrairenvoi := !renvoi;
    )
  else if taille = 2 then
    vrairenvoi := concat13 tableau.(0) tableau.(1) y;
  !vrairenvoi
;;


(* On va faire une petite pause théorique.
 *
 * On dit qu'une partie P de IN est représentée par une formule ayant une unique
 * variable libre F(v) lorsqu'on a l'équivalence :
 *   "F(n) est vraie <=> n appartient à P"
 * Il existe un nombre dénombrable de formules mais un nombre indénombrable de
 * parties de IN : il existe donc forcément des parties de IN impossibles à
 * représenter par une formule.
 *
 * On appelle ensemble arithmétique tout ensemble "représentable", autrement dit
 * tel qu'il existe une formule F(v) qui le représente. Une relation
 * R(x1,x2,…,xn) est arithmétique s'il existe une formule F(x1,…,xn) qui est
 * vraie ssi R(x1,…,xn). Une fonction f(x1,…,xn) est arithmétique si la
 * relation R(x1,…,xn,y) équivalente à f(x1,…,xn)=y est arithmétique.
 *
 * On a donc vu par exemple, que l'addition, la multiplication, ou plus
 * compliqué, la concaténation en base 13, étaient toutes des fonctions
 * arithmétiques.
 *
 * Une des idées géniales de Gödel, c'est d'établir une bijection entre
 * l'ensemble des expressions et IN : ainsi, on pourra associer à chaque formule
 * un nombre unique, et considérer des ensembles de formules comme des ensembles
 * de nombres. Ce procédé sera appelé la numérotation de Gödel. Il existe
 * plusieurs manières de créer des fonctions bijectives de l'ensemble des
 * expressions dans IN : on utilisera ici une modification de la méthode de
 * Quine (Mathematical Logic, 1940), en décomposant nos expressions en base 13.
 * À chacun des 13 symboles de notre alphabet, on associe le chiffre suivant :
 *   0   '   (   )   f   ,   v   ~   =>  \/  =   <=  #
 *   1   0   2   3   4   5   6   7   8   9   a   b   c
 *
 * l'expression correspondant à la variable v2 par exemple, qui s'écrit sans
 * abréviation "(v,,)", a pour numéro de Gödel 26553. Le fait que le chiffre 0 a
 * été attribué à "'" et pas à "0", s'explique par la simplification obtenue :
 * pour tout nombre entier n, le numéro de Gödel de sa représentation dans cet
 * alphabet est 13^n.
 *
 * Maintenant qu'on a une correspondance entre des entiers et des formules, on
 * peut se demander si certains ensembles de formules sont ou non
 * représentables. Par exemple, l'ensemble des expressions prouvables est-il
 * représentable ? On va voir que oui, et la formule qui exprime cet ensemble
 * est à la base de l'énoncé indécidable que nous allons exhiber ici.
 *
 * Intéressons-nous au système formel d'axiomes qui est à la base de
 * l'arithmétique de Peano. Ce système est composé de 19 schémas d'axiomes et de
 * deux règles de déduction. Ces 19 schémas d'axiomes peuvent être classés en 4
 * groupes :
 *
 * Groupe I : schémas d'axiomes du calcul propositionnel
 *   L1 : F => (G => F)
 *   L2 : (F => (G => H)) => ((F => G) => (F => H))
 *   L3 : (~F => ~G) => (G => F)
 *
 * Groupe II : schémas d'axiomes additionnels, pour la logique du premier ordre
 * avec identité
 *   L4 : (\/v (F => G)) => ((\/v F) => (\/v G))
 *   L5 : F => (\/v F)               (si v n'apparaît pas dans F)
 *   L6 : ~(\/v ~(v = t))            (si v n'apparaît pas dans t)
 *   L7 : (v = t) => (XvY => XtY)    (si X et Y sont deux expressions telles que
 *                                   XvY soit une formule atomique)
 *
 * (On peut remarquer que ces schémas d'axiomes comportent chacun une infinité
 * d'axiomes : toutes les formules de la forme L1 sont vraies, par exemple, et
 * ceci pour n'importe quelles formules F et G. Plus généralement, les schémas
 * d'axiomes L1 à L7 sont vrais si F, G et H sont des formules, si v est une
 * variable, et si t est un terme.)
 *
 * Groupe III : schémas ne comportant qu'un axiome (contrairement à ceux du
 * groupe I et II)
 *   N1  : (v1' = v2') => (v1 = v2)
 *   N2  : ~(0 = v1')
 *   N3  : (v1 + 0) = v1
 *   N4  : (v1 + v2') = (v1 + v2)'
 *   N5  : (v1.0) = 0
 *   N6  : (v1.v2') = ((v1.v2) + v1)
 *   N7  : (v1 <= 0) eq (v1 = 0)
 *   N8  : (v1 <= v2') eq ((v1 <= v2) ou (v1 = v2'))
 *   N9  : (v1 <= v2) ou (v2 <= v1)
 *   N10 : (v1 e 0) = 0'
 *   N11 : (v1 e v2') = ((v1 e v2).v1)
 * (on a ici écrit "eq" et "ou" pour les symboles "équivalence" et
 * "disjonction", pour éviter une écriture trop lourde)
 *
 * Groupe IV : récurrence mathématique
 *   N12 : F(0) => ((\/v1 (F(v1) => F(v1'))) => (\/v1 F(v1)))
 * (où F(a) désigne le résultat de la substitution du terme a à toutes les
 * occurrences libres de v1 dans F(v1))
 *
 * Et les règles de déduction sont les suivantes :
 *   Règle 1 (Modus Ponens)   : De F et de (F => G), on en déduit G
 *   Règle 2 (Généralisation) : De F, on déduit (\/v F)
 *
 * On appelle preuve (dans le système P.A.) une suite finie de formules telles
 * que chaque terme de la suite soit ou bien un axiome, ou bien directement
 * dérivable à partir de deux termes antérieurs par application de la règle 1,
 * ou bien directement dérivable à partir d'un terme antérieur par application
 * de la règle 2.
 *
 * Une formule F est dite prouvable s'il existe une preuve dont le dernier terme
 * est F ; et une telle suite est appellée preuve de F. Une formule F est dite
 * réfutable si sa négation est prouvable.
 *
 * On va prouver que l'ensemble des formules prouvables est un ensemble
 * arithmétique, et à partir de la relation qui l'exprime, exhiber un énoncé
 * indécidable. Pour ça, on va procéder par étapes. On va prouver que certaines
 * relations et fonctions sont arithmétiques, jusqu'à arriver à l'ensemble des
 * formules prouvables. Beau programme, non ? ^^ *)

(* La formule "commence x y" est vraie ssi la décomposition en base 13 de x est
 * un préfixe de celle de y *)
let commence x y =
  let z = (min (pgvdt x) (pgvdt y)) - 1 in
  let w = z - 1 in
  (x === y) |/ (ieb (z,y) 
                    (ieb (w,y) 
                         ((puiss13 (var w)) 
                            ^^^ (concat13 (x ** (var w)) (var z) y))))
;; 

(* La formule "termine x y" est vraie ssi la décomposition en base 13 en x est
 * un suffixe de celle de y *)
let termine x y =
  let z = (min (pgvdt x) (pgvdt y)) - 1 in
  (x === y) |/ (ieb (z,y) (concat13 (var z) x y ))
;; 

(* La formule "partie x y" est vraie ssi la décomposition en base 13 de x est un
 * sous-mot de celle de y *)
let partie x y =
  let z = (min (pgvdt x) (pgvdt y)) - 1 in
  ieb (z,y) ((termine (var z) y) ^^^ (commence x (var z)))
;; 

(* La formule "grossePartie [x1;x2;…;xn] y" est vraie ssi la décomposition en
 * base 13 de x1*x2*…*xn est un sous-mot de celle de y *)
let grossePartie tableau y =
  let v = ref 0 in
  Array.iter (fun x -> v := min (!v) (pgvdt x)) tableau;
  decr v;
  let z = !v in
  ieb (z,y) ((grosseConcat tableau (var z)) ^^^ (partie (var z) y))
;; 

(* Jusqu'ici, on ne s'est pas servi du symbole "#". Ce symbole va nous être
 * utile pour définir une suite finie de termes.
 *
 * Le n-uplet d'expressions (dont chacune ne comporte pas #) (X1,…,Xn) va être
 * représenté formellement par l'expression #X1#…#Xn#, et son numéro de Gödel
 * sera appelé "numéro de suite" *)

let diese = Nombre 12 ;;

(* La formule "seq x" est vraie ssi x est un numéro de liste *)
let seq x =
  let y = (pgvdt x) - 1 in
  (commence diese x)
    ^^^ (termine diese x)
    ^^^ (diese =/= x)
    ^^^ (~~~ (grossePartie [|diese ; diese|] x))
    ^^^ (ptb (y,x) ((grossePartie [|diese ; (nb 0) ; (var y)|] x)
                      ==> (commence diese (var y))))
;;

(* La formule "appartient x y" est vraie ssi y est un numéro de suite et x un
 * terme de cette suite. *)
let appartient x y =
  (seq y) ^^^ (grossePartie [|diese;x;diese|] y) ^^^ (~~~ (partie diese x))
;; 

(* La formule "estSitueAvant x y z" est vraie ssi z est un numéro de suite, que
 * x et y sont des termes de cette suite, et que la première occurence de x dans
 * z précède la première occurence de y. *)
let estSitueAvant x y z =
  let w = (min (min (pgvdt x) (pgvdt y)) (pgvdt z)) - 1 in
  (appartient x z)
    ^^^ (appartient y z) 
    ^^^ ieb (w,z) ((commence (var w) z)
                     ^^^ (appartient x (var w))
                     ^^^ (~~~ (appartient y (var w))))
;; 

(* Une simple abréviation *)
let pourToutAppartenant x y f =
  pt x ((appartient (var x) y) ==> f)
;; 
let pta = pourToutAppartenant ;;

(* Une autre abréviation un peu plus tordue *)
let ilExisteSitueAvant x y z w f =
  ie x (ie y ((estSitueAvant (var x) z w)
                ^^^ (estSitueAvant (var y) z w) ^^^ f))
;; 
let iesa = ilExisteSitueAvant ;;

(* On a défini par récurrence ce qu'étaient des termes et des formules, il faut
 * remplacer ces définitions par des définitions explicites, en s'aidant de
 * l'outil des suites que l'on vient de définir.
 *
 * On définit une relation Rt comme suit : pour tout triplet d'expressions
 * (X,Y,Z), Rt(X,Y,Z) est vraie si et seulement si Z est une des expressions
 * (X+Y), (X.Y), (XeY) ou (X'). On désignera par la dénomination "suite de
 * constructions de termes" une suite finie d'expressions (X1,…,Xn) telles que
 * pour chaque élément Xi de la suite, Xi est soit une variable, soit un nombre,
 * soit une expression telle que Rt(Xj,Xk,Xi), où j et k sont dans [[1,i-1]]. Du
 * coup, on peut dire qu'une expression X est un terme si et seulement s'il
 * existe une suite de construction de termes dont X est un élément. 
 *
 * De même, on définit Rf comme suit : pour tout triplet de formules (X,Y,Z),
 * Rf(X,Y,Z) est vraie si et seulement si Z est une des expressions (~X),
 * (X=>Y), ou (\/v X) pour une variable v. On pourra dire de la même façon que X
 * est une formule si et seulement s'il existe une "suite de construction de
 * formules" dont X est un élément. *)

(* La formule "imp x y z" est vraie ssi E{z}=(E{x}=>E{y}) *)
let imp x y z =
  grosseConcat [|(nb 2) ; x ; (nb 8) ; y ; (nb 3)|] z
;; 

(* La formule "neg x y" est vraie ssi E{y}=~E{x} *)
let neg x y =
  concat13 (nb 7) x y
;; 

(* La formule "pl x y z" est vraie ssi E{z}=(E{x}+E{y}) *)
let pl x y z =
  grosseConcat [|(nb 2) ; x ; (nb 4) ; (nb 5) ; y ; (nb 3)|] z
;; 

(* La formule "mult x y z" est vraie ssi E{z}=(E{x}.E{y}) *)
let mult x y z =
  grosseConcat [|(nb 2) ; x ; (nb 4) ; (nb 5) ; (nb 5) ; y ; (nb 3)|] z
;; 

(* La formule "exp x y z" est vraie ssi E{z}=(E{x}eE{y}) *)
let exp x y z =
  grosseConcat [|(nb 2) ; x ; (nb 4) ; (nb 5) ; (nb 5) ; (nb 5) ; y ; (nb 3)|] z
;; 

(* La formule "suc x y" est vraie ssi E{y}=E{x}' *)
let suc x y =
  concat13 x (nb 0) y
;; 

(* La formule "id x y z" est vraie ssi E{z}="E{x}=E{y}" *)
let id x y z =
  grosseConcat [|x ; (nb 10) ; y|] z
;; 

(* La formule "inf x y z" est vraie ssi E{z}="E{x}<=E{y}" *)
let inf x y z =
  grosseConcat [|x ; (nb 11) ; y|] z
;; 

(* La formule "estChaineDIndices x" est vraie ssi
 * E{x} est de la forme ",,,[…]," *)
let estChaineDIndices x =
  let y = (pgvdt x) - 1 in
  ptb (y,x) ((partie (var y) x) ==> (partie (nb 5) (var y)))
;; 

(* La formule "estUneVariable x" est vraie ssi
 * E{x} est une variable *)
let estUneVariable x =
  let y = (pgvdt x) - 1 in
  ieb (y,x) ((estChaineDIndices (var y))
               ^^^ (grosseConcat [|(nb 2) ; (nb 6) ; (var y) ; (nb 3)|] x))
;; 

(* La formule "estNombre x" est vraie ssi x est un nombre *)
let estUnNombre x =
  puiss13 x
;; 

(* La formule "rt x y z" est vraie ssi la relation Rt(x,y,z) est vérifiée *)
let rt x y z =
  (pl x y z) |/ (mult x y z) |/ (exp x y z) |/ (suc x y)
;; 

(* La formule "seqt x" est vraie ssi
 * E{x} est une suite de construction de terme *)
let seqt x =
  let y = (pgvdt x) - 1 in
  let z = y - 1 in
  let w = z - 1 in
  (seq x) ^^^ (pta y x ((estUneVariable (var y)) |/ (estUnNombre (var y)) 
                        |/ (iesa z w (var y) x (rt (var z) (var w) (var y)))))
;; 

(* La formule "tm x" est vraie ssi E{x} est un terme *)
let tm x =
  let y = (pgvdt x) - 1 in
  ie y ((seqt (var y)) ^^^ (appartient x (var y)))
;; 

(* La formule "estFormuleAtomique x" est vraie ssi E{x} est une formule atomique *)
let estFormuleAtomique x =
  let y = (pgvdt x) - 1 in
  let z = y - 1 in
  ieb (y,x) 
      (ieb (z,x) 
           ((tm (var y))
              ^^^ (tm (var z))
              ^^^ ((id x (var y) (var z)) |/ (inf x (var y) (var z)))))
;; 

(* La formule "gen x y" est vraie
 * ssi il existe une variable w telle que E{y}=\/w E{x} *)
let gen x y =
  let z = (min (pgvdt x) (pgvdt y)) - 1 in
  ieb (z,y) ((estUneVariable (var z)) ^^^ (grosseConcat [|(nb 9) ; (var z) ; x|] y))
;; 

(* La formule "genbis v x y" est vraie ssi E{y}=\/v E{x} *)
let genbis v x y =
  (estUneVariable v) ^^^ (grosseConcat [|(nb 9);v;x|] y)
;;

let rf x y z =
  (imp x y z) |/ (neg x z) |/ (gen x z)
;; (* La formule "rf x y z" est vraie ssi la relation Rf(x,y,z) est vérifiée *)

(* La formule "seqf x" est vraie ssi
 * E{x} est une suite de construction de formule *)
let seqf x =
  let y = (pgvdt x) - 1 in
  let z = y - 1 in
  let w = z - 1 in
  (seq x) ^^^ (pta y x ((estFormuleAtomique (var y))
                          |/ (iesa z w (var y) x (rf (var z) (var w) (var y)))))
;; 

(* La formule "fm x" est vraie ssi E{x} est une formule *)
let fm x =
  let y = (pgvdt x) - 1 in
  ie y ((seqf (var y)) ^^^ (appartient x (var y)))
;; 

(* On atteint une partie pas très drôle : on va montrer que l'ensemble des
 * formules de la forme L1, … , L7, N1, … , N12 est un ensemble arithmétique. Ça
 * ne pose aucune difficulté théorique, mais il faut le faire si on veut obtenir
 * notre ensemble des numéros de Gödel des propositions démontrables. *)

(* Les formules "li x" sont vraies si E{x} est de la forme du schéma d'axiome
 * Li. Ce ne sont que des réécritures dans notre langage des propositions
 * écrites plus simplement dans la grosse parenthèse précédente.*)

let l1 x =
  let va = (pgvdt x) - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) 
                               ((fm (var va))
                                 ^^^ (fm (var vb))
                                 ^^^ (fm (var vc)) 
                                 ^^^ (imp (var vb) (var va) (var vc))
                                 ^^^ (imp (var va) (var vc) x)))))
;;

let l2 x = (* Attention les yeux *)
  let va = (pgvdt x) - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vd = vc - 1 in
  let ve = vd - 1 in
  let vf = ve - 1 in
  let vg = vf - 1 in
  let vh = vg - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) (ieb (vd,x)
  (ieb (ve,x) (ieb (vf,x) (ieb (vg,x) (ieb (vh,x)
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (fm (var vc)) ^^^ (fm (var vd))
         ^^^ (fm (var ve)) ^^^ (fm (var vf)) ^^^ (fm (var vg)) ^^^ (fm (var vh))
         ^^^ (imp (var vb) (var vc) (var vd))
         ^^^ (imp (var va) (var vb) (var ve))
         ^^^ (imp (var va) (var vc) (var vf))
         ^^^ (imp (var va) (var vd) (var vg))
         ^^^ (imp (var ve) (var vf) (var vh))
         ^^^ (imp (var vg) (var vh) x))))))))))
;;

let l3 x =
  let va = (pgvdt x) - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vd = vc - 1 in
  let ve = vd - 1 in
  let vf = ve - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) (ieb (vd,x) (ieb (ve,x) (ieb (vf,x)
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (fm (var vc))
         ^^^ (fm (var vd)) ^^^ (fm (var ve)) ^^^ (fm (var vf))
         ^^^ (neg (var va) (var vc))
         ^^^ (neg (var vb) (var vd))
         ^^^ (imp (var vb) (var va) (var ve))
         ^^^ (imp (var vc) (var vd) (var vf))
         ^^^ (imp (var vf) (var ve) x))))))))
;;

let l4 x =
  let va = (pgvdt x) - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vd = vc - 1 in
  let ve = vd - 1 in
  let vf = ve - 1 in
  let vg = vf - 1 in
  let vi = vf - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) (ieb (vd,x)
  (ieb (ve,x) (ieb (vf,x) (ieb (vg,x) (ieb (vi,x) 
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (fm (var vc)) ^^^ (fm (var vd))
         ^^^ (fm (var ve)) ^^^ (fm (var vf)) ^^^ (fm (var vg))
         ^^^ (estUneVariable (var vi)) 
         ^^^ (imp (var va) (var vb) (var vc))
         ^^^ (genbis (var vi) (var vc) (var vd))
         ^^^ (genbis (var vi) (var va) (var ve))
         ^^^ (genbis (var vi) (var vb) (var vf))
         ^^^ (imp (var ve) (var vf) (var vg))
         ^^^ (imp (var vd) (var vg) x))))))))))
;;

let l5 x =
  let va = (pgvdt x) - 1 in
  let vb = va - 1 in
  let vi = vb - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vi,x)
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (estUneVariable (var vi))
         ^^^ (genbis (var vi) (var va) (var vb))
         ^^^ (~~~ (partie (var vi) (var va)))
         ^^^ (imp (var va) (var vb) x)))))
;;

let l6 x =
  let t = (pgvdt x) - 1 in
  let va = t - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vi = vc - 1 in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) (ieb (t,x) (ieb (vi,x)
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (fm (var vc))
         ^^^ (estUneVariable (var vi)) ^^^ (tm (var t))
         ^^^ (~~~ (partie (var vi) (var t)))
         ^^^ (id (var vi) (var t) (var va))
         ^^^ (neg (var va) (var vb))
         ^^^ (genbis (var vi) (var vb) (var vc))
         ^^^ (neg (var vc) x)))))))
;;

let l7 x =
  let t = (pgvdt x) - 1 in
  let x1 = t - 1 in
  let x2 = x1 - 1 in
  let va = x2 - 1 in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vd = vc - 1 in
  let vi = vd - 1 in
  (ieb (t,x) (ieb (x1,x) (ieb (x2,x) (ieb (va,x)
  (ieb (vb,x) (ieb (vc,x) (ieb (vd,x) (ieb (vi,x)
      ((fm (var va)) ^^^ (fm (var vb)) ^^^ (fm (var vc)) ^^^ (fm (var vd))
         ^^^ (estUneVariable (var vi)) ^^^ (tm (var t))
         ^^^ (id (var vi) (var t) (var va))
         ^^^ (grosseConcat [|(var x1) ; (var vi) ; (var x2)|] (var vb))
         ^^^ (grosseConcat [|(var x1) ; (var t) ; (var x2)|] (var vc))
         ^^^ (imp (var vb) (var vc) (var vd))
         ^^^ (imp (var va) (var vd) x))))))))))
;;


(* Pour les axiomes du groupe III, il suffit de vérifier si x correspond à un
 * numéro de Gödel d'un des axiomes N1 à N11*)

(* godelv1 est une constante égale à (Nombre k), où k est le numéro de Gödel de
 * l'expression "(v')" *)
let godelv1 =
  nb (3 + 13 * (0 + 13 * (6 + 13 * 2)))
;; 

(* Idem pour l'expression "(v'')" *)
let godelv2 =
  nb (3 + 13 * (0 + 13 * (0 + 13 * (6 + 13 * 2))))
;; 

let godelplus = 
  nb (5 + 13 * 4)
;;

let godelmult =
  nb (5 + 13 * (5 + 13 * 4))
;;

let godelexp =
  nb (5 + 13 * (5 + 13 * (5 + 13 * 4)))
;;

let trad = function
  | '0' -> (nb 1)
  | '\'' -> (nb 0)
  | '(' -> (nb 2)
  | ')' -> (nb 3)
  | 'f' -> (nb 4)
  | ',' -> (nb 5)
  | 'v' -> (nb 6)
  | '~' -> (nb 7)
  | '>' -> (nb 8)
  | 'A' -> (nb 9)
  | '=' -> (nb 10)
  | '<' -> (nb 11)
  | '#' -> (nb 12)
  |  _  -> failwith "wat"
;;

(* Les formules l1 à l7 sont valables mais sont très lourdes algorithmiquement.
 * Aussi je vais les recoder, en utilisant le moins de formules intermédiaires
 * possibles, et en ne vérifiant pas si ce sont bien des formules ; cette
 * vérification sera faite uniquement à la fin, dans la fonction "estUnAxiome".
 * En effet, si F n'est pas une formule, (F => (G => F)) est une expression bien
 * définie, mais certainement pas une formule. *)

let l1bis x =
  let f = (pgvdt x) - 1 in
  let g = f - 1 in
  (ieb (f,x) (ieb (g,x)
      (grosseConcat [|trad '(' ; var f ; trad '(' ; var g ;
                      trad '>' ; var f ; trad ')' ; trad ')'|] x)))
;;

let l2bis x =
  let f = (pgvdt x) - 1 in
  let g = f - 1 in
  let h = f - 1 in
  (ieb (f,x) (ieb (g,x) (ieb (h,x) 
      (grosseConcat [|trad '(' ; var f ; trad '>' ; trad '(' ; var g ;
                      trad '>' ; var h ; trad ')' ; trad ')' ; trad '>' ;
                      trad '(' ; trad '(' ; var f ; trad '>' ; var g ;
                      trad ')' ; trad '>' ; trad '(' ; var f ; trad '>' ;
                      var h ; trad ')' ; trad ')'|] x))))
;;

let l3bis x =
  let f = (pgvdt x) - 1 in
  let g = f - 1 in
  (ieb (f,x) (ieb (g,x)
      (grosseConcat [|trad '(' ; trad '~' ; var f ; trad '>' ; trad '~' ;
                      var g ; trad ')' ; trad '>' ; trad '(' ; var g ;
                      trad '>' ; trad 'f' ; trad ')'|] x)))
;;

let l4bis x =
  let vi = (pgvdt x) - 1 in
  let f = vi - 1 in
  let g = f - 1 in
  (ieb (vi,x) (ieb (f,x) (ieb (g,x)
      (grosseConcat [|trad '(' ; trad 'A' ; var vi ; trad '(' ; var f ;
                      trad '>' ; var g ; trad ')' ; trad '>' ; trad '(' ;
                      trad 'A' ; var vi ; var f ; trad '>' ; trad 'A' ;
                      var vi ; var g ; trad ')' ; trad ')' ;|] x))))
;;

let l5bis x =
  let vi = (pgvdt x) - 1 in
  let f = vi - 1 in
  (ieb (vi,x) (ieb (f,x)
      ((~~~ (partie (var vi) (var f)))
         ^^^ grosseConcat [|trad '(' ; var f ; trad 'A' ;
                            var vi ; var f ; trad ')'|] x)))
;;

let l6bis x =
  let vi = (pgvdt x) - 1 in
  let t = vi - 1 in
  (ieb (vi,x) (ieb (t,x)
      ((~~~ (partie (var vi) (var t)))
         ^^^ grosseConcat [|trad '~' ; trad 'A' ; var vi ; trad '~' ; trad '(' ;
                            var vi ; trad '=' ; var t ; trad ')'|] x)))
;;

let l7bis x = 
  let vi = (pgvdt x) - 1 in
  let t = vi - 1 in
  let x1 = t - 1 in
  let x2 = x1 - 1 in
  (ieb (vi,x) (ieb (t,x) (ieb (x1,x) (ieb (x2,x)
      (grosseConcat [|trad '(' ; var vi ; trad '=' ; var t ; trad '>' ;
                      trad '(' ; var x1 ; var vi ; var x2 ; trad '>' ;
                       var x1 ; var t ; var x2; trad ')' ; trad ')'|] x)))))
;;

(* La formule "libis x" est vraie ssi E{x} est de la forme du schéma d'axiomes
 * li, i allant de 1 à 7. Enfin, pas exactement.  E{x} pourrait par exemple être
 * de la forme du schéma d'axiomes l1, mais avec F et G deux expressions ne
 * signifiant rien et n'étant pas des formules. Il faudra donc vérifier par la
 * suite que l'on obtient bien une formule. (Ce choix est fait pour éviter le
 * nombre d'appels à la fonction "fm x", fonction qui s'écrit en plusieurs
 * centaines de milliers de caractères…) À propos de la formule l7bis, on ne
 * vérifie nulle part que X1viX2 soit une formule atomique : je considère
 * qu'étant donné l'impossibilité théorique d'obtenir une formule du type "\/vi
 * ( […] \/vi ([…]))", cette vérification est inutile. *)
let n12bis x =
  let f = (pgvdt x) - 2 in
  let vi = f - 1 in
  let f0 = vi - 1 in
  let fvi = f0 - 1 in
  let fviprime = fvi - 1 in
  (ieb (f,x) (ieb (vi,x) (ieb (f0,x) (ieb (fvi,x) (ieb (fviprime,x)
      ((~~~ (partie (var vi) (var f)))
         ^^^ grosseConcat [|trad 'A' ; var (-1) ; trad '(' ;
                            var (-1) ; trad '=' ; nb 0 ; trad '>' ;
                            var f ; trad ')'|] (var f0)
         ^^^ grosseConcat [|trad 'A' ; var vi ; trad '(' ; var (-1) ; trad '=' ;
                            nb 0 ; trad '>' ; var f ; trad ')'|] (var fvi)
         ^^^ grosseConcat [|trad 'A' ; var vi ; trad '\'' ; trad '(' ;
                            var (-1) ; trad '=' ; nb 0 ; trad '>' ;
                            var f ; trad ')'|] (var fviprime)
         ^^^ grosseConcat [|trad '(' ; var f0 ; trad '>' ; trad '(' ; trad 'A' ;
                            var vi ; trad '(' ; var fvi ; trad '>' ;
                            var fviprime ; trad ')' ; trad '>' ; trad 'A' ;
                            var (-1) ; var f ; trad ')'|] x))))))
;;

(* La formule "estAxiomeDuGroupeIII x" est vraie ssi E{x} est un axiome du
 * groupe III. Le lecteur observateur aura sans doute remarqué que ce qui est le
 * plus simple d'un point de vue théorique est le plus pénible à écrire en
 * pratique… *)
let estAxiomeDuGroupeIII x =
  grosseConcat [|trad '(' ; godelv1 ; trad '\'' ; trad '=' ;
                 godelv2 ; trad '\'' ; trad '>' ; godelv1 ; trad '=' ;
                 godelv2 ; trad ')'|] x
    |/ grosseConcat [|trad '~' ; trad '0' ; trad '=' ;
                      godelv1 ; trad '\''|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelplus ; trad '0' ;
                      trad ')' ; trad '=' ; godelv1|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelplus ; godelv2 ; trad '\'' ;
                      trad ')' ; trad '=' ; trad '(' ; godelv1 ; godelplus ;
                      godelv2 ; trad ')' ; trad '\''|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelmult ; trad '0' ;
                      trad ')' ; trad '=' ; trad '0'|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelmult ; godelv2 ;
                      trad '\'' ; trad ')' ; trad '=' ; trad '(' ; trad '(' ;
                      godelv1 ; godelmult ; godelv2 ; trad ')' ; godelplus ; 
                      godelv1 ; trad ')'|] x
    |/ grosseConcat [|trad '~' ; trad '(' ; trad '(' ; godelv1 ; trad '=' ;
                      trad '0' ; trad '>' ; godelv1 ; trad '<' ; trad '0' ;
                      trad ')' ; trad '>' ; trad '~' ; trad '(' ; godelv1 ;
                      trad '<' ; trad '0' ; trad '>' ; godelv1 ; trad '=' ;
                      trad '0' ; trad ')' ; trad ')'|] x
    |/ grosseConcat [|trad '~' ; trad '(' ; trad '(' ; trad '(' ; trad '~' ;
                      godelv1 ; trad '<' ; godelv2  ; trad '>' ; godelv1 ;
                      trad '=' ; godelv2 ; trad '\'' ; trad ')' ; trad '>' ;
                      godelv1 ; trad '<' ; godelv2 ; trad '\''  ; trad ')' ;
                      trad '>' ; trad '~' ; trad '(' ; godelv1 ; trad '<' ;
                      godelv2 ; trad '\''  ; trad '>' ; trad '(' ; trad '~' ;
                      godelv1 ; trad '<' ; godelv2  ; trad '>' ; godelv1 ;
                      trad '=' ; godelv2 ; trad '\'' ; trad ')' ; trad ')' ;
                      trad ')'|] x
    |/ grosseConcat [|trad '(' ; trad '~' ; godelv1 ; trad '<' ; godelv2 ;
                      trad '>' ; godelv2 ; trad '<' ; godelv1 ; trad ')'|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelexp ; trad '0' ; trad ')' ;
                      trad '=' ; trad '0' ; trad '\''|] x
    |/ grosseConcat [|trad '(' ; godelv1 ; godelexp ; godelv2 ; trad '\'' ;
                      trad ')' ; trad '=' ; trad '(' ; trad '(' ; godelv1 ;
                      godelexp ; godelv2 ; trad ')' ; godelv1 ; trad ')'|] x
;; 

(* La formule "n12 x" est vraie ssi E{x} est de la forme du schéma d'axiomes
 * n12. Point négatif : il faut plus que plisser les yeux pour comprendre ce
 * charabia, mais je n'y peux rien. J'ai opté ici pour une autre solution que
 * celle de l'ouvrage, qui me paraissait assez peu valable. En effet, en suivant
 * rigoureusement les instructions de l'énoncé, j'aurais obtenu un schéma
 * d'axiomes du type "\/v1 ( […] (\/v1 ([…])))", et je ne suis pas certain
 * qu'une telle expression ait un sens. Ma solution est une reformulation de ce
 * schéma d'axiomes qui évite le problème. *)
let n12 x =
  let va = pgvdt x in
  let vb = va - 1 in
  let vc = vb - 1 in
  let vd = vc - 1 in
  let ve = vd - 1 in
  let vf = ve - 1 in
  let vg = vf - 1 in
  let vh = vg - 1 in
  let vi = vh - 1 in
  let vj = vi - 1 in
  let vk = vj - 1 in
  let vl = vk - 1 in
  let vm = vl - 1 in
  let vn = vm - 1 in
  let f = vn - 1 in
  let v1 = (var (-1)) in
  (ieb (va,x) (ieb (vb,x) (ieb (vc,x) (ieb (vd,x) (ieb (ve,x)
  (ieb (vf,x) (ieb (vg,x) (ieb (vh,x) (ieb (vi,x) (ieb (vj,x)
  (ieb (vk,x) (ieb (vl,x) (ieb (vm,x) (ieb (vn,x)
      ((fm (var vf)) ^^^ (fm (var vg)) ^^^ (fm (var vh))
         ^^^ (estUneVariable (var vi)) ^^^ (fm (var vj)) ^^^ (fm (var vk))
         ^^^ (fm (var vl)) ^^^ (fm (var vm)) ^^^ (fm (var vn)) ^^^ (fm (var f))
         ^^^ (id v1 (nb 0) (var va))
         ^^^ (id v1 (var vi) (var vb))
         ^^^ (id v1 (succ (var vi)) (var vc))
         ^^^ (genbis v1 (var f) (var vd))
         ^^^ (imp (var va) (var f) (var ve))
         ^^^ (imp (var vb) (var f) (var vf))
         ^^^ (imp (var vc) (var f) (var vg))
         ^^^ (genbis v1 (var ve) (var vh))
         ^^^ (genbis v1 (var vf) (var vj))
         ^^^ (genbis v1 (var vg) (var vk))
         ^^^ (imp (var vj) (var vk) (var vl))
         ^^^ (genbis (var vi) (var vl) (var vm))
         ^^^ (imp (var vm) (var vd) (var vn))
         ^^^ (imp (var vh) (var vn) x))))))))))))))))
;; 

(* On peut maintenant écrire ce pour quoi l'on s'est embêtés à écrire les 200
 * dernières lignes *)

let estAxiomeBis x =
  (fm x) ^^^ ((l1bis x) |/ (l2bis x) |/ (l3bis x) |/ (l4bis x)
                |/ (l5bis x) |/ (l6bis x) |/ (l7bis x)
                |/ (estAxiomeDuGroupeIII x)
                |/ (n12bis x))
;;

(* La formule "estAxiome x" est vraie ssi E{x} est un axiome de P.A. \o/ *)
let estAxiome x =
  (l1 x) |/ (l2 x) |/ (l3 x) |/ (l4 x)
  |/ (l5 x) |/ (l6 x) |/ (l7 x) 
  |/ (estAxiomeDuGroupeIII x)
  |/ (n12 x)
;; 

(* La formule "mp x y z" est vraie ssi on peut déduire E{z} de E{x} et de E{y}
 * par la règle 1 *)
let mp x y z =
  imp x z y
;; 

(* La formule "der x y z" est vraie ssi on peut déduire logiquement E{z} de E{x}
 * et de E{y} *)
let der x y z =
  (mp x y z) |/ (gen x z)
;; 

(* La formule "pv x" est vraie ssi E{x} est une preuve dans P.A. *)
let pv x =
  let y = (pgvdt x) - 1 in
  let z = y - 1 in
  let w = z - 1 in
  (seq x) ^^^ (pta y x ((estAxiomeBis (var y)) |/ (iesa z w (var y) x (der (var z) (var w) (var y)))))
;; 

(* La formule "estProuvable x" est vraie ssi E{x} est prouvable dans P.A. *)
let estProuvable x =
  let y = (pgvdt x) - 1 in
  ie y ((pv (var y)) ^^^ (appartient x (var y)))
;; 

(* L'ensemble des propositions démontrables dans l'arithmétique de Peano (noté
 * PE) est donc un ensemble arithmétique.
 *
 * Encore quelques petits points de théorie et on a fini ^^
 *
 * On appelle "énoncé de Gödel" d'une partie A de IN un énoncé X qui vérifie les
 * conditions suivantes :
 *   - Soit X est vrai et son numéro de Gödel est dans A
 *   - Soit X est faux et son numéro de Gödel n'est pas dans A
 * et pour arriver au théorème de Tarski, on va prouver le lemme suivant :
 *   Tout ensemble arithmétique possède un énoncé de Gödel.
 *
 * Si F(v) est une formule à une unique variable libre v, l'énoncé F(n) est
 * équivalent à l'énoncé "\/v((v=n)=>F(v))". L'avantage de cette écriture, c'est
 * que pour n'importe quelle expression E, "\/v((v=n)=>E)" est une expression
 * bien définie (alors que F(v) est plus difficile à traduire formellement, si F
 * est une expression quelconque). Pour cette raison, on n'utilisera plus que
 * cette écriture, que l'on notera F[n]. En d'autres termes, pour toute
 * expression E et pour tout nombre n :
 *   E[n] est l'abréviation de l'expression "\/v((v=n)=>E)".
 
 * Maintenant, pour tout couple d'entiers naturels (e,n), on désigne par r(e,n)
 * le numéro de Gödel de l'expression E[n], où E est l'expression unique ayant
 * e pour numéro de Gödel. La fonction r est arithmétique. En effet, si on note
 * k le numéro de Gödel de l'expression "\/v1(v1=", on a r(x,y) = k*13^y*8*x*3.
 * On peut donc coder la fonction correspondante. Sauf que k vaut, en base 13,
 * 9260322603a, ce qui est trop grand pour être stocké par un entier Caml
 * standard. On va donc le couper en deux =D *)

(* La formule "r x y z" est vraie ssi r(x,y)=z *)
let r x y z =
  let v = (min (min (pgvdt x) (pgvdt y)) (pgvdt z)) - 1 in
  ie v (((var v) === ((nb 13)^^y))
          ^^^ grosseConcat [|(nb 262460) ; (nb 812939) ; (var v) ;
                             (nb 8) ; x ; (nb 3)|] z)
;; 

(* Maintenant, on va introduire la fonction d, appellée fonction diagonale du
 * système, qui jouera un rôle clé dans la suite. Elle est simplement définie
 * par d(x) = r(x,x). En d'autres termes, si on désigne par E{n} l'expression
 * ayant pour n pour numéro de Gödel, d(x) est le numéro de Gödel de
 * l'expression E{n}[n]. Elle est trivialement arithmétique. *)

(* La formule "d x y" est vraie ssi d(x)=y *)
let d x y =
  r x x y
;; 

(* Pour tout ensemble de nombres A, on désigne par A* l'ensemble de tous les
 * entiers n tels que d(n) soit dans A. On a alors une proposition intéressante
 * : si A est arithémtique, alors A* l'est aussi. En effet, si F(v1) est une
 * formule qui exprime l'ensemble A, A* est exprimé par la formule suivante
 * (dépendant de la variable vi) "\/v1 ((d(vi)=v1) => (F(v1)))", où vi est une
 * variable n'apparaissant pas dans F (là encore, je ne suis pas d'accord avec
 * l'ouvrage sur lequel je me base).
 *
 * La proposition précédente en implique une autre qui va nous fournir le
 * dernier outil dont nous avons besoin pour exhiber l'énoncé indédicable de
 * Gödel : pour tout ensemble arithmétique A, il existe un énoncé de Gödel pour
 * A. En effet, comme A* est aussi arithmétique, on peut trouver une formule
 * H(v1) qui l'exprime. Soit h le numéro de Gödel de cette formule. Alors la
 * formule H[h], qui s'écrit "\/v1 ((v1=h) => H)". Alors H[h] est vraie si et
 * seulement si h appartient à A*, donc si et seulement si d(h) appartient à A.
 * Mais comme d(h) est le numéro de Gödel de H[h], H[h] est un énoncé de Gödel
 * pour A.
 *
 * Soit P(v1) la formule "estProuvable v1". Elle exprime l'ensemble des
 * propositions démontrables de P.A. La formule ~P(v1) exprime donc le
 * complémentaire de PE dans l'ensemble LE des expressions de P.A. D'après ce
 * qu'on vient de voir, on peut trouver une formule H(v1) exprimant l'ensemble
 * (LE\PE)* : sa diagonalisation H[h] est un énoncé de Gödel pour l'ensemble PE.
 *
 * Et la magie apparaît : H[h] est donc vrai si et seulement si H[h] n'est pas
 * prouvable dans P.A. Comme P.A. est un système que l'on a supposé correct,
 * H[h] est nécessairement vrai. Puisqu'il est vrai, il est non prouvable dans
 * P.A., ce qui achève la démonstration.
 *
 * Puisqu'on n'a pas fait tout ce code CamL pour rien, on va quand même écrire
 * cette proposition. Soit "var 0" le nombre h ; on pourrait exhiber de manière
 * précise ce nombre mais pour le coup, ça serait franchement monstrueux. *)

let v1 = -1 ;;
let v2 = -2 ;;

let propositionIndecidable =
  pt v1 (((var v1) === (var 0))
           ==> (pt v2 ((d (var v1) (var v2))
                         ==> ( ~~~ (estProuvable (var v2))))))
;;

imprimeFormule propositionIndecidable ;;

let log10 n =
  let renvoi = ref 1 in
  let hop = ref 10 in
  while !hop < n do
    incr renvoi;
    hop := !hop * 10
  done;
  !renvoi
;;

let rec tailleTerme = function
  | Variable v -> 4
  | Nombre n -> log10 n
  | Addition (a,b) -> 3 + (tailleTerme a) + (tailleTerme b)
  | Multiplication (a,b) -> 3 + (tailleTerme a) + (tailleTerme b)
  | Exponentiation (a,b) -> 3 + (tailleTerme a) + (tailleTerme b)
  | Successeur a -> 1 + (tailleTerme a)
;;

let rec tailleFormule = function
  | Egal (t1,t2) -> 5 + (tailleTerme t1) + (tailleTerme t2)
  | InferieurOuEgal (t1,t2) -> 6 + (tailleTerme t1) + (tailleTerme t2)
  | Negation f -> 1 + (tailleFormule f)
  | Implication (f1,f2) -> 6 + (tailleFormule f1) + (tailleFormule f2)
  | PourTout (v,f) -> 1 + (tailleTerme (var v)) + (tailleFormule f) 
;;

let tf = tailleFormule ;;