Собственно, это примерно и есть математическая индукция
Не совсем. Если надо доказать истинность предиката для всех
![$n$ $n$](https://dxdy-02.korotkov.co.uk/f/5/5/a/55a049b8f161ae7cfeb0197d75aff96782.png)
- это индукция, а если построить функцию - это уже рекурсия.
По индукции доказывается, что для любого
![$i\in\mathbb{N}$ $i\in\mathbb{N}$](https://dxdy-02.korotkov.co.uk/f/d/7/f/d7f485c356a9b455ff39123c51610a0882.png)
существует функция
![$f_i: \{1,\cdots,i\}\to X$ $f_i: \{1,\cdots,i\}\to X$](https://dxdy-03.korotkov.co.uk/f/a/7/9/a798cbbf6935a32221c43cfa0ee9ff9182.png)
:
![$\\
f_1(1)\\
f_2(1), f_2(2)\\
f_3(1), f_3(2), f_3(3)\\
\cdots$ $\\
f_1(1)\\
f_2(1), f_2(2)\\
f_3(1), f_3(2), f_3(3)\\
\cdots$](https://dxdy-01.korotkov.co.uk/f/0/9/5/095c1a26ce1fafde5f7e0b176afc488582.png)
Мы с удовольствием объединили бы графики этих частичных функций и получили единую функцию
![$f: \mathbb{N}\to X$ $f: \mathbb{N}\to X$](https://dxdy-02.korotkov.co.uk/f/1/8/0/180c9f0894cda877c5a57f2fc05f064682.png)
, но для этого частичные функции должны быть согласованы друг с другом. Если рекурсивное определение однозначно определяет следующее значение на основе предыдущих (как, скажем, определение факториала), это очевидным образом соблюдается. А вот если написано "пусть предыдущие
![$i-1$ $i-1$](https://dxdy-03.korotkov.co.uk/f/6/f/4/6f471fb05a43809706b83a28f399076c82.png)
элементов выбраны, выберем какой-нибудь элемент из оставшихся", то без аксиомы выбора не обойтись, она дает нам функцию выбора, которую можно использовать в каждой частичной
![$f_i$ $f_i$](https://dxdy-02.korotkov.co.uk/f/9/b/6/9b6dbadab1b122f6d297345e9d3b8dd782.png)
и получить их согласованными. Можно сказать, что мы будем выбирать не какой-нибудь произвольный, а "самый первый" из оставшихся, чтобы выбор на каждом шаге стал однозначным.
Еще раз подчеркну: для построения каждой
![$f_i$ $f_i$](https://dxdy-02.korotkov.co.uk/f/9/b/6/9b6dbadab1b122f6d297345e9d3b8dd782.png)
аксиома выбора не требуется, она нужна, чтобы построить их согласованными.