Метатеорема

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

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

Приклади

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

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

Див. також

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

Література

• Geoffrey Hunter (1969), Metalogic.
• Alasdair Urquhart (2002), «Metatheory», A companion to philosophical logic, Dale Jacquette (ed.), p. 307

Посилання

• Метатеорема в Енциклопедії математики (англ.)
• Маргарита Баріл Метатеорема(англ.) на сайті Wolfram MathWorld.