Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
I am new to logic so I'm trying to understand the relationship between some of the symbols and concepts. I am specifically trying to understand the turnstile character, or 'proves' concept. If something proves something else, then is it true that this is equivalent to saying that if it is true, then something follows? As below...?
Δ ⊢ a is equivalent to Δ → a
...Perhaps it should be stated...
Δ ⊢ a "implies" Δ → a
In this case Δ → a would not necessarily imply Δ ⊢ a ?
It does not make sense to ask whether the two are equivalent for two reasons.
The first is that $\Delta$ is typically taken to be a list or a set of propositions, depending on context. Thus, unless $\Delta$ consists of exactly one proposition, we cannot form the proposition $\Delta \to A$.
We could relax this by taking $\Delta$ to be a single proposition. But even then, it does not make sense to ask whether $\Delta \vdash A$ and $\Delta \to A$ are equivalent. This is because $\Delta \vdash A$ is a proposition in the metatheory, while $\Delta \to A$ is a proposition.
What we can say is that $\Delta \vdash A$ if and only if $\vdash \Delta \to A$.
I think, in this connection, it is worth quoting a passage from an unpublished manuscript of Alan Turing (in Mathematical Logic: Collected Works of A. M. Turing volume 4, Elsevier, 2001, p. 217). On the previous page, Turing remarks
The deduction theorem should be taken account of, i.e. it should be recognised that numerous forms of argument consist in one form or another of applications of the deduction theorem. The deduction theorem should therefore be as well known as the rule for integration by parts.
and offers a rare statement of conceptual reflections on the deduction theorem:
Letters described under iv) and v) above are known respectively as free and bound variables. Free variables are really comparatively rare. This is because we do not often make statements such as '$x=x$' but more often something like 'for all real numbers $x,x=x$': in this the opening phrase 'binds' the variable. Thus $x$ is bound in the whole statement, but is free in the part $x = x$. The difference between the constants iii) and the free variables is somewhat subtle. The constants appear in the formula superficially as if they were free variables, but we cannot substitute for them. In these cases there has always been some assumption made about the variable (or constant) previously; thus we may have the equation $$v=\frac{4}{3}\pi a^{3}$$ in which we cannot substitute for $v$ and $a$, these being constants because we have made these assumptions about them '$a$ is the radius and $v$ is the volume of the sphere'. The 'deduction theorem' states that in such a case, where we have obtained a result by means of some assumptions, we can state the result in a form where the assumptions are included in the result, e.g., 'If $a$ is the radius and $v$ is the volume of the sphere then $v=\frac{4}{3}\pi a^{3}$'. In this statement $a$ and $v$ are no longer constants. We are now able to substitute for them: we might substitute $v$ for $a$ and get a statement with the same meaning, or we could substitute $2$ for both $a$ and $v$ getting a true statement, but one of rather unorthodox character. This process whereby we pass from P proved under an assumption H to 'If H then P' may be called 'absorption of hypotheses'. The process converts constants or 'restricted variables' into free variables. Variables whose character changes in this way from restricted to free usually seem to be described as 'parameters', although it is very difficult to give any very definite meaning to the term.
