ПОСЛЕДОВАТЕЛНО ИЗЧИСЛЯВАНЕ

ИЗЧИСЛЯВАНЕТО НА ПОСЛЕДОВАТЕЛНОСТТАе една от основните форми на представяне на логическите системи, използвани в логиката заедно с аксиоматичните системи (тип Хилберт) и системите за естествени (естествени) изводи. Терминът "последователност" идва от думата sequent (последователност). Той е въведен в логиката от П. Херц (1929) и е заимстван отГ. Гентцен, който е първият, който формулира класическата и интуиционисткалогика на предикатитеот първи ред под формата на секвенционно смятане.

Секвентът е формална нотация на връзката на логическото извеждане на формата F→Θ, където Г и Θ са последователности (възможно празни) от формули, разделени със запетаи. Вместо стрелка може да се използва "⊢" или друг знак за логическо извеждане. Лявата страна на последователността се нарича антецедент, а дясната страна се нарича последваща. В оригиналната версия на Генцен, секвент означава, че от връзката на формулите, включени в нейния антецедент, дизюнкцията на формулите, включени в нейния сукцедент, е логически изведена. Например: A1, . An, → B1, . Bm означава A1& . & & ⊢B1∨. ∨Bm; →В1, . Bm означава ⊢ В1,∨. ∨Bm; A1, . An, → означава ⊢ (Α1& . & &An); последователност, двете части на която са празни, може да се тълкува като логическо противоречие.

Секвентното смятане се състои от два основни компонента: основната секвенция и правилата за извод (понякога наричани правила за извод). Главната секвенция в оригиналната версия на Генцен е секвенция от формата A → A, където A е формула, но могат да се използват и главни секвенции от друг тип. Правилата за заключение се делят на два вида: логически и структурни. Логическите правила на заключението от своя страна се разделят на правила за въвеждане на логически знак в антецедента и правилатавъвеждането на логически знак в секвенцията на последователността. Според логическото правило от формулите, включени в неговите помещения (странични формули), в заключението чрез въвеждане на логически знак се получава по-сложна формула (основната формула). По този начин логическите правила ви позволяват да изграждате сложни формули от по-прости. Броят на логическите правила в последователното смятане се определя от броя на логическите константи, използвани в това смятане. Структурните правила (пренареждане, намаляване и изтъняване) не засягат структурата на отделните формули, а структурата на последователностите. В резултат на прилагането на тези правила, появяванията на формули в предшестващия или последващия ред на последователността се пренареждат, намаляват или добавят. Логическите и структурните правила за извод за класическите и интуиционистичните логики са симетрични в смисъл, че всяко предходно (следващо) правило съответства на точно едно следващо (предшестващо) правило.

Специална роля в смятането на последователностите играе правилото, наречено "сечение":

Това е единственото правило, в резултат на което формулата на сечението (в случая A) се изтрива от изхода. Всички други правила запазват така нареченото свойство на подформулата на извеждането: всички формули, включени в предпоставките на дадено правило, са подформули на някои формули, включени в заключението на това правило. Изводът в последователното смятане има формата на последователно дърво, чието изграждане започва с основната(ите) последователност(и) и продължава според правилата за заключение. Казва се, че една секвенция може да бъде изведена в секвенционното смятане, ако е възможно да се конструира производна, в която тя е последната (крайна) секвенция. Строго погледнато, дърветата в последователното смятане не са изводи в стандартния смисъл на термина "извод", а метаконструкции, сконструкцията на която се извършват логически преходи от един запис на изводкъмдруги. В този случай интерпретацията на секвенциите може да бъде различна, което отваря широки възможности за изучаване на общите свойства на формалните логически доказателства.

Основният резултат на съвременната логика, получен от G.Gentzen, е свързан с смятането на последователностите - теоремата за елиминиране на секциите, или теоремата за елиминиране. В доказателството на тази теорема G. Gentzen заменя напречното сечение с правилото за смесване:

където Δ* и Θ* не съдържат формулата A и показва, че от всяко извеждане в последователното смятане на класическата и интуиционистична логика от първи ред, всички приложения на това правило могат да бъдат елиминирани.

Има много модификации на оригиналната версия на Генцен на секвенционното смятане за класически и некласически логики. Методологически тези модификации се свеждат до промяна на формата и/или броя на основните секвенции, формата и/или броя на правилата за извод и/или въвеждане на ограничения върху използването на специфични правила за извод при конструиране на дърво за извод. Понякога самата концепция за последователност се променя и се използват обекти като „суперпоследователности“, „кортежи от последователности“, „структури“ и т.н. Достатъчно прозрачен и ефективен подход към формулирането на смятането, при който на правилата на заключението се придава "глобален" характер - тяхното приложение зависи не само от вида на помещенията, но и от състоянието на заключенията на тези помещения. Такива правила, по-специално, разширяват възможностите за доказване на теоремата за елиминиране на секциите за некласически логики.

Изчисленията на последователностите са тясно свързани с табличните представяния на логическите системи и осигуряват естествен преход между синтактичните и семантичните нива на анализ на некласическите логики. Те са удобен инструмент за изследване.количествени и качествени характеристики на логическите изводи и процедури за търсене на логически доказателства.

1. Математическа теория на логическото заключение. М., 1969.