Solovay Completeness without Diagonal Lemma
Fedor Pakhomov

Completeness of Gödel-Löb provability logic GL with respect to provability semantics have been proved by R. Solovay in 1976. The key part of Solovay proof was to evaluate all propositional variables x from a given modal formula φ, GL⊬φ, by arithmetical sentences x* such that PA doesn't prove the corresponding arithmetical interpretation φ*. Sentences x* have been constructed using formulas that are produced by Diagonal Lemma. In the talk we will present a new more explicit method of constructing evaluations x* that doesn't rely on Diagonal Lemma.