Логическая гармония , название, придуманное Майклом Дамметом , является предполагаемым ограничением правил вывода , которые могут использоваться в данной логической системе .
Логик Герхард Гентцен предположил, что значения логических связок могут быть заданы правилами их введения в дискурс. Например, если кто-то считает, что небо голубое, а также считает, что трава зеленая , то можно ввести связку и следующим образом: Небо голубое И трава зеленая. Идея Генцена заключалась в том, что подобные правила придают смысл чьим-то словам или, по крайней мере, определенным словам. Эта идея также была связана с витгенштейновским представлением о том, что во многих случаях мы можем сказать, что значение — это использование . Большинство современных логиков предпочитают думать, чтоправила введения и правила исключения выражения одинаково важны. В этом случае и характерны следующие правила:
Очевидная проблема с этим была указана Артуром Прайором : почему мы не можем иметь выражение (назовем его " тонк "), правило введения которого является правилом ИЛИ (от "р" до "р тонк q"), но чье правило исключения это И (от "p tonk q" до "q")? Это позволяет нам вывести что угодно из любой отправной точки. Прайор предположил, что это означает, что правила вывода не могут определять значение. Ему ответил Нуэль Белнап , что, хотя правила введения и исключения могут составлять значение, не любая пара таких правил будет определять осмысленное выражение — они должны удовлетворять определенным ограничениям, таким как не позволять нам выводить какие-либо новые истины из старого. запас слов.
Таким образом, гармония относится к определенным ограничениям, которые система доказательства должна поддерживать между правилами введения и исключения, чтобы она была значимой, или, другими словами, чтобы ее правила вывода были смыслообразующими.
Применение гармонии к логике можно считать частным случаем; имеет смысл говорить о гармонии применительно не только к системам вывода, но и к концептуальным системам в человеческом познании, и к системам типов в языках программирования.
Семантика этой формы не бросила серьезного вызова семантике, изложенной в семантической теории истины Тарского , но многие философы, заинтересованные в воссоздании семантики логики таким образом, чтобы уважать смысл Людвига Витгенштейна , считали, что гармония сохраняется . ключ.