А в матлогике такие, так скажем, наборы слов, про которые неизвестно, истинны они или нет, и предложениями-то не будут считаться, так что, соответственно, они и не могут служить посылками.
Что-то абсурд какой-то написан. "Предложение", оно же "высказывание", в математической логике определяется чисто синтаксически, так что всегда можно проверить, является ли высказыванием данная последовательность символов. А уж знает ли кто-нибудь, истинно оно или нет, к делу вообще никакого отношения не имеет.
А это уже вопрос к фантазии выводящего
Ничего подобного. Если высказывание недоказуемо, то никакая "фантазия выводящего" не поможет его доказать.
Расширьте базу формул.
Нельзя. Если мы добавим ещё одну аксиому (Вы ведь это имели в виду?), то получим другую формальную теорию. Естественно, в другой формальной теории высказывание может быть выводимым, но это не имеет никакого отношения к первоначальной теории.
Ведь, к примеру, как было с аксиомой параллельных? Сначала сказали: "Да, она верная", построили геометрию, начали применять ее для объяснения мира всем было хорошо, все смеялись. Потом всем математикам дружно подумалось: "а вдруг". Копали, копали вывели наконец-то, что она на следует из других аксиом и только после этого объявили ее полноценной, добавили ее в список формул.
Ничего подобного не было.
(Оффтоп)
Постулат о параллельных (пятый постулат) сформулировал Евклид (в его формулировке параллельные вообще не упоминались, но у этого постулата тьма эквивалентных формулировок). Впоследствии его (постулата) формулировка многим стала казаться слишком сложной и не очевидной, и его стали пытаться доказать, чтобы от него избавиться. Однако ничего не вышло.
В конце XVIII — начале XIX века нашлись три математика, которые пришли к выводу, что доказать пятый постулат нельзя, и что, приняв за аксиому утверждение, что этот постулат неверен, можно построить другую геометрию, столь же последовательную и непротиворечивую, как и геометрия Евклида, и занялись успешным построением этой геометрии. Первым был Карл Фридрих Гаусс, который утверждал, что это ему известно с 1792 года, но ничего на эту тему не публиковал, убоявшись "криков беотийцев" (хотя в частной переписке он на эту тему намёки делал). Практически одновременно (друг с другом, но не с Гауссом) к этому же выводу пришли Николай Иванович Лобачевский и Янош Бойяи (его фамилия в русской литературе имеет множество вариантов написания). Лобачевский опубликовал свой труд в 1829 году (был также доклад в 1826 году), а Бойяи — в 1932 году (имеется также письмо, датированное 1831 годом) в качестве приложения к учебнику математики своего отца. Сочинение это было написано на латинском языке, издано, видимо, малым тиражом и потому труднодоступно. В общем, на него никто не обратил внимание. Ну а Лобачевского его коллеги сочли чуть ли не сумасшедшим. Тем не менее, он продолжал развивать свою "воображаемую геометрию". Отношение к Лобачевскому изменилось уже после его смерти, когда в 1860 году была опубликована переписка Гаусса, в которой он восторженно отзывался о работах Лобачевского.
Вывод: список аксиом по мере необходимости может быть расширен, пусть даже с неимоверным скрипом.
Да, может быть, и такие случаи были.
(Оффтоп)
Например, к системе аксиом теории множеств, сформулированных Эрнстом Цермело в 1908 году, позже (в 1922 году) Абрахамом Френкелем была добавлена схема аксиом замены, поскольку оказалось, что схема аксиом выделения, сформулированная Цермело, недостаточна для формализации некоторых широко используемых математиками рассуждений. Ещё позже, в 1925 году, Джон фон Нейман добавил аксиому регулярности. За последующие 90 лет ни одной новой аксиомы к теории ZFC добавлено не было, несмотря на то, что в этой теории существует тьма интересных утверждений, которые нельзя ни доказать, ни опровергнуть.
Что касается аксиомы выбора, то никто её не добавлял. Она была с системе Цермело с самого начала. Она необходима, так как позволяет формализовать очень широко используемую в математике схему рассуждений. Споры были связаны с "неконструктивностью" этой аксиомы: она утверждает существование функции выбора, не указывая никакой конкретной функции. По этому поводу у меня есть некоторые замечания.
Во-первых, аксиома выбора не является единственным источником неконструктивности в современной математике. Например, классический закон исключённого третьего или доказательства "от противного" также являются неконструктивными.
Часто применяемый в рассуждениях оборот "пусть
— какая-нибудь точка интервала
…" также является источником неконструктивности. В случае интервала мы легко можем исправить эту неконструктивность, написав "пусть
; тогда
…", но множество, в котором нам нужна точка, может оказаться устроенным настолько сложно, что мы не сможем указать в нём никакую конкретную точку, несмотря на то, что совершенно точно знаем, что множество не пустое. Неконструктивность аксиомы выбора имеет точно такой же характер.
Во-вторых, как это ни странно, в конструктивной математике аксиома выбора верна (в соответствующей формулировке): если нам конструктивно задано некоторое семейство множеств и мы можем конструктивно доказать, что все эти множества непустые (это означает, что мы можем конструктивно указать конкретные элементы во всех множествах семейства), то нет ничего удивительного, что можно предъявить функцию выбора.