On weak expressibility of formulas in the simplest non-trivial propositional provability logic

Abstract

They say formula F is weak-expressible by formulas of the system Σ in the logic L if F can be obtained from unary formulas of L and from formulas of Σ by applying the rule of weak substitution (which allows to pass from the formulas A and B to the result of the substitution of one of them in another one instead of all occurrences of the same variable, say p) and by the rule of replacement by an equivalent formula (which permit to pass from the formula A to an equivalent to it in L formula B).