Trouble with a proof in propositional logic

[HJ Farnsworth]

Greetings everyone,

I have been teaching myself mathematical logic for amusement by going through Stephen Cole Kleene’s textbook, “Mathematical Logic”. I am stuck on the following problem (problem 13.2 on page 58, if you happen to have the book):

Show that, if |- A_m+1, then A₁, … , A_m |- B if and only if A₁, … , A_m, A_m+1 |- B.

Above and throughout the rest of this post, |- indicates the turnstile symbol., ie., "yields", or "proves". I could not find how to type the actual symbol into this post. Also, I am using => for "if, then" and <=> for "if and only if".

Anyways, I started the problem by relabeling A₁, …, A_m as C, and relabeling A_m+1 as just A, so that the problem becomes:

Show that [(|- A) => (C |- B)] <=> (A, C |- B)

I’d like to use only the axiom schemata provided on pages 15 to 16 (the introduction/elimination rules on page 44 would be fine also) in the book in solving the problem – here is a link: http://books.google.com/books?id=uV...ntend that the student should" kleene&f=false

I keep running into dead ends, due mainly to the fact that the formula has several |-‘s in the middle of it, and I can’t find rules for how they might be "redistributed" in any of the axiom schemata.

So I hate to do this, but I was basically wondering if somebody could solve the problem for me, showing a list of steps and what axiom schema you used to go from each step to the next, so that I can better understand how to manipulate the axiom schemata.

Thanks for any help you can give.

-HJ Farnsworth

 

[Preno]

This doesn't really have to do with manipulating axiom schemata. Left to right, each proof of B from A₁, ..., A_m is by definition a proof of B from A₁, ..., A_m+1. To prove the other direction, you want to transform a proof of B from A₁, ..., A_m+1 into a proof of B from A₁, ..., A_m given a proof of A_m+1. There is a very simple way of doing that, namely...

 

[HJ Farnsworth]

Thanks for responding, Preno.

What you said about going from left to right is true, but I don't think it applies to this problem, since I'm not assuming that A₁,...A_m => B, but rather that (|-A_m+1) => (A₁,...,A_m => B).

I'm still wanting to do the problem using axiom schemata, since I want to get used to using those fairly rigorously. I think the main thing that I was missing (well not missing, but more not sure if I was allowed to use) is to treat (|-A) => A as an axiom, since the provability of a statement indicates that the statement is true. This let's me simply replace each conclusion of the form (|-A) with A, and each premise of the form A with (|-A). Then, left to right, I have the following:

1. (|-A_m+1) => (A₁,...,A_m |- B) - Assumed
2. (|-A_m+1) => (|-A₁,...,A_m => B) - Equivalence of A |- B and |- A => B
3. |-A₁,...,A_m,(|-A_m+1) => B - Axiom schema 4a, ie., (A => (B => C)) <=> (A,B => C)
4. A₁,...,A_m, (|-A_m+1) |- B - Equivalence of A |- B and |- A => B
5. A₁,...,A_m,A_m+1 |- B - (|-A) => A, and a couple of schema if I want to be more rigorous.

Right to left, I would have:
1. A₁,...,A_m,A_m+1 |- B - Assumed
2. A_m+1, |- A₁,...,A_m => B - Equivalence of A |- B and |- A => B
3. A_m+1 => (|- A₁,...,A_m => B) - Axiom schema 4a, ie., (A => (B => C)) <=> (A,B => C)
4. A_m+1 => (A₁,...,A_m |- B) - Equivalence of A |- B and |- A => B
5. (|-A_m+1) => A_m+1 - (|-A) => A
6. (|-A_m+1) => (A₁,...,A_m |- B).

Is something like axiom schema 4a what you were hinting at at the end of your post?

-HJ Farnsworth

 

[AKG]

Anyways, I started the problem by relabeling A₁, …, A_m as C, and relabeling A_m+1 as just A, so that the problem becomes:

Show that [(|- A) => (C |- B)] <=> (A, C |- B)

That's not right, it would be:

[tex](\vdash A) \Rightarrow [(C \vdash B) \Leftrightarrow (A,C \vdash B)][/tex]

How do you prove an implication? (One way is to) start by assuming the antecedent, so we're assuming [itex](\vdash A)[/itex]. Given this assumption, we want to show the consequent is true, and the consequent is a biconditional. How do we show a biconditional is true? (One way is to) show each separate implication. First let's do the forward implication:

[tex](C \vdash B) \Rightarrow (A, C \vdash B)[/tex]

This is obviously true (we don't even need to make use of our assumption [itex](\vdash A)[/itex] here). Now let's try to show the reverse implication:

[tex](C \vdash B) \Leftarrow (A, C \vdash B)[/tex]

Now we want to prove this implication using the assumption [itex](\vdash A)[/itex], and again, we can show an implication by assuming the antecedent and proving the consequent. So, we assume:

(1) [tex]\vdash A[/tex]
(2) [tex]A, C \vdash B[/tex]

and want to show:

[tex]C \vdash B[/tex]

Now by (2), we get:

[tex]C \vdash (A \rightarrow B)[/tex]

Putting this together with (1), we get:

[tex]C \vdash B[/tex]

Done!

 

[Preno]

Well, the problem is that you are repeatedly confusing the object language and metalanguage, specifically, the object language connective which I will label '->' (Kleene uses the [itex]\supset[/itex] symbol) and the metalanguage abbreviation for "if ..., then ..." which I will label '=>' (Kleene uses the [itex]\rightarrow[/itex] symbol). These are two entirely different things and you absolutely cannot conflate them. Ask yourself, why does Kleene use two different symbols ([itex]\supset[/itex], [itex]\rightarrow[/itex]) while your posts only use one ('=>')?

'->' connects two strings of symbols in the object language to yield another string of symbols in th eobject language. '=>' is simply an abbreviation for "if ..., then ...", thus it connects two statements in the metalanguage (English).

'|-A' is then an abbreviation for "the formula A is provable", not a formula of the object language.

For instance:

What you said about going from left to right is true, but I don't think it applies to this problem, since I'm not assuming that A1,...Am => B, but rather that (|-Am+1) => (A1,...,Am => B).

No, now you're confusing the roles of |-A and A and of A => B and A |- B.

Second, (|-A) => A doesn't even make sense (A is simply an object language formula), what you presumably wanted to say is |-A => |=A (which is true but it has nothing to do with the problem at hand).

Third:

This let's me simply replace each conclusion of the form (|-A) with A, and each premise of the form A with (|-A).

This doesn't make sense. Again, |-A is simply an abbreviation for the metalanguage statement "A is provable". A, otoh, is simply a sequence of symbols in the object language. It doesn't have any truth value. What does have a truth value are statements such as "A is provable" or "A is valid" or "A is satisfiable".

If you are confused about the status of statements like "|-A" and "A => B", you should avoid them all together and write them out as "A is provable" and "if A, then B". These are entirely different from "A" (a singular term referring to a formula) and "A->B" (a formula whose antecedent is A and whose consequent is B), both of which are singular terms, not statements. You can claim that |-A, but it makes no sense to claim that A (just like it makes no sense to claim that 2 or that +).

I'm still wanting to do the problem using axiom schemata, since I want to get used to using those fairly rigorously. I think the main thing that I was missing (well not missing, but more not sure if I was allowed to use) is to treat (|-A) => A as an axiom, since the provability of a statement indicates that the statement is true.

That not what axioms are. Axioms are formulas in the object language (which includes propositional variables and the operations &, v, -> and ~). The object language doesn't include the symbol "|-" (or, for that matter, the symbol, "=>", although it does include '->').

3. |-A₁,...,A_m,(|-A_m+1) => B

Again, this makes no sense.

Is something like axiom schema 4a what you were hinting at at the end of your post?

No. The solution is that a proof of B from A₁, ..., A_m is obtained from a proof of B from A₁, ..., A_m+1 and a proof of A_m+1 by simply pasting the latter in front of the former.

Re AKG's proof, it uses the deduction theorem, which is more difficult to prove than this simple exercise.

 

[HJ Farnsworth]

Thanks again for responding, AKG and Preno.

For instance:

What you said about going from left to right is true, but I don't think it applies to this problem, since I'm not assuming that A1,...Am => B, but rather that (|-Am+1) => (A1,...,Am => B).

No, now you're confusing the roles of |-A and A and of A => B and A |- B.

The way I had the problem written (not how AKG corrected me, since I was assuming that a series of if then statements occurred left to right rather than right to left), I still think that I could not have automatically used the fact that A₁,...,A_m |- B gives, by definition, A₁,...,A_m,A_m+1 |- B, since I did not start off with A₁,...,A_m |- B. However, the way AKG has the problem written, I could certainly have used that property, since in that case I did start off with A₁,...,A_m |- B.

Could you please elaborate on why "(|-A) => A" doesn't make sense, and in general why A does not have a truth value? To me, it seems to say, "if A is provable, then A [is true]", which as far as I can tell makes perfect sense. You say that A has no truth value, but doesn't it have a truth value assuming a truth value for another statement? eg., assuming B=>A is t and B is t gives A is t?

Also, Kleene defines -> as "if...then" (page 5), so I thought that => and -> are synonomous. Could you please elaborate on the difference between them?

Thanks for continuing to purge me of my rookie misconceptions.

-HJ Farnsworth

 

[AKG]

Could you please elaborate on why "(|-A) => A" doesn't make sense, and in general why A does not have a truth value? To me, it seems to say, "if A is provable, then A [is true]", which as far as I can tell makes perfect sense. You say that A has no truth value, but doesn't it have a truth value assuming a truth value for another statement? eg., assuming B=>A is t and B is t gives A is t?

You have a language and a meta-language in which you talk about the language. [itex]A[/itex] is a formula in the language, and [itex]\Rightarrow[/itex] is a connective in your language. On the other hand, [itex]\vdash[/itex] is a symbol in the meta-language, which relates a (set of) formula(s) in your language with another (set of) formula(s) in your language. Since [itex](\vdash A)[/itex] is a statement in the meta-language, you can't use it as the antecedent of a symbol, namely [itex]\Rightarrow[/itex], of your language.

Now if [itex]A[/itex] is a proposition in your language, then [itex]A[/itex] itself means nothing. If [itex]A[/itex] is a compound proposition, then its truth depends on the truth values assigned to the atomic propositions comprising [itex]A[/itex]. If [itex]A[/itex] happens to be a tautology, that is, true in every interpretation of the atomic propositions, we denote this by [itex]\vDash A[/itex]. So you can say something like:

[tex]\vdash A[/tex] implies [tex]\vDash A[/tex]

-----------------

In the solution I gave you, I used the Deduction Theorem, as preno points out. Of course this theorem isn't necessary. Remember the non-trivial part of the problem is to show that:

[tex]C \vdash B[/tex]

assuming:

(1) [tex]\vdash A[/tex]
(2) [tex]A, C \vdash B[/tex]

Given these assumptions how would we deduce [itex]B[/itex] from [itex]C[/itex]? Let [itex]A_0, \ \dots , \ A_n = A[/itex] be the sequence of formulas constituting a proof of [itex]A[/itex], which exists by (1). Let [itex]B_0,\ \dots ,\ B_m = B[/itex] be a sequence of formulas constituting a proof of [itex]B[/itex] from [itex]A, C[/itex] which exists by (2). Then it's easy to see that [itex]A_0, \dots , A_n, B_0, \dots , B_m = B[/itex] is a valid proof of [itex]B[/itex] from [itex]C[/itex].

 

[HJ Farnsworth]

Thanks, AKG.

I think I'm starting to get it. The metalanguage is taking place one level above the object language. eg., in English, if I have something like:

I said, "where are you going?"

then "where are you going?" is in the object language, and "I said" is in the metalanguage. I can't have the response to the question "where are you going?" be in the metalanguage, nor would it make sense to have the metalanguage continue within the quotation, ie., the following two things would not make sense:

I said, "where are you going?". To the baseball game.

I said, "where are you going? Then I went there."

Now, onto symbols in mathematical logic. (|=A) => A places a metalanguage statement in the context of the object language, and is thus nonsensical. It would be analogous to something like:

“I said, ‘where are you going?’” implies “where are you going?”

Basically, (|=A) => A muddles up a comment about the sentence A (that it can be deduced) with the sentence A itself. Above, I said:

To me, it seems to say, "if A is provable, then A [is true]", which as far as I can tell makes perfect sense

This was incorrect, because I inferred a comment about A on the right side of the =>, the [is true] part, which isn’t actually there.

Does what I have said sound correct?

I am still unclear as to the difference between -> and =>. It seems to me that they are synonymous, and that both are perfectly acceptable so long as they don’t jump between different “levels” of language. Does this sound correct, and if not, why?

Thanks.

-HJ Farnsworth

 

[AKG]

Does what I have said sound correct?

Yes, sounds good!

I am still unclear as to the difference between -> and =>.

I don't think there is one, they're just symbols both used for the same thing, which one you use is just a matter of typographical preference. In philosophy classes, you also see the horseshoe symbol [itex]\supset[/itex] used as well to denote implication.