First some definitions to make it clear what I'm talking about:

A deductive system is a set $J$ of judgments together with a set $R$ of inference rules each of the form $$ j_0 \leftarrow j_1, j_2, \ldots, j_k \qquad\qquad(k\ge 0)$$ where $j_0$ is a judgment called the conclusion of the rule and the other $j_i$s are premises.

(For my present purposes I'm not interested in the internal structure of judgments, though it is usual to assume that $J$ is a easily recognizable formal language over some alphabet and that $R$ is a the union of finitely many easily decidable subsets of $J\times J^*$. An "axiom" in this definition is just an inference rule with zero premises).

When $A$ is any (possibly infinite) set of judgments and $j$ is some judgment, we say that $j$ can be derived from A, written $A\vdash j$ iff there is a finite sequence of judgments ending with $j$, such that each element in the sequence is a member of $A$ or is the conclusion of a inference rule whose premises all appear earlier in the sequence. (In the notation $A \vdash j$ we can write $A$ as a list without set brackets, so in particular "$\vdash j$" means $\varnothing\vdash j$.)

(Equivalently, $A\vdash j$ if there is a tree (or pointed dag) whose interior nodes are labeled with (concrete) inference rules and leaves with elements of $A$, and the edges connect premises with conclusions in the obvious way, and the root concludes $j$).

This framework works well to describe Hilbert-style logics. Then the "judgments" are just well-formed formulas, and the inference rules are all instances of modus ponens, the logical axioms, primitive rules for quantifiers and so forth. If we have a particular theory in the logic, we have a choice between elevating its non-logical axioms to nullary inference rules (thus fusing the logic and the theory into a single deductive system), or to put the set of non-logical axioms to the left of the turnstile and saying that $\phi$ is a thorem iff $T\vdash\phi$ in the deductive system of pure logic.

The framework also allows natural deduction (with environments) or sequent calculus to be deductive systems. In the latter case the judgments are sequents, and the majority of inferences rules are not axioms. But there is a notational problem here, because sequents themselves are written with a turnstile symbols, which clashes with the above use of a turnstile to assert the existence of a formal proof for a judgment.

My question: Is there a well-established symbolic way to distinguish between "outer" turnstiles that assert that some judgments can be derived from other ones, and the "inner" turnstiles that are "just punctuation" in the syntax of sequents? Are there better words to explain the difference between these two roles than the long cumbersome description I've given here?

As one example of what I'd like to express, suppose that we write the outer turnstiles as $\Vdash$. Then we could speak about a "meta-deduction theorem" for sequent calculus:

$\Vdash (\Gamma, \phi \vdash \psi)$ if and only if $(\Gamma \vdash \phi)\Vdash(\Gamma \vdash\psi)$.


2 Answers 2


As for how best to explain the inner/outer distinction, things get complicated, for that depends how we are to understand sequents, and I've heard different proof-theorists say different things about that. But here's an answer to the notational question.

In Sam Buss's "An introduction to proof theory" in the 1998 Handbook of Proof Theory he edited, the sequent-former -- the inner turnstile, as you call it -- is a simple arrow (though scaled up, it seems, from the usual '$\to$').

In Sara Negri & Jan von Plato's 2001 Structural Proof Theory, the sequent-former is the arrow '$\Rightarrow$'.

And the historical antecedent of the use of some kind of arrow is of course Gentzen himself who used an arrow as the sequent-former.


In proof complexity and also in proof theory it is common to use a distinguished arrow for the internal part, so a sequent is written as $\Gamma \Rightarrow \varphi \vdash \Gamma \Rightarrow \psi$. There is not really a standard for what kind of arrow to use, some use the arrow ending in triangle (and use $\supset$ for implication) while others use $\Rightarrow$.

In Martin-Lof's type theories where the distinction between judgments and dependent propositions are taken more seriously the assumptions are expressed in pranthesis after the proposition and there is nothing on the left side of the turnstile symbol (which is more correct philosophically with the intended meaning of the symbol by Frege). I don't know if they have any linear form of expressing rules, it is often expressed using something like:

$$ \vdash \varphi \ (\Gamma) \over \vdash \psi \ (\Gamma) $$

(However others move the $\Gamma$ to the left side and right $\Gamma \vdash \varphi$.)

  • $\begingroup$ Also see this. $\endgroup$
    – Kaveh
    Sep 18, 2012 at 20:20

You must log in to answer this question.

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