反证法（归谬法）：先假设命题的否定形式成立，然后再进行推理，引出矛盾。
矛盾：命题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)不会结束，矛盾！