Аннотация:Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics. We propose symbolic models for single-conclusion proof logics (FLP and its extensions). The corresponding soundness and completeness theorems are proven. The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization. In particular, we construct an extension of FLP that enjoys the strong proof internalization property with empty context.