Большая Советская Энциклопедия (ЛО)
Шрифт:
Формула называется интуиционистски общезначимой тогда и только тогда, когда можно утверждать всякое высказывание, получаемое из в результате подстановки любых математических суждений вместо логических переменных; точнее говоря, в том случае, когда имеется общий метод, позволяющий при произвольной такой подстановке получать построение, требуемое результатом подстановки. При этом понятие общего метода интуиционисты также считают первоначальным.
Формулы 1—10 являются интуиционистски общезначимыми, тогда как формула 11, выражающая классический закон исключенного третьего, не является таковой.
В известном отношении близкой к интуиционизму является точка зрения конструктивной математики, уточняющая несколько расплывчатые интуиционистские понятия импликации и общего метода на основе точного понятия алгоритма. С этой точки зрения закон исключенного
С методом формализации доказательств связано понятие формальной системы. Формальная система включает следующие элементы.
1. Формализованный язык с точным синтаксисом, состоящий из точных и формальных правил построения осмысленных выражений, называется формулами данного языка.
2. Чёткую семантику этого языка, состоящую из соглашений, определяющих понимание формул и тем самым условия их истинности.
3. Исчисление (см. выше), состоящее из формализованных аксиом и формальных правил вывода. При наличии семантики эти правила должны быть согласованы с ней, т. е. при применении к верным формулам давать верные формулы.
Исчисление определяет выводы (см. выше) и выводимые формулы — заключительные формулы выводов. Для выводов имеется распознающий алгоритм — единый общий метод, с помощью которого для любой цепочки знаков, применяемых в исчислении, можно узнавать, является ли она выводом. Для выводимых формул распознающий алгоритм может быть и невозможен (примером является исчисление предикатов, см. Логика предикатов).
Об исчислении говорят, что оно непротиворечиво, если в нём не выводима никакая формула вместе с формулой `u. Задача установления непротиворечивости применяемых в математике исчислений является одной из главных задач математической Л. Имея в виду охват той или иной содержательно определённой области математики, исчисление считают полным относительно этой области, если в нём выводима всякая формула, выражающая верное утверждение из этой области. Другое понятие полноты исчисления связано с требованием иметь для всякого утверждения, формулируемого в данном исчислении, либо его доказательство, либо его опровержение. Первостепенное значение в связи с этими понятиями имеет теорема Гёделя, утверждающая несовместимость требований полноты с требованием непротиворечивости для весьма широкого класса исчислений. Согласно теореме Гёделя, никакое непротиворечивое исчисление из этого класса не может быть полным относительно арифметики: для всякого такого исчисления может быть построено верное арифметическое утверждение, формализуемое, но не выводимое в исчислении. Эта теорема, не снижая значения математической Л. как мощного организующего средства в науке, убивает надежды на эту дисциплину как на нечто способное осуществить охват математики в рамках одной формальной системы. Надежды такого рода высказывались многими учёными, в том числе основоположником математического формализма Гильбертом.
В 70-е гг. 20 в. получила развитие идея полуформальной системы. Полуформальная система — это также система некоторых правил вывода. Однако некоторые из этих правил могут иметь существенно иной характер, чем правила вывода формальной системы. Они, например, могут допускать выведение новой формулы после того, как с помощью интуиции создалось убеждение в выводимости любой формулы такого-то вида. Сочетание этой идеи с идеей ступенчатого построения математической Л. лежит в основе одного из современных построений логики конструктивной математики. В приложениях математической Л. часто применяются исчисления предикатов — классическое и интуиционистское.
Математическая Л. органически связана с кибернетикой, в частности с математической теорией управляющих систем и математической лингвистикой. Приложения математической Л. к релейно-контактным схемам основаны на том, что всякая двухполюсная релейно-контактная схема в следующем смысле моделирует некоторую формулу классического исчисления высказываний. Если схема управляется n реле, то столько же различных пропозициональных переменных содержит , и если обозначить через i суждение «Реле номер i сработало», то цепь будет тогда и только тогда замкнута, когда будет верен результат подстановки суждений i вместо соответствующих логических переменных в . Построение такой моделируемой формулы, описывающей «условия работы» схемы, оказывается особенно простым для т. н. П-схем, получаемых из элементарных одноконтактных цепей путём параллельных и последовательных соединений. Это связано с тем, что параллельные и последовательные соединения цепей моделируют соответственно дизъюнкцию и конъюнкцию суждений. Действительно, цепь, полученная путём параллельного (последовательного) соединения цепей Ц1 и Ц2, тогда и только тогда замкнута, когда замкнута цепь Ц1 или (и) замкнута цепь Ц2. Применение исчисления высказываний к релейно-контактным схемам открыло плодотворный подход к важным проблемам современной техники. Это же применение обусловило постановку и частичное решение многих новых и трудных проблем математической Л., к числу которых в первую очередь относится т. н. проблема минимизации, состоящая в разыскании эффективных методов нахождения простейшей формулы, равносильной данной формуле.
Релейно-контактные схемы являются частным случаем управляющих схем, применяемых в современных автоматах. Управляющие схемы иных типов, в частности схемы из электронных ламп или полупроводниковых элементов, имеющие ещё большее практическое значение, также могут быть разрабатываемы с помощью математической Л., которая доставляет адекватные средства как для анализа, так и для синтеза таких схем. Язык математической Л. оказался также применимым в теории программирования, создаваемой в связи с развитием машинной математики. Наконец, созданный математической Л. аппарат исчислений оказался применимым в математической лингвистике, изучающей язык математическими методами.
А. А. Марков.
Научные учреждения и издания. Преподавание и исследовательская работа по Л. являются неотъемлемой частью научной и культурной жизни большинства стран мира. В СССР научно-исследовательская работа в области Л. ведётся в основном в научно-исследовательских центрах Москвы, Ленинграда, Новосибирска, Киева, Кишинева, Риги, Вильнюса, Тбилиси, Еревана и др. городов отделениями математических институтов АН СССР и союзных республик, институтами философии, кафедрами Л. университетов и некоторых др. вузов. Публикации работ по Л. в СССР осуществляются: в непериодических изданиях в форме тематических сборников и монографий (в частности, начиная с 1959 в серии «Математическая логика и основания математики»), в непериодических изданиях «Трудов Математического института им. В. А. Стеклова АН СССР» (с 1931), в сборниках «Алгебра и логика» (Новосибирск, с 1962), в «Записках» научных семинаров по Л., в математических и философских журналах. В реферативном журнале «Математика» и в реферативных журналах института научной информации по общественным наукам АН СССР систематически освещаются работы советских и зарубежных авторов по Л. Из специальных зарубежных изданий, освещающих проблематику Л., наиболее известны: международная монографическая серия «Studies in Logic...» (Amst., с 1965) и журналы: «The Journal of Symbolic Logic» (Providence, с 1936); «Zeitschrift f"ur mathematische Logik und Grundlagen der Mathematik» (В., с 1955); «Archiv f"ur mathematische Logik und Grundlagenforschung» (Stuttg., с 1950); «Logique et analyse» (Louvain, с 1958); «Journal of philosophical logic» (Dordrecht, с 1972); «International logic review» (Bologna, с 1970); «Studia Logica» (Warsz., с 1953); «Notre Dame Journal of formal Logic» (Notre Dame, с 1960).
Основную организационную работу, связанную с обменом научной информацией в области Л., осуществляет пользующаяся поддержкой ООН Ассоциация символической логики. Ассоциация организует международные конгрессы по Л., методологии и философии науки. Первый такой конгресс состоялся в 1960 в Станфорде (США), второй — в 1964 в Иерусалиме, третий — в 1967 в Амстердаме, четвёртый — в 1971 в Бухаресте.
З. А. Кузичева, М. М. Новосёлов.
Лит.: Основные классические работы. Аристотель, Аналитики первая и: вторая, пер. с греч., М., 1952; Leibniz G. W., Fragmente zur Logik, В., 1960; Кант И., Логика, пер. с нем., П., 1915; Милль Дж. С., Система логики силлогистической и индуктивной, пер. с англ., 2 изд., М., 1914; De Morgan A., Formal logic or the calculus of inference, necessary and probable, L., 1847 (перепечатка, L., 1926); Boole G., The mathematical analysis of logic, being an essay toward a calculus of deductive reasoning, L. — Camb., 1847 (перепечатка, N. Y., 1965); Schr"oder Е., Der Operationskreis des Logikkalkuls, Lpz., 1877; Frege G., Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle, 1879; Джевонс С., Основы науки, Трактат о логике и научном методе, пер. с англ., СПБ, 1881; Порецкий П. С., О способах решения логических равенств и об обратном способе математической логики, Казань, 1884; Whitehead A. N., Russell B., Principia mathematica, 2 ed., v. 1—3, Camb., 1925—27.