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

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

* и посмотрим на соответствующую ей аксиому 
![$\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)
 обе истинны.
Придадим какие-нибудь значения 

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

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

. Когда 

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

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

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

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

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

, так что 

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

.
* Если 

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