Я хочу сказать о том, как выглядит начальная «теория». Как уже было сказано, вместо совокупностей должны быть строки (списки, кортежи, конечные последовательности) символов.
SomePupil в сообщении #1300361
wrote:
Преподаватель ответила "про совокупности символов". Я переспросил: "Значит, все-таки про множества символов?" После нескольких итераций преподаватель невольно согласилась, что говорится о множествах. Я бы сказал: "о строках символов".
Потом зашла речь про правила вывода. Оказывается, это отношения, заданные на формулах.
Эти отношения обычно бесконечны, поэтому в начальной теории их быть не может. В начальной теории правило вывода есть список вида (следствие, список посылок). Следствия и посылки — это формулы. С помощью правил вывода проверяется правильность вывода.
В целом для начальной теории достаточно конечных множеств, списков и конечных деревьев. Формулы — это списки символов, выводы (доказательства) — деревья. В принципе, можно сказать, что формулы — это деревья, да и доказательства оформить в виде списков символов, но традиционно так, как выше.