НОВОСТИ    БИБЛИОТЕКА    ЭНЦИКЛОПЕДИЯ    БИОГРАФИИ    КАРТА САЙТА    ССЫЛКИ    О ПРОЕКТЕ  

ВЫВОД

ВЫВОД логический - формальный вывод в исчислении, содержащем логические правила и имеющем в качестве основных выводимых объектов формулы (интерпретацией к-рых являются суждения; см. Логические исчисления, Логико-математические исчисления). Поскольку обычно такие исчисления снабжаются семантикой, то в некоторых случаях под логическим В. понимают содержательное рассуждение, позволяющее от сформулированных аксиом и гипотез (допущений) переходить к новым утверждениям, логически вытекающим из исходных.

При зафиксированных аксиомах и правилах логических переходов (см. Вывода правило) говорят, что последовательность формул является выводом (своего последнего члена A) из гипотез А1, ..., Аn (n ≥ 0), если каждый член последовательности либо является аксиомой или одной из гипотез, либо получается из предыдущих формул последовательности по одному из правил. Это записывается в виде А1, ..., Аn ⊢ А; при этом формула А наз. выводимой из А1, ..., Аn. В случае n = 0 запись ⊢ А означает, что А выводимо в рассматриваемом исчислении без к.-л. допущений; применяется также запись А1, ..., Аn ⊢, означающая, что «допущения А1, ..., Аn ведут к противоречию» (в большинстве изучавшихся систем А1, ..., Аn ⊢ влечет выводимость из этих гипотез любой формулы). Напр., в исчислении, содержащем аксиому A ⊃ (B ⊃ A) и правило модус поненс, последовательность A, A ⊃ (B ⊃ A), В ⊃ А является выводом B ⊃ A из А (т. е. А ⊢ B ⊃ A). Свойствами логияеекой выводимости являются: А ⊢ А; если Г ⊢ Δ, то А, Г ⊢ Δ; если А, А, Г ⊢ Ä, то А, Г ⊢ Δ; если Г, А, В, Г' ⊢ Δ, то Г, В, А, Г' ⊢ Δ; если Г ⊢ А и А, Г' ⊢ Δ, то Г, Г' ⊢ Δ (здесь А и В - формулы, Г и Г'- списки формул, Δ - формула или пустое слово). Эти свойства позволяют существенно преобразовывать списки гипотез и, наряду с правилами введения и удаления логических символов (см. Выводимое правило), сближают системы со знаком ⊢ с Генцена формальными системами. Для исчислений, основанных на классич. логике, характерно свойство ⏋⏋А ⊢ А. Для интуиционистской логики (конструктивной логики) в широких предположениях удается доказывать принципы брауэровского понимания выводимости: 1) если Г ⊢ A ∨ B, то имеет место одна из выводимостей Г ⊢ А или Г ⊢ В; 2) если Г ⊢ ∃xA(х), то, для некоторого терма t, Г ⊢ A(t) (упомянутые предположения во всяком случае выполнены при пустом Г). Возможности избавления от допущений, включая переход к выводам без гипотез, регулируются дедукции теоремой.

Формирование понятия В. (и систем, в терминах к-рых это понятие получает смысл) знаменовало собой возникновение современной математич. логики. Новое, более строгое понимание аксиоматич. метода, при к-ром формализации подлежат не только аксиомы, но и логические средства, открыло возможность математич. определения понятия доказательства и изучения доказательств математич. методами (см. Доказательств теория). Понятие формального В. оказалось хорошим приближением к понятию математич. истины (см. Гёделя теорема о полноте, Гёделя теорема о неполноте). Искусственная формализация понятия логической выводимости в дальнейшем существенно сблизилась с реальными способами содержательного математич. рассуждения (см. Естественный логический вывод).

Лит.: [1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Математическая теория логического вывода, сб. переводов, М., 1967.

С. Ю. Маслов.


Источники:

  1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.











© MATHEMLIB.RU, 2001-2021
При копировании материалов проекта обязательно ставить ссылку на страницу источник:
http://mathemlib.ru/ 'Математическая библиотека'
Рейтинг@Mail.ru