Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: G. Frege on 17 Dec 2005 10:50 On Sat, 17 Dec 2005 07:56:51 -0600, David C. Ullrich <ullrich(a)math.okstate.edu> 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)
From: Charlie-Boo on 17 Dec 2005 12:31 Torkel Franzen wrote: > "Charlie-Boo" <chvol(a)aol.com> writes: > > And: So "~(A<->~A) is a propositional calculus wff" is wrong? > > Aha, I see! You mistakenly thought that the argument was about > classical logic! No, I said quite the opposite - my whole point, in fact. I wrote, "These different systems are merely different syntaxes to represent case analysis." I never said it was about classical logic alone. I still ask: Are any of the proofs being discussed not instances of propositional calculus wffs that can be proven by examining their truth tables (i.e. case analysis)? If there are, then point them out. Otherwise, as I said, you are talking about different syntaxes (systems) for the same semantics (case analysis.) C-B
From: Torkel Franzen on 17 Dec 2005 17:47 "Charlie-Boo" <chvol(a)aol.com> writes: > No, I said quite the opposite - my whole point, in fact. I wrote, > "These different systems are merely different syntaxes to represent > case analysis." I never said it was about classical logic alone. Of course not, given that you are unaware of the difference between classical and constructive logic.
From: Charlie-Boo on 17 Dec 2005 19:15 Torkel Franzen wrote: > "Charlie-Boo" <chvol(a)aol.com> writes: > > > No, I said quite the opposite - my whole point, in fact. I wrote, > > "These different systems are merely different syntaxes to represent > > case analysis." I never said it was about classical logic alone. > Of course not Yet you wrote, "You mistakenly thought that the argument was about classical logic!" My comment was that all you and Frege were discussing was what he often talks about: different ways to prove propositional calculus wffs that are all just case analysis (and that he should try formalizing something new and not so trivial.) I asked you to give an example of a proof within the thread that couldn't be accomplished by examining truth tables (case analysis.) As you are unable to give any examples, you have verified my assertion. Thanks! C-B
From: Torkel Franzen on 17 Dec 2005 19:39
"Charlie-Boo" <chvol(a)aol.com> writes: > Yet you wrote, "You mistakenly thought that the argument was about > classical logic!" What do you find odd about this? |