Категорная логика - как вводится истинность?

[jhanjaa]

Здравствуйте! Пожалуйста, может кто знает или даст ссылку:
При интерпретации линейной логики в *-автономной категории (или интуиционистской в замкнутой моноидальной) формулы интерпретируются как объекты, доказательства - как стрелки и из тривиального набора аксиом с помощью правил вывода, интерпретирующих операции, получаются объекты-следствия. Все такие объекты по построению истинны. Но ведь есть и ложные формулы. Как же они получаются?

Тот же вопрос иначе: категорная логика имеет дело с доказательствами, но не имеет дело с истинностью. Есть ли какой-то внутренний способ ввести понятие истинности в такую интерпретацию логики? Например, в топосах есть объект истинностных значений и истинностные стрелки. Здесь же ничего подобного мне найти не удалось. Есть только начальный и терминальный объекты; дуализирующий объект, тензорная 1, которые в каком-то смысле аналогичны true и false, но оценки истинности формул нет.

[JMH]

Не уверен, что вполне понимаю Ваш вопрос, если не в тему - игнорируйте. В теории категорий истина и ложь - наименования специфичных морфизмов, не более; посмотреть можно в Goldblatt, "Topoi".

P.S. Ищите в глоссарии "true", "false".

[jhanjaa]

Так, в частности, в том-то и вопрос - есть ли в моноидальных замкнутых категориях объект истинностных значений, как в топосах? Т.е. есть ли в таких категориях объекты-степени?
Но шире, как вообще при таком подходе к логике, когда интересует доказательство, а не истинность, в произвольной категории ввести такое понятие истинности?

[jhanjaa]

Ну, вот http://ncatlab.org/nlab/show/power+object - для наличия объекта-степени категория должна быть конечно полна. Если при этом объект-степень есть для любого объекта, то - это топос.
Остается общий вопрос - как вводить истинность в категорной логике.

[jhanjaa]

Если кто заинтересовался, то может посмотреть ссылки здесь: http://ncatlab.org/nlab/show/linear+logic