Теория доказательств для формул 2го порядка.

[Yorick]

Здравствуйте.
Плохо себе представляю, что есть доказательство формулы 2го порядка.
Понятный пример теории 2го порядка: https://en.wikipedia.org/wiki/Second-order_arithmetic
Верно ли, написанное ниже?
1) Похоже, что терм в полиморфном лямбда-исчисление (AKA System F) можно считать таким доказательством, да? (Как и любое другое из нужной половинки лямбда-куба.)
2) Однако явный терм - это конструктивное доказательство. (если отождествлять типы и утверждения).
А мне надо понимать как оперировать и с классическими, невычислимыми доказательствами.
3) В логике 1го порядка - есть корректность и полнота.
В логике 2го - только корректность.
Невозможно перечислить аксиомы/правил авывода и т.п.

Спрашиваю, потому что не понимаю что в таких теориях есть доказательство. (мне бы пример очень простого формального док-ва неарифметического(квантующего подмножества) утверждения про второпорядковую арифметику)

Нписанное выше я совершенно не понимаю, поэтому буду признателен за советы о том, какие книги по теме надо прочитать.
Спасибо.

[Pphantom]

Тема перемещена из форума «Математика (общие вопросы)» в форум «Помогите решить / разобраться (М)»

[stef]

Любое описание правил вывода дало бы нам возможность алгоритмически перечислять все доказательства, а тем самым, будь верна теорема полноты, и перечислять все истинные утверждения.

Во-первых, это можно опровергнуть чисто технически: утверждение об $\mathbb{N}$ истинно тогда и только тогда, когда оно следует в языке второго порядка из аксиом Пеано

$$ \forall x,y (S(x)=S(y) \rightarrow x=y), \forall x (\neg S(x)=0), \forall P ((P(0) \land (\forall x P(x) \rightarrow P(S(x)))) \rightarrow \forall x P(x))$$

Но множество всех истинных утверждений не может быть перечислимо алгоритмически по теореме Тарского о невыразимости истины.

Во-вторых, можно формализовать в логике второго порядка структуру $\mathcal{P}(\mathbb{N})$ (множество всех подмножеств $\mathbb{N}$), и получать из нашей гипотетической, пусть неэффективной системы доказательств различные утверждения. Однако среди утверждений о $\mathcal{P}(\mathbb{N})$ целая прорва фактов, в классической математике недоказуемых, и про которые большинство математиков не имеют консенсуса, следует ли их считать истинными. Простейший пример -- континуум-гипотеза (формализуемая как 'для любого множества множеств натуральных чисел есть либо его инъекция во множество натуральных чисел, либо его биекция на множество всех подмножеств натуральных чисел').

[george66]

Добавим к логике первого порядка переменные по высказываниям $\alpha,\beta\ldots$ и кванторы по ним. Правило введения для квантора всеобщности:
если мы доказали $\varphi(\ldots\alpha\ldots)$ из посылок, не содержащих $\alpha$ свободно
мы можем считать доказанным $\forall\alpha\varphi(\ldots\alpha\ldots)$
Например, если логика классическая, мы можем доказать
$\alpha\vee\neg\alpha$
и из этого вывести
$\forall\alpha(\alpha\vee\neg\alpha)$
Полиморфные лямбда-термы исчисления F соответствуют доказательствам примерно в таком исчислении (с квантором всеобщности по высказываниям). Правило удаления для квантора всеобщности можно записать так:
если мы доказали $\forall\alpha\varphi(\ldots\alpha\ldots)$
мы можем считать доказанным $\varphi(\ldots\psi\ldots)$
где вместо $\alpha$ подставляется произвольная формула $\psi$. Например, из
$\forall\alpha(\alpha\vee\neg\alpha)$
мы можем вывести (взяв в качестве $\psi$ формулу $\beta\Rightarrow\gamma$)
$(\beta\Rightarrow\gamma)\vee\neg(\beta\Rightarrow\gamma)$
Для арифметики второго порядка с переменными по множествам $P,Q\ldots$ выводы примерно такие же. Например, если логика классическая, мы можем вывести
$P(0)\vee\neg P(0)$ (другой вариант записи $(0\in P)\vee\neg(0\in P)$)
и из этого заключить
$\forall P(P(0)\vee\neg P(0))$
Чтобы сформулировать правило удаления, удобнее всего добавить к языку термы вида $\{n\mid\varphi(n)\}$ и аксиому
$\forall m( m\in\{n\mid\varphi(n)\}\Leftrightarrow\varphi(m))$
тогда правило удаления позволяет из формулы
$\forall P\varphi(P)$
вывести $\varphi(T)$
где T - любой терм второго порядка (то есть, обозначающий множество). Например, из формулы
$\forall P((0\in P)\vee\neg(0\in P))$
мы можем вывести (подставив вместо P терм $\{n\mid n=n+1\}$)
$(0\in \{n\mid n=n+1\})\vee\neg(0\in \{n\mid n=n+1\})$

-- 05.10.2017, 20:59 --

Что почитать - вопрос более сложный. Совсем доходчивого введения не знаю. Попробуйте начать с этой книжки
http://gen.lib.rus.ec/search.php?req=ur ... column=def