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