Logique et métalogique

Sherwyn

Bonjour !
Quand on énonce "A implique B logiquement si et seulement si A->B est une tautologie", alors on est en train d'émettre une proposition sur la logique qu'on est en train d'étudier. Du coup, prouver cette proposition requiert l'utilisation d'une métalogique. Néanmoins, puisque la métalogique est elle-même un recueil de propositions et de règles d'inférences, alors on pourrait également émettre la même proposition depuis ses confins, ce qui fait qu'on aurait besoin d'une métamétalogique pour pouvoir la démontrer, etc ... ad infinitum.
Tout ça est normal ou est-ce qu'il y a un truc qui m'échappe ? 

Foys

Une démonstration est un cas particulier de programme informatique (Curry Howard). Les grands théorèmes de théorie de la démonstration sont essentiellement des programmes informatiques qui transforment des programmes informatiques en d'autres.

Médiat_Suprème

@Sherwyn, 3 remarques : 
1) on peut considérer que les mathématiques sont de la logique appliquée (rien de méprisant, mais je me doute que certains se sentiront, à tort, insultés), la logique, elle, est de la métalogique appliquée, la métalogique est de la métamétalogique appliquée, ad infinitum.

2)Il est impossible d'écrire un dictionnaire dont chaque mot ne serait défini qu'à l'aide des précédents (ordre non lexicographique), c'est un problème de type "moteur immobile".

3) Si on considère le Trilemme de Münchhausen, il me semble que deux cas peuvent être éliminés pour décrire cette situation.