Так сколько схем аксиом в ИВ?

[Sinoid]

Здравствуйте! Столкнулся с такой ситуацией. В книге Верещагина, Шеня "Языки и исчисления" приводится 11 схем аксиом как здесь. В задачнике же Лаврова, Максимовой приводится всего 10 аксиом, только вместо девятой аксиомы у них аксиома такая: $((A\supset\neg B)\supset(B\supset\neg A))$. То, что аксиомы разные при одинаковом их числе, объяснить можно. А вот почему в разных источниках их разное количество? И на каком наборе аксиом в действительности строится ИВ?

[Sonic86]

Очевидно, что системы аксиом у ИВ м.б. разные. Для системы аксиом даже требование независимости не обязательно. Отсюда все и следует.
Кроме того, в Игошине вообще всего 3 аксиомы, причем все 3 есть в каждом из приведенных Вами списков.

[arseniiv]

Sinoid
В действительности строится на любом достаточном. Например, если избавиться от всех связок кроме $\neg,\to$, можно использовать две схемы $((\varphi\to\psi)\to\chi) \to (\chi\to\varphi) \to \tau \to\varphi$, $(\neg\varphi\to\neg\psi)\to\psi\to\varphi$ (первая достаточна для вывода любых тавтологий, содержащих только импликацию; Лукасевич, 1948). Не исключено, что можно обойтись даже одной схемой с обеими связками, а так же одной (гигантской) схемой даже для традиционных наборов связок, но этим особо не интересовался.

-- Вс янв 29, 2017 19:15:02 --

А в сторону увеличения числа схем уже Sonic86 сказал. Так что в результате обеих возможностей сокращения (с учётом того, что я не в курсе, как далеко можно зайти, но фундаментальных ограничений этому не видно) и расширения схем может в принципе быть практически сколько угодно.

Кроме того, можно конвертировать схемы аксиом в правила вывода с нулём посылок и обратно. Это уже формализационное читерство, конечно, но возможность обойтись одними правилами вывода — это маленькая приятная деталь для тех, кому интересно, насколько единообразно можно определить систему вывода.

[Sinoid]

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

[Someone]

Sinoid в сообщении #1188325 писал(а):

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

Можно. И порочные круги здесь вообще ни при чём. Можете объявлять аксиомами любые утверждения, сформулированные в языке геометрии, лишь бы не возникало противоречий.

[Sinoid]

Someone в сообщении #1188335 писал(а):

Можно. И порочные круги здесь вообще ни при чём. Можете объявлять аксиомами любые утверждения, сформулированные в языке геометрии, лишь бы не возникало противоречий.

Да, правда, так более обще. Спасибо всем за помощь.