Base de donnée mathématique

[danslideal]

Je me demande : existe il une base de donnée mathématique, organisé comme suit :

chaque "affirmation" serait associé à une suite de déduction clair et précise. De sorte qu'on puisse y voir clair, à savoir sur quelle axiome, repose tel ou tel proposition.
Il y aurait seulement comme "principe de base", la comparaison, les axiomes tel que

"x" = "x" quelque soit x

et la remplaçabilité

si x est variable avec conditions alors

"expression(x)" => "expression(y)"

quelque soit y dans les conditions..


Je suis sur que ça ne serait pas si difficile à développer !
-----

[Matmat]

Je crois qu'on peut voir toute base de donnée relationnelle comme cela.

par exemple avec:
une table des villes par pays ( id : code ville ),
une table d'adresses ( id: code adresse ),
une table de personalités ( id : code personnalité )

la table des personnalités contient un code adresse, la table des adresse contient un code ville.

Ici, les proposition ne sont rien d'autres que des résultats de requêtes et :

la vérité (ou la fausseté) de la proposition "Einstein habite Berne" est décidée par une jointure sur le code adresse entre la tables des personnalités et la table des adresse.

la vérité (ou la fausseté) de la proposition "berne est en Suisse" est décidée par une jointure sur le code ville entre la table des adresses et la tables des villes par pays.

ET La déduction "Einstein habite Berne" => "Einstein habite en Suisse"
est donc décidée par les deux jointures précédentes, une suite de déductions n'est qu'une suite de jointures ...En définitive c'est les jointures qui déterminent sur quelle propositions élémentaires reposent telle ou telle proposition.

[danslideal]

Je crois qu'on peut voir toute base de donnée relationnelle comme cela.

par exemple avec:
une table des villes par pays ( id : code ville ),
une table d'adresses ( id: code adresse ),
une table de personalités ( id : code personnalité )

la table des personnalités contient un code adresse, la table des adresse contient un code ville.

Ici, les proposition ne sont rien d'autres que des résultats de requêtes et :

la vérité (ou la fausseté) de la proposition "Einstein habite Berne" est décidée par une jointure sur le code adresse entre la tables des personnalités et la table des adresse.

la vérité (ou la fausseté) de la proposition "berne est en Suisse" est décidée par une jointure sur le code ville entre la table des adresses et la tables des villes par pays.

ET La déduction "Einstein habite Berne" => "Einstein habite en Suisse"
est donc décidée par les deux jointures précédentes, une suite de déductions n'est qu'une suite de jointures ...En définitive c'est les jointures qui déterminent sur quelle propositions élémentaires reposent telle ou telle proposition.

Je n'ai pas dit le contraire (encore que les bases de donnée relationnel sont rarement utiliser pour générer des séries de propositions)..
L'idée c'est d'en faire un site, de façon à ce qu'à chaque affirmation, théoréme, on est tout de suite la démonstration formel et précise sous les yeux, garanti par le fonctionnement stricte du logiciel.

Qu'on puisse naviguer d'une proposition à l'autre etc..
Quelque chose qui ressemble au macros du c++ pour ceux qui connaissent.

ça permettrait de minimiser l'erreur humaine..

[danslideal]

Un exemple de jusqu'ou ça peut aller:

On peut justifier
f) "4+5=9"
par

a) "4=succ(succ(succ(succ(0)) ))"
b) "5=succ(succ(succ(succ(succ(0) ))))"
c) "9=succ(succ(succ(succ(succ(su cc(succ(succ(succ(0)))))))))"
d) "succ(a)+b=a+succ(b)" avec a et b variable
e) "0+a=a" avec a variable

En faisant uniquement des "rechercher/remplacer", on arrive à démontrer f) à partir de a) b) c) d)e)..

L'idée est de trouver les raisonnement minimaux que l'ordinateur pourra vérifier de façon infaillible, sans qu'aucun "instinct" ne soit plus nécessaire.

La multiplication
g) "succ(a)*b=a*b+b" avec a et b variable
h) "a*0=0" avec a et b variable

Aprés la vérifiction ne serait plus qu'une exploration de graphe (certe, rapidement extrêmement vaste)

[A voir en vidéo sur Futura]

[danslideal]

Excusez moi, je viens d'apprendre qu'un raisonnement applicable à tout les éléments d'un ensemble était sois disant non généralisable à "tout" les éléments de l'ensemble
(ça n'a tellement pas de sens qu'on a du mal à l'écrire ! )

- "pour tout x dans E"
serait différent de
- "pour y, quelque soit y dans E"

Oubliez les mathématiques, on vous a menti !