Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Например, $x \vee \neg x$? Можно использовать, к примеру,... - вопрос №1436313

стандартную гильбертову аксиоматику. Я смотрю на примеры доказательств (они не без помарок, но в общем понятные). Там вывод осуществляется из гипотез (которые неявно объединены в конъюнкцию), есть семантическое следование из них в доказываемое высказывание. Здесь же у нас нет гипотез, нет следования. Я где-то читал что-то в том роде, что мы можем вводить гипотезы — но как? Как конкретно доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Я пытаюсь решить (наметить план решения) третье задание следующего содержания (файлы PDF давать запрещено, поэтому перепишу основную его часть): «Написать программу, строящую доказательство указанного во входном файле высказывания (если оно общезначимо), либо дающую оценку пропозициональных переменных, на которых высказывание ложно (если оно опровержимо). Входной файл состоит из единственной строки, содержащей формулу исчисления высказываний, которую требуется доказать или опровергнуть. Высказывание удовлетворяет грамматике из первого задания. Выходной файл должен либо содержать доказательство высказывания (в формате доказательства из первого задания)…» Первое задание (тоже непонятно как решать) задаёт грамматику формами Бэкуса-Наура и его основная часть звучит следующим образом: «Написать программу, проверяющую доказательства в исчислении высказываний на корректность.Входной файл представляет из себя последовательность высказываний, по высказыванию на строку.… Результатом работы программы должен быть проаннотированный текст доказательства, касательно каждой строки должно быть указано, из чего и как она получается.»