Cтраница 2
В основу приговора, определения могут быть положены только доказательства, исследованные в судебном С. Следственные и судебные действия по собиранию и проверке доказательств могут производиться только на предварительном или соответственно судебном С. Поэтому обнаружение неполноты доказательственного материала влечет его возобновление ( дополнительное С. [16]
Непременное свойство формальной математической системы заключается в существовании вычислимого способа решить, является ли некоторая строка символов доказательством соответствующего математического утверждения или нет. Весь смысл формализации понятия математического доказательства в конечном счете сводится к тому, чтобы не требовалось никакого дополнительного суждения о состоятельности того или иного типа рассуждений. Необходимо обеспечить возможность проверять полностью механическим и заранее определенным способом, что предполагаемое доказательство и в самом деле является таковым - то есть должен существовать алгоритм для проверки доказательств. С другой стороны, мы не требуем существования алгоритмической процедуры нахождения доказательств истинности ( или ложности) предлагаемых математических утверждений. [17]
Вполне осуществимым и уже сегодня практичным автоматизированным средством является система проверки доказательств. Если ей сообщить шаги доказательства, выполненного человеком, она может проверить соответствие каждого шага известным ей правилам вывода. Таким образом она может искать ошибки в подготовленных человеком доказательствах. Однако остальные доказывающие системы ( за исключением систем проверки доказательств) еще долгое время вряд ли будут применимы к реальным программам. [18]
Необходимо отметить, что отыскание такого доказательства, или последовательности правильных формул, совершенно отлично от проверки уже имеющегося доказательства. Для проверки доказательства каждую его строку необходимо исследовать по отношению к предыдущим строкам, чтобы определить, какой закон логики был использован для ее вывода. Такую проверку было бы довольно просто запрограммировать: каждая формула, или строка доказательства, была бы списком символов или слов в памяти машины, а законы логики - подпрограммами. Будем считать, что для нашей машины такая программа проверки доказательства уже составлена. [19]
Если при описании какой-либо аксиоматической теории используемая система логических правил предполагается уже известной, мы будем говорить, что эта теория есть неформальная ( содержательная) теория. В математической практике аксиоматические теории обычно описываются в виде неформальных теорий; что же касается предполагаемой при этом логики, то обычно считается, что это та интуитивная логика, которая усваивается в ходе изучения математики. Сказанное отнюдь не имеет характер порочного круга, как это может показаться вначале. Более того, можно привести многочисленные доводы в защиту мнения, согласно которому точное определение логической правильности, выдвигаемое символической логикой, хорошо согласуется с тем интуитивным представлением о строгости рассуждений, которым пользуются математики. Многочисленные примеры, подтверждающие тот тезис, что логические принципы, считающиеся строгими большинством математиков, принимаются в качестве таковых в символической логике ( и наоборот), собраны в книге Дж. На наш взгляд, не будет преувеличением сказать, что в глазах подавляющего большинства математиков современная символическая логика есть попросту формализация того интуитивного способа рассуждений, которого они фактически всегда придерживаются. Это мнение, правда, не выглядит столь убедительным по отношению к тем математикам, которые проводят формальные доказательства и используют для проверки их правильности формальные процедуры исчисления предикатов. Однако и для таких математиков проверка доказательств формальными, механическими методами играет скорее роль некоторой страховки в сложной цепи рассуждений, дополняющей в сложных случаях содержательные методы рассуждений, но не подменяющей их. [20]