= 27d567bc2d48d9f40e9ccc20ea370b15)
Nisan comments on Formulas of arithmetic that behave like decision agents - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (33)
Fact 5 (Converse Barcan formula). For every formula)
with one free variable,
(The formula))
is shorthand for %20\urcorner,%20x)))
. Whenever a free variable appears inside the 
predicate, there's an implicit 
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
, 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.