1. Le joueur A retire 2 allumettes, il en reste 8
2. Le joueur B retire 1 allumettes, il en reste 7
3. Le joueur A retire 3 allumettes, il en reste 4
4. Le joueur B retire 2 allumettes, il en reste 2
5. Le joueur A retire 2 allumettes, il n'en reste plus, le joueur A a gagné.

Afin de bien mieux comprendre le système formel en question, nous ferons souvent référence au parallèle avec le jeu des allumettes.
Néanmoins, il doit être bien compris que le système formel en lui même n'a aucun sens. C'est nous qui choisissons de lui en attribuer un, qui signifie quelque chose pour nous.

Le vocabulaire de notre système sera les lettres A,B et les nombres entiers. Une formule correcte de notre système sera de la forme : "lettre lettre entier". Par exemple, AB14 et BB3 sont des formules bien formées, alors que 4B12 n'est pas une formule.

On peut trouver une signification à ces formules. Convenons que la formule AB12 signifie le joueur A peut gagner de façon sûre si c'est au joueur B de jouer et qu'il reste 12 allumettes. De la même façon, la formule BB6 signifiera : le joueur B peut gagner de façon sûre si c'est au joueur B de jouer et qu'il reste 6 allumettes.

Chacune de ces formules peut être vraie ou fausse. Nous verrons plus loin que la formule AA10 est vraie. En effet, le joueur A peut gagner de façon sûre si c'est à lui de jouer et qu'il reste 10 allumettes. Par contre, la formule AA8 est fausse, car le joueur 1 ne peut pas gagner de façon sûre si c'est à lui de jouer et qu'il reste 8 allumettes.

Dans ce jeu, les formules ont une négation. Cela signifie qu'à toute formule on peut en associer une autre de façon à ce que si l'une est fausse, l'autre soit vraie et inversement.
En effet, pour une position donnée (un nombre d'allumettes x et le nom du joueur (A ou B) qui va jouer), un des deux joueurs a forcément la possibilité de gagner. Ainsi, si ABx est vraie c'est que BBx est fausse, et si AAx est fausse c'est que BAx est vraie.

Comment déduire d'une formule vraie une autre formule vraie ? On voit bien que si AB16 est vraie, alors AA17 l'est aussi, car : Si A gagne alors que c'est à B de jouer et qu'il reste 16 allumettes, alors A gagne aussi si c'est à lui de jouer et qu'il en reste 17 (car il lui suffit d'en enlever une).
Voici la liste des règles d'inférence de notre système (n remplace n'importe quel entier):

1. ABn => AAn+1
2. ABn => AAn+2
3. ABn => AAn+3
4. ABn => ABn+4
5. BAn => BBn+1
6. BAn => BBn+2
7. BAn => BBn+3
8. BAn => BAn+4

Nous devons trouver les vérités de base de notre système. On peut les choisir arbitrairement, mais si on veut obtenir des formules qui signifient toujours quelque chose par rapport au jeu, il faut que nos axiomes soient vrais dans le jeu : AB4 et BA4 sont de bons axiomes, effectivement vrais dans le jeu, car le joueur A gagne forcément si c'est au joueur B de jouer et qu'il reste 4 allumettes et de même le joueur B gagne forcément si c'est au joueur A de jouer et qu'il reste 4 allumettes.

Partant des axiomes et du système formel, on peut déduire un certain nombre de formules.

Par exemple, AB4 et vrai (c'est un axiome) donc AA5 est vraie aussi (en utilisant la règle 1), AB8 est vraie aussi (en utilisant la règle 4). On peut aussi enchaîner les règles : BA4 => BA8 => BB10

Avec nos 2 axiomes de base, et nos 8 règles d'inférence, nous pouvons ainsi déduire plusieurs formules (théorèmes), qui nous donnent pour l'ensemble des configurations de plus de 4 allumettes le nom du joueur gagnant.

À l'aide d'un ordinateur, on peut s'affranchir du côté mécanique du système formel pour qu'il applique systématiquement les 8 règles à l'ensemble des théorèmes lorsque c'est possible.
Partant des 2 axiomes de base, et en appliquant les règles applicables à chacun d'eux, il démontre les 8 formules suivantes : AA5, AA6,AA7, AB8, BB5, BB6, BB7, BA8
Puis en réappliquant les règles (quand c'est possible) à nos 8 nouveaux théorèmes, la machine peut démontrer 8 nouveaux théorèmes, et ainsi de suite, car le processus ne s'arrête jamais.

Nous avons vu que les formules possédaient des négations. la négation de AA5 (notée non(AA5)) est BA5. En effet, soit l'un soit l'autre des joueurs a la possibilité de gagner de façon sûre dans n'importe quelle configuration. Choisissons une formule (par exemple AB7654) de notre système, et attendons infiniment longtemps (en théorie) pour voir si l'ordinateur la démontre. Quatre cas peuvent se présenter :

1. Il démontrera AB7654 et pas BB7654 (la négation de AB7654)
2. Il démontrera BB7654 , et pas la formule AB7654
3. Il démontrera la formule AB7654 et la formule BB7654
4. Il ne démontrera ni AB7654 , ni BB7654

Les 2 premiers cas ne posent pas de problème. En revanche, si le troisième se présentait nous pourrions dire que le système est inconsistant. En effet, il permet de démontrer une chose et son contraire. Il est bien évident que dans toute configuration (ici B7654) il est impossible que les 2 joueurs aient une stratégie gagnante à la fois...
Le quatrième cas pose aussi un problème. Si vous étudiez mieux le jeu, vous verrez facilement que dans toutes configuration, un des joueurs a une stratégie gagnante. Par conséquent, nous savons que soit AB7654, soit BB7654 est vraie (en l'occurrence, c'est AB7654). Si le quatrième cas se présentait, nous pourrions dire que le système formel est incomplet, car il existerait certaines vérités qu'il ne permet pas de démontrer.

Bien entendu, dans notre exemple simple, le système est en fait consistant et complet, c'est à dire qu'il ne permet pas de démontrer une chose et son contraire, et qu'il permet de démontrer toutes les formules qui sont vraies.

Mais il n'en est pas de même pour tous les systèmes. Le travail de Gödel a consisté à démontrer que dans les systèmes formels suffisament complexes pour contenir l'arithmétique :

• on ne peut pas simplement démontrer la consistance ;
• si le système formel est consistant, alors il est incomplet