Nisan comments on Formulas of arithmetic that behave like decision agents

[Nisan]

Fact 5 (Converse Barcan formula). For every formula

) with one free variable,

)%20\to%20\forall%20x%20\operatorname{Prv}(\phi(\dot{x}))).

(The formula

)) is shorthand for

%20\urcorner,%20x))). Whenever a free variable appears inside the $operatorname\left\{Prv\right\}$ predicate, there’s an implicit $operatorname\left\{Sub\right\}$ predicate there. I’m using a dot instead of an underline now.)

This fact is the converse of the Barcan formula in quantified provability logic. I’m not going to prove this, because it would be tedious and it would depend on the exact definition of $operatorname\left\{Prv\right\}$, which I want to avoid in this post. Fact 5 is asserted without proof here, and Boolos[1] asserts it with barely more than no proof.

The converse Barcan formula implies some theorems of the form

%20\to%20\operatorname{Prv}(\phi(\dot{x})))). This doesn’t work for all predicates

) — for example, take

) to be a sentence that is true for the natural numbers but not provable. Here are the theorems we will need:

Lemma 6.

(a) If

%20\to%20Q(x_1,%20\dots,%20x_k))),

then

)%20\to%20\operatorname{Prv}(Q(\dot{x}_1,%20\dots,%20\dot{x}_k))))

(b)

))

(c)

)

(d)

)

(e)

))

(f)

))

You may want to skip the proof if you’re mainly interested in how the decision agent works. Now we can give a proof of Proposition 3 that doesn’t use Löb’s theorem, and we can finally prove Conjecture 4 (now Proposition 4).

[1] Boolos, George. The Logic of Provability. Cambridge University Press: 1993. Ch. 17.