Давайте от начала к концу. Зачем вообще нужны аксиоматические теории? Это один из способов определить множество истинных формул (в данном случае это ровно тавтологии, но в логике первого порядка ситуация становится интереснее), которое обычно бесконечное. Взяв любую формулу, было бы неплохо иметь алгоритм, определяющий её истинность (поскольку, ну знаете, не все множества разрешимы и уж тем более счётны — математика против этого ничего не имеет, а вот нам для счёта это очень полезно). Иногда он есть — в частности, в случае исчисления высказываний. И, конечно, не один, но эта тема — про вывод.
Итак, вывод. Нужно, чтобы (1) всякая выводимая формула была истинной и (2) всякая истинная формула была выводимой. Если первого ещё добиться легко и можно много где (например, можно всегда обойтись пустым множеством выводимых формул), то второе требует от выбора аксиом аккуратности. Можно взять и не включить что-нибудь важное; можно усердно добавлять и не надобавляться (но нам повезло: исчисление высказываний конечно аксиоматизируемо). Правила вывода, как диктует первое, должны как минимум выводить из истинных посылок истинные заключения. MP этому удовлетворяет, а произвольное правило — смотреть надо.
Можно жить легко и просто, если взять упомянутые вами аксиомы со связками
![$\to,\neg$ $\to,\neg$](https://dxdy-02.korotkov.co.uk/f/5/4/b/54ba70700f82c65c4ee6b169b4f127e682.png)
и добавить к ним аксиомы, определяющие другие связки через эти (можно побольше). А также взять Modus ponens и добавить к нему другие правила вывода, включающие, например, те новые связки. Так мы не уменьшим множество теорем, которое уже содержит все тавтологии, но при неудаче (аксиомы — не тавтологии, правила вывода не удовлетворяют тому, что выше) можем сделать теоремой не тавтологию. Это всё придётся показать — при том, что трёх аксиом и MP было уже вполне достаточно.
Тут есть компромисс: связки можно определить, в принципе, как сокращения. То есть, смотрим на
![$A\vee B$ $A\vee B$](https://dxdy-01.korotkov.co.uk/f/4/e/f/4ef8bbb924df876bc1dc66378948866782.png)
, а видим
![$\neg A\to B$ $\neg A\to B$](https://dxdy-03.korotkov.co.uk/f/2/5/7/25764548064c6b1d828e15b315f8472d82.png)
; смотрим на
![$A\wedge B$ $A\wedge B$](https://dxdy-01.korotkov.co.uk/f/0/2/4/0241b8571863ad1e7b946ce2fa4466b382.png)
, а видим
![$\neg(A\to\neg B)$ $\neg(A\to\neg B)$](https://dxdy-01.korotkov.co.uk/f/0/5/1/05129667f27221f86e625b83aead1f0182.png)
и т. д.. Процедура перевода легко формализуется. Новые правила вывода можно тоже сделать «сокращениями», но сокращениями уже кусков вывода (из гипотез) — они потому будут зваться
производными правилами вывода. Удобные производные правила можно получить, «переведя» все аксиомы, например, системы Клини
(сюрприз внутри)
Клини как-то раз писал(а):
в производные правила, пользуясь и теоремой о дедукции. (Правда, сначала надо будет доказать из трёх аксиом остальные, если мы решили их не добавлять, и они станут тоже, по сути, производными правилами, но не такими удобными, какие можно получить допиливанием.) Например, из (4) можно получить правило вывода
![$\dfrac F{F\vee G}$ $\dfrac F{F\vee G}$](https://dxdy-02.korotkov.co.uk/f/d/7/4/d746318e919c2e821fdace88bf2db29782.png)
. Формализация перевода вывода, использующего производные правила, в вывод, их не использующий, тоже легка. В итоге ничего нового вводить не потребовалось — только добавить правила перевода, которые никак не влияют на связь выводимости в этой системе с истинностью выводимого.
или самое главное чтобы они содержали выбранные знаки?
Это в любом случае обязательно. Формула — это определённая строка над выбранным алфавитом, в который входящие в формулу связки не входить не могут.
Ну и немного ещё о том, важно ли, какие аксиомы выбирать: представьте, что формулы — это всего лишь произвольные непустые строки из двух букв A, B, и попробуйте найти какие-нибудь аксиомы и правила вывода, чтобы выводились все строки с чётным (конечно, включая ноль) числом A и не выводились с нечётным (и других нет). Это довольно просто — и алфавит маленький, и правила определения «истинности» простые.