Касательно теорем Гёделя о неполноте

[Tcirkubakin]

Да, я хотел таким образом написать про замену переменных(старался следовать нотации учебника). Что касается долларов в формуле, то я пытался указать, что y не принадлежит к множеству переменных формул альфа и терма t. Попытаюсь разобраться, как написать остальные формулы

[Tcirkubakin]

Для доказательства 13 формулы из 4 параг-фа 2 главы

$$\forall y(y=t\to \alpha \frac{y}{x})\equiv \alpha \frac{t}{x} \equiv \exists y(y=t\,\wedge \, \alpha \frac{y}{x}) \,(y \notin \, \text{var}\alpha, t)$$

мне не хатает вывода формулы

$$\varphi \frac{y}{x} \frac{t}{y}=\varphi \frac{t}{x}\,\text{for}\,y\notin \, \text{var$\varphi$} $$

Она доказыв-ся в упраж.4 к 2 параг-фу 2 главы, но разъяснения к нему у автора нет. Она очевидна, но как это строго доказать? Индукцией, или как-то ещё?

Следующая формула (в том же самом упраж-ии) не обяз-на для док-ва, но строгий вывод был бы интересен. Я правильно понял, что здесь знак = означает эквив-ность формул при применении к ним одинаковой модели с доп. условием, что модели x и t должны совпадать?

$$ \varphi \frac{t}{x} = \varphi\,\text{for}\,x\notin \, \text{free$\varphi$} $$

Пояснения(var-множество переменных, t дробь x это замена переменной x термом t и т.д; такова нотация автора)

[mihaild]

Да, такие вещи доказываются индукцией по построению формулы. Для примитивных термов $x \frac{y}{x} \frac{t}{y} = y\frac{t}{y} = t$ и $x \frac{t}{x} = t$, на остальные переменные ни та ни другая замена не влияет, дальше индукцией.

Знак $=$ в данном случае означает синтаксическое равенство формул. Эквивалентность формул это $\equiv$.

[Tcirkubakin]

Наконец дошло, благодарю. И напоследок. Если появятся новые вопросы, то дописывать в эту тему или для каждого создавать новые?

[mihaild]

Насколько я понимаю правила, новые вопросы в отдельную тему. Но вряд ли это так уж важно.

[KhAl]

(Оффтоп)

Anton_Peplov, пианист, mihaild
Раз уж зашла речь о "лучших" книгах по теореме Гёделя: что думаете о книжках Успенского, "Теорема Гёделя о неполноте" и Смаллиана, "Вовеки неразрешимое. Путь к Гёделю через занимательные загадки"? Они обе сделаны быть максимально простыми и идейно приблизить читателя к теореме Гёделя, при этом минимизируя формализм и количество сведений по мат. логике в целом. (хотя делают они это совершенно по-разному. во второй, если я не путаю, формулировки теоремы Гёделя вообще нет, зато она развивает навыки работы с "логическими" выражениями и вкладывает нужные идеи)

[пианист]

KhAl в сообщении #1578239 писал(а):

что думаете о книжках Успенского, "Теорема Гёделя о неполноте" и Смаллиана, "Вовеки неразрешимое. Путь к Гёделю через занимательные загадки"

К сожалению, не читал ни одну, ни другую, так что никакого мнения не имею.

[Anton_Peplov]

KhAl в сообщении #1578239 писал(а):

что думаете о книжках Успенского "Теорема Гёделя о неполноте"

Меня в свое время она скорее запутала, чем распутала. Успенский говорит о "синтаксической и семантической" формулировке теоремы Геделя о неполноте, но при этом не объясняет разницу между истинностью и выводимостью, между теорией моделей и теорией доказательств. В итоге читателю очень легко в этом месте напридумывать ерунды, что со мной тогда и произошло. Ясность внес только учебник.

KhAl в сообщении #1578239 писал(а):

Смаллиана, "Вовеки неразрешимое. Путь к Гёделю через занимательные загадки"

Не читал.