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