Как доказать невыводимость используя правила вывода?

[Xaositect]

Dialectic в сообщении #408330 писал(а):

Берем формулы его, и подставляем в эти схемы, получаем в итоге аксиомы. Разве не так?

В конкретно этом случае - нет.
Аксиом ровно 4.
Например, $Y\to Y\vee Z$ будет не аксиомой, а теоремой, выводится из аксиомы b с помощью правила подстановки.

[Dialectic]

Xaositect в сообщении #408337 писал(а):

Dialectic в сообщении #408330 писал(а):

Берем формулы его, и подставляем в эти схемы, получаем в итоге аксиомы. Разве не так?

В конкретно этом случае - нет.
Аксиом ровно 4.
Например, $Y\to Y\vee Z$ будет не аксиомой, а теоремой, выводится из аксиомы b с помощью правила подстановки.

Ах, вон оно что... Теперь понятно, спасибо.

[epros]

creative в сообщении #408308 писал(а):

где именно можно прочитать об этом аспекте (а именно о том, что нельзя только в терминах аксиом и правил вывода судить о невыводимости некоторой формулы)?

А что значит "только в терминах аксиом и правил вывода"? Если это значит "используя только выводы в рамках данной системы", то вывод о невыводимости некой формулы конечно же невозможен. Но в рамках некоторой внешней теории это можно сделать.