Метатеорема

Метатеоре́ма — логічне твердження про формальну систему, доведене метамовою. На відміну від теорем, доведених у рамках даної формальної системи, метатеорема доводиться в рамках метатеорії і може посилатися на поняття, які присутні в метатеорії, але не в теорії об'єктів^[en].^[1][2]

Формальна система визначається формальною мовою і дедуктивною системою (аксіомами і правилами висновування). Формальну систему можна використати для доведення конкретних речень формальної мови за допомогою цієї системи. Метатеореми, однак, доводяться зовні відносно розглянутої системи, в її метатеорії. Загальні метатеорії, що використовуються в логіці, — це теорія множин (особливо в теорії моделей) і проста рекурсивна арифметика^[en] (особливо в теорії доведень). Замість того щоб демонструвати доказовість конкретних речень, метатеорема може показати, що кожне з широкого класу речень можна довести, або показати, що деякі речення довести неможливо.

Приклади

Прикладами метатеорем є:

• Теорема про дедукцію для логіки першого порядку каже, що речення вигляду ${\displaystyle \varphi \rightarrow \psi }$ доказове з набору аксіом «A» тоді й лише тоді, коли речення ${\displaystyle \psi }$ доказове зі системи, аксіоми якої складаються з ${\displaystyle \varphi }$ і всіх аксіом «A».
• Теорема про існування класів теорії множин фон Неймана — Бернайса — Геделя каже, що для кожної формули, квантори якої варіюються тільки за множинами, існує клас, що складається зі множин, які задовольняють формулі.
• Доведення несуперечливості таких систем, як арифметика Пеано.

Див. також

• Метаматематика
• Відмінність між використанням і згадуванням^[en]