множество теорем IL (Интуционистская логика) перечислимо

zzzXAXAXAzzz

Задача. Докажите, что множество теорем IL (Интуционистская логика) перечислимо.
Опр. Мно-во слов M из A* перечислимо, если существует система Поста Е над А, такая что M=L(E).
Опр. L(E) = {a из A*| в Е выводится a} - язык, порожденный E.
Опр. Система Поста над А - это четвертка (A, B, V, S). где
1. A,B,V попарно непересекаются
2. S - множество кортежей вида (t_1,...,t_n, t где t_i, t принадлежит (A объедин. B объедин. V)*
A - основной алфавит, B - вспомогательный, V - множество переменных, S - множество схем.

zzzXAXAXAzzz

рассуждал так...
Очевидно, что нужно построить систему Поста.
Доказательство (скорее всего) начинается так...
Строим. Берем A={p, | (то есть у нас есть p_1, p_2,..., p_n & (лог. и логическое или, -> (лог. следует отрицание, скобки}
B={Lambda,F}, где Lambda и F - метки.
V={x,y} то есть переменные
Остается определить S
S = { Ap, \frac{Ax}{Ax|}, \frac{Ax}{Fx}, \frac{Fx}{F not(отрицание)x}, \frac{Fx,Fy}{F(x&y)}, \frac{Fx,Fy}{F(x или y)}, \frac{Fx,Fy}{F(x->y)}, \frac{Fx}{x} + аксиомы IL, правило вывода (Mp) }
Соответственно как вывести аксиомы и правило вывода я не знаю...
Аксиомы я перечислю, чтобы путаницы не было (брал с вики):
1. A->(B->A)
2. A->(B->C)->A->B)->(A->C
3. A & B -> A
4. A & B -> B
5. A -> (B -> A&B)
6. A->A или B
7. B -> A или B
8. (A->C) -> ( (B->C) -> (A или B -> C) )
9. NOT(A) -> (A -> B)
10. (A -> B) -> ( (A->NOT(B -> NOT(A) )
Правило вывода (Mp) (оттудаже)
\frac{A, A->B}{B} - схематичная запись. Смысл, что если мы доказали А, и из А следует В, то мы доказали и В

luherstag

Жесть про систему Поста.
Теорема - это ведь выводимая формула? Надо перебирать всевозможные выводы.

zzzXAXAXAzzz

Конечно жесть, но лектор давал определение именно через систему Поста, такое решение и просит.
Оставить комментарий
Имя или ник:
Комментарий: