вопрос по генценовскому анализу

[jhanjaa]

Пожалуйста, объясните, что значит выводимость из пустого контекста: $\vdash\Gamma$?
Ведь секвенция интуитивно вводится как импликация:$A\vdash\Gamma$ трактуется как А влечет $\Gamma$. Как, в таком случае, понимать импликацию с одним пустым членом? Ведь пустой - это не ноль или что-то еще определенное, что могло бы быть объектом категории, в которой моделируется логика.

[Sonic86]

Я не знаю, что такое генценовский анализ, более менее знаю, что такое исчисление высказываний (ИВ), потому отвечу в рамках ИВ.
В ИВ есть просто определение выводимости:
$A\vdash\Gamma$ тогда и только тогда, когда существует последовательность формул, каждая из которых - либо аксиома, либо принадлежит множеству гипотез $A$, либо получена из двух предыдущих формул по имеющемуся правилу вывода. При $A=\varnothing$ получаем просто вывод из аксиом (т.е. все-таки не из ничего).

jhanjaa в сообщении #745042 писал(а):

Как, в таком случае, понимать импликацию с одним пустым членом?

Интуитивно их можно рассматривать как самоочевидные истины - тавтологии. Можно также считать, что посылка импликации - тавтология. В конце концов, при формализации понятий интуитивный смысл может дополнятся или даже не сохранятся.

[jhanjaa]

Дополню. В линейной логике есть 0, который при интерпретации в моноиде (фазовом пространстве) почти всегда пустое множество. Но в аксиомах различаются вывод из пустого контекста и из 0: $\vdash 1$, но $\Gamma,0\vdash\Theta$. Т.е. из 0 выводится все, что угодно, а из пустого контекста только единица (нейтральный элемент тензорного произведения, наибольший открытый факт, $\bot^{\bot}$).

[Joker_vD]

"The interpretation of a sequent is that the conjunction of the formulas in the antecedent implies the disjunction of the formulas in the succedent. [...] A conjunction of zero formulas corresponds to true, and a disjunction of zero formulas corresponds to false."

Но это и так очевидно:

$$\frac{\vdash\Delta}{A\vdash\Delta}\quad(LW)$$

И стоит все-таки отличать суждения $A\vdash B$ от высказываний $\vdash A\supset B$ — да, у вас есть теорема о дедукции, но все равно, это разные вещи.

[jhanjaa]

И стоит все-таки отличать суждения $A\vdash B$ от высказываний $\vdash A\supset B$ — да, у вас есть теорема о дедукции, но все равно, это разные вещи.
Спасибо! И все-таки - в чем же разница? Ведь секвенция не определяется, а поясняется отсылкой к импликации: А влечет В?

[Joker_vD]

Разница в том, что секвенция "$A\vdash B$" не является формулой теории. Это отношение между множеством формул $\{A\}$ и формулой $B$. "$A\supset B$" же — это как раз формула теории, т.е. просто последовательность трех символов алфавита. Она не говорит вам абсолютно ничего о том, связаны ли (под)формулы "$A$" и "$B$" отношением вывода.

[jhanjaa]

Спасибо.

[Deggial]

jhanjaa, оформляйте, пожалуйста, цитаты правильно. Это можно делать ручками, либо пользоваться тегом quote с панели:

[quote="name"]bla-bla-bla[/quote]

либо с помощью кнопок и . В случае неправильного оформления тема будет перемещена в Карантин.