Метатеоре́ма — логічне твердження про формальну систему, доведене метамовою. На відміну від теорем, доведених у рамках даної формальної системи, метатеорема доводиться в рамках метатеорії і може посилатися на поняття, які присутні в метатеорії, але не в .Столл, Роберт Р. Множества. Логика. Аксиоматические теории. — , Просвещение, 1968. — с. 183Метатеорема // Математический энциклопедический словарь. — , Советская энциклопедия, 1988. — с. 364
Формальна система визначається формальною мовою і дедуктивною системою (аксіомами і правилами висновування). Формальну систему можна використати для доведення конкретних речень формальної мови за допомогою цієї системи. Метатеореми, однак, доводяться зовні відносно розглянутої системи, в її метатеорії. Загальні метатеорії, що використовуються в логіці, — це теорія множин (особливо в теорії моделей) і (особливо в теорії доведень). Замість того щоб демонструвати доказовість конкретних речень, метатеорема може показати, що кожне з широкого класу речень можна довести, або показати, що деякі речення довести неможливо.
Приклади Прикладами метатеорем є:
Теорема про дедукцію для логіки першого порядку каже, що речення вигляду доказове з набору аксіом «A» тоді й лише тоді, коли речення доказове зі системи, аксіоми якої складаються з і всіх аксіом «A». Теорема про існування класів теорії множин фон Неймана — Бернайса — Геделя каже, що для кожної формули, квантори якої варіюються тільки за множинами, існує клас, що складається зі множин, які задовольняють формулі. Доведення несуперечливості таких систем, як арифметика Пеано.
Див. також
Метаматематика
Примітки
Література Geoffrey Hunter (1969), Metalogic. Alasdair Urquhart (2002), «Metatheory», A companion to philosophical logic, Dale Jacquette (ed.), p. 307
Посилання Метатеорема в Енциклопедії математики