Аннотация:The extended operational (term-labeled modal) language is used to give the axiomatic description for functional proof predicate supplied with effective operations on proofs induced by modus ponens and necessitation rules. An additional operation is involved which restores a statement from its proof. The arithmetical completeness and decidability theorems are proved. The cut-elimination property for Gentzen style reformulation of corresponding logic is established.
Partially supported by Grant INTAS-RFBR No. 95-0095 and by Grant RFBR No.96-01-01470.