# How can you derive a formula without premises? [duplicate]

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.

• I guess you can find the answer here, here, here, here, here, etc. Commented Jul 27, 2020 at 18:57
• @Taroccoesbrocco I had already looked at every single one of those and not a single one elaborates or explains what $\vdash A$ means with empty antecedents. The notion of a formula syntactically derived from nothing is precisely what confused me; Which is why I explicitly stipulated in the question that I was wondering about the case with empty antecedents. Commented Jul 27, 2020 at 19:04
• Since the OP claims that the answers of similar questions are not satisfactory for this question, I changed the title of OP's question because the original title was slightly misleading and seemed a duplicate of other questions. Commented Jul 28, 2020 at 7:37
• See also the post Can we deduce anything from the empty set of axioms? Commented Jul 28, 2020 at 9:46
• And see also Is a derivation a proof? for the definition of derivation or deduction in a formal system. Commented Jul 28, 2020 at 9:53

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

• I'm still a bit confused but this helped a lot. So I was on the correct line of thinking that it meant "starting formula" for deriving other formulas? Commented Jul 27, 2020 at 19:02
• @ColinHicks Not necessarily - it's a "starting formula" or something which can be deduced from only "starting formulas." See my example: in a given system, we might have $\vdash x=x$ as a right-off-the-bat correct sequent; from that + the other sequent rules we can deduce that $\vdash (x=x)\wedge(x=x)$ is also a valid sequent, but it wasn't one of the starting ones. In terms of formulas, $x=x$ is a "starting formula" but $(x=x)\wedge (x=x)$ isn't - the latter can be deduced from starting formulas, but it's not literally one of the ones we start with. Commented Jul 27, 2020 at 19:42

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.

• So out of curiosity, if $\Gamma$ is a set of axioms and $A$ is not an axiom why do we write $\vdash A$ as opposed to $\Gamma \vdash A$ if $A$ is derived from the set of axioms $\Gamma$ Commented Jul 27, 2020 at 20:25
• @ColinHicks - There are two kinds of "axioms": logical axioms and specific assumptions (which I call here hypotheses). A clear discussion about their differences (and similarities) is here, in particular in this answer. Quoting from it: "The reason for distinguishing between them is that there are other contexts where we're only interested in $Γ$ (i.e. the specific assumptions) and where the logical axioms are considered to be an "internal detail" in the definition of consequence." Commented Jul 27, 2020 at 20:37
• ok that makes a lot of sense and I think it clears up most of the rest of my confusion. Thank you for your help! Commented Jul 27, 2020 at 20:55
• @ColinHicks To clarify: Taroccoesbrocco's "logical axioms" are my "starting sentences" - I avoided using the word "axiom" in this context, but on balance that may have made things less clear. Commented Jul 27, 2020 at 23:00