ЛОГИКО-МАТЕМАТИЧНИ ИЗЧИСЛЕНИЯ
приложно смятане, - формализиране на математически. теории. L.-m. и. е зададен на собствения си език и списък с постулати (тези елементи формират синтаксиси в повечето случаи се доставя семантика.
Основните характеристики, които отличават L.-m. и. от аксиоматичен. Теориите на традиционната математика са: 1) идентификация на използваните логически теории. означава чрез формулиране на всички аксиоми и правила за извод, позволява да се изведе едно съждение от друго; 2) преходът от говорим език към точен официален език. Обикновено L.-m. и. изграден въз основа на определена логическо смятане (основно логическо смятане). Езикът на Л.-м. и. се получава от езика на тази логика. смятане чрез добавяне на символи за специални функции и предикати (и може би премахване на предикатни променливи и променливи за функции). Списъкът с постулатите на L.-m. и. получени чрез добавяне към списъка на постулатите на основната логика. смятане (разбирано във връзка с нов език) на определени постулати, описващи свойствата на добавените функции и предикати. Например, езикът на теорията на елементарните групи се получава по тази схема от езика на класиката. предикатно смятане с равенство: символите (умножение), inv (инверсия) и e (едно) се добавят и всички предикатни символи с изключение на равенството се изхвърлят. Допълнителен постулат
гласи че д - групова единица, inv (x) - обратното на x и умножението е асоциативно.
L.-m. - функтор (чийто номер в някаква предварително определена номерация на разглеждания клас е равен на t). Постулатите на -deletion и -introduction са модифицирани:
Добавя се аксиомата !т, Където т - субект променлива или константа, както и аксиоми на формата
Използва се и L.-m. и. за описване на изчислими функционални функции от различен тип: 0 е тип (обектите от тип 0 са естествени числа); ако s и t са типове, т.е. тип (на операции, обработващи обекти от тип и обекти от тип t). Това са окончателни типове (вж. Теория на видовете). Разглеждат се и трансфинитни типове. За всеки тип са посочени променливи и константи от този тип, които обикновено включват операционен символ, всички стойности на които са равни на O, както и обект от тип „За всеки s често е включен примитивен рекурсионен оператор в броя на константите на типа. Извикват се термини от тип s. променливи и константи от тип a, изрази на формата r (s), където r е термин от тип s - термин от тип t, както и израз на формата, който се интерпретира като обозначение на функционал, който обработва xv r (x), където -тип b, xtype a и без квантор L.-M. и. за функционали от краен тип се използват математически. изучаване на квантор L.-m. и. По-специално, използвайки система без квантификатор на примитивни рекурсивни функционали, е възможно да се докаже последователността на формалната аритметика; добавяне на оператор т.нар. баровата рекурсия ви позволява да докажете последователността на формализирания анализ.