How can you derive a formula without premises?

Question

What is the difference between $\vdash A $ and $\models A$?

I'm not asking about the general difference between syntactic entailment and semantic entailment.

I specifically don't understand the difference in the case where the antecedents are empty.

According to Wikipedia, $\vdash A $ is a theorem, whereas $\models A$ is a tautology. I think I understand the double turnstile being a tautology, but with the single turnstile is $A$ an axiom (which is supposedly a purely syntactic entity)?

I'm confused on how a formula could be derivable without premises.

Answer 1

There are in any system derivation rules which operate without premises. You can think of these as logical axioms: having a rule of the form "$\vdash A$ is a correct sequent" in our deduction system amounts to $A$ being a "starting sentence" which we're allowed for free.

However, $\vdash A$ may be a correct sequent without $\vdash A$ being one of our basic sequent rules. For example, one of the standard sequent rules in many systems is "$\vdash x=x$ is a correct sequent." From this we can get $\vdash (x=x)\vee (x=x)$ by applying further sequent rules, even though "$\vdash (x=x)\vee (x=x)$ is a valid sequent" is not explicitly one of our starting rules.

Note that in the above I'm talking about deriving sequents, not sentences or formulas. This is a useful shift: it's often best to think of the deductive apparatus of first-order logic as defining a set of correct sequents, expressions of the form "$\Gamma\vdash A$" for $\Gamma$ a set of formulas and $A$ a formula, via induction starting with some basic rules (e.g. "$\vdash x=x$ is correct" or "If $\Gamma\vdash A$ and $\Gamma\vdash B$ are correct, then $\Gamma\vdash A\wedge B$ is correct"). Talking about deducing one formula $A$ from a set of formulas $\Gamma$ is then equivalent to talking about deducing the correctness of the sequent $\Gamma\vdash A$.

Answer 2

I guess you use the symbol $\vdash$ to mean the derivability in a particular deduction system $\mathcal{D}$ (there are many deductive systems), so the proper notation would be $\vdash_\mathcal{D}$. Often, when no ambiguity arises, the subscript $\mathcal{D}$ is omitted because many deductive systems are equivalent and you are not interested in the specific syntactic definition of the deductive system $\mathcal{D}$.

Writing $\vdash_\mathcal{D} A$ means that the formula $A$ is derivable in $\mathcal{D}$ without any hypotheses, i.e. without any assumption other than the logical axioms of $\mathcal{D}$. It does not mean that $A$ is necessarily a logical axiom of $\mathcal{D}$, because from logical axioms other formulas can be derived by means of the inference rules of $\mathcal{D}$.

To explain better this, it is necessary to be a little more precise.

---

The deductive system $\mathcal{D}$ is made up of logical axioms (some tautologies that serve as premises or starting points for further reasoning) and inference rules (that allows you to derive a formula from other formulas). A derivation in $\mathcal{D}$ from the hypotheses $B_1, \dots, B_m$ to the conclusion $A$ is a finite sequence of formulas $(A_1, \dots, A_n)$ such that $A_n = A$ and, for all $1 \leq i \leq n$:

1. either $A_i$ is an hypothesis (i.e. $A_i = B_j$ for some $1 \leq j \leq m$);
2. or $A_i$ is a logical axiom of $\mathcal{D}$;
3. or $A_i$ is obtained by applying an inference rule of $\mathcal{D}$ from the premises $A_{i_1}, \dots, A_{i_k}$ (where $i_1, \dots, i_k < i$).

We write $B_1, \dots, B_m \vdash_\mathcal{D} A$ if there is a derivation in $\mathcal{D}$ from the hypotheses $B_1, \dots, B_m$ to the conclusion $A$. In particular, we write $\vdash_\mathcal{D} A$ in the case there is a derivation with no hypotheses, i.e. the derivation is obtained by applying only the cases 2 and 3 above: $A$ is either an axiom of $\mathcal{D}$ or obtained from the axioms of $\mathcal{D}$ by applying the inference rules of $\mathcal{D}$.

For instance, suppose that $A$ is an axiom of $\mathcal{D}$ (hence $\vdash_\mathcal{D} A$) and a tautology, so $A \lor A$ is still a tautology but (possibly) $A \lor A$ is not an axiom of $\mathcal{D}$. However, $A \lor A$ can be derived from $A$ using the inference rules of $\mathcal{D}$, hence still $\vdash_\mathcal{D} A \lor A$.

The hypotheses $B_1, \dots, B_m$ can be seen as non-logical axioms, i.e. formulas that are not tautologies but that you assume to investigate their consequences. They can be the axioms of a specific mathematical theory, for instance Peano arithmetic or group theory.

---

Which are the logical axioms and the inference rules of $\mathcal{D}$? It depends on the deductive system $\mathcal{D}$. Some deductive systems (such as natural deduction) are essentially without logical axioms, but even in that case it makes sense to write $\vdash_\mathcal{D} A$. Indeed, such deduction systems have an inference rule (sometimes called deduction theorem) that allows hypotheses to be discharged, i.e. such that if $B \vdash_\mathcal{D} A$ then $\vdash_\mathcal{D} B \to A$.

To give a concrete example, let $A$ be any formula. How can we prove the formula $A \to A$ (which is a tautology) without any hypotheses? Clearly, $A \vdash_\mathcal{D} A$ (case 1 in the definition of derivation: if you suppose $A$ then you can conclude $A$) an then $\vdash_\mathcal{D} A \to A$ by the deduction theorem.