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.
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.