В) Метод доказательств и опровержений
Гамма. Я предлагаю принять цилиндр в качестве настоящего контрапримера для рассматриваемой теоремы. Я изобретаю новую лемму (или леммы), которая этим примером опровергается, и добавляю эту лемму (леммы) к первоначальному списку. Это как раз и делал Альфа. Но, вместо того чтобы «скрывать» их так, чтобы они сделались скрытыми, я возвещаю их публично.
Теперь цилиндр, ставивший ранее в тупик, – опасный глобальный, а не локальный контрапример (третьего типа) по отношению к старому анализу доказательства и соответствующей старой теореме, этот цилиндр станет безопасным глобальным и одновременно локальным контрапримером (второго типа) по отношению к новому анализу доказательства и соответствующей новой теореме.
Альфа думал, что его классификация контрапримеров была абсолютной; в действительности же она относилась только к его анализу доказательства. По мере роста анализа доказательства контрапримеры третьего типа превращаются в контрапримеры второго типа.
Ламбда. Это верно. Анализ доказательства будет «строгим», или «имеющим силу», и соответствующая математическая теорема – истинной тогда и только тогда, если не будет для них контрапримеров третьего типа. Я называю этот критерий принципом обратной передачи ложности, так как он требует, чтобы глобальные контрапримеры были также локальными: ложность должна быть передана обратно от интуитивной догадки к леммам, от последующей части теоремы к предшествующей. Если какой-нибудь глобальный, но не локальный контрапример нарушает этот принцип, мы восстанавливаем его добавлением к анализу, доказательства подходящей леммы. Таким образом, принцип обратной передачи ложности является регулятивным принципом для анализа доказательства in statu nasoendi[76], а глобальный, но не локальный контрапример – ферментом в росте анализа доказательства.
Гамма. Вспомните, раньше, даже не найдя ни одного опровержения, мы все же сумели обнаружить три подозрительные леммы и продвинуться в анализе доказательства!
Ламбда. Это верно. Анализ доказательства может начинаться не только под давлением глобальных контрапримеров, но также и когда люди уже выучились остерегаться «убедительных» доказательств[77].
В первом случае все глобальные контрапримеры появляются в виде контрапримеров третьего типа и все леммы начинают свою карьеру в качестве «скрытых лемм». Они приводят нас к постепенному построению анализа доказательства и так один за другим превращаются в контрапримеры второго типа.
Во втором случае – когда мы уже начинаем подозревать и ищем опровержений, – мы можем прийти к далеко зашедшему вперед анализу доказательства без всяких контрапримеров. Тогда мы имеем две возможности. Первая возможность состоит в том, что нам при помощи локальных контрапримеров удастся опровергнуть все леммы, содержащиеся в нашем анализе доказательства. Мы можем установить, как следует, что они будут также глобальными контрапримерами.
Альфа. Вот именно так я и открыл раму картины: я искал многогранник, который после удаления одной грани не мог быть развернут в один лист на плоскости.
Сигма. Тогда не только опровержения действуют как ферменты для анализа доказательства, но и анализ доказательства может действовать как фермент для опровержения. Какой нехороший союз между кажущимися врагами!
Ламбда. Это верно. Если догадка кажется вполне допустимой или даже самоочевидной, то должно доказать ее; может оказаться, что она основана на весьма софистических и сомнительных леммах. Опровержение лемм может привести к какому-нибудь неожиданному опровержению первоначальной догадки.
Сигма. К опровержениям, порожденным доказательством!
Гамма. Тогда «мощь логического доказательства заключается не в том, что оно принуждает верить, а в том, что оно наводит на сомнения»[78].
Ламбда. Но позвольте мне вернуться ко второй возможности: когда мы не находим никаких локальных контрапримеров для подозреваемых лемм.
Сигма. То есть когда опровержения не помогают анализу доказательства. Что же тогда может случиться?
Ламбда. Мы тогда окажемся общепризнанными чудаками. Доказательство приобретает абсолютную респектабельность и леммы сбросят всякое подозрение. Наш анализ доказательства скоро будет забыт[79]. Без опровержений нельзя поддерживать подозрение; прожектор подозрения скоро выключается, если контрапример не усиливает его, направляя яркий свет опровержения на пренебреженный аспект доказательства, который остался незамеченным в сумерках «тривиальной истины».
Все это показывает, что мы не можем поместить доказательство и опровержение на отдельные полочки. Вот почему я предлагаю наш «метод включения лемм» перекрестить в «метод доказательств и опровержений». Позвольте мне выразить его основные черты в трех эвристических правилах.
Правило 1. Если вы имеете какую-нибудь догадку, то попробуйте доказать ее и опровергнуть ее. Тщательно рассмотрите доказательство, чтобы приготовить список нетривиальных лемм (анализ доказательства); найдите контрапримеры и для догадки (глобальные контрапримеры) и для подозрительных лемм (локальные контрапримеры).
Правило 2. Если у вас есть глобальный контрапример, то устраните вашу догадку, добавьте к вашему анализу доказательства подходящую лемму, которая будет опровергнута им, и замените устраненную догадку исправленной, которая включила бы эту лемму как условие[80]. Не позволяйте отбрасывать опровержения как монстры[81]. Сделайте явными все «скрытые леммы»[82].
Правило 3. Если у вас есть локальный контрапример, то проверьте его, не будет ли он также глобальным контрапримером. Если он будет им, то вы можете легко применить правило 2.