MODAL LOGIC OF HERBRAND CONSISTENCY IN WEAK ARITHMETICS

Model logic of Herbrand-style provability in weake arthmetics is studied. Though full axiomation of this logic is an open problem, we present some axioms and rules of this logic which are sufficient to derive a formalized form of Godels second incompleteness theorem for Herbrand provability of I∆0+Ω1. In other world, we shown that I∆0+Ω1 can prove the unprovability of its Herbarand consistency in itself.

Keywords:

Provability Logic , Herbrand Provability and Cut-Free Provability , Weak Arithmetics