Logique du premier ordre et fonctions

[Clise]

Bonjour,

J'aimerais savoir s'il est possible de construire des "fonctions récursives" dans le langage de la logique du premier ordre et si non, pourquoi.

Par exemple, je me place de le système formel de Peano (moins l'axiome d'induction pour ne pas être dans du second ordre) i.e un système formel où l'addition la multiplication et < sont définis par des axiomes. Donc, si je veux définir la fonction d'exponentiation, est ce que je peux le faire de la manière suivante :
est une fonction binaire du système formel et satisfait l'axiome suivant :


Est ce valide ? sinon comment faire ?

Merci pour vos réponses.

[Doraki]

Tu refuses l'axiome d'induction mais est-ce que tu acceptes le schéma d'induction ? (c'est une infinité d'axiome à la place d'un axiome du 2nde ordre)
De toutes façons, l'induction t'en as besoin seulement pour démontrer des formules, pas pour faire des définitions.

Pour définir l'exponentiation, là tu as rajouté son symbole dans le langage et t'as rajouté un axiome à ta théorie.
Tu as défini une extension de l'arithmétique de Peano.
(d'ailleurs dans l'arithmétique de peano que je connais, < n'est pas dans le langage, mais il est facilement définissable)
L'inconvénient c'est que en faisant ça tu risques (bon ok faut vraiment que tu te gourres pour que ça arrive) d'obtenir un système incohérent où tu peux prouver n'importe quoi (ce qui n'est pas très utile en soi).

Une vraie définition de l'exponentiation dans l'arithmétique de Peano ce serait donner une formule P(x,y,z) qui soit vraie lorsque x^y = z.
Un tel prédicat existe mais il est pas aussi simple qu'on aimerait qu'il soit :
Ca ressemble à un truc du style "il existe un nombre qui est le codage d'une preuve de x^y = z" où la notion de preuve de x^y = z repose sur ta définition de l'exponentiation.
Le codage est super laid et t'obtiens une formule qui cache l'algorithmique de l'exponentielle derrière plein de trucs arithmétiques.

Ensuite, on aimerait par exemple montrer des théorèmes sur ce prédicat.
Sans schéma d'induction, tu ne pourras pas montrer que ce prédicat représente une fonction.
Une fois que t'as fait ça tu peux montrer que cette fonction vérifie les propriétés que t'as donnés (x^0 = 1 et x^(y+1) = x*x^y) mais l'induction est indispensable pour montrer que c'est une fonction.

D'ailleurs je crois que c'est comme ça qu'on montre la cohérence relative de l'arithmétique de peano et de l'arithmétique de peano + fonction exponentielle avec ton axiome qui va avec.

En fait, l'induction est indispensable pour montrer quoi que ce soit avec les codages de Gödel parcequ'il faut faire marcher la mécanique derrière le codage et ça m'étonnerait qu'on puisse faire grand chose sans induction. Genre 2^3 = 8, ça va, mais quoi que ce soit d'autre, bof.

L'arithmétique est suffisemment puissante pour pouvoir exprimer de cette manière toutes les fonctions calculables. Pas seulement l'exponentielle, mais aussi la fonction d'ackermann, la prouvabilité dans l'arithmétique de peano etc etc. Le truc dur c'est de montrer que ce sont des effectivement des fonctions et surtout de montrer qu'elles sont totales (enfin quand c'est possible).

[Doraki]

Par exemple,


où désigne


Avec ça tu as une formule Exp qui vérifie les propriétés de l'exponentielle mais démontrer quoi que ce soit dessus demande d'avoir droit à l'induction.

[Clise]

Merci pour tes réponses.

Je ne suis pas sure de bien comprendre en quoi

Par exemple,


où désigne

définit l'exponentielle ... Peut être ai je simplement du mal a lire ceci. :briques:

Sinon, pour l'axiome d'induction, oui je suis d'accord. De plus, la page wikipedia en anglais sur les axiomes de Peano (http://en.wikipedia.org/wiki/Peano_axioms) dit que "The induction schema consists of a countably infinite set of axioms. For each formula (x,y1,...,yk) in the language of Peano arithmetic, the first-order induction axiom for is the sentence



where is an abbreviation for y1,...,yk. The first-order induction schema includes every instance of the first-order induction axiom, that is, it includes the induction axiom for every formula ."

Est ce bien la même chose que ton "infinité d'axiome à la place d'un axiome du 2nde ordre" ? J'avoue que, étant débutante en logique, j'ai un peu de mal a me représenter une "infinité d'axiomes"... :marteau:

[Doraki]

Oui, c'est une infinité d'axiome.
Mais ça ne pose pas de problème parceque ça reste facile de savoir si une formule donnée est un axiome ou pas.

C'est normal que ce soit dur de comprendre pourquoi cette formule définit l'exponentielle parceque ce n'est pas du tout une transcription directe de la définition par induction de la fonction. Au contraire elle utilise des résultats non triviaux d'arithmétique pour fonctionner.

Pour pouvoir dire "exp(x,y,z) := il existe une suite z0...zy telle que z0=1,zy = z, et pour tout i, z(i+1) = x * zi" il faut être d'ordre 2.
Mais comme l'arithmétique est suffisement expressive pour encoder n'importe quel processus calculable, il y a des moyens tordus de simuler ça tout en restant dans le 1er ordre.

En l'occurence ici tu as besoin d'un truc pour encoder les suites finies d'entiers dans seulements quelques nombres, et c'est là que t'as besoin d'arithmétique.
Dans mon exemple, je dis que (p,m) est le code de la suite (zi) avec zi = p modulo 1+(i+1)*m.
C'est laid mais ça marche, pour chaque suite (zi) de (y+1) entiers il y une infinité de paires (p,m) qui permettent de retrouver les (zi) de cette manière.