Без заголовка
Я продолжаю утверждать, что в мозгу есть два разных когнитивных механизма: статистический (контент-анализ, ассоциации и аналогии, марковские цепи и т.д.) и формально-логический (с HOL).
Насчет формально-логического - все сложнее.
Всякие формальные логики - это скорее способы записи (формализации то бишь) рассуждений, со всякими разными полезными свойствами, типа системы типов, которые гарантируют отсутствие некоторых неприятных возможностей, но одновременно сужают в чем-то выразительные возможности. Как говориццо, теорема Гёделя о неполноте и все такое.
К примеру, для математиков HOL недостаточно - хотя вроде как все эти логики и придумывали для формализации математики. Но разные варианты HOL заточены под разные математические проблемы, а для других они бывают сильно не удобны.
Вобщем я бы сказал что формальные логики - это способ держать буйную фантазию в узде, что одновременно и приземляет ее к реальности и ограничивает.