Types of reasoners

Abstract

These are presented as extensions of classic propositional calculus, the hierarchies of deductive systems SCR-(n+1) and CP-n with n ≥ 0. SCR- n is the belief system of type-n reasoners and CP-n is the associated propositional calculus for type-n reasoners. The theorems of SCR- n systems are interpreted as the beliefs of type-n reasoners. In CP-n systems the belief notion is formalized by using the [R] operator, in the following sense: X is a belief of a type-n reasoner (X is a SCR- n theorem) if and only if [R] X is a CP-n theorem. The junction of these systems produces the SCR-w system, which agrees with the K modal logic system, therefore, the SCR-n hierarchy is located between the classic propositional calculus and K modal system. The way in which the systems are built guarantees that a type (n+1) system knows that it is of type-n in the following sense: in SCR-(n+1) system there is a theorem, besides the SCR-n theorems, the belief in such theorems, and the type (n+1) knows that it applies the inference rules used by a type-n reasoner. Since a type-n reasoner does not always know that it is of type- n, resoners of the hierarchy are not self-conscious. Self-consciousness can only be guaranteed by extending the SCR-w system to the modal K4 system.