相關定義
反證法（歸謬法）：先假設命題的否定形式成立，然後再進行推理，引出矛盾。
矛盾：命題P和它的否定形式非P都成。
examples：證明不存在最大的整數、質數是無窮的。
可數（countable/enumerable)：集合的元素是有限的，或者集合中的所有元素都與正整數一一對應（即元素可一一列出）。
可數集合examples：
1)有限集合是可數的；
2)0以上的所有偶數的集合是可數的；
3)所有整數的集合是可數的（正負數互動編號）;
4)所有有理數的集合是可數的；
5)程式（符合程式語言語法的有限字元的排列）的集合是可數的；
不可數集合：元素不能與1以上的整數（1,2,3….）一一對應的集合；
無論採用什麼對應規則，總會有遺漏的元素。
不可數集合examples：
1)“所有整數數列（無窮個整數的排列）的集合”是不可數的；[對角論證法，康托爾]
2)“所有實數的集合”….
3)“所有函式的集合”….
處理無窮集合的“個數”使用一一對應方法，因為一一對應是既無“遺漏”也無“重複”的對應。
不可解問題：”原則上不能用程式來解決的問題“
關於存在不可解問題的討論：
”輸入1以上的整數時，輸出一個整數的函式“的集合不可數；
所有程式的集合可數；
二者不能一一對應（函式“個數”比程式“個數”多）
故，在輸入1以上的整數時，輸出一個整數的函式中，存在無法用程式表達的函式。
實例
不可解問題的判定以特定的不可解性為其研究對象，是數理邏輯的重要研究領域之一。
圖靈在1936年（那時還沒電腦，我們的父親是在沒有設備支持的純理論基礎上提出來的，提出了第一個不可解問題的實例：The Halting Problem。
The Halting Problem是問，輸入一段程式代碼和一個針對此程式的輸入，能否編程判斷運行這個程式後程式是否會終止。
這個問題的答案是否定的。也就是說，不可能有一種算法可以正確判斷一個指定的程式運行後，給予指定的輸入，程式最後出不出得來。換句話說，The Halting Problem是一個不可解問題。
雖然這感覺似乎不可能，但在嚴格的證明下誰也無法發言反對。
證明過程非常簡單，假設The Halting Problem是有解的，並且已經用程式實現了，那么我們只需要再編寫一個程式Program Bug，就會發現存在矛盾。
反證：既然解決The Halting Problem的算法已經實現了，那么我們一定能定義一個函式
Function Halting(a,b:input_type):boolean;
其中，a是讀入的程式源碼，b是輸入數據。這個函式的功能就是返回對於指定的程式源碼和輸入數據，程式是否能順利退出。
下面編寫一個程式：
Program Bug;
var
code:input_type;
begin
get(code); //讀入code
if halting(code,code) then repeat until false
else halt;
end.
好，現在運行Bug這個程式，並且輸入Bug這個程式本身的代碼。這樣，halting(code,code)其實質就是在判斷這個Bug程式本身了。如果The Halting Problem認為Bug程式會正常退出，那么就讓程式進入一個死循環，否則立即退出程式。矛盾產生。
對角論證
對角論證運用不當的例子：
“所有能用程式生成的整數數列的集合”是可數的。[圖靈]
（雖然可以用對角論證法做出一個整數數列不包含在表中，但不能保證此數列是“能用程式生成的”，正如證明“有理數是可數的”一樣，不能保證做出的肯定是有理數）
註：有理數是整數和分數的集合，整數也可看做是分母為一的分數。 有理數的小數部分是有限或為無限循環的數。不是有理數的實數稱為無理數，即無理數的小數部分是無限不循環的數。
停機問題
程式的行為有兩種：Data->Program->1)Result;2)永不結束運行。
程式本質是計算機存儲設備上的數據。
“處理程式的程式”examples：
1)compiler（轉換程式的程式）
2)source code checker（讀取程式的程式）
3)debugger（調試程式的程式）
停機問題（Halting Problem):判斷“某程式在給定數據下，是否能在有限時間內結束運行”的問題。
判斷程式是否會結束運行的程式HaltChecker：
1)必須準確判斷給定的程式會如何運行；
2)還可能需要根據給定的數據模擬程式的運行；
3)它自身必須要在有限時間內結束運行。
根據以上條件，不能通過實際運行 對象程式來進行判斷。（因為若是對象程式永不結束，則判斷程式也永遠得不出判斷結果）
停機問題是不可解的，能普遍解決停機問題的程式不存在。[反證法]
SelfLoop(p){ halts=HaltChecker(p,p); if(halts){ while(1>0){ } }}123456789
當程式作為數據輸入，例如
假設SelfLoop(SelfLoop)會結束
=> halts=false
=>HaltChecker(SelfLoop,SelfLoop)=false
=> SelfLoop(SelfLoop)不會結束，矛盾！
