The observational predicate calculus and complexity of computations (Preliminary communication)
Pavel Pudlák · Czech digital mathematics library · 1975
A close connection between the languages nondeterministically recognizable in polynomial time and protectively definable classes of finite structures is shown. A hierarchy of projective classes of structures is introduced and studied.