2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Теория доказательств для формул 2го порядка.
Сообщение05.10.2017, 00:25 


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

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

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

 Профиль  
                  
 
 Posted automatically
Сообщение05.10.2017, 01:09 
Супермодератор
Аватара пользователя


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

 Профиль  
                  
 
 Re: Теория доказательств для формул 2го порядка.
Сообщение05.10.2017, 08:38 


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

Во-первых, это можно опровергнуть чисто технически: утверждение об $\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})$ целая прорва фактов, в классической математике недоказуемых, и про которые большинство математиков не имеют консенсуса, следует ли их считать истинными. Простейший пример -- континуум-гипотеза (формализуемая как 'для любого множества множеств натуральных чисел есть либо его инъекция во множество натуральных чисел, либо его биекция на множество всех подмножеств натуральных чисел').

 Профиль  
                  
 
 Re: Теория доказательств для формул 2го порядка.
Сообщение05.10.2017, 20:52 
Заслуженный участник


31/12/15
884
Добавим к логике первого порядка переменные по высказываниям $\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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 4 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group