В еврейской логике есть 13 правил вывода Рабби Ишмаэля. Посылками для правил вывода служат стихи из Торы. Но есть еще метаправила — правила о том, как применять правила вывода. Например, два раза подряд нельзя использовать правило гзера-шава. Таким образом, еврейский вывод не монотоничен.

Благодаря этим метаправилам получается прикол.
(1) У нас есть нормальные линейные доказательства (как в обычной логике и математике). (2) У нас есть параллельные доказательства для тем, которые не пересекаются, и в этих доказательствах используются разные правила вывода (например, для данной темы никогда не используется правило каль-вахомер — таково метаправило). (3) И, наконец, внимание, у нас есть конкурирующие доказательства — параллельные, но по одной теме! И есть метаправила, кого можно выбрать из конкурирующих доказательств и в каких случаях.

Каково?

Есть математическая логика. Ее часто путают с символической логикой. Объясню разницу. Математическая логика — экспликация логики математиков, формализация математики. Символическая логика — любая логика, в которой вывод строится автоматически (машинно) на основании ряда правил. Таким образом, математическая логика — часть символической логики, но не наоборот. Есть еще философская логика как часть символической логики — свободно придумывается любая система вывода. Например, многозначная логика является символической логикой как философская логика, но она не является математической логикой. Ни один математик не доказал пока ни одной теоремы математики с помощью многозначной логики (не берем интуиционизм, они использовали логику Гёделя, частный случай BL). Есть еще прикладная логика как часть символической логики. Там придумываются системы вывода для информатики.

Еврейскую логику можно формализовать как философскую логику и сделать ее символической логикой. Это успешно делается целой группой разных ученых. Но речь пойдет не о еврейской логике, а о логике математической.

В программе Гильберта была высказана вера, что математическая логика вскорости покроет всю математику и формализует любое математическое доказательство. Но эта логика пукнула и застряла на простых вещах. Считалось, что арифметика будет базой новой математики. Ее хорошенько и разобрали. Но дальше так и не продвинулись. Например, оказалось, что в теорию множеств математику засунуть нельзя. А с формализацией математических доказательств и вовсе вышла проблема. Даже простые теории не умещаются в логику предикатов первого порядка. А за ее пределами логика слепа и двигается на ощупь.

В итоге математическая логика перестала развиваться и ушла в философскую логику или прикладную. А знаете почему? Потому что математические логики были не знакомы с еврейской логикой. Их желание уместить математическое доказательство в линейное доказательство глубоко болезненно: А1, А2, …, Ап, где Ап — вывод, а каждое утверждение А1, А2, …, Ап-1 есть либо аксиома для вывода Ап, либо получено из предыдущего утверждения с помощью правила вывода. Даже Талмуд в такие доказательства не умещается, а математика и подавно.

Есть Великая теорема Ферма. Ее было сложно доказать не потому, что она такая сама по себе сложная, а потому, что ее утверждение независимо от базовых утверждений формальной арифметики. Это значит, нам нужно придумать для арифметики совершенно новые конструкции, расширить арифметику, внести новые допущения. И вот тогда Великую теорему Ферма можно было доказать.

Так в математике все и работает. Придумывается теория. А затем она расширяется новыми конструкциями. Эти новые конструкции — гибриды. Они не вытекают из аксиом теории. Ну не следует Великая теорема Ферма из аксиом формальной арифметики. Как бы Вы не старались. Ну не следует Проблема Пуанкаре, решенная Перельманом, из базового курса топологии Александрова.

А теперь подумаем, как формализовать живое доказательство математиков, которое постоянно выходит за пределы исходной теории? Уж точно как линейное доказательство это не формализуемо. И вот здесь появляются параллельные и конкурирующие доказательства. Например, с аксиомой выбора поле действительных чисел линейно упорядочивается. Если мы отбросим эту идею, у нас возникнет поле гипердействительных чисел. Вот и вышел конкурирующий объект.

И вот для формализации математического доказательства стандартный аксиоматический метод не работает. Например, Великая теорема Ферма не выводима в формальной арифметике. Поэтому вместо аксиоматического метода мы должны использовать что-то иное. Например, нечеткие пересекающиеся друг с другом аксиомы. Скажем, вот в этом доказательстве Великой теоремы Ферма 90% аксиом формальной арифметики (нормальных, независимых утверждений), но 10% — гибридных допущений. Эти гибридные допущения как паразиты проникают еще в такие и такие нетривиальные доказательства. Они чаще всего пересекаются вот с такими другими гибридными допущениями. Эти допущения формализуемы как такие и такие нечеткие аксиомы. Лишь в процессе накопления нетривиальных доказательств эти аксиомы, лежащие в основе гибридных допущений, все более и более обретают четкость.

Итак, в большой математике нет линейных доказательств. Странно, что логики этого не понимали. Доказательства там — нелинейные, сообщающиеся (concurrent) — они используют гибридные допущения с пересекающимися нечеткими аксиомами.

И вот для такой логики тоже понадобятся метаправила — правила относительно правил вывода в математике. Мол здесь такие гибридные допущения не приемлемы, а здесь приемлемы в таком и таком виде.

Заметим, что 13 правил вывода Рабби Ишмаэля — это все выводы по аналогии, хотя и строгие, однозначные. Математическая логика с гибридными допущениями тоже станет использовать свои строгие правила аналогии.