Re: Simple yet Profound Metatheorem

On Sat, 17 Dec 2005 07:56:51 -0600, David C. Ullrich
<ullrich@xxxxxxxxxxxxxxxx> wrote:

>>
>> ...what is wrong with:
>>
>> Thm. (|- (P=Q)) => ((|- P) = (|- Q))
>>
> If my guess regarding what you mean is correct then
> this is a true fact, not that the "derivation"
> below makes much sense.
>
Imho it's rather helpful to adopt two different sets of symbols for
logical connectives: one for object-level and one for meta-level.

Object language: ^, v, -, ->, <->
Meta-language: &, or, ~, =>, <=>

This way we can avoid confusion.

So we had the meta-theorem:

|-(P <-> Q) => (|-P <=> |-Q)

Meta-proof:

1. |-(P <-> Q) A
2. |-(P -> Q) ^ (Q -> P) 1 Def. <->
3. |-(P -> Q) 2 ^E
4. |-(Q -> P) 2 ^E
5. |-P A
6. |-Q 3,5 ->E
7. |-P => |-Q 5,6 =>I
8. |-Q A
9. |-P 4,8 ->E
10. |-Q => |-P 8,9 =>I
11. (|-P => |-Q) & (|-Q => |-P) 7,8 &I
12. |-P <=> |-Q 11 Def. <=>
13. |-(P <-> Q) => (|-P <=> |-Q) 12 =>I

>>
>> Thm. ((|- P) = (|- Q)) => |- (P=Q)
>>

Claim (Charlie-Boo):

(|-P <=> |-Q) => |-(P <-> Q)

>
> This on the other hand is obviously false:
> If P is provable and Q is provable (so that
> |- P <=> |- Q is true) then P <-> Q is
> certainly provable. [...]
> But if neither P nor Q is provable (so that
> |- P <=> |- Q is true) it certainly
> does not follow that P <-> Q _is_ provable.
>
> [slightly changed your notation --F.]
>
> For example, suppose P and Q are both atomic
> formulas in the predicate calculus: P = p
> and Q = q, where _those_ equal signs denote
> _equality_. Then P is not provable, Q is not
> provable, and neither is P <-> Q.)
>

Very good point. :-)

Hence there should be something wrong with Charlie's "proof":

>>
>> 1. ((|- P) = (|- Q)) Premise
>> 2. (|- P) => (|-Q) Definition 1
>> 3. (|-Q) => (|-P) Commutativity and Definition 1
>> 4. |- (P=>Q) Deduction Theorem 2
>> 5. |- (Q=>P) Deduction Theorem 3
>> 6. |- (P=Q) Definition 4,5
>>

Let's see:

1. |-P <=> |-Q A
2. (|-P => |-Q) & (|-Q => |-P) 1 Def. <=>
3a. |-P => |-Q 2 &E
3b. |-Q => |-P 2 &E

This corresponds to steps 1-3 in Charlie's "proof".

Now...

>>
>> 4. |- (P=>Q) Deduction Theorem 2
>> 5. |- (Q=>P) Deduction Theorem 3
>>

Of course, adopting our convention concerning logical symbols, this
should read:

>>
>> 4. |-(P -> Q) Deduction Theorem 2
>> 5. |-(Q -> P) Deduction Theorem 3
>>

So the question is, if the following steps are valid:

(|-P => |-Q)
* ------------
|-(P -> Q)
and
(|-Q => |-P)
* ------------
|-(Q -> P)

Charlie mentions the rule "Deduction Theorem"...?!

Using your counter example from above, we can show that this steps are
not valid, hence Charlie's "Deduction Theorem" (whatever he means by
this) is not a valid rule of derivation in this context.


F.

--
"I do tend to feel Hughes & Cresswell is a more authoritative
source than you." (David C. Ullrich)
.