Berka I 401
Consistency Proof/Gödel: a proof of consitency cannot be performed if the metalanguage does not contain higher type variables.
>
Metalanguage, >
Levels, >
Provability, cf. >
Type theory.
Undecidability: is eliminated when the examined theory (object language) is enriched with higher type variables.
(1)
>
Object language.
- - -
Berka I 474f
Consistency/Logical Form/Tarski: is present when - for any statement x:
either x ~ε FL(X) or ~x ~ε FL(x).
((s) Either x is not an inference from the system or its negation is not an inference.)
But:
Completeness: accordingly: if - for any statement x
either x ε FL(X) or ~x ε FL(X)
((s) if either any statement or its negation is an inference from the system).
I 529 f
Law of Contradiction/Tarski: "x ~ε contradiction or ~x ~ε contradiction".
We cannot make any generalization from the class of these statement functions.
The generalization of these statement functions would itself be a (general) statement, namely the of the law of contradiction.
Problem: infinite logical product that cannot be derived with normal methods of inference.
I 531
Solution: "rule of infinite induction" - (differs from all other rules of inference by infinitist character).
(2)
1. A.Tarski, „Grundlegung der wissenschaftlichen Semantik“, in: Actes du Congrès International de Philosophie Scientifique, Paris 1935, VOl. III, ASI 390, Paris 1936, pp. 1-8
2. A.Tarski, Der Wahrheitsbegriff in den formalisierten Sprachen, Commentarii Societatis philosophicae Polonorum. Vol 1, Lemberg 1935
