Arithmetical Semantics of the Logic of Proofs
9.2 
• an evaluation of propositional letters by sentences of arithmetic,
• an evaluation of proof variables and constants by natural numbers.
We assume that * commutes with Boolean connectives, and
Corollary 9.6 (Arithmetical soundness of LP(CS)) If LP(CS) ' F, then F is provably valid under the constant specification CS.
The provability semantics for LP, given earlier, may be characterized as a call-by-value semantics because the evaluation F* of a given LP-formula F depends upon the value of participating functions. A different call-by-name provability semantics for LP was introduced in Artemov (1995) and then used in Krupski (1997) and Sidon (1997). In the latter semantics, F* depends upon the particular programs for the functions participating in *.
9.3
More on the topic Arithmetical Semantics of the Logic of Proofs:
- Arithmetical Completeness of the Logic of Proofs
- Artemov S., Fitting M.. Justification Logic: Reasoning with Reasons. Cambridge: Cambridge University Press,2019. — 271 p., 2019
- Basic and Mkrtychev Models for the Logic of Proofs LP
- Self-Referentiality of Justifications