introduction to metamathematics -- Kleene
Background
I am reading the book to get more understanding of type theory and logics establishment underneath programing. Though the book itself is not that easy for me.
I found a pretty good summary here:
And here is what I got most:
Numbers
We can define numbers as an infinite set, naturally, start with 0 and combine with a successor function suc so suc(0) = 1, recursively 2, 3, ...
With set theory, we can see we can have a set A with some numbers contain subsets, which is constructed by A's elements. In this process we define a predicate contain.
Things works until we have a set E with infinite numbers. We can build a subset F contains infinite numbers as well. But can we say E contains F as well, since we can apply suc so elements in F to
build a new elem not in E at the moment of observation. If we put the new element in E, then by applyingsuc to the new element in F we can keep this paradox.
Classic vs Intuitionistic Logic
Classic logic
P or not P is a full set.( P or not P == True)
This is The excluded of middle, true or not true, only either one will stands
Intuitionistic Logic
Liar's Lie: A liar say: he is always lying. Then, is he lying as well on the above sentence?
Like the paradox in the set theory example, we can never tell until we observe all elements/the liar's mind. So the excluede of middle is not true.
There is a state besides true and false, where we can not tell.
Gödel’s incompleteness theorem
If an object(number, set) is consistent(P and not P cannot be both true) then the object is incomplete
Gödel’s number
let the world only have variable or function variable A, F.. And operator & | ~ .. we can assign them each with a number, then every proposition like A & B | C can be represented with a number, that is Gödel’s number
Primitive recursive and General recursive.
General recursive is like lambda-definable,Turing's computable. ? Not computable 1. Ackermann function, we can prove its Gödel’s number's increase speed is faster than primitive? recursive functions. So Ackermann function is not computable 2. Or through enumeration, we can find some number between computable function's Gödel’s number that is not computable.
