НГУ
http://forum.nsu.ru/

Выводимы ли в ZF аксиомы Пеано ?
http://forum.nsu.ru/viewtopic.php?f=24&t=24209
Страница 1 из 1

Автор:  alex_dorin [ Пн дек 30, 2013 3:16 pm ]
Заголовок сообщения:  Выводимы ли в ZF аксиомы Пеано ?

Выводимы ли в ZF аксиомы Пеано ?

Автор:  AGu [ Пн дек 30, 2013 11:46 pm ]
Заголовок сообщения:  Re: Выводимы ли в ZF аксиомы Пеано ?

Если этой фразе придать должный смысл, то — да, выводимы. А смысл — такой: множество натуральных чисел, снабженое стандартными операциями, является "внутренней моделью" арифметики Пеано в ZF. Точнее говоря, если N(x) — классическая теоретико-множественная формализация утверждения "x является натуральным числом", 0(x) — формализация утверждения "x является нулем", s(x,y) — формализация утверждения "y является числом, следующим за x" и аналогично для сложения +(x,y,z) и умножения *(x,y,z), то в ZF доказуема релятивизация на N любой аксиомы (и теоремы) арифметики Пеано с соответствующими интерпретациями нуля 0, следования s, сложения + и умножения *.

Автор:  alex_dorin [ Вт дек 31, 2013 3:06 am ]
Заголовок сообщения:  О выводимости аксиом Пеано в ZF

Для представлении в ZF натуральных чисел я принял -
натуральное число -- конечное множество
арифметическая сумма 2- х натуральных чисел -- объединение 2-х непересекающихся множеств
арифметическое произведение 2-х натуральных чисел -- декартово произведение 2-х множеств
равенство 2-х натуральных чисел -- равномощнсть 2-х множеств

Однако, ни один пруверов за приемлемое время не смог доказать формулу
(a + b) * c = a * c + b * c

Автор:  AGu [ Вт дек 31, 2013 6:55 pm ]
Заголовок сообщения: 

Вероятно, пруверам оказался не по зубам такой подход. Не уверен, что это поможет, но попробуйте использовать определения из раздела "A standard construction" на странице Википедии Natural number. (Там, правда, не приведены определения для сложения и умножения.)

Страница 1 из 1 Часовой пояс: UTC + 7 часов
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/