Modélisation des preuves formelles

Congru
Modifié (November 2023) dans Fondements et Logique
Bonjour
Un langage du premier ordre $\mathcal L$ étant donné, je cherche à savoir quels sont les formalisations connues de "l'ensemble des démonstrations des formules de $\mathcal L$" (en déduction naturelle) comme structure sur un langage $\mathcal W$ (à fournir) du premier ordre.
Merci d'avance.

Réponses

  • Qu'est-ce qu'un langage du premier ordre ? Logique du premier ordre, je vois bien ce que c'est, mais langage du premier ordre ? Voulez-vous parler de $\mathcal L_{\omega, \omega}$
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Bonjour @Médiat_Suprème , je veux dire "symboles de constante; symboles de fonction, symboles de relation".
  • Congru
    Modifié (November 2023)
    La réponse "je n'en connais pas" est acceptable aussi (si elle vient d'un logicien, pour des raisons évidentes).
    Edit. Merci quand même.
  • Bonjour @Congru ,
    Je ne suis pas sûre que ma réponse soit celle de ta question mais, une preuve d'une formule $\psi$ sur $\mathcal{L}$ en déduction naturelle est un arbre tel que :  
    1) les nœuds sont des couples $(\Gamma,\varphi)$ où $\varphi$ est une formule sur $\mathcal{L}$ et $\Gamma$ est un ensemble fini de formules sur $\mathcal{L}$.
    2) les arêtes entre les nœuds sont étiquetées par des règles de $NK1$
    3) la racine est $\psi$
    Tu peux donc voir l'ensemble des démonstrations valides de formules de $\mathcal{L}$ comme un langage d'arbre sur l'alphabet des couples $(\Gamma,\varphi)$. Tu peux gérer les arêtes (indicées sur le langage des règles de $NK1$) comme un second langage pour étiqueter l'arbre ou créer artificiellement des nœuds pour tes arêtes (mais la seconde solution est très moche).
  • Congru
    Modifié (November 2023)
    Bonjour @Heuristique,
    merci pour ta réponse. En ce qui concerne la notion d'arbre, je trouve que l'approche classique en mathématiques n'est pas adéquate. Il est possible d'utiliser une autre approche qui se rapproche de celle utilisée en informatique lors de la définition du type "arbre"...
    Une preuve formelle est censée être un objet mathématique, mais les outils utilisés pour la modélisation de cette notion ne sont pas les bons, et n'aident pas à la manipulation de cette notion. J'ai "eu l'idée" de modéliser les preuves formelles de telle sorte à en faire des structures du premier ordre car leur "définition" classique en tant qu'arbre me poussait vers cette direction.
    Je procède ainsi:
    1. Je crée un langage fonctionnel $\mathcal L _1$ dont les symboles de fonctions sont les règles de la déduction naturelle qui auront pour arité dans ce langage leur arrité en tant que règles. Les termes clos de $\mathcal L _1$ seront notés $P_1$
    2. J'interprète les symboles de fonction de $\mathcal L _1$ de façon appropriée $\iota$.  $(P_1;\iota )$ une $\mathcal L _1$-structure, et l'ensemble des preuves est tout simplement la sous-structure de $(P_1;\iota )$ engendrée par l'ensemble vide.
    Edit. On est bien d'accord que cette modélisation (même si je n'ai pas tout précisé) n'est pas connue ?
  • Tout dépend quelle définition d'arbre tu utilises. Ici, mieux vaut prendre celle récursive (un arbre est soit vide, soit constitué d'un noeud et d'une liste de sous-arbres) que la caractérisation connexe acyclique.
    Si je ne dis pas de bêtise, ta formulation par les termes d'un langage fonctionnel correspond justement à des arbres, les noeuds étant constitués des symboles de fonctions.
  • Congru
    Modifié (December 2023)
    Merci @Heuristique t'es le seul qui ait pris le temps de me répondre. Merci encore.
    J'avais lâché le forum car j'avais l'impression d'être boycotté. Mais bref qu'importe, boycotté ou non, ce n'est pas grave.
    Je suppose que tu voulais écrire "un arbre est soit une feuille, soit constitué d'un nœud et d'une liste de sous-arbres".
    Cette définition, je ne l'ai jamais vue dans un livre de mathématique (même si c'est la définition que je préfère), je ne l'ai vu que dans des livres d'informatique. Et tu as raison sur le fait que termes d'un langage du premier ordre c'est une autre façon de parler d'arbres.
    Edit. J'avais oublié @Médiat_Suprème , désolé.
  • Une preuve est une liste $A_1,...,A_n$ où pour tout $k\leq n$, $A_k$ est un axiome, ou il existe $i,j < k$ tels que $A_j = A_i \Rightarrow A_k$.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Congru
    Modifié (December 2023)
    Bonjour @Foys
    La définition avec les listes ne me convenait pas trop. Notamment à cause de la difficulté à montrer qu'une liste est une démonstration (s'il n'y a rien qui indique quand on a utilisé le modus ponens ou la généralisation).
  • @Congru On peut annoter la liste ("modus ponens avec la ligne 7 et la ligne 12"; "généralisation de la ligne 34"). Ou simplement reconnaître la forme des formules envisagées (cela rendrait l'algorithme qui vérifie la validité de la preuve moins performant cela dit).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Congru Je préfère ma version de définition récursive, la tienne ne considérant pas l'arbre vide. Une feuille (donc un arbre réduit à un nœud ) est représentée chez moi par Nœud( f , [ ] ). Ma définition initialise à 1, la tienne à 0.
    On peut relancer le débat sur les maths et l'info. Mon espoir est, qu'un jour, ces 2 disciplines se parlent davantage et que chacune utilise les connaissances de l'autre pour mieux se comprendre elle-même. Je qualifie donc bon nombre de livres d'informatique de livre de maths car bon nombre de mathématiciens qui liraient un tel livre découvrirait une branche des maths qui leur est inconnue.
  • Congru
    Modifié (December 2023)
    Merci à @Foys et @Heuristique, désolé de mon absence prolongée.
    @Heuristique, je suis d'accord avec toi sur le fait que beaucoup de mathématiciens découvriraient une branche des maths qu'ils ne connaissent pas s'ils lisaient des livres d'informatique.
  • Congru
    Modifié (December 2023)
    @Heuristique ta définition d'arbres correspond au cas particulier du mien où il n'y a qu'un symbole de fonction d'arité $0$. Dans ma définition, il y a au moins un symbole de fonction d'arité $0$, ces symboles sont ce que j’appelle les feuilles.
    Correctif. Je crois que je dis une bêtise, dans ta formulation des arbres, les nœuds ne semblent pas être d'une arité précise, sauf l'arbre vide dont l'arité est $0$, les autres semblent avoir des arités variables. Dans ma formulation qui utilise les termes d'un langage du premier ordre, chaque nœud a une arité précise.
  • Oui pardon, je vais clarifier mon propos. Je parlais de la définition d'arbres de manière générale, où aucune arité n'est fixée. Dans le cas des arbres représentant des termes de la logique du premier ordre, les nœuds ont effectivement une arité précise et l'arbre vide n'est pas un terme.
Connectez-vous ou Inscrivez-vous pour répondre.