本文把程式碼省去了，為了更加簡單準確
在演算法中的應用見
https://www.cnblogs.com/qianxinn/p/15625052.html

數學歸納法

The simplest and most common form of mathematical induction infers that a statement involving a natural number n (that is, an integer n ≥ 0 or 1) holds for all values of n. The proof consists of two steps:

數學歸納法最簡單和最常見的形式是推斷包含自然數 n（即整數 n ≥ 0 或 1）的陳述對 n 的所有值都成立。證明包括兩個步驟：

The initial or base case: prove that the statement holds for 0, or 1.

初始或基本情況：證明該陳述對 0 或 1 成立。

The induction step, inductive step, or step case: prove that for every n, if the statement holds for n, then it holds for n + 1. In other words, assume that the statement holds for some arbitrary natural number n, and prove that the statement holds for n + 1.

歸納步驟、歸納步驟或步驟案例：證明對於每個 n，如果該陳述對 n 成立，則它對 n + 1 成立。換句話說，假設該陳述對某個任意自然數 n 成立，並證明該陳述對 n + 1 成立。

The hypothesis in the inductive step, that the statement holds for a particular n, is called the induction hypothesis or inductive hypothesis. To prove the inductive step, one assumes the induction hypothesis for n and then uses this assumption to prove that the statement holds for n + 1.

歸納步驟中的假設，即該陳述對特定 n 成立，稱為歸納假設或歸納假設。為了證明歸納步驟，我們假設 n 的歸納假設，然後使用這一假設來證明該陳述對 n + 1 成立。

Authors who prefer to define natural numbers to begin at 0 use that value in the base case; those who define natural numbers to begin at 1 use that value.

在基本情況下，喜歡將自然數定義為從 0 開始的人使用 0 值；那些將自然數定義為從 1 開始的人使用 1 值。

一階邏輯和二階邏輯

在邏輯和數學中，二階邏輯是一階邏輯的擴充套件，而一階邏輯是命題邏輯的擴充套件。

First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence \({\displaystyle \forall P\,\forall x(Px\lor \neg Px)}\) says that for every formula \(P\) , and every individual \(x\), either \(Px\) is true or not(\(Px\)) is true (this is the law of excluded middle). Second-order logic also includes quantification over sets, functions, and other variables (see section below). Both first-order and second-order logic use the idea of a domain of discourse（論域） (often called simply the "domain" or the "universe"). The domain is a set over which individual elements may be quantified.

一階邏輯量詞僅適用於個體範圍內的變數（論域的元素）；而二階邏輯也量化了關係。

First-order logic can quantify over individuals, but not over properties. That is, we can take an atomic sentence like Cube(b) and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:\(∃x Cube(x)\)。

一階邏輯可以量化個體，但不能量化屬性。也就是說，我們可以取一個像\(Cube(b)\)這樣的原子語句，通過將名稱替換為一個變數並附加一個量詞來得到一個量化的句子：\(∃x Cube(x)\)。

但是我們不能對謂詞做同樣的事情。也就是說，下面的表示式：\(∃P P(b)\)不是一階邏輯的句子。但這是一個合法的二階邏輯語句。

數學歸納法形式化

數學歸納法一般無法形式化，所以演算法常常不如數學嚴謹。

在數學中的二階邏輯中，可以寫出“歸納公理”如下：

\({\displaystyle \forall P{\Bigl (}P(0)\land \forall k{\bigl (}P(k)\to P(k+1){\bigr )}\to \forall n{\bigl (}P(n){\bigr )}{\Bigr )}}\)

其中 P(.) 是涉及一個自然數的謂詞的變數，k 和 n 是自然數的變數。

換句話說，基本情況 P(0) 和歸納步驟（即歸納假設 P(k) 暗示 P(k + 1)）一起暗示 P(n) 對於任何自然數 n。歸納公理斷言從基本情況和歸納步驟推斷 P(n) 對任何自然數 n 成立的有效性。

良基關係

In mathematics, a binary relation \(R\) is called well-founded (or wellfounded) on a class \(X\) if every non-empty subset \(S ⊆ X\) has a minimal element with respect to \(R\), that is, an element \(m\) not related by \(sRm\) (for instance, "\(s\) is not smaller than \(m\)") for any \(s ∈ S\). In other words, a relation is well founded if
\({\displaystyle (\forall S\subseteq X)\;[S\neq \emptyset \implies (\exists m\in S)(\forall s\in S)\lnot (sRm)].}\)

一般演算法的核心都是演算法中具有良基關係的那部分關係。

ChangeLog

• 12月1日 15:09 本文仍將不斷更新。二階邏輯，良基關係以及數學歸納法等地方仍有大量問題。