# Theorems/entailment notation

When defining a predicate logic system with natural deduction, we can define the syntatic entailment with the operator $\vdash$. Generally, I see authors using the formula $\vdash \phi$ to say that $\phi$ is a theorem of the logical system. However I was used to say that $\phi$ is a theorem too even if it is the entailment of another formula, say $\psi$ (we obtain $\phi$ from $\psi$ by using the rules of natural deduction). But that is the same as affirming $\psi \vdash \phi$.

1) So, authors generally define theorems as those formulas which are always derivable regardless of the theory that they are in, and regardless of any formulas present in the system?

2) If 1) is correct, then saying that the Gödel incompleteness theorem asserts that there are theorems which are not true under the standard interpretation of Peano Arithmetic is false, because the formulas which are not true have to be derived from the axioms of the Peano Arithmetic.

-

A theorem of the predicate calculus is a sentence (or, if you prefer, formula) that can be derived without additional axioms. If $T$ is a theory (that is, a set of sentences) then a theorem of $T$ is a sentence $\varphi$ such that $\psi\vdash \varphi$ for some finite conjunction $\psi$ of sentences of $T$. So a theorem of the predicate calculus is a sentence $\varphi$ which is a theorem of the "empty" theory.
The Incompleteness Theorem says, among other things, that there are sentences $\varphi$ that are true in the natural numbers, but that are not provable in the theory $T$ whose axioms are the usual axioms of (first-order) Peano Arithmetic (if that theory is consistent).