последовательность является выводом в исчислении предикатов первого порядка:
1. А(х) - допущение
2. ∀xA(x) - генерализация 1
Но А(х) |- ∀хА(х) писать нельзя, так как такая запись со штопором используется только относительно выводов, в которых нет генерализации свободных переменных в допущениях?
В выражении А(х) переменная не связана
Это зависит от того, в рамках каких ограничений работаете. Например можно было бы полагать, что формулы из множества допущений должны быть замкнутыми. Вы можете просто припомнить, что такая выводимость по теореме дедукции позволяет построить доказательство соответствующей формулы (схемы формул). И в формулировке теоремы дедукции в книге, по которой вы работаете, будут указаны ограничения для теоремы дедукции (они могут быть разными). На них и ориентируйтесь (ну там и соответствующее определение вывода будет)
Мне интересно, как запрет на наличие символа в Г можно формализовать
В смысле как построить теорию с ограничениями? Или просто как можно было бы символьно записать?
Второе. Как x-variant формально, только вот это.
Обсуждают сегодня