313
правок
Изменения
Новая страница: «Введем обозначение. Будем говорить, что <tex>\alpha (x_1, \dots x_n)</tex> — это формула с <tex>n</tex> своб...»
Введем обозначение. Будем говорить, что <tex>\alpha (x_1, \dots x_n)</tex> — это формула с <tex>n</tex> свободными переменными, если переменные <tex>x_1, ... x_n</tex> входят в <tex>\alpha</tex> свободно. Запись <tex>\alpha (y_1, \dots y_n)</tex> будем трактовать, как <tex>\alpha [x_1 := y_1, ... x_n := y_n]</tex>, при этом мы подразумеваем, что <tex>y_1, \dots y_n</tex> свободны для подстановки вместо <tex>x_1, \dots x_n</tex> в <tex>\alpha</tex>.
Также, запись <tex>B(x_1, \dots x_n) := \alpha(x_1, \dots x_n)</tex> будет означать, что мы определяем новую формулу с именем <tex>B</tex>. Данная формула должна восприниматься только как сокращение записи, макроподстановка.
{{Определение
|definition=
Арифметическая функция {{---}} функция <tex>f: N^n \rightarrow N</tex>.
Арифметическое отношение {{---}} <tex>n</tex>-арное отношение, заданное на <tex>N</tex>.
}}
{{Определение
|definition=
Арифметическое отношение <tex>R</tex> называется выразимым (в формальной арифметике), если существует такая формула <tex>\alpha (x_1, \dots x_n)</tex> с <tex>n</tex> свободными переменными, что для любых натуральных чисел <tex>k_1</tex> ... <tex>k_n</tex>
# если <tex>R(k_1, \dots k_n)</tex> истинно, то доказуемо <tex>\alpha (\overline{k_1}, \dots \overline{k_n})</tex>
# если <tex>R(k_1, \dots k_n)</tex> ложно, то доказуемо <tex>\neg \alpha (\overline{k_1}, \dots \overline{k_n})</tex>.
}}
Например, отношение <tex>(<)</tex> является выразимым в арифметике: Рассмотрим формулу <tex>\alpha (a_1, a_2) = \exists b (\neg b = 0 \& a_1 + b = a_2)</tex>. В самом деле, если взять некоторые числа <tex>k_1</tex> и <tex>k_2</tex>, такие, что <tex>k_1 < k_2</tex>, то найдется такое положительное число <tex>b</tex>, что <tex>k_1 + b = k_2</tex>. Можно показать, что если подставить <tex>\overline{k_1}</tex> и <tex>\overline{k_2}</tex> в <tex>\alpha</tex>, то формула будет доказуема.
Наметим доказательство: Тут должно быть два доказательства по индукции, сперва по <tex>k_2</tex>, потом по <tex>k_1</tex>. Рассмотрим доказательство по индукции: пусть <tex>k_1 = 0</tex>, индукция по 2-му параметру: Разберем доказательство базы при <tex>k_2 = 1</tex>. Тогда надо показать <tex>\exists b (\neg b = 0 \& 0 + b = 1)</tex>:
<table>
<tr class="odd">
<td align="left">(1)</td>
<td align="left"><tex>\neg 1 = 0 \& 0 + 1 = 1</tex></td>
<td align="left">Несложно показать</td>
</tr>
<tr class="even">
<td align="left">(2)</td>
<td align="left"><tex>(\neg 1 = 0 \& 0 + 1 = 1) \rightarrow \exists b (\neg b = 0 \& 0 + b = 1)</tex></td>
<td align="left">Cх. акс. для <tex>\exists</tex></td>
</tr>
<tr class="odd">
<td align="left">(3)</td>
<td align="left"><tex>\exists b (\neg b = 0 \& 0 + b = 1)</tex></td>
<td align="left">M.P. 1 и 2.</td>
</tr>
</table>
{{Определение
|definition=
Введем следующее сокращение записи: пусть <tex>\exists ! y \phi (y)</tex> означает <tex>\exists y \phi (y) \& \forall a \forall b (\phi(a) \& \phi(b) \rightarrow a=b)</tex> Здесь <tex>a</tex> и <tex>b</tex> — некоторые переменные, не входящие в формулу <tex>\phi</tex> свободно.
}}
{{Определение
|definition=
Арифметическая функция <tex>f</tex> от <tex>n</tex> аргументов называется представимой в формальной арифметике, если существует такая формула <tex>\alpha (x_1, \dots x_{n+1})</tex> с <tex>n+1</tex> свободными пременными, что для любых натуральных чисел <tex>k_1</tex> ... <tex>k_n</tex>
# <tex>f(k_1, \dots k_n) = k_{n+1}</tex> тогда и только тогда, когда доказуемо <tex>\alpha (\overline{k_1}, \dots \overline{k_{n+1}})</tex>.
# Доказуемо <tex>\exists ! b (\alpha (\overline{k_1}, \dots \overline{k_n}, b)</tex>
Комментарии:
Функция называется сильно представимой, если в свойстве 2 натуральные числа заменить на переменные: <tex>\exists ! b (\alpha (a_1, \dots a_n, b)</tex>
}}
Комментарии:
Очевидно, что сильно представимая функция также является представимой --- с помощью уже встречавшегося ранее трюка с введением квантора всеобщности, а потом с подстановкой конкретного терма вместо переменной мы можем подставить любые константы вместо переменных.
{{Теорема
|statement=
Функции <tex>Z</tex>, <tex>N</tex>, <tex>U^n_i</tex> являются представимыми.
|proof=
Наметим доказательство. Для этого приведем формулы, доказательство корректности этих формул оставим в виде упражнения.
* Примитив <tex>Z</tex> представит формула <tex>Z (a, b) := (a=a \& b=0)</tex>.
* Примитив <tex>N</tex> представит формула <tex>N (a, b) := (a' = b)</tex>.
* Примитив <tex>U^n_i</tex> представит формула <tex>U^n_i (a_1, ...a_n, b) = (a_1=a_1) \& ... \& (a_n=a_n) \& (b= a_i)</tex>.
}}
{{Теорема
|statement=
Если функции <tex>f</tex> и <tex>g_1</tex>, ... <tex>g_m</tex> представимы, то функция <tex>S\langle{}f,g_1,\dots g_m\rangle</tex> также представима.
|proof=
Поскольку функции <tex>f</tex> и <tex>g_i</tex> представимы, то есть формулы <tex>F</tex> и <tex>G_1, \dots G_m</tex>, их представляющие. Тогда следующая формула представит <tex>S\langle{}f,g_1,\dots g_m\rangle</tex>: <tex>S (a_1, \dots a_n, b) := \exists b_1 \dots \exists b_m
(G_1 (a_1, \dots a_n, b_1) \& \dots \& G_m (a_1, \dots a_n, b_m) \& F (b_1, \dots b_m, b))</tex>
}}
{{Определение
|definition=
Характеристическая функция арифметического отношения <tex>R</tex> — это функция <tex>C_R (x_1, ... x_n) = \left\{\begin{array}{ll}0 &R (x_1,...x_n)\\1 & R (x_1,...x_n) \textrm{ неверно}\end{array}\right.</tex>
}}
Очевидно, что характеристическая функция представима тогда и только тогда, когда отношение выразимо.
{{Определение
|definition=
<tex>\beta</tex>-функция Геделя - это функция <tex>\beta (b,c,i) = b \% (1 + c \cdot (i + 1))</tex>. Здесь операция (%) означает взятие остатка от целочисленного деления.
}}
{{Лемма
|statement=
Функция примитивно-рекурсивна, и при этом представима в арифметике формулой <tex>B (b,c,i,d) := \exists q ((b = q \cdot (1 + c \cdot (i+1)) + d) \& (d < 1 + c \cdot (i+1)))</tex>
|proof=
Упражнение.
}}
{{Лемма
|statement=
Для любой конечной последовательности чисел <tex>k_0</tex> ... <tex>k_n</tex> можно подобрать такие константы <tex>b</tex> и <tex>c</tex>, что <tex>\beta (b,c,i) = k_i</tex> для <tex>0 \le i \le n</tex>.
|proof=
Возьмем число <tex>c = max(k_1,\dots k_n,n)!</tex>. Рассмотрим числа <tex>u_i = 1 + c \cdot (i+1)</tex>.
* Никакие числа <tex>u_i</tex> и <tex>u_j</tex> <tex>(0 \le j < i \le n)</tex> не имеют общих делителей кроме 1. Пусть это не так, и есть некоторый общий делитель <tex>p</tex> (очевидно, мы можем предположить его простоту — разложив на множители, если он составной). Тогда <tex>p</tex> будет делить <tex>u_i - u_j = c \cdot (i - j)</tex>, при этом <tex>p</tex> не может делить <tex>c</tex> — иначе окажется, что <tex>u_i = (1 + c \cdot (i+1))</tex> делится на <tex>p</tex> и <tex>c \cdot (i+1)</tex> делится на <tex>p</tex>. Значит, <tex>p</tex> делит <tex>i-j</tex>, то есть все равно делит <tex>c</tex>, так как <tex>c</tex> — факториал некоторого числа, не меньшего <tex>n</tex>, и при этом <tex>i-j \le n</tex>.
* Каждое из чисел <tex>k_i</tex> меньше, чем <tex>u_i</tex>: в самом деле, <tex>k_i \le c < 1 + c \cdot (i+1) = u_i</tex>.
* Согласно китайской теореме об остатках, если некоторые натуральные числа <tex>u_0, \dots u_n</tex> попарно взаимно просты, то для любых целых чисел <tex>k_0, \dots k_n</tex>, таких, что <tex>0 \le k_i < u_i</tex>, найдется такое целое число <tex>b</tex>, для которого выполнено <tex>k_i = b \% u_i</tex>. Возьмем <tex>b</tex>, подсказываемое теоремой об остатках.
}}
{{Теорема
|statement= Всякая рекурсивная функция представима в арифметике.
|proof=
Представимость первых четырех примитивов уже показана. Покажем представимость примитивной рекурсии и операции минимизации.
Пусть есть некоторый <tex>R \langle{} f,g \rangle</tex>. Соответственно, <tex>f</tex> и <tex>g</tex> уже представлены как некоторые формулы <tex>F</tex> и <tex>G</tex>. Из определения <tex>R\langle{}f,g\rangle</tex> мы знаем, что для значения <tex>R \langle{} f,g \rangle (x_1,...x_{n+1})</tex> должна существовать последовательность <tex>a_0 ... a_{x_{n+1}}</tex> результатов применения функций f и g — значений на одно больше, чем итераций в цикле примитивной рекурсии, а это количество определяется последним параметром функции <tex>R \langle{}f,g\rangle</tex>. При этом:
Значит, по лемме, должны существовать такие числа <tex>b</tex> и <tex>c</tex>, что <tex>\beta (b,c,i) = a_i</tex> для <tex>0 \le i \le x_{n+1}</tex>.
Приведенные рассуждения позволяют построить следующую формулу, представляющую <tex>R\langle{}f,g\rangle (x_1, ... x_{n+1})</tex>:
<tex> R(x_1, \dots x_{n+1}, a) := \exists b \exists c (\exists k (B (b, c, 0, k) \& F (x_1,...x_n, k)) \& B(b, c, x_{n+1}, a) \& \forall k (k < x_{n+1} \rightarrow \exists d \exists e (B (b, c, k, d) \& B (b, c, k', e) \& G (x_1,..x_n, k, d, e)))</tex>
Рассмотрим конструкцию <tex>\mu\langle{}f\rangle</tex>. <tex>f</tex> уже представлено как некоторая формула <tex>F</tex>. Тогда формула <tex>M (x_1, \dots x_n,y) := F(x_1, \dots x_n,y,0) \& \forall z (z < y \rightarrow \neg F (x_1, \dots x_n,z,0))</tex> представит <tex>\mu\langle{}f\rangle</tex>.
}}
Также, запись <tex>B(x_1, \dots x_n) := \alpha(x_1, \dots x_n)</tex> будет означать, что мы определяем новую формулу с именем <tex>B</tex>. Данная формула должна восприниматься только как сокращение записи, макроподстановка.
{{Определение
|definition=
Арифметическая функция {{---}} функция <tex>f: N^n \rightarrow N</tex>.
Арифметическое отношение {{---}} <tex>n</tex>-арное отношение, заданное на <tex>N</tex>.
}}
{{Определение
|definition=
Арифметическое отношение <tex>R</tex> называется выразимым (в формальной арифметике), если существует такая формула <tex>\alpha (x_1, \dots x_n)</tex> с <tex>n</tex> свободными переменными, что для любых натуральных чисел <tex>k_1</tex> ... <tex>k_n</tex>
# если <tex>R(k_1, \dots k_n)</tex> истинно, то доказуемо <tex>\alpha (\overline{k_1}, \dots \overline{k_n})</tex>
# если <tex>R(k_1, \dots k_n)</tex> ложно, то доказуемо <tex>\neg \alpha (\overline{k_1}, \dots \overline{k_n})</tex>.
}}
Например, отношение <tex>(<)</tex> является выразимым в арифметике: Рассмотрим формулу <tex>\alpha (a_1, a_2) = \exists b (\neg b = 0 \& a_1 + b = a_2)</tex>. В самом деле, если взять некоторые числа <tex>k_1</tex> и <tex>k_2</tex>, такие, что <tex>k_1 < k_2</tex>, то найдется такое положительное число <tex>b</tex>, что <tex>k_1 + b = k_2</tex>. Можно показать, что если подставить <tex>\overline{k_1}</tex> и <tex>\overline{k_2}</tex> в <tex>\alpha</tex>, то формула будет доказуема.
Наметим доказательство: Тут должно быть два доказательства по индукции, сперва по <tex>k_2</tex>, потом по <tex>k_1</tex>. Рассмотрим доказательство по индукции: пусть <tex>k_1 = 0</tex>, индукция по 2-му параметру: Разберем доказательство базы при <tex>k_2 = 1</tex>. Тогда надо показать <tex>\exists b (\neg b = 0 \& 0 + b = 1)</tex>:
<table>
<tr class="odd">
<td align="left">(1)</td>
<td align="left"><tex>\neg 1 = 0 \& 0 + 1 = 1</tex></td>
<td align="left">Несложно показать</td>
</tr>
<tr class="even">
<td align="left">(2)</td>
<td align="left"><tex>(\neg 1 = 0 \& 0 + 1 = 1) \rightarrow \exists b (\neg b = 0 \& 0 + b = 1)</tex></td>
<td align="left">Cх. акс. для <tex>\exists</tex></td>
</tr>
<tr class="odd">
<td align="left">(3)</td>
<td align="left"><tex>\exists b (\neg b = 0 \& 0 + b = 1)</tex></td>
<td align="left">M.P. 1 и 2.</td>
</tr>
</table>
{{Определение
|definition=
Введем следующее сокращение записи: пусть <tex>\exists ! y \phi (y)</tex> означает <tex>\exists y \phi (y) \& \forall a \forall b (\phi(a) \& \phi(b) \rightarrow a=b)</tex> Здесь <tex>a</tex> и <tex>b</tex> — некоторые переменные, не входящие в формулу <tex>\phi</tex> свободно.
}}
{{Определение
|definition=
Арифметическая функция <tex>f</tex> от <tex>n</tex> аргументов называется представимой в формальной арифметике, если существует такая формула <tex>\alpha (x_1, \dots x_{n+1})</tex> с <tex>n+1</tex> свободными пременными, что для любых натуральных чисел <tex>k_1</tex> ... <tex>k_n</tex>
# <tex>f(k_1, \dots k_n) = k_{n+1}</tex> тогда и только тогда, когда доказуемо <tex>\alpha (\overline{k_1}, \dots \overline{k_{n+1}})</tex>.
# Доказуемо <tex>\exists ! b (\alpha (\overline{k_1}, \dots \overline{k_n}, b)</tex>
Комментарии:
Функция называется сильно представимой, если в свойстве 2 натуральные числа заменить на переменные: <tex>\exists ! b (\alpha (a_1, \dots a_n, b)</tex>
}}
Комментарии:
Очевидно, что сильно представимая функция также является представимой --- с помощью уже встречавшегося ранее трюка с введением квантора всеобщности, а потом с подстановкой конкретного терма вместо переменной мы можем подставить любые константы вместо переменных.
{{Теорема
|statement=
Функции <tex>Z</tex>, <tex>N</tex>, <tex>U^n_i</tex> являются представимыми.
|proof=
Наметим доказательство. Для этого приведем формулы, доказательство корректности этих формул оставим в виде упражнения.
* Примитив <tex>Z</tex> представит формула <tex>Z (a, b) := (a=a \& b=0)</tex>.
* Примитив <tex>N</tex> представит формула <tex>N (a, b) := (a' = b)</tex>.
* Примитив <tex>U^n_i</tex> представит формула <tex>U^n_i (a_1, ...a_n, b) = (a_1=a_1) \& ... \& (a_n=a_n) \& (b= a_i)</tex>.
}}
{{Теорема
|statement=
Если функции <tex>f</tex> и <tex>g_1</tex>, ... <tex>g_m</tex> представимы, то функция <tex>S\langle{}f,g_1,\dots g_m\rangle</tex> также представима.
|proof=
Поскольку функции <tex>f</tex> и <tex>g_i</tex> представимы, то есть формулы <tex>F</tex> и <tex>G_1, \dots G_m</tex>, их представляющие. Тогда следующая формула представит <tex>S\langle{}f,g_1,\dots g_m\rangle</tex>: <tex>S (a_1, \dots a_n, b) := \exists b_1 \dots \exists b_m
(G_1 (a_1, \dots a_n, b_1) \& \dots \& G_m (a_1, \dots a_n, b_m) \& F (b_1, \dots b_m, b))</tex>
}}
{{Определение
|definition=
Характеристическая функция арифметического отношения <tex>R</tex> — это функция <tex>C_R (x_1, ... x_n) = \left\{\begin{array}{ll}0 &R (x_1,...x_n)\\1 & R (x_1,...x_n) \textrm{ неверно}\end{array}\right.</tex>
}}
Очевидно, что характеристическая функция представима тогда и только тогда, когда отношение выразимо.
{{Определение
|definition=
<tex>\beta</tex>-функция Геделя - это функция <tex>\beta (b,c,i) = b \% (1 + c \cdot (i + 1))</tex>. Здесь операция (%) означает взятие остатка от целочисленного деления.
}}
{{Лемма
|statement=
Функция примитивно-рекурсивна, и при этом представима в арифметике формулой <tex>B (b,c,i,d) := \exists q ((b = q \cdot (1 + c \cdot (i+1)) + d) \& (d < 1 + c \cdot (i+1)))</tex>
|proof=
Упражнение.
}}
{{Лемма
|statement=
Для любой конечной последовательности чисел <tex>k_0</tex> ... <tex>k_n</tex> можно подобрать такие константы <tex>b</tex> и <tex>c</tex>, что <tex>\beta (b,c,i) = k_i</tex> для <tex>0 \le i \le n</tex>.
|proof=
Возьмем число <tex>c = max(k_1,\dots k_n,n)!</tex>. Рассмотрим числа <tex>u_i = 1 + c \cdot (i+1)</tex>.
* Никакие числа <tex>u_i</tex> и <tex>u_j</tex> <tex>(0 \le j < i \le n)</tex> не имеют общих делителей кроме 1. Пусть это не так, и есть некоторый общий делитель <tex>p</tex> (очевидно, мы можем предположить его простоту — разложив на множители, если он составной). Тогда <tex>p</tex> будет делить <tex>u_i - u_j = c \cdot (i - j)</tex>, при этом <tex>p</tex> не может делить <tex>c</tex> — иначе окажется, что <tex>u_i = (1 + c \cdot (i+1))</tex> делится на <tex>p</tex> и <tex>c \cdot (i+1)</tex> делится на <tex>p</tex>. Значит, <tex>p</tex> делит <tex>i-j</tex>, то есть все равно делит <tex>c</tex>, так как <tex>c</tex> — факториал некоторого числа, не меньшего <tex>n</tex>, и при этом <tex>i-j \le n</tex>.
* Каждое из чисел <tex>k_i</tex> меньше, чем <tex>u_i</tex>: в самом деле, <tex>k_i \le c < 1 + c \cdot (i+1) = u_i</tex>.
* Согласно китайской теореме об остатках, если некоторые натуральные числа <tex>u_0, \dots u_n</tex> попарно взаимно просты, то для любых целых чисел <tex>k_0, \dots k_n</tex>, таких, что <tex>0 \le k_i < u_i</tex>, найдется такое целое число <tex>b</tex>, для которого выполнено <tex>k_i = b \% u_i</tex>. Возьмем <tex>b</tex>, подсказываемое теоремой об остатках.
}}
{{Теорема
|statement= Всякая рекурсивная функция представима в арифметике.
|proof=
Представимость первых четырех примитивов уже показана. Покажем представимость примитивной рекурсии и операции минимизации.
Пусть есть некоторый <tex>R \langle{} f,g \rangle</tex>. Соответственно, <tex>f</tex> и <tex>g</tex> уже представлены как некоторые формулы <tex>F</tex> и <tex>G</tex>. Из определения <tex>R\langle{}f,g\rangle</tex> мы знаем, что для значения <tex>R \langle{} f,g \rangle (x_1,...x_{n+1})</tex> должна существовать последовательность <tex>a_0 ... a_{x_{n+1}}</tex> результатов применения функций f и g — значений на одно больше, чем итераций в цикле примитивной рекурсии, а это количество определяется последним параметром функции <tex>R \langle{}f,g\rangle</tex>. При этом:
Значит, по лемме, должны существовать такие числа <tex>b</tex> и <tex>c</tex>, что <tex>\beta (b,c,i) = a_i</tex> для <tex>0 \le i \le x_{n+1}</tex>.
Приведенные рассуждения позволяют построить следующую формулу, представляющую <tex>R\langle{}f,g\rangle (x_1, ... x_{n+1})</tex>:
<tex> R(x_1, \dots x_{n+1}, a) := \exists b \exists c (\exists k (B (b, c, 0, k) \& F (x_1,...x_n, k)) \& B(b, c, x_{n+1}, a) \& \forall k (k < x_{n+1} \rightarrow \exists d \exists e (B (b, c, k, d) \& B (b, c, k', e) \& G (x_1,..x_n, k, d, e)))</tex>
Рассмотрим конструкцию <tex>\mu\langle{}f\rangle</tex>. <tex>f</tex> уже представлено как некоторая формула <tex>F</tex>. Тогда формула <tex>M (x_1, \dots x_n,y) := F(x_1, \dots x_n,y,0) \& \forall z (z < y \rightarrow \neg F (x_1, \dots x_n,z,0))</tex> представит <tex>\mu\langle{}f\rangle</tex>.
}}
