Objets bien formésdit

Si une collection d’objets (symboles et séquences de symboles) doit être considérée comme « bien formée », un algorithme doit exister pour déterminer, en s’arrêtant par une réponse « oui » ou « non », si l’objet est bien formé ou non (en mathématiques, un wff abrège une formule bien formée). Cet algorithme, à l’extrême, peut nécessiter (ou être) une machine de Turing ou une machine équivalente à Turing qui « analyse » la chaîne de symboles présentée sous forme de « données » sur sa bande; avant qu’une machine de Turing universelle puisse exécuter une instruction sur sa bande, elle doit analyser les symboles pour déterminer la nature exacte de l’instruction et/ou de la donnée qui y est codée. Dans les cas plus simples, une machine à états finis ou un automate pushdown peut faire le travail. Enderton décrit l’utilisation d' »arbres » pour déterminer si une formule logique (en particulier une chaîne de symboles avec des parenthèses) est bien formée. Église Alonzo 1934 décrit la construction de « formules » (encore une fois: séquences de symboles) comme écrit dans son λ-calcul en utilisant une description récursive de la façon de démarrer une formule, puis de construire sur le symbole de départ en utilisant la concaténation et la substitution.

Exemple: Church a spécifié son λ-calcul comme suit (ce qui suit est une version simplifiée laissant de côté les notions de variable libre et de variable liée). Cet exemple montre comment une théorie des objets commence par une spécification d’un système d’objets de symboles et de relations (en particulier par utilisation de la concaténation de symboles) :

(1) Déclare les symboles : {, },(,), λ, plus un nombre infini de variables a, b, c,…, x, … (2) Définir la formule: une séquence de symboles (3) Définir récursivement la notion de « formule bien formée » (wff) en commençant par la « base » (3.i):

• (3.1)(basis) Une variable x est un wff
• (3.2) Si F et X sont des wff, alors {F}(X) est un wff ; si x se produit dans F ou X alors on dit qu’il s’agit d’une variable dans {F}(X).
• (3.3) Si M est bien formé et que x se produit dans M alors λx est un wff.

(4) Définir diverses abréviations:

• {F} abréviation de F(X) si F est un symbole unique
• F{\displaystyle {{F}}}
  

  abréviation de {F}(X, Y) ou F(X,Y) si F est un symbole unique

• λx1λx2…] abréviation de λx1x2…xn*M
• λab*a(b) abréviation de 1
• λab*a(a(b)) abréviation de 2, etc.

(5)Définir la notion de « substitution » de la formule N pour la variable x dans M (Church 1936)

Objets non définis (primitifs)

Certains objets peuvent être « indéfinis » ou « primitifs » et recevoir une définition (en termes de leurs comportements) par l’introduction des axiomes.

Dans l’exemple suivant, les symboles non définis seront { ※, ↀ, }}. Les axiomes décriront leurs comportements.

AxiomsEdit

Kleene observe que les axiomes sont constitués de deux ensembles de symboles : (i) les objets indéfinis ou primitifs et ceux qui sont connus précédemment. Dans l’exemple suivant, il est connu précédemment dans le système suivant (O, ※, ↀ, ∫) que O constitue un ensemble d’objets (le « domaine »), ※ est un objet du domaine, and et are sont des symboles pour les relations entre les objets, = > indique l’opérateur logique « SI ALORS », ε est le symbole qui indique « est un élément de l’ensemble O », et « n » sera utilisé pour indiquer un élément arbitraire de l’ensemble d’objets O.

Après (i) une définition de la « chaîne de S »—un objet qui est un symbole ※ ou de symboles concaténés ※, ↀ ou ∫, et (ii) la définition de « bien formé » de chaînes – (base) ※ et ↀS, ∫S où S est une chaîne, viennent les axiomes:

• ↀ※ => ※, en d’autres mots: « SI ↀ est appliquée à l’objet ※ PUIS l’objet ※ résultats. »
• ∫n ε O, en mots « SI ∫ est appliqué à l’objet arbitraire « n » dans O ALORS cet objet ∫n est un élément de O ».
• εn ε O, « SI ↀ est appliqué à l’objet arbitraire « n » en O ALORS cet objet ↀn est un élément de O ».
• ↀ∫n = >n, « SI ↀ est appliqué à l’objetnn ALORS l’objet n résulte. »
• nn=>n, »SI ∫ est appliqué à l’objet ↀn ALORS l’objet n résulte. »

Alors, quelle pourrait être l’interprétation (prévue) de ces symboles, définitions et axiomes?

Si nous définissons ※ comme « 0 », ∫ comme « successeur » et ↀ comme « prédécesseur » alors※ ※=> ※ indique « soustraction appropriée » (parfois désignée par le symbole ∸, où « prédécesseur » soustrait une unité d’un nombre, donc 0 ∸1 = 0). La chaîne « nn = > n » indique que si d’abord le successeur est appliqué à un objet arbitraire n, puis le prédécesseur is est appliqué ànn, les résultats n originaux. »

Cet ensemble d’axiomes est-il « adéquat » ? La bonne réponse serait une question: « Adéquat pour décrire quoi, en particulier? » »Les axiomes déterminent à quels systèmes, définis de l’extérieur de la théorie, la théorie s’applique. » (Kleene 1952:27). En d’autres termes, les axiomes peuvent être suffisants pour un système mais pas pour un autre.

En fait, il est facile de voir que cet ensemble d’axiomes n’est pas très bon — en fait, il est incohérent (c’est-à-dire qu’il donne des résultats incohérents, quelle que soit son interprétation):

Exemple: Définissez ※ comme 0,※※ comme 1 et ↀ1 = 0. À partir du premier axiome,※※ = 0, donc※※ =0 0 = 1. Mais le dernier axiome spécifie que pour tout n arbitraire, y compris ※ = 0, ∫ↀn = > n, donc cet axiome stipule que ∫ↀ0= > 0, pas 1.

Observez également que l’ensemble d’axiomes ne spécifie pas quenn ≠n. Ou, à l’exception du cas n = ※, ↀn ≠ n. Si nous devions inclure ces deux axiomes, nous aurions besoin de décrire les notions intuitives « égales » symbolisées par = et non – égales symbolisées par ≠.