2
$\begingroup$

I am going through the following lecture notes by Frank Pfenning :

http://www.cs.cmu.edu/~fp/courses/15317-f17/lectures/02-natded.pdf

In page no 5 I cam across the introduction rule .

The rule reads that $A$ is contained in $B$ if $B$ is true under the assumption that $A$ is true .

But in the text a subtle point about the beginning bar of the proof is mentioned which are a below in the images :

enter image description here

enter image description here

Why would it be incorrect to say that "The truth of A leads to the truth of B " . Even if the truth of A has been introduced durng the process of proving the truth of B , it surely means that the truth of A leads to truth of B . As in the graph or pictorial representation there are no other statement which are in conjuction with "A" anywhere .

What is the subtlety here in emphasing a misconception or a misleading picture obtained from omiting the bar ?

P.S : I did go through the following paragraphs illustrating the proof of a statement . This paragraph emphasizes on some phenomenon called discharging of assumptions , which I feel would require a detail understanding and might come up in the next question that I would be posting so as to gain a better understanding of the content . But for the time being , I would try to understand the matter in this question with the hope that it might help while understanding the following topics .

$\endgroup$
4
$\begingroup$

Let's try an example. Let's say you're trying to prove the following:

Simple Theorem over the natural numbers: If $n$ is even, then $n+1$ is odd.

What he's trying to say is that you don't need an independent proof that $n$ is even. In the natural numbers, this isn't even true, since not all numbers are even. What he's trying to say is that when trying to prove an implication like the Simple Theorem above, you're allowed to introduce the assumption that $n$ is even, and from that assumption, together with whatever other axioms you're using, try to prove that $n+1$ is odd. If you succeed in this, you can now correctly conclude that the implication is true.

From his paper:

The rule makes intuitive sense, a proof justifying A ⊃ B true assumes, hypothetically, the left-hand side of the implication so that A true, and uses this to show the right-hand side of the implication by proving B true. The proof of A⊃B true constructs a proof of B true from the additional assumption that A true.

The whole painful stuff with the bars and labels is a variation of the pain that comes with other deduction systems when you're trying to create a proof context to hold the introduction of an assumption. When these contexts get nested in a complicated proof, it requires machinery analogous to lexical variable scoping rules in programming languages. The assumptions have to come and go properly so they don't allow unsound deductions in other parts of the proof.

EDIT: per request of original poster.

OK, let's dig into this some more. I'm going to use some different notation. The notation

$$ \Gamma \vdash \sigma $$

means some set of axioms $\Gamma$ proves some formula $\sigma$, where the turnstile $\vdash$ means "proves". Now the inference rule we're looking at can be written like this. We can conclude

$$ \Gamma \vdash A \rightarrow B $$

if we can prove

$$ \{\Gamma; A\} \vdash B $$

where the semicolon means we've added formula $A$ to the set of axioms $\Gamma$. Note that this also creates what I've been calling a "proof context" where we're keeping track of assumptions we've been making. The Pfenning paper uses labels on bars to do the same thing.

Let's try it on a complicated example with nested proof contexts: prove the tautology

$$ A \rightarrow (B \rightarrow (C \rightarrow B)) $$

In our notation, proving this tautology looks like this:

$$ \{\} \vdash A \rightarrow (B \rightarrow (C \rightarrow B)) $$

That is, $\Gamma$ is empty since we're proving a tautology.

Here we go, using our rule of inference.

We can prove

$$ \{\} \vdash A \rightarrow (B \rightarrow (C \rightarrow B)) $$

if we can prove

$$ \{A\} \vdash B \rightarrow (C \rightarrow B) $$

Let's keep going.

We can in turn prove

$$ \{A\} \vdash B \rightarrow (C \rightarrow B) $$

if we can prove

$$ \{A, B\} \vdash (C \rightarrow B) $$

One more application of our rule:

We can prove

$$ \{A, B\} \vdash (C \rightarrow B) $$

if we can prove

$$ \{A, B, C\} \vdash B $$

But this follows easily: since B is already an axiom, it follows that we can prove it. But we only got this axiom from our inference rule that allowed us to add it safely.

$\endgroup$
  • $\begingroup$ Thanks for the answer . Could you elaborate a bit about the painful stuff with the bars and labels ? $\endgroup$ – Sheldon Kripke May 15 '18 at 3:34
2
$\begingroup$

To state the obvious, proving the implication $A \implies B$ (written $A \supset B$ in the notes you refer to) usually goes by assuming $A$ and proving $B$. Or in other words, proving $B$ under a new assumption $A$. Of course, this new assumption must only be used in the proof of $B$, which is the meaning of discharging of assumption. Thus, when you prove an implication you obtain an additional axiom (note the bar above the first derivation in your question), which can only be used in the branch of the proof that corresponds to the implication you want to prove.

$\endgroup$
  • $\begingroup$ So the truth of A is an assumption using which we reach up to the "consequent truth of B given the truth of A " , so that is to say "we have assumed the truth of A just to prove that B is true whenever A is true " and "The truth of A , however, has not been guaranteed " ..right ? And as such a faulty assumption of A's truth should not span out to affect any other logical conclusion ..right ? $\endgroup$ – Sheldon Kripke May 15 '18 at 7:29
  • $\begingroup$ Yes, exactly. That is why the new assumption is tagged, and it should not escape its scope (the branch in which the implication is proved). $\endgroup$ – Rodolphe Lepigre May 15 '18 at 11:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.