Logical consequence (⊨ and ⊢) — A statement? A judgement? A meta-statement?

84 Views Asked by At

I'm trying to understand the terminology used in mathematical logic and I'm confused about the distinctions between statement, proposition, judgement, claim, and meta-variants of those. In particular, I'm wondering what to call formulas that express semantic consequence ($\Gamma \vDash \varphi$) and syntactic consequence ($\Gamma \vdash \varphi$). Say that I want to prove that $$p \to q, p \vDash q$$ by appealing to the definition of $\vDash$. What is the thing I am proving? Can I simply call such a formula a statement? Or is it a statement about statements?