4
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ I guess you can find the answer here, here, here, here, here, etc. $\endgroup$ Commented Jul 27, 2020 at 18:57
  • 2
    $\begingroup$ @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. $\endgroup$ Commented Jul 27, 2020 at 19:04
  • $\begingroup$ 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. $\endgroup$ Commented Jul 28, 2020 at 7:37
  • $\begingroup$ See also the post Can we deduce anything from the empty set of axioms? $\endgroup$ Commented Jul 28, 2020 at 9:46
  • $\begingroup$ And see also Is a derivation a proof? for the definition of derivation or deduction in a formal system. $\endgroup$ Commented Jul 28, 2020 at 9:53

2 Answers 2

4
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Commented Jul 27, 2020 at 19:02
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Jul 27, 2020 at 19:42
4
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ 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$ $\endgroup$ Commented Jul 27, 2020 at 20:25
  • 3
    $\begingroup$ @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." $\endgroup$ Commented Jul 27, 2020 at 20:37
  • $\begingroup$ 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! $\endgroup$ Commented Jul 27, 2020 at 20:55
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Jul 27, 2020 at 23:00

Not the answer you're looking for? Browse other questions tagged .