Abstract:
A basic justification model is sharp when the evidence term constructors $\cdot, +, !$ in it mean exactly the application of modus ponens rule, the union and the verification of evidences. We construct an example of a sharp model for the logic of proofs LP and establish that in any sharp model of LP every proof term is equivalent to some proof polynomial.