Feasible interpretability
Rineke Verbrugge · 1993
Abstract Abstract In PA, or even in 1.Δ.o+ EXP, we can define the concept of feasible interpretability. Informally stated, U feasibly interprets V iff: for some interpretation, U proves the interpretations of all axioms of V by proofs with Giidel numbers of length polynomial in the length of the Gödel numbers of those axioms.