# Is it "technically consistent" to interpret a Gentzen-style proof caclulus as a Hilbert system with $\vdash$ as a variadic logical connective?

Is it internally consistent to interpret $$\vdash$$ in Gentzen-style systems as a variadic-but-otherwise-ordinary connective? If it is consistent, is there a way to show that interpreting $$\vdash$$ this way leads to really bad predictions or is substantially less parsimonious than the correct interpretation?

Alternatively, what's the most concrete way to show that the interpretation of $$\vdash$$ as a variadic logical connective instead of a metalogical symbol is "wrong" in some sense, assuming that such a way exists?

I think misunderstanding that $$\vdash$$ and the comma are metalogical symbols and instead interpreting them as part of the syntax is common among folks who are new to logic or studying it on their own. I, at least, thought this way for years before learning the correct interpretation.

What follows is a more complete explanation of the question with an example.

Here's a Gentzen-style system for propositional calculus for classical logic with the connectives $$\to$$ for implication and $$\nrightarrow$$ for nonimplication.

This is a variant of system LK as presented in the Wikipedia article, but with fewer connectives and hence fewer rules. The structural rules are omitted entirely for brevity.

$$\frac{}{A \vdash A} \;\; \text{is the identity rule}$$

$$\frac{\Gamma \vdash \Delta, A \;\; \text{and} \;\; A, \Sigma \vdash \Pi}{\Gamma, \Sigma \vdash \Delta, \Pi} \;\;\text{is cut elimination}$$

$$\frac{\Gamma \vdash A, \Delta \;\; \text{and} \;\; \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \to B \vdash \Delta, \Pi} \;\; \text{is left implication introduction}$$

$$\frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \to B, \Delta} \;\; \text{is right implication introduction}$$

$$\frac{\Gamma, A \vdash B, \Delta}{\Gamma, A \nrightarrow B \vdash \Delta} \;\; \text{is left nonimplication introduction}$$

$$\frac{\Gamma \vdash A, \Delta \;\; \text{and} \;\; \Sigma, B \vdash \Pi}{\Gamma, \Sigma \vdash A \nrightarrow B, \Delta, \Pi} \;\; \text{is right nonimplication introduction}$$

In this notation, $$A$$ is a well-formed formula, $$\Gamma, \Delta, \Sigma, \Pi$$ are finite sets of well-formed formulas, $$\to$$ and $$\nrightarrow$$ are logical connectives, and $$\vdash$$, the comma, the line of inference and the $$\text{and}$$ that separates premises are metalogical symbols.

However, if we squint, $$( \text{formula, \cdots, formula} \vdash \text{formula, \cdots, formula})$$ looks like a connective similar to $$\to$$ or $$\nrightarrow$$, just one that takes an arbitrary number of left arguments and an arbitrary number of right arguments.

I'm now wondering whether interpreting $$\vdash$$ as a variadic connective with an unlimited number of left arguments and an unlimited number of right arguments is internally consistent.

By the faux-Hilbert-system interpretation, the premise of the right implication introduction rule $$\Gamma, A \vdash B, \Delta$$ would be a well-formed formula with a toplevel connective $$\vdash$$ and the interpretation of the right implication introduction rule would just be a rule that takes this well-formed formula and outputs the related well-formed formula $$\Gamma \vdash A \to B, \Delta$$. The rule would be interpreted the same way more familiar rules like modus ponens are interpreted. In modus ponens, shown below, $$A$$ and $$B$$ are syntactic metavariables that bind to particular subformulas in an application of modus ponens.

$$\frac{A \;\;\text{and}\;\; A \to B}{B} \;\; \text{is Hilbert-style modus ponens}$$

In faux-Hilbert-style modus ponens $$A$$ and $$B$$ are syntactic metavariables, and $$\Gamma$$ and $$\Delta$$ are a special kind of syntactic metavariable that stands for a collection of arguments to a variadic function, which are themselves well-formed formulas.

• Your question uses a lot of unclear terminology. First of all, I think you need to make it clear what you mean by "internally consistent". Commented Feb 28, 2021 at 23:58
• @RobArthan By "internal consistency", I don't mean a formal mathematical concept. I mean, is taking a language with $\vdash$ as a logical connective that takes an unlimited number of left and right arguments a coherent idea. Commented Mar 1, 2021 at 0:40
• Well clearly it's a coherent idea: $\Gamma \vdash \Delta$ is (morally and semantically) equivalent to $\bigwedge \Gamma \to \bigvee \Delta$. Commented Mar 1, 2021 at 0:49
• $\Gamma \to \Delta$ 's truth conditions are the same as $\bigwedge \Gamma \to \bigvee \Delta$ or to $\big(\lnot\Gamma_1 \lor \cdots \lor \lnot\Gamma_{n} \lor \Delta_1 \lor \cdots \lor \Delta_m\big)$, true, but $\vdash$ is formally a metalogical symbol. I guess I'm wondering what being a metalogical symbol instead of a logical connective entails, and if there's a way to show that analyzing metalogical symbols as just a special type of logical connective is a bad analysis in some way. Commented Mar 1, 2021 at 16:23

The sequent calculus comes in two layers: A structural layer, which describes how formulas are shifted around in sequents, and a logical layer, which describes how formulas can be decomposed depending on their outermost logical connective. Your suggestion amounts to removing the structural layer by treating $$\vdash$$ as a logical connective. In this way, you obtain a Hilbert-style proof system which is based on formulas instead of sequents.
First, there are some technical obstacles. As you mention yourself, $$\vdash$$ seen as a binary connective does not have a fixed arity. A more substantial issue is that you do not have nestings of $$\vdash$$, since $$\vdash$$ appears only as the outermost symbol in sequents. Consequently the formulas of your logic would not be closed under substitution, as it is usually the case. E.g., $$p\vdash A$$ and $$q\vdash B$$ are formulas but $$(q\vdash B)\vdash A$$ is not. So even if you take $$\vdash$$ to be a logical connective, its treatment will have to be quite different from that of the standard logical connectives.
1. It is a nice property of the logical rules of sequent calculus that they depend only on the outermost logical connective of formulas; we never have to look deep inside a formula to see which rules are applicable. This property will be obfuscated in the "faux-Hilbert"-approach, where the outermost connective is $$\vdash$$.
2. The vital subformula property will be obfuscated as well. The subformula property (established via cut elimination) states that every sequent has a proof in which all occuring formulas are subformulas of the endsequent. Note that the "structural layer" is swept under the carpet here: We only care about whether a formula appears in a sequent or not, but not how often or in which order. Consider for example the proof: $$\frac{A\vdash A}{\vdash \lnot A,A}$$ This proof satisfies the subformula property because every formula appearing in the upper sequent (i.e., $$A$$) is a subformula of one of the formulas in the lower sequent (i.e., $$A$$ and $$\lnot A$$). On the other hand, $$A\vdash A$$ seen as a single formula with main connective $$\vdash$$ is not a subformula of $$\vdash\lnot A,A$$, and so at least the naive subformula property fails in the "faux-Hilbert" approach. You sometimes read this point being expressed as analyticity holds only modulo the structure of the proof system $$-$$ that is, if we ignore $$\vdash$$ and $$,$$ (comma) and concentrate on the formulas only. This is another good reason for keeping the the structural layer of the sequent calculus separate from the logical one.