Ну да, я как раз и пытаюсь понять разницу между свободными переменными и переменными под квантором всеобщности. Так что фраза «параметрами там просто называются свободные переменные формулы» мало что объясняет в этом плане.
А, это. Раз значение формулы не зависит от значений переменных, которые в ней связаны, то можно считать, что их в ней вообще нет: вы уже видели эквивалентность формул
и
. Использование кванторов с переменными — это просто более частое из двух соглашений, оба из которых ведут к своим неудобствам при описании (это — к недопустимым заменам); другое соглашение — это
индексы де Брёйна (de Bruijn) [не смотрите на λ-исчисление, они применимы и здесь], и дня него, в свою очередь, при подстановке надо сделать кое-какие действия с индексами и вообще иметь расширенный для этого синтаксис формул. Зато нет необходимости в переименовании связанных переменных, и две эквивалентные по такому преобразованию формулы в таком случае переводятся в одну и ту же.
Может я действительно чего-то не понимаю. Преобразуйте вывод
в вывод
на примере этого вывода:
Этого я как раз сделать сейчас не могу, потому что у меня нет выводов
,
. Могу только показать «шаблон» вывода:
(Но в книге вы нечто подобное и так видели, так что вряд ли это ново.) Пометка «inc[lude].
, номера» тут означает, что мы выше помеченной формулы включили (но не показали здесь — оттого индексы у меня не конкретные числа) вывод, которым было доказано
, во всех его формулах сделав одинаковые замены так, чтобы гипотезы превратились в формулы нашего вывода по указанным номерам,* а
превратилась в формулу, которая помечена этим самым inc.. Это не более чем сокращённая запись, если использованные выводимости у нас до этого уже были показаны. Как раз-таки две последние пока здесь и не показаны!
* Если гипотезы в inc-выводе стоят не в том же порядке, что формулы у нас в шаблоне, мы переставляем куски одного из выводов соответствующим образом; такое действие не влияет на корректность вывода, т. к., по сути, это укладка специального вида орграфа в «массив» (наверно, вы видели, как бинарные деревья иногда представляют массивом, а не динамической структурой с блоками где попало в виртуальной памяти), и частичный порядок, задаваемый этим графом, можно дополнить до линейного порой не единственным способом. В принципе, если все выводы строить специальным образом, то переставление кусков, вроде, не понадобится. (Если это заинтересовало, но не понятно, обсудим ниже этого поста. Вам такая процедура не понадобится, потому что наши пропозициональные штучки имеют по одной гипотезе, и их выводы мы сразу сделаем так, чтобы эта гипотеза была самой первой. В таком случае никаких смещений не нужно.)
Как
я обозначил первое правило Бернайса.
И вот чтобы понять, как по такому шаблону получить вывод, я и предлагал те штучки с конъюнкциями в предыдущем посте. Вот как это сработает с ними.
Вывод
простой:
(Формулы я пронумеровал буквами для будущего удобства.)
Вывод
можно составить теперь такой:
Зная вывод
, мы теперь можем его корректно вставить. Я сделаю два столбца индексов, дополнительно показывая индексы формул из этого вывода, заменой которых получились конечные.
Всё! Получен корректный вывод
.
Как здесь видно, «inc-сокращения» в использовании неотличимы от правил вывода. Мы можем предположить, что такие правила (
производные правила вывода) у нас действительно есть наряду с MP и правилами Бернайса, и выводить с помощью них что-нибудь — а потом мы просто воспринимаем полученный вывод как сокращение, а вместо применений производных правил вставлять соответствующие выводы как это делалось выше. Надеюсь, вы о производных правилах вывода уже где-нибудь читали, но просто не успели составить картину.
Если применения правил вывода сравнить с вызовами функций (а аксиомы — константы), то разворачивание производных правил вывода аналогично компиляции inline-функций, код которых с соответствующими изменениями засовывается прямо в вызывающий код. Кстати, в подобной аналогии можно последнюю формулу вывода обозвать результатом, а гипотезы — аргументами какой-то функции. (В результате мы получили кривенькую аналогию изоморфизма Карри—Говарда, но про него уже другая история.
)
-- Ср май 06, 2015 03:23:54 --(Оффтоп)
Оказалось, я скопировал недоредактированный вывод из вашего сообщения. Надеюсь, вы не против, если я его не буду менять у себя (и так сто лет писал
).
-- Ср май 06, 2015 03:39:45 --Ах да, чтобы не отрываться от смысла: когда математик говорит: «то-то и то-то по теореме такой-то» — он как раз использует производное правило вывода, подразумевая, что тот результат, где это всё он упомянул, можно переписать так, чтобы получился обычный вывод из одних только аксиом и гипотез теории. Корректность такого вывода притом зависит только от корректности вывода с производными правилами и корректности выводов, соответствующих самим этим правилам, и потому мы даже не пытаемся всё развернуть (и, наоборот, пытаемся отрефакторить всё так, чтобы выводы были поминиатюрнее, потому что в человеческую голову сразу много не влезает). Обычный математический текст можно понимать как много-много сокращений сначала введением производных правил в формальный вывод, а потом ещё приведением полученного вывода в читаемую форму с использованием остальной информации из контекста (и влияя на него тоже).
UPD: Исправил оригинальное написание де Брёйна.