Métathéorème, théorème d’ordre 1 ou d’ordre supérieur ?

[Tomlindo]

Bonsoir à tous,
Je poste ici cette question relativement épineuse car, après recherche, je n’ai pas trouvé de réponse satisfaisante à celle-ci…
Alors voilà, je me lance:

Le premier théorème d’incomplétude de Gödel est-il un théorème d’ordre 1, d’ordre 2 ou d’un ordre supérieur encore ? N’est-ce pas un métathéorème ?

Je suis actuellement en L1 de double licence maths/physique, et en ayant parlé avec mon prof d’algèbre qui est logicien de formation, il m’a répondu que c’était un théorème d’ordre 1, sans me donner de justifications suffisantes concernant le fait qu’il ne puisse pas être d’ordre 2 — car nous n’en avions pas le temps! —. Mais, pour autant que je sache sur la logique ordre 2, une formule quantifiant des propositions est une formule d’ordre 2… Par exemple la formule:
\forall P \exists x \exists y P(x,y),
(qui n’est pas une tautologie en prenant P l’antilogie…) ou une formule similaire est décrite sur internet (peut-être sur une page Wikipédia) comme étant d’ordre 2 typiquement. Mais puisque le théorème de Gödel s’énonce ainsi:
\exists P (\neg Dem(P) \wedge \neg Dem(\neg P)),
Il semble être un théorème d’ordre 2… (Pour autant, il semble s’appliquer à des théories de tout ordre logique et est démontré — avec le codage — dans le cadre de la logique d’ordre 1…)

Je dois avouer que je trouve difficilement des documents me permettant de bien saisir toutes les nuances sur les ordres logiques, car dans la totalité des cours de logique qu’il m’a été donné de lire, lesdits ordres sont négligés (considérés comme des considération considérablement secondaires!!!!)

Merci d’avance pour vos réponses… et bonne journée ou soirée !
-----

[Tomlindo]

Finalement, j'ai répondu à mon problème sans trop de difficultés par documentations...
Si ça peut en aider certains, sachez qu'il s'agit simplement ici d'une question liée à une imprécision sur les définitions. La logique d'ordre 2 ne s'applique pas tellement dans ce sens-ci, mais dans un sens plus profond et plus intimement lié à la logique d'ordre 1 encore...
Quant à la métathéorie, si le théorème de complétude de Gödel est un métathéorème pour ceci qu'il affirme sur des objets relevant du métalangage tels que la démontrabilité, il peut en être de même donc sur le premier théorème d'incomplétude de Gödel: on affirme des choses sur des démontrabilités... Cependant, comme il est souvent démontré autour d'une logique d'ordre 1, on dira que c'est un théorème d'ordre 1...