A. Godel’s Completeness Theorem
Theorem 1:
Every valid logical expression is provable. Equivalently, every logical expression is either satisfiable or refutable.
Theorem 2 (Godel’s Fixed Point Theorem):
If φ(v0) is a formula of number theory, then there is a sentence ψ such that P ⊢ ψ ↔ φ(⌈ψ⌉), where ⌈ψ⌉ is the formal term corresponding to the natural number code of ⌈ψ⌉.
B. Godel’s Incompleteness Theorem
Theorem 3 (Godel’s First Incompleteness Theorem):
If P is ω-consistent, then there is a sentence which is neither provable nor refutable from P.
Theorem 4 (Godel’s Second Incompleteness Theorem):
If P is consistent, then Con(P) is not provable from P.
Theorem 5:
Given any recursive function f there are provable sentences φ of arithmetic such that the shortest proof is greater than f(⌈φ⌉) in length.
Theorem 6:
Let n be a natural number > 0. If f is a computable function, then there are infinitely many formulas A, provable in Sn, such that if k is the length of the shortest proof of A in Sn and l is the length of the shortest proof of A in Sn+1, then k > f(l).
Theorem 7:
There is no realization with finitely many elements (truth values) for which the formulas provable in H, and only those, are satisfied (that is, yield designated values for an arbitrary assignment). H is intuitionistic propositional logic, after Heyting.
Theorem 8:
Infinitely many systems lie between H and the system A of the ordinary propositional calculus, that is, there is a monotonically decreasing sequence of systems all of which include H as a subset and are included in A as subsets.
Theorem 9:
Let F be a propositional formula. Then H ⊢ F if and only if A ⊢ F′, that ¬F follows from H if and only if ¬F follows from A, for any propositional formula F. The translation in this case can be taken to map A′ to A for atomic A. Moreover, we let ∀xA(x)′ = ∀xA′(x) :
Theorem 10:
Suppose A is a first order formula. If A is provable in classical first order logic, then A′ is provable in intuitionistic first order logic.
Theorem 11:
Suppose A is a first order formula of arithmetic. If A is provable in classical Peano arithmetic, then A′ is provable in intuitionistic first order arithmetic.
Theorem 12:
Let A be a formula of IPL, and let A′ be its translation. Then IPL ⊢ A implies G ⊢ A′.
Theorem 13:
Suppose F′ = ∃y∀zA(y, z, x). If F is provable in intuitionistic first order arithmetic, then there are computable functionals Q of finite type such that A(Q(x), z, x) is provable in T.
————————————-
Source: “The Consistency of the Continuum Hypothesis” by Kurt Godel (1906-1978) | English | Princeton, N.J.: Princeton University Press, (1951, © 1940), 69 p |
———————————————————
Esai @ Ahmad Yulden Erwin, 2015
