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

Арифметизация метаматематики
http://forum.nsu.ru/viewtopic.php?f=24&t=18961
Страница 1 из 1

Автор:  Amigo [ Сб июл 26, 2008 8:09 pm ]
Заголовок сообщения:  Арифметизация метаматематики

Господа, подскажите пожалуста, как можно арифметизировать метавысказывание - "Данная формула есть аксиома ФТЧ".
ФТЧ - формальная теория чисел.

Автор:  Коба [ Вс июл 27, 2008 3:52 am ]
Заголовок сообщения: 

Ох, опять Вы за своё...

Для начала определитесь с тем, что такое "арифметизация". Скорее всего Вы имеете в виду некое соответствие, которое высказываниям метаязыка (например, утверждению о доказуемости некоторой формулы из некоторого конкретного списка аксиом) сопоставляет высказывания формального языка теории чисел. Аргументами (специалисты по математической логике предпочитают вместо слова "аргументы" употреблять термин "свободные переменные") высказываний метаязыка являются формулы, аргументами формул формального языка --- числа. Кроме того, имеется некая нумерация формул. Ну и тогда если формула формального языка истинна не некотором наборе чисел в том и только в том случае, когда другая формула --- формула метаязыка истинна на наборе формул, номерами которых являются эти числа, то логично называть первую формулу "арифметизацией" последней.

Теперь у Вас что есть? Если формула метаязыка Ф(а), утверждающая, что а --- формула формального языка, являющаяся аксиомой формальной теории. Вам надо найти формулу формального языка ф(x), истинную тогда и только тогда, когда x является номером некоторой формулы, на которой истинно Ф. Ну и в чём проблемы? Вперёд, как говориться, и с песней! Программируем на машине Тьюринга алгоритм, распознающий номера аксиом, находим номер программы, берём формулу формального языка, представляющую универсальную частично рекурсивную функцию и подставляем туда всё, что надо. Процесс этот долгий, трудный и кропотливый, требующий большого количества бумаги и многодневных нетривиальных вычислений с большими числами. А главное в этом процессе то, что он никому нахер не нужен. Но если уж приспичило --- флаг, как говориться, в руки!

Автор:  Amigo [ Вс июл 27, 2008 1:35 pm ]
Заголовок сообщения: 

Коба писал(а):
Ох, опять Вы за своё...

Так шо делать? Я по своей дурости стал вникать в различные разделы логики: исчисление высказываний, предикатов и д.р.Уже потрачено не мало времени и бросать сейчас, когда я , как кажется, уже дошёл до того, что понял каким образом можно арифметизировать метавысказывание –"формула F1 есть подформула формулы F2" - меня жаба душит…

Коба писал(а):
Для начала определитесь с тем, что такое "арифметизация". Скорее всего Вы имеете в виду некое соответствие, которое высказываниям метаязыка (например, утверждению о доказуемости некоторой формулы из некоторого конкретного списка аксиом) сопоставляет высказывания формального языка теории чисел. Аргументами (специалисты по математической логике предпочитают вместо слова "аргументы" употреблять термин "свободные переменные") высказываний метаязыка являются формулы, аргументами формул формального языка --- числа. Кроме того, имеется некая нумерация формул. Ну и тогда если формула формального языка истинна не некотором наборе чисел в том и только в том случае, когда другая формула --- формула метаязыка истинна на наборе формул, номерами которых являются эти числа, то логично называть первую формулу "арифметизацией" последней.

Совершенно верно. Приведу пример:
пусть имеются две формулы F1 и F2 имеющие геделевские номера N1 и N2. Допустим мы хотим арифметизировать метаутверждение –«формула F1 есть подформула формулы F2 ФТЧ». Очевидно, что формула F1 есть подформула формулы F2, тогда и только тогда, когда N1 делит N2. На языке арифметики, это можно записать так:]a: a*N1=N2. ( ] – существует, \/ - для любого).
Таким образом метапредикат –"формула F1 есть подформула формулы F2 ФТЧ" может быть изображён внутри ФТЧ, посредством формулы
]a: a*N1=N2.
Моя ближайшая цель, состоит теперь в том, что бы арифметизировать следующие метапредикаты:
1. Формула F есть аксиома ФТЧ.
2. Последовательность формул ФТЧ F1,F2,..,Fn, обладает свойством – каждая из них либо аксиома, либо для формулы с номером h –существуют такие номера I,j что ( i меньше h), (j меньше h) и формулы Fi, Fj = Fi-->Fh – имеются в нашей последовательности.

Коба писал(а):
Теперь у Вас что есть? Если формула метаязыка Ф(а), утверждающая, что а --- формула формального языка, являющаяся аксиомой формальной теории. Вам надо найти формулу формального языка ф(x), истинную тогда и только тогда, когда x является номером некоторой формулы, на которой истинно Ф. Ну и в чём проблемы? Вперёд, как говориться, и с песней! Программируем на машине Тьюринга алгоритм, распознающий номера аксиом, находим номер программы

Как мне составить этот алгоритм? Я пока не вижу этого даже просто, в так сказать «алгоритмической схеме», не то, что записанный на машине Тьюринга. Вот к примеру несколько формул ФТЧ:
1.X-->((X’-->X) -->X)
2.(X’-->X)-->((X-->X’) -->(X’-->X))
3. ((X’-->X) -->X)-->(((X-->X’) -->X’) -->((X’-->X) -->X)) ,где вместо Х можно подставить любое арифметическое выражение, например: SS0+SS0=SSS0.
Все они получены по схеме (F-->(G-->F)), потому являются аксиомами, но они визуально настолько разные, что я никак не могу понять, что между ними общего. И как составить алгоритм, распознающий аксиомность, мне совершенно не ясно.

Автор:  Коба [ Вс июл 27, 2008 3:23 pm ]
Заголовок сообщения: 

Amigo писал(а):
Я по своей дурости стал вникать в различные разделы логики...

И как составить алгоритм, распознающий аксиомность, мне совершенно не ясно.


Пусть AGu с Вами занимается, он энтузиаст.

А мой совет: возьмите нормальный задачник по мат. логике и прорешайте самостоятельно десяток-другой секвенций. Если сделаете это, все вопросы сами-собой рассосутся.

Автор:  Amigo [ Вс июл 27, 2008 3:50 pm ]
Заголовок сообщения: 

Эх, жаль, что энтузиазм, сегодня такая редкая добродетель...

Автор:  AGu [ Вс июл 27, 2008 7:21 pm ]
Заголовок сообщения: 

Amigo писал(а):
Все они получены по схеме (F-->(G-->F)), потому являются аксиомами, но они визуально настолько разные, что я никак не могу понять, что между ними общего.

Между ними общего -- то, что они получены по схеме (F-->(G-->F)). :-)

Пусть f(x,y,z) -- формула, код которой арифметизирует тот факт, что x -- это код формулы, имеющей вид (F-->(G-->F)), где F -- формула с кодом y, а G -- формула с кодом z. (Как именно выглядит формула f(x,y,z) -- зависит от способа арифметизации связки "-->".) Тогда аксиомы, полученные по схеме (F-->(G-->F)), можно арифметизовать кодом формулы (Ey)(Ez) f(x,y,z).

Собственно, все арифметизируется примерно в таком духе. Нужно просто произнести вслух утверждение, продлежащее арифметизации (например, "x является аксиомой ФТЧ"), максимально подробно раскрыть все сокращения в этой фразе (например, "x является аксиомой ФТЧ" <=> "[существует такая формула F, что x имеет вид (F-->F)] или [x такое] или [x сякое] или [...] или ..."), разбить полученую гигантскую фразу на более простые и каждую из них тупо записать в виде формулы. Ну а потом вычислить код полученной формулы, естессно.

Арифметизацию конкретных утверждений вряд ли можно назвать общественно полезным трудом. Нормальные люди обычно останавливаются сразу после того, как убедят себя в том, что это в принципе возможно. :-)

Автор:  Amigo [ Пн июл 28, 2008 2:04 am ]
Заголовок сообщения: 

Уважаемый AGu огромное спасибо Вам за участие, но к сожалению мне завтра на работу, поэтому подумать над тем, что Вы сказали, я смогу не раньше пятницы. Хотя постараюсь найти время и раньше. Спасибо.

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