Энциклопедия в четырех томах научно-редакционный совет


ИСЧИСЛЕНИЕ ПРЕДИКАТОВ катав



страница117/393
Дата11.03.2018
Размер9.68 Mb.
1   ...   113   114   115   116   117   118   119   120   ...   393
ИСЧИСЛЕНИЕ ПРЕДИКАТОВ катав.

см. Логика преди-
ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ - одна из основных форм представления логических систем, применяемая в логике наряду с аксиоматическими системами (гильбертовского типа) и системами натурального (естественного) вывода. Термин «секвенция» происходит от слова sequent (последовательность). Он введен в логику П. Герцем (1929) и заимствован Г. Генценом, который впервые сформулировал в форме исчисления секвенций классическую и интуиционистскую логику предикатов первого порядка.

Секвенция — это формальная запись отношения логической выводимости вида Г-» Θ, где Г и θ — последовательности (возможно пустые) разделенных запятыми формул. Вместо стрелки может использоваться «ι—» или любой другой знак логической выводимости. Левую часть секвенции называют антецедентом, а правую — сукцедентом. Содержательно в исходном генценовском варианте секвенция означает, что из конъюнкции формул, входящих в ее антецедент, логически выводима дизъюнкция формул, входящих в ее сукцедент. Напр.:А|, ...,Ап-»В),..., Вп, означает а| &... &&А„ i—B|V...vByn;-»Bi,..., Вщ означает l— b|v ... νΒη,,Αι, ...,Αη-» означает ι— -ι(Αι& ...& &Αη); а секвенция, обе части которой пусты, может интерпретироваться как логическое противоречие.




==184


ИТАЙ


Исчисление секвенций состоит из двух главных компонентов: основной секвенции и правил заключения (иногда их называют правилами вывода). Основная секвенция в первоначальном генценовском варианте — это секвенция вида А->А, где А — формула, но могут применяться основные секвенции и другого вида. Правила заключения делятся на два типа: логические и структурные. Логические правила заключения в свою очередь делятся на правила введения логического знака в антецедент и правила введения логического знака в сукцедент секвенции. По логическому правилу из формул, входящих в его посылки (боковых формул), в заключении с помощью введения логического знака получается более сложная формула (главная формула). Таким образом, логические правила позволяют строить сложные формулы из более простых. Число логических правил в исчислении секвенций определяется числом используемых в данном исчислении логических констант. Структурные правила (перестановка, сокращение и утончение) влияют не на структуру отдельных формул, а на структуру секвенций. В результате применения этих правил вхождения формул в антецедент или сукцедент секвенции переставляются, сокращаются или добавляются. Логические и структурные правила заключения для классической и интуиционистской логик симметричны в том смысле, что каждому антецедентному (сукцедентному) правилу соответствует в точности одно сукцеденгное (антецедентное) правило.

Особую роль в исчислении секвенций играет правило, называемое «сечением»: Γ-»Θ,Α Α,Δ->Ψ Γ,Δ-^Θ,Ψ

Это единственное правило, в результате применения которого формула сечения (в данном случае А) вычеркивается из вывода. Все остальные правила сохраняют так называемое свойство подформульности вывода: все формулы, входящие в посылки конкретного правила, являются подформулами некоторых формул, входящих в заключение этого правила.

Вывод в исчислении секвенций имеет форму дерева секвенций, построение которого начинается с основной секвенции (основных секвенций) и продолжается по правилам заключения. Секвенция считается выводимой в исчислении секвенций, если можно построить вывод, в котором она является последней (конечной) секвенцией. Строго говоря, деревья в исчислении секвенций являются не выводами в стандартном смысле термина «логический вывод», а метаконструкциями, при построении которых выполняются логические переходы от одних записей о выводимости к другим. Интерпретация секвенций при этом может быть различной, что открывает широкие возможности для исследования общих свойств формальных логических доказательств.

С исчислением секвенций связан полученный Г. Генценом фундаментальный результат современной логики — теорема об устранении сечения, или элиминационная теорема. В доказательстве этой теоремы Г. Генцен заменяет сечение правилом смешения: Γ-»Θ,Α Α,Δ-»Ψ Г, Δ*-»θ·, Ψ

где Δ* и θ* не содержат формулы А, и показывает, что из любого вывода в исчислении секвенций классической и интуиционистской первопорядковой логики можно устранить все применения этого правила.


Существует множество модификаций первоначального генценовского варианта исчисления секвенций для классической и неклассических логик. Методологически эти модификации сводятся к тому, что изменяется форма или/и число основных секвенций, форма или/и число правил заключения или/и вводятся ограничения на применения конкретных правил заключения при построении дерева вывода. Иногда изменяется само понятие секвенции и используются такие объекты, как «надсеквенции», «кортежи секвенций», «структуры» и т. д. Достаточно прозрачен и эффективен подход к формулировке исчисления, при котором правилам заключения придается «глобальный» характер — их применение зависит не только от вида посылок, но и от состояния выводов этих посылок. Такие правила, в частности, расширяют возможности доказательства теоремы об устранении сечения для неклассических логик.

Исчисления секвенций тесно связаны с табличными представлениями логических систем и обеспечивают естественный переход между синтаксическим и семантическим уровнями анализа неклассических логик. Они являются удобным аппаратом исследования количественных и качественных характеристик логических выводов и процедур поиска логических доказательств. Лит.: Математическая теория логического вывода. М., 1969.



П. И. Быстрое

ИТАЙ (кит. — эфир) — категория, которой оперировали китайские мыслители кон. 19 — нач. 20 в. Заимствованное из европейских естественных наук и философии, в Китае это понятие претерпело существенные изменения.

Кан Ювэй трактовал «итай» как этическое начало, «гуманность» (жэнь) и «сострадание» (бу жэнь). Сунь Ятсен видел в итае творящий хаос, который «в своем движении порождает электроны; электроны, сгущаясь, создают элементы; элементы, соединяясь, создают материю; материя, собираясь воедино, создает планету».

В системе идей Тань Сытуна итай — основополагающее понятие, не имеющее четких дефиниций и раскрываемое через множество близких, но не тождественных характеристик. Важнейшие его атрибуты — вечность и несотворенность. Сфера его распространения не имеет предела: итай существует в микро- и макромирах, в явлениях реальной жизни и в надмировом абсолюте — «едином первоначале» (и юань). Итай многофункционален, он одного порядка с «чувством», «разумом» и понятием «дянь» (момент наивысшего напряжения сил инь ян; переводится также как «электрон», «электричество»). Итай — это импульс развития и реальная основа мира; из него «рождаются миры, возникает пустота и появляется все живое». Он выступает как условие единства мира, некий наполнитель, «склеивающий» отдельные явления: «Итай, все склеивая, [приводя] в соответствие, связывая, наполняет [собой] отдельные вещи». Он удерживает все предметы и явления в равновесии, препятствует не только их распаду, но и слиянию. Его действие распространяется и на общество, и на космические явления, и на тело человека.

Тань Сытун тем не менее не наделял итай свойствами первоначала. Если итай разлит повсюду и условно его можно изобразить в виде лишенной иерархичности субстанции, то «единое первоначало» предполагает иерархию, которую оно же и венчает. Через «единое первоначало» итай соотносится со своим коррелятом — «гуманностью». Все характеристики итая распространяются на «гуманность», приобретая этическую



==185


ИТАЛИЙСКАЯ ФИЛОСОФИЯ


окраску. Через «гуманность» итай и его свойства проецируются на общество и его законы.

Е. Ю. Стабурова


Каталог: sites -> default -> files
files -> Валявский Андрей Как понять ребенка
files -> Народная художественная культура. Профиль Теория и история народной художественной культуры
files -> Отчет о научно-исследовательской работе за 2014 год ростов-на-Дону 2014
files -> Учебно-методический комплекс дисциплины философия для образовательной программы по направлениям юридического факультета: Курс 1
files -> Цветков Андрей Владимирович, кандидат психологических наук, доцент кафедры клинической психологии программа
files -> Программа итогового (государственного) комплексного междисциплинарного экзамена по направлению 521000 (030300. 62) «Психология»


Поделитесь с Вашими друзьями:
1   ...   113   114   115   116   117   118   119   120   ...   393


База данных защищена авторским правом ©znate.ru 2019
обратиться к администрации

    Главная страница