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