ЛОГІКО-МАТЕМАТИЧНІ ЗЛІЧЕННЯ - це
прикладні обчислення - формалізації математич. теорій. Л.-м. в. задається своєю мовою та переліком постулатів (ці елементи утворюютьсинтаксис).і в більшості випадків забезпечуєтьсясемантикою.
Істотними рисами, що відрізняють Л.-м. в. від аксіоматич. Теорії традиційної математики, є: 1) виявлення використовуваних теорій логіч. засобів шляхом формулювання всіх аксіом і виводу правил, що дозволяють виводити одне судження з іншого; 2) перехід від розмовної мови до точноїформальної мови.Зазвичай Л.-м. в. будується з урахуванням нек-рогологічного обчислення(базисного логічного обчислення). Мова Л.-м. в. виходить із мови цього логіч. обчислення додаванням символів спеціальних функцій та предикатів (і, можливо, видаленням предикатних змінних та змінних для функцій). Перелік постулатів Л.-м. в. виходить шляхом додавання до переліку постулатів базисного логіч. обчислення (розумінних стосовно нової мови) деяких постулатів, що описують властивості доданих функцій і предикатів. Напр., мова елементарної теорії груп виходить за цією схемою з мови класич. обчислення предикатів з рівністю: додаються символи (множення), inv (звернення) та е(одиниця), а викидаються всі предикатні символи, крім рівності. Додатковий постулат
стверджує, щое -групова одиниця, inv(x)-елемент, зворотний до x, і множення асоціативно.
Л.-м. - функтор (номер якого в деякій заздалегідь фіксованої нумерації класу, що розглядається, дорівнює t).Постулати -видалення і -введення модифікуються:
Додається аксіома !t,деt -предметна змінна або константа, а також аксіоми виду
Використовуються такожЛ.-м. в. для опису обчислюваних функціоналів різних типів: є тип (об'єкти типу 0 - натуральні числа); якщо s і t – типи, тобто тип (операцій, що переробляють об'єкти типу ав об'єкти типу t). Це - кінцеві типи (див.Типова теорія).Розглядаються також трансфінітні типи. Для кожного типу вказуються змінні і константи цього типу, в їх число зазвичай входить символ операції, всі значення якої рівні О, а також об'єкт типу Для кожного s число констант типу часто включають оператор примітивної рекурсії. Термами типу s зв. змінні та константи типу а, вирази виду r(s), де r - терм типу s - терм типу t, а також вираз виду до-роє інтерпретується як позначення функціоналу, що переробляє хв r(х),де rтипу b, хтипу a та Безкванторні Л.-м. в. для функціоналів кінцевих типів використовують для математич. вивчення кванторних Л.-м. в. Зокрема, за допомогою безкванторної системи примітивно-рекурсивних функціоналів вдається довести несуперечність формальної арифметики; додавання оператора т.з. бар-рекурсії дозволяє довести несуперечність формалізованого аналізу.
Важливе властивість Л.-м. в. - дедуктивна повнота: вона означає, що кожна формула без вільних змінних виводиться або спростовується. Із дедуктивної повноти Л.-м. в. слід розв'язність проблеми виведення - існування алгоритму, що дозволяє за кожною формулою дізнатися, виводиться вона чи ні. Прикладом дедуктивно повного Л.-м. в. є теорія замків алгебри полів (система Тарського). Відповідно доГеделя теоремі про неповнотудедуктивно повні теорії рідкісні: всяке Л.-м. і., що містить деякий дуже вузький фрагмент арифметики, дедуктивно неповно. Для ще ширшого класу Л.-м. в. проблема виведення алгоритмічно нерозв'язна.
Важлива характеристика Л.-м. і.- його виразна здатність. Часто вдається ввести виразні засоби, що не фігурують явно в мові Л.-м. в. Так, у безкванторних мовах вдається запровадити логіч. зв'язки та обмежені квантори:
У мові формальної арифметики можна говорити про кінцеві множини, частково рекурсивні функції і т. д. Одні логіч. зв'язки виражаються через інші; Так було в обчисленнях 2-го порядку (зокрема заснованих на інтуїціоністської логіці) все зв'язки виражаються через напр. еквівалентно Принципові обмеження виразної здатності мови дає теорема Тарського: при природній нумерації формул мови, що містить деякий мінімум арифметики, неможливо вказати формулу Т(х). цієї мови таку, що Т(п). істинно тоді і тільки тоді, коли>п - номер істинної формули. Для Л.-м. і., заснованих на конструктивній (інтуїціоністській) логіці, часто має місце теорема про "розщеплення" диз'юнкцій: з виведення замкнутої формули випливає виведення однієї з формулА, В.Для дослідження структури таких Л.-м. в. застосовуються різні аналоги поняттяреалізованості.Питання несуперечності Л.-м. і., незалежності окремих постулатів, існування відокремлених аксіоматик (тобто таких, що кожна формула, що виводиться, має висновок, що використовує постулати лише для імплікації та символів, що входять до А),існування інтерпретацій одних Л.-м . в. в інших досліджуються вдоказів теорії.
Літ.:[1] Гільберт Д., Берн ай з П., Підстави математики. Логічні обчислення та формалізація арифметики, пров. з ньому., М., 1979; [2] Новіков П. С., Елементи математичної логіки, 2 видавництва, М., 1973; [3] Кліні С. К., Введення в метаматематику, пров. з англ., М., 1957; [4] Черч А., Введення уматематичну логіку, пров. з англ., т. 1, М., I960; [5] Лін до н Р., Нотатки з логіки, пров. з англ., М., 1968.
Математична енциклопедія. - М.: Радянська енциклопедія. І. М. Виноградов. 1977-1985.