16
$\begingroup$

In Wikipedia, here in the last axiom of the Natural deduction system, it says "From [accepting $p$ allows a proof of $q$], infer $(p \to q)$." Isn't that a tautology? In the big table "Basic and Derived Argument Forms" that follows, I see it using a new symbol "$\vdash$" to express "therefore". Isn't that something can be done by the symbol "$\to$"? For example, what's the difference between "$(p \land q) \vdash p$" and "$(p \land q) \to p$"?

An interesting symbolic representation of the last axiom of NDS is that $(p \vdash q) \vdash (\vdash p \to q)$. Which I don't understand why is made so complicated.

What also puzzles me is in the "example of a proof" that follows. Since you list "$A$" as a promise, which is basically saying "assuming $A=\text{True}$", then why you have to go around such a big circle, using disjunction, conjunction, and conjunction elimination to prove back that "$A$" is true? If it is me, I would say "assuming $A=\text{True}$, we will know that $A=\text{true}$. Bang! Now we get $A \vdash A$, so we have $\vdash A \to A$." What's wrong in this deduction?

$\endgroup$
1

4 Answers 4

Reset to default
22
$\begingroup$

$(p \land q) \to p$ is a sentence in propositional calculus. When $p$ and $q$ are assigned truth values, that sentence always gets the value true, that is, is a tautology.

$(p \land q) \vdash p$ is a statement in a metalanguage about propositional calculus. It says that $p$ can be deduced from $p \land q$ according to whatever deduction rules are valid.

$\endgroup$
10
  • 4
    $\begingroup$ If that is the case, I think the shape of the symbol "$\to$" is highly deceptive, because actually it is just an operation, no more special than other operations like "$\land$" or "$\lor$", and is not the synonym of "implication", because using it won't ensure the implicational relationship exist. $\endgroup$
    – xzhu
    Dec 12, 2011 at 13:40
  • 1
    $\begingroup$ Thus: some elementary logic texts use "if, then" for $\rightarrow$ and avoid using "implies". Others may use two different symbols $\rightarrow$ and $\Rightarrow$ for these two things. $\endgroup$
    – GEdgar
    Dec 12, 2011 at 14:03
  • 2
    $\begingroup$ Voldemort, as outlined in your question there's a close relationship between the material conditional and the provability relation. The deduction theorem shows that if from $P$ we can prove $Q$, then we may legitimately infer the conditional statement $P \rightarrow Q$. Taking $P \rightarrow Q$ to be synonymous with $P \vdash Q$ is an error, but not a particularly egregious one since we can move between them seamlessly in most contexts. $\endgroup$
    – Benedict Eastaugh
    Dec 12, 2011 at 14:42
  • 3
    $\begingroup$ Matt, $p$ and $q$ in the question are meant to denote propositions, i.e. atoms of the propositional calculus, not variables in the predicate calculus. $\endgroup$
    – Benedict Eastaugh
    Dec 12, 2011 at 14:43
  • 1
    $\begingroup$ @Voldemort: yes, that's a fine way to view the material conditional. Its strange truth table has long been a subject of dispute amongst philosophers of logic, and students often find it confusing when it's first introduced. It may help to think of it in terms of the equivalent statement, $\lnot{}P \vee Q$ (classical logic is often formulated with only negation and conjunction or disjunction, as the other connectives can be introduced merely as abbreviations). $\endgroup$
    – Benedict Eastaugh
    Dec 12, 2011 at 15:14
12
$\begingroup$

The connection between the material conditional and provability is an important one, and very intuitive once the basic definitions are understood. In a formal proof we assume a set of premises and derive a particular conclusion. Let's call the set of premises $\Gamma$ and the conclusion $\psi$. Now suppose we want to prove $\varphi$, but our premises are too weak to prove it by themselves. So we additionally assume $\theta$, and manage to derive $\varphi$. We represent this symbolically by saying that $\Gamma \cup \left\{\theta\right\} \vdash \varphi$.

Contrast this with a conditional statement, like the following: if $x + y < z$, then $x < z \wedge y < z$ (for $x,y,z \in \mathbb{N}$). We can formalise this in the predicate calculus using the material conditional: $\forall{x}\forall{y}\forall{z} (x + y < z \rightarrow x < z \wedge y < z)$.

The deduction theorem states that given $\Gamma \cup \left\{\theta\right\} \vdash \varphi$, we can assert that our initial set of premises $\Gamma$ proves the conditional statement $\theta \rightarrow \varphi$. Formally, $(\Gamma \cup \left\{\theta\right\} \vdash \varphi) \vdash (\Gamma \vdash \theta \rightarrow \varphi)$, which is just a slightly more general version of the conditional proof rule $(p \vdash q) \vdash (\vdash p \rightarrow q)$.

It's important to bear in mind the distinction here between the object language, which is the language in which the premises, conclusion and all steps of the proof are stated, and the metalanguage which lets us make assertions about what can be proved from what. $\rightarrow$ is a symbol of the object language, which informally corresponds to the if...then locution in English. $\vdash$ is a symbol of the metalanguage, and corresponds to provability: from these premises, this conclusion can be derived. The importance of the deduction theorem is that it shows a way for us to move from statements of the metalanguage to statements of the object language.

Here's an updated answer to your second question, having looked at the link page for more than a second. The example proof is complicated just so they can show a chain of reasoning with steps between the initial assumption and the derivation of $A \vdash A$.

  1. $A$ (Assumption)
  2. $A$ (From 1)
  3. $A \vdash A$ (From 1 and 2)
  4. $\vdash A \rightarrow A$ (From 3 by CP)

So far, so obvious. And of course by simply inspecting the truth table for $A \rightarrow A$ we can see that it's a tautology; this is the semantic approach, while the derivation shown on the Wikipedia page is a syntactic approach.

The problem with the truth table approach is that it doesn't scale to first-order logic: what's the truth table for $\forall{x} \; P(x)$? Assuming we assigned constants to every element of the domain, we could posit some kind of analogue for a truth table, but if the domain were infinite then the truth table would be infinitely wide! This is why semantics for first-order logic are given by model theory, not truth tables. However, the deduction theorem still holds in first-order logic (for closed formulae).

$\endgroup$
2
  • 1
    $\begingroup$ Thank you. Except that I think to prove "$A \to A$" means to prove that the proposition "$A \to A$" can be derived from nothing (not $A$). And in order to prove so we should prove that "$A \vdash A$". I think this is important because not only "$A \to A$" is a theorem when $A$ is a theorem, but also when $\neg A$ is a theorem. And the importance of the deduction theorem is it points out that, if "$p \vdash q$", then "$p \to q$" can be deduced, regardless of whether $p$ is or is not a theorem. $\endgroup$
    – xzhu
    Dec 13, 2011 at 4:38
  • $\begingroup$ I must admit, I answered this in a bit of a hurry and didn't read the Wikipedia proof too carefully. You're quite right; I have amended my answer to reflect this. Do let me know if anything is still unclear. $\endgroup$
    – Benedict Eastaugh
    Dec 16, 2011 at 20:58
1
$\begingroup$

Talk of the 'metalanguage' can be a little confusing in my opinion, so maybe an order-theoretic perspective would be clearer? In particular, let $P$ denote a Heyting algebra. Consider $p,q \in P$. Then:

  • $p \wedge q \leq p$ is simply true.
  • $(p \wedge q) \rightarrow p$ is an element of $P$.
  • That element happens to equal $1$.

Furthermore, $\vdash$ is a bit like $\leq$, except you can have multiple inputs on the left. For example, we could define:

Definition. A multiposet is a thin multicategory.

We write $x_0,\ldots, x_{n-1} \vdash y$ to mean that there exists a multiarrow $x_0,\ldots,x_{n-1} \rightarrow y$.

$\endgroup$
0
$\begingroup$

In addition to what got pointed out in the other comments, (p∧q)→p, once we write exactly what the author means, that is ((p∧q)→p), we have a well-formed formula (or formula or statement form). On the other hand, ((p∧q)⊢p) is not a well-formed formula, as it doesn't follow the formation rules of some language, or at least needs a set of formation rules distinct from that of ((p∧q)→p) as it exists in the metalanguage, not the object language.

$\endgroup$

You must log in to answer this question.

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