НГУ

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

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

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

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

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

_________________
Don't let the sun blast your shadow
Don't let the milk float ride your mind

Так шо делать? Я по своей дурости стал вникать в различные разделы логики: исчисление высказываний, предикатов и д.р.Уже потрачено не мало времени и бросать сейчас, когда я , как кажется, уже дошёл до того, что понял каким образом можно арифметизировать метавысказывание –"формула 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 – имеются в нашей последовательности.


Как мне составить этот алгоритм? Я пока не вижу этого даже просто, в так сказать «алгоритмической схеме», не то, что записанный на машине Тьюринга. Вот к примеру несколько формул ФТЧ:
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)), потому являются аксиомами, но они визуально настолько разные, что я никак не могу понять, что между ними общего. И как составить алгоритм, распознающий аксиомность, мне совершенно не ясно.

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

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

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

_________________
Don't let the sun blast your shadow
Don't let the milk float ride your mind

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

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

Между ними общего -- то, что они получены по схеме (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 сякое] или [...] или ..."), разбить полученую гигантскую фразу на более простые и каждую из них тупо записать в виде формулы. Ну а потом вычислить код полученной формулы, естессно.

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

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

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.