Пусть в схему можно подставить только формулы. При подстановке получаются новые формулы. Как проверить их истинность?
Ну вот вам неформальный набросок. Возьмём формулу

со свободными переменными

* и посмотрим на соответствующую ей аксиому
![$\varphi[0/x]\wedge\forall x(\varphi\to\varphi[Sx/x])\to\forall x\,\varphi$ $\varphi[0/x]\wedge\forall x(\varphi\to\varphi[Sx/x])\to\forall x\,\varphi$](https://dxdy-04.korotkov.co.uk/f/b/0/3/b0370ac97ff124c1805d1b5c8ab1da5e82.png)
схемы индукции. Надо проверить, что при всех значениях

если
![$A\equiv\varphi[0/x]\wedge\forall x(\varphi\to\varphi[Sx/x])$ $A\equiv\varphi[0/x]\wedge\forall x(\varphi\to\varphi[Sx/x])$](https://dxdy-02.korotkov.co.uk/f/1/5/5/155545a3b6c2c4bfdaa5c31e277ed90182.png)
истинна, то истинна и

, в стандартной интерпретации.

истинна тогда и только тогда, когда
![$A_0\equiv\varphi[0/x]$ $A_0\equiv\varphi[0/x]$](https://dxdy-04.korotkov.co.uk/f/b/6/6/b66101adf761877f8f03eac67f2510b882.png)
и
![$A_S\equiv\forall x(\varphi\to\varphi[Sx/x])$ $A_S\equiv\forall x(\varphi\to\varphi[Sx/x])$](https://dxdy-01.korotkov.co.uk/f/0/7/4/07477e063a50f171ca308c516381fa3982.png)
обе истинны.
Придадим какие-нибудь значения

. Интерпретация

при этом будет задавать какое-то подмножество

. Когда

истинна, это множество содержит ноль. Когда

истинна, это множество вместе с

содержит всегда

. Таким образом,

индуктивно, и

, так что

, и выполняется

.
* Если

не входит в них, ясно как.