为了定义非负整数集合作为其定义域的函数，使用两个步骤：
基础步骤：规定这个函数在0处的值。递归步骤：给出从较小的整数处的值来求出当前的值得规则。例1 假定f是用f(0)=3,f(n+1)=2f(n)+3来递归定义的。求出f(1)、f(2)、f(3)和f(4)。
解：从这个递归定义得出
$$f(1)=2f(0)+3=2 \cdot 3 + 3 = 9$$$$f(2)=2f(1)+3=2 \cdot 9 + 3 = 21$$$$f(3)=2f(2)+3=2 \cdot 21 + 3 = 45$$$$f(4)=2f(3)+3=2 \cdot 45 + 3 = 93$$递归定义的函数是良定义的。即对于每一个正整数，函数对应取值是清楚定义的。这意味着给定任意整数，我们可以使用定义的这两个部分得到对应整数的函数值，无论怎么使用这两部分定义都会得到同样的值。
正如在函数的递归定义中那样，集合的递归定义有两个部分：基础步骤和递归步骤。在基础步骤中，规定初始的一些元素。在递归步骤中，给出用来从已知属于集合的元素来构造集合的新元素的规则。
例5：考虑如下定义的整数集合的子集S。
基础步骤：$3 \in S$。
递归步骤：若$x \in S$ 且 $y \in S$，则$x+y \in S$。
基础步骤中求出的S中的新元素是3，递归步骤的首次应用求出的是3+3=6，递归步骤的第二次应用求出的是3+6=6+3=9以及6+6=12，等。
定义1：字母表$\sum$上的字符串的集合$\sum^*$递归地定义为：
定义2：通过连接运算可以组合两个字符串。设$\sum$是符号的集合，$\sum^*$是$\sum$中符号形成的字符串的集合。可以如下定义两个字符串的连接，用$\cdot$表示：
递归定义的另一种重要用途是定义各种类型的合式公式。
例8（复合命题的合式公式）：可以定义关于T、F、命题变元以及集合$\{\lnot,\land\lor,\to,\leftrightarrow\}$中运算的复合命题的合式公式的集合。
定义3：以下步骤可以递归地定义根树的集合，其中根树是由一个顶点集合和连接这些顶点的边组成的，顶点集合包含的一个特殊顶点，称为树根。
定义4：以下这些步骤可以递归地定义扩展二叉树的集合：
定义5：以下这些步骤可以递归地定义满二叉树的集合：
结构归纳法证明包含如下两个部分：
可以定义$N \times N$（非负整数的有序对）上的序，规定如果$x_1 < x_2$或者$x_1 =x_2$且$y_1 < y_2$，则$(x_1, x_2)$小于等于$(y_1, y_2)$。这称为字典序。具有这个序的集合$N \times N$具有性质：$N \times N$的每个子集合都有最小元。这意味着可以递归地定义满足$m \in N$和$n \in N$的项$a_{m,n}$，并且用数学归纳法的变种来证明关于这些项的结果。
若对每个可能的输入来说程序都产生正确的输出，则说这个程序是正确的。一个程序的正确性证明包括两个部分。第一部分证明：若程序终止，则获得正确的答案。证明的第一部分证明了程序的部分正确性。证明的第二部分证明：程序总是终止。
为了规定程序产生正确的输出是什么意思，使用两个命题。第一个是初始断言，它给出输入值必须具有地性质。第二个是终结断言，它给出假如程序做了要求它做的事情，则程序应当具有地性质，
定义1：若当对一个程序或程序段S地输入值来说初始断言p为真时，就有对S的输出值来说终结断言q为真，则说S是相对于p和q部分正确的。记号p{S}q说明程序或程序段S是相对于初始断言p和终结断言q部分正确的。
注意：记号p{S}q称为霍尔三元组。
一条有用的推理规则是通过把一个程序分成一系列子程序，然后证明每个子程序为正确的来证明这个程序为正确的。
假定把程序S分成子程序$S_1$和$S_2$。写$S=S_1;S_2$来表示S是由$S_1$后接$S_2$来组成的。假定已经证明了$S_1$相对于初始断言p和终结断言q地正确性，以及$S_2$相对于初始断言q和终结断言r的正确性。由此得出了若p为真且$S_1$执行并终止则q为真；若q为真且$S_2$执行并终止则r为真。因此，若p为真且$S=S_1;S_2$执行并终止则r为真。这条推理规则称为合成规则，它可以叙述成：
if condition then
S
$(p \land condition)\{S\}q$
$(p \land \lnot condition)\to q$
$---$
$\therefore p\{if\ condition\ then\ S\}q$
if condition then
S1
else
S2
$(p \land condition)\{S_1\}q$
$(p \land \lnot condition)\{S_2\}q$
$---$
$\therefore p\{if\ condition\ then\ S_1\ else\ S_2\}q$
while condition
S
$(p \land condition)\{S\}p$
$---$
$\therefore p\{while\ condition\ S\}(\lnot condition \land p)$
In [ ]: