0
$\begingroup$

I have a small question about Deduction Theorem. According to Deduction Theorem, we have the following: $$A\vdash B\ \Leftrightarrow\ \langle\ \rangle\vdash A\rightarrow B.$$ Here I use $\langle\ \rangle$ to denote an empty context. My questions are related to the use of empty context $\langle\ \rangle$.

[Question 1] By weakening rule, it seems to me that the following should hold, right? $$\langle\ \rangle\vdash A\ \Leftrightarrow\ \langle\ \rangle\vdash\langle\ \rangle\rightarrow A.$$ [Question 2] Then by monotonicity, if $\langle\ \rangle\vdash\langle\ \rangle\rightarrow A$ holds, we also have $$\Gamma\vdash\langle\ \rangle\rightarrow A.$$ But what does $\Gamma\vdash\langle\ \rangle\rightarrow A$ exactly mean? More concretely, I am wondering whether $\Gamma$ really plays a role in $\Gamma\vdash\langle\ \rangle\rightarrow A$; putting it in another way, whether the truth of $A$ in $\Gamma\vdash\langle\ \rangle\rightarrow A$ depends on the assumptions collected in $\Gamma$?

$\endgroup$

1 Answer 1

3
$\begingroup$

The answer to both of your questions is that "$\langle \rangle \to A$" doesn't exist. $\phi \to \psi$ is a formula iff $\phi$ is a formula and $\psi$ is a formula, but $\langle \rangle$ is not a formula, so $\langle \rangle \to A$ isn't, either. $A\vdash B\ \Leftrightarrow\ \langle\ \rangle\vdash A\rightarrow B$ is the smallest sequent to which the deduction theorem is applicable.

We do have a generalization in the other direction, though: It holds for arbitrary sequents with $n$ pemises that

$$A_1, \ldots, A_n \vdash B \ \Longleftrightarrow \ \vdash (A_1 \land \ldots \land A_n )\to B.$$

The right-hand side $(A_1 \land \ldots \land A_n )\to B$ can logically equivalently be expressed as $A_1 \to (\ldots \to (A_n \to B))$, i.e. for each premise add one implication. In the limit case with zero premises, there is no implication at all, what you mean by "$\langle \rangle \to A$" is just $A$, and the two sides of the deduction theorem, $\vdash A$ and $\vdash A$, coincide.

$\endgroup$
1
  • $\begingroup$ Nice to meet you again! Thanks! $\endgroup$
    – Fred
    Commented Jul 5, 2020 at 21:20

You must log in to answer this question.

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