Can you explain more formally what is the difference between ⊢ and □? I’ve looked in Wikipedia and in Cartoon Guide on Löb’s theorem, but still can’t get it.
I’ve now fleshed out the notation section to elaborate on this a bit. Is it better now?
In short, ⊢ is our symbol for talking about what PA can prove, and □ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.
“⊢ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “⊢” applies to the whole line that follows it. Also, ⊢ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.
“□(1+1=2)” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”⊢ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.
″□X ” is short for “□(X)” in cases where “X” is just a single character of text.
“X⊢Y” means “PA, along with X as an additional axiom/assumption, can prove Y”. In this post we don’t have any analogous notation for □.
A set of axioms Σ within a vanilla first-order-logic language does not necessarily allow for the ability to speak about what statements are provable from Σ within that language. Consider the axioms scheme ∀x∀y(x=y). There’s not enough strength in Σ to create encodings of statements, which is neccesary to make formal statements in the language which could be interpreted in some standard model to mean “Statement X is provable”. Seriously, try doing it. It should clear things up the need to build in some notion of provability into the syntax and semtantics of a logic if you want to talk about provability within a language. Then read upto section 3 in this SEP article.
EDIT: That is assuming you know stuff about provability predicates already, and things like arithmetization. If you don’t, then the above exercise is way too hard. In that case, I’d just say that Σ⊢ψ and Σ⊢□(ψ) represent “axioms Σ proves statement ψ” and “axioms Σ proves that ψ is provable in some set of axioms T”. T is a “sufficiently strong” set of axioms, like Peano arithmetic, which can do interesting things.
Can you explain more formally what is the difference between ⊢ and □? I’ve looked in Wikipedia and in Cartoon Guide on Löb’s theorem, but still can’t get it.
I’ve now fleshed out the notation section to elaborate on this a bit. Is it better now?
Thank you, it’s much more clear now.
A set of axioms Σ within a vanilla first-order-logic language does not necessarily allow for the ability to speak about what statements are provable from Σ within that language. Consider the axioms scheme ∀x∀y(x=y). There’s not enough strength in Σ to create encodings of statements, which is neccesary to make formal statements in the language which could be interpreted in some standard model to mean “Statement X is provable”. Seriously, try doing it. It should clear things up the need to build in some notion of provability into the syntax and semtantics of a logic if you want to talk about provability within a language. Then read upto section 3 in this SEP article.
EDIT: That is assuming you know stuff about provability predicates already, and things like arithmetization. If you don’t, then the above exercise is way too hard. In that case, I’d just say that Σ⊢ψ and Σ⊢□(ψ) represent “axioms Σ proves statement ψ” and “axioms Σ proves that ψ is provable in some set of axioms T”. T is a “sufficiently strong” set of axioms, like Peano arithmetic, which can do interesting things.