Метатеорема

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

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

Приклади

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

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

Див. також

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

Примітки

1. Столл, Роберт Р. Множества. Логика. Аксиоматические теории. — М., Просвещение, 1968. — с. 183
2. Метатеорема // Математический энциклопедический словарь. — М., Советская энциклопедия, 1988. — с. 364

Література

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

Посилання

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