markov_teorija_algorifmov (522344), страница 13
Текст из файла (страница 13)
Таким образом, высказывание В верно при его рассмотрении как материальной импликации, что и требовалось доказать. 5 15. Дедуктивная импликация 1. Рассмотренные случаи импликаций — импликации с разрешимыми и полуразрешимыми посылками, — очевидно, не исчерпывают всех возможностей. Поэтому уместно продолжать поиск возможных трактовок импликации. Обычное объяснение смысла импликации, упомянутое в 5 13.2, показалось нам недостаточно ясным из-за того, что оно было связано с предложением „предположить" нечто верным и тогда „быть вынужденными" признать верным нечто другое. Нельзя ли, однако, все это уточнить? Нельзя ли считать, что' импликация «если А, то В» выражает возможность вывести В из А по определенным фиксированным формальным и вместе с тем разумным правилам? Тогда при установлении истинности импликации нам не нужно было бы заботиться ни о смысле, ни об истинности ее посылки и ее заключения.
Конечно, для этого было бы необходимо, чтобы посылки и заключения рассматриваемых импликаций формулировались на некотором формальном языке, имеющем точный синтаксис. Естественно также требовать, чтобы этот язык имел четкую семантику, т. е. чтобы осмысленные ггл. ! дедуктивпля нмплнкдция введения выражения этою языка — нх можно называть высказываниями нлн формулами — имели ясно определенный смысл.
Разумеется, следует разрешить привлекать в процессе вывода В нз А любые верные высказывания данного языка в соответствии с обычной практикой математического рассуждения. Это, однако, равносильно тому, что всякое верное высказывание данного языка будет считаться выводимым нз А. Таким образом, в числе правил вывода естественно иметь правило всякое верное высказывание (данного языка) считается выводимым из А.
Естественно также иметь правило А счиошется выводимым из А. Другие правила вывода могут иметь внд (1) в случае, когда С выводимо из А, а Е так-то и так-то связано с С, Е считается выводимым из А, нлн (2) в случае, когда С и !л выводимы из А, а Е так-то и так-то связано с С и ду, Е считается выводимым из А, нлн еще более сложный аналогичный внд. Здесь под связями между высказываниями подразумеваются чисто формальные синтаксические связи, для обнаружения которых надо лишь исследовать этн высказывания как некоторые тексты, не апеллнруя к нх смыслу.
Правила вывода могут, однако, иметь н следующий более сложный внд: (3) в случае, когда из А выводимо всякое высказывание такого-то вида Я, считается выводимым из А и высказывание Е, так-то и так-то связанное с высказываниями вида й. Для применения правил этого вида бывает необходимо знать, что всякое высказывание данного вида выводимо нз А. Уверенность в этом как в истинности высказывания общности мы можем приобрести, например, на основаннн ограниченного опыта вывода некоторых высказываний этого вида (ср.
$91 с помощью других правил вывода. Правила вывода характеризуют вывод нз А как процесс. Онн дают возможность получать все новые высказывания, выводимые нз А, Порядок применения правил вывода, ко- печно, зависит от нас. Поэтому процесс вывода из А не определен однозначно. На некоторых стадиях этого процесса может потребоваться наша уверенность в осуществимости любого нз некоторых других процессов вывода нз А.
Эта уверенность может быть основана на нашей ннтунцнн общности. 2. Выше мы потребовали, чтобы правила вывода были „разумными", Этому требованию целесообразно придать следующий смысл, Каждое нз правил вывода должно быть такнм, что, будучи применено к верным формулам, оно дает верные формулы. Например, во всяком правиле вида ! (1) связь между С н Е должна гарантировать истинность Е в случае истинности С; во всяком правиле вида 1 (2) связь между О, С н Е должна гарантировать истинность Е в случае истинности О н С; во всяком правиле вида 1 (3) связь между Я н Е должна гарангнровать истинность Е в случае истинности всякого высказывання вида Я.
Прн соблюдении этого требования разумности (нлн семантической пригодности) всякое высказывание, выводимое нз истинного высказывання, будет истинным. 3. Имея формальный язык, на котором формулируются рассматриваемые высказывания, н достаточно мощную систему семантнческн пригодных правил вывода, мы можем следующим образом определить смысл нмплнкацнн: нмплнкацня выражает выводнмость своего заключения нз своей посылки прн данной совокупности правил вывода. Так понимаемую нмплнкацню мы будем называть дедуктивной имплихацией *).
Недостаток определения дедуктивной нмплнкацнн можно усмотреть в том, что оно связано с определенной системой правил вывода н завнснмо от этой снстемы. Однако некоторые рассмотренные первым нз авторов (1151, 1211) системы правил вывода являются в этом отношении естественными. Основанные на ннх понятия дедуктивной нмплнкацнн, во всяком случае, заслуживают внимания.
4. Через дедуктивную нмплнкацню может быть определено еще одно поннманне отрицания. Это понимание соответствует тому, что в математике принято называть «прнведеннем к нелепости». Имея надлежащий формальный язык н семантически пригодную систему формальных правил вывода для высказываний, формулируемых на этом языке, мы можем определить приведение высказывания А к нелепости как ') Возникающие здесь трудности обсуждаются Д.
Г н и ь бе р то м и П. Б е р н а й сом 121. См., и частности, с. 437, 438. ИДЕЯ СТУПЕНЧАТОЙ СЕМАНТИЧЕСКОЙ СИСТЕМЫ бз н'л. 1 ВВЕДЕНИЕ б!б! выведение определенного высказывания — „стандартной нелепости" — из А. Какое именно высказывание считается прн этом стандартной нелепостью, бывает прн этом довольно безразлично. Важно лишь, чтобы его ложность была очевидна. Отрицание высказывания Л (формулированного на данном языке) будет тогда пониматься как дедуктивная имплнкация несли А, то .7», где через Л обозначена стандартная нелепость. Так понимаемое отрицание мы будем называть редукционным отрицание»< (от латинского геднс1)о аб аЬбцгбцш). Поскольку редукционное отрицание определено через дедуктивную импликацию, многое из сказанного выше о дедуктивной импликации может быть сказано и о редукционном отрицании. Установление истинности редукционного отрицания какого-нибудь высказывания не требует вникания в смысл этого высказывания.
Высказывание, для которого установлена истинность редукционного отрицания. ложно. Конечно, понимание редукционного отрицания зависит от избранной системы правил вывода. Но это не мешает нам интересоваться редукционным отрицанием, соответствующим определенной естественной системе правил вывода.
5 16. Идея ступенчатой семантической системы 1. Трактовка импликации как дедуктивной вынуждает нас строить для конструктивной математической логики специальные формальные языки. При этом недостаточно одного такого языка. В самом деле, имея формальный язык, пригодный для построения высказываний определенного вида, мы сможем оказаться в состоянии ввести, как описано выше, дедуктивные импликацни с посылками и заключениями этого вида. Однако сами эти дедуктивные импликации уже не будут вьражаться формулами этого языка.
Мы же, естественно, пожелаем рассматривать эти дедуктивные импликации тоже как высказывания, которые можно комбинировать с помощью логических связок. В частности, мы можем пожелать рассматривать импликации, посылками и заключениями которых будут уже построенные дедуктивные импликации. Если мы и такие импликации пожелаем трактовать как дедуктивные, то нам, очевидно, понадобится новый формальный язык, спо- собный выразить дедуктивные импликации, связывающие высказывания нашего прежнего языка. Это приводит нас к следующей идее ступенчатого построения конструктивной математической логики.
Нужные нам формальные языки строятся друг за другом путем последовательных расширений. Применение логической связки к формулам какого-либо из этих языков не всегда дает формулу этого же языка, но всегда — формулу языка следующей ступени Осуществление этого плана вкратце описано в заметках А. А. М а р к о в а 1181 — 1241.
Очень существенную роль играет в нем понятие нормального алгорифма и другие понятия, связанные с рассмотрением слов в данном алфавите. В этой монографии, могущей служить введением по отношению к данному плану, мы, в частности, изложим и этот вводный материал. Он в значительной степени покрывается монографией А. А. М а р к о в а 121. Однако изложение является теперь более строгим и систематическим, а также более приспособленным к построению ступенчатой семантической системы конструктивной логики. В начале книги мы будем стараться тщательно анализировать смысл применяемых нмпликаций и отрицаний. По мере того, как у читателя будет накапливаться опыт, мы, чтобы не загромождать изложение, будем уменьшать число семантических разъяснений.