Вывод

логический - формальный вывод в исчислении, содержащем логические правила и имеющем в качестве основных выводимых объектов формулы (интерпретацией к-рых являются суждения;см. Логические исчисления. Логико-математические исчисления). Поскольку обычно такие исчисления снабжаются семантикой, то в некоторых случаях под логическим В. понимают содержательное рассуждение, позволяющее от сформулированных аксиом и гипотез (допущений) переходить к новым утверждениям, логически вытекающим из исходных. При зафиксированных аксиомах и правилах логических переходов (см. Вывода правило).говорят, что последовательность формул является выводом (своего последнего члена А).из гипотез [img: http://localhost:8080/file/010321-140.jpg] [img: http://localhost:8080/file/010321-141.jpg], если каждый член последовательности либо является аксиомой или одной из гипотез, либо получается из предыдущих формул последовательности по одному из правил. Это записывается в виде [img: http://localhost:8080/file/010321-142.jpg] при этом формула Аназ. выводимой из A1,..., An. В случае n=0 запись [img: http://localhost:8080/file/010321-143.jpg] означает, что Авыводимо в рассматриваемом исчислении без к.-л. допущений; применяется также запись [img: http://localhost:8080/file/010321-144.jpg] означающая, что "допущения [img: http://localhost:8080/file/010321-145.jpg] ведут к противоречию" (в большинстве изучавшихся систем [img: http://localhost:8080/file/010321-146.jpg] влечет выводимость из этих гипотез любой формулы). Напр., в исчислении, содержащем аксиому [img: http://localhost:8080/file/010321-147.jpg] и правило модус поненс, последовательность [img: http://localhost:8080/file/010321-148.jpg] [img: http://localhost:8080/file/010321-149.jpg] является выводом [img: http://localhost:8080/file/010321-150.jpg] из [img: http://localhost:8080/file/010321-151.jpg] Свойствами логической выводимости являются: [img: http://localhost:8080/file/010321-152.jpg] если [img: http://localhost:8080/file/010321-153.jpg] если [img: http://localhost:8080/file/010321-154.jpg] если [img: http://localhost:8080/file/010321-155.jpg] [img: http://localhost:8080/file/010321-156.jpg] (здесь Аи В - формулы, Г и Г'- списки формул, [img: http://localhost:8080/file/010321-157.jpg] - формула или пустое слово). Эти свойства позволяют существенно преобразовывать списки гипотез и, наряду с правилами введения и удаления логических символов (см. Выводимое правило), сближают системы со знаком [img: http://localhost:8080/file/010321-158.jpg] с Генцена формальными системами. Для исчислений, основанных на классич. логике, характерно свойство [img: http://localhost:8080/file/010321-159.jpg]. Для, интуиционистской логики (конструктивной логики) в широких предположениях удается доказывать принципы брауэровского понимания выводимости: 1) если [img: http://localhost:8080/file/010321-160.jpg], то имеет место одна из вы-водимостей [img: http://localhost:8080/file/010321-161.jpg] или [img: http://localhost:8080/file/010321-162.jpg]; 2) если [img: http://localhost:8080/file/010321-163.jpg], то, для некоторого терма t, [img: http://localhost:8080/file/010321-164.jpg]. (упомянутые предположения во всяком случае выполнены при пустом Г). Возможности избавления от допущений, включая переход к выводам без гипотез, регулируются дедукции теоремой. Формирование понятия В. (и систем, в терминах к-рых это понятие получает смысл) знаменовало собой возникновение современной математич. логики. Новое, более строгое понимание аксиоматич. метода, при к-ром формализации подлежат не только аксиомы, но и логические средства, открыло возможность математич. определения понятия доказательства и изучения доказательств математнч. методами (см. Доказательств теория). Поня-. тие формального В. оказалось хорошим приближением к понятию математич. истины (см. Гёделя теорема о полноте, Гёделя теорема о неполноте). Искусственная формализация понятия логической выводимости в дальнейшем существенно сблизилась с реальными способами содержательного математич. рассуждения (см. Естественный логический вывод).