In his "Epistemic Set Theory," William Reinhardt says:

It is the purpose of this paper to formulate axioms for Gödel's modal operator B for provability (see [3], [8]) in the context of set theory. This provides a framework for consideration of the Post-Turing thesis which is more adequate than arithmetic with B, where the thesis can only be expressed as a schema.

Aside from not really understanding what that's all about, I'm somewhat puzzled by the talk of B as a modal operator. Why I'm puzzled is that in the SEP article on the incompleteness theorems, they talk about a provability predicate. So, I wonder if there are different formulations of the theorems based on the modal-operator/predicate distinction. Presently, however, my question is just why modal operators or predicates would be required, over and above the turnstile notation? Or, rather, is it necessary to use more than the turnstile notation, or are modal operators/predicates used to shorten expressions that could be made out by an elaborate use of the turnstile?

Motivation: I'm trying to limit the number of epistemic modal operators in my system, so it would be more convenient if provability weren't given via its own modal operator. I suppose I could live with a provability predicate, though. Still, it would be nice if I could use just the turnstile in this connection. So if that's not possible, woe to my system, again!

1 Answer 1


The critical thing here is to understand the distinction between the object language and the metalanguage. The turnstile ⊢ is a metalinguistic symbol that states derivability. When we formulate theories we usually want to do so in the object language.

The significance of Gödel's B operator is that it allows us to write sentences in the object language whose interpretation is such that Bp means "p is provable (in some specified sense)". We can then formulate axioms for this operator and hopefully prove interesting things about it. Representing provability in the object language is not trivial. We can choose some axioms but there is real work to be done in demonstrating that these are adequate to describe our understanding of provability. Indeed for some specific concept of provability that we may have, there is no guarantee that it is axiomatisable.

There is an analogy here with Gödel's first incompleteness theorem. Gödel constructs a predicate Bew(n) in the object language of arithmetic that is satisfied by a number n if and only if n is the Gödel number of a sentence that is provable in a given formal system. Here it is the Bew(n) predicate that is performing the role of representing the metalevel provability relation within the object language. The famous result is that, subject to assumptions of consistency, recursive axiomatisability, and sufficient strength of the arithmetic, a formal system is not able to prove or disprove all the sentences within its language.

In the case of Gödel's B operator, the object language is not that of arithmetic, but instead a modal extension of the propositional calculus. Gödel's axiom system is S4, which is not suitable for expressing provability within arithmetic. Reinhardt uses a system of his own because he wishes to include quantification, though it looks to me very much like S4 together with the Barcan formula (schemas L7 through L10 in his paper).

Reinhardt's paper is older than George Boolos' book, The Logic of Provability (Cambridge, 1994) and you might be better off referring to that. Boolos uses the modal system K4W rather than S4. This is preferable because K4W lacks the T axiom, which is undesirable since it builds in the assumption of soundness, and it adds the W axiom of converse well-foundedness, which corresponds to the requirement that proofs are finite.

  • "the W axiom of converse well-foundedness, which corresponds to the requirement that proofs are finite." That's incorrect: converse well-foundedness corresponds to Lob's theorem, not the finiteness of proofs (in particular a version of Lob's theorem will hold for some infinitary proof-systems). Dec 24, 2023 at 0:06
  • @NoahSchweber I stand corrected. I am aware that K4W proves Löb's theorem, but I had thought that the converse well-foundedness axiom in effect enforces finite proofs by imposing a frame condition of finite chains of accessible possible worlds. But if W is consistent with infinitary proof systems then obviously that is not so. Thanks.
    – Bumble
    Dec 24, 2023 at 2:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .