Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: Charlie-Boo on 9 Jan 2006 10:26 Daryl McCullough wrote & Charlie-Boo says... > Yes, intuitionistic propositional logic is a *particular* subset of > classical propositional logic, namely those that are provable using > intuitionistically valid rules of inference. That's it. That's my point. But you forget that Frege has already devoted his life to proving and re-proving propositional calculus wffs using an endless variety of axioms and rules (and even different adequate sets of connectives), despite it all being encompassed by simple case analysis. (Who should break the news to him?) How much effort should someone use to explain something that a simple computer program can compute? I say, not after elementary school during which the children learn to compute these recursive functions themselves. Have you ever heard of anyone seriously questioning Occam's Razor? C-B > Daryl McCullough > Ithaca, NY
From: Daryl McCullough on 9 Jan 2006 11:28 Charlie-Boo says... > >Daryl McCullough wrote & Charlie-Boo says... > >> Yes, intuitionistic propositional logic is a *particular* subset of >> classical propositional logic, namely those that are provable using >> intuitionistically valid rules of inference. > >That's it. That's my point. Your point was that you shouldn't use case analysis if you are interested in finding out which propositional formulas are intuitionistically valid? If so, I agree---you shouldn't use case analysis. -- Daryl McCullough Ithaca, NY
From: Charlie-Boo on 9 Jan 2006 17:58 David C. Ullrich wrote: > In formal Logic we don't use one symbol to denote > two diffferent things in the same expression. The > fact that I knew that is exactly why I had no idea > that you meant what you say you meant by that > expression. I did not change the semantics, only the syntax in a one-to-one manner from that used in Modal Logic. Thus your criticism applies equally well to the standard use of Modal Logic. > > A better > >counterexample for you (than meaningless propositional variables) would > >be P is any Godel sentence and Q is FALSE. > > A counterexample that depends on an _actual_ deep theorem is > "better" than a simple and totally elementary counterexample? > Fascinating. Your "proof" says, "suppose P (is an) atomic formula in the predicate calculus. Then P is not provable." This is not well-formed. (It is meaningless.) If P is an Atomic Formula then it consists of a Predicate Letter applied to terms. But then P == |-P has no meaning since P is not interpreted. P has no proof - nor does it have any truth value. When we talk about true, provable, unprovable etc. we are talking about interpreted wffs, not uninterpreted Predicate Letters. Atomic Formulas have no proof nor truth value, and so talking about whether P is == |-P or not is meaningless. (Mendelson 1964 pg 46-53) As I then pointed out, after trying combinations of Godel sentences, I realized that P is a Godel sentence and Q is FALSE refutes this earlier version of my theorem, not a trivial misuse of concepts of Mathematical Logic. C-B > ************************ > > David C. Ullrich
From: Charlie-Boo on 9 Jan 2006 18:17 David C. Ullrich wrote: > You post a "theorem" that's obviously false, where > "obviously false" means that it takes no effort whatever to > find a counterexample, counterexamples are simply obvious. Your "refutation" is meaningless as it refers to the truth of an Atomic Formula. It is not provable because it is not interpreted but then it also lacks a truth value and it is meaningless to talk about P==|-P when P can have unquantified free variables. C-B > And in reply to an utterly simple counterexample all you > can say is that it's not a very good counterexample > because it's too trivial. Huh. > > Hint: An utterly trivial counterexample here is better > because it better illustrates how _obviously_ false the > theorem was. > > Another hint: Credibility-wise it doesn't seem like a good > idea for you to point out that a "Godel sentence" gives > a counterexample. Because all this started with your > amazing profundities about Godel this and Godel that - > if I were you I'd hope that nobody _noticed_ that what > I was saying was obviously inconsistent with Godel's > theorems. > > >By that logic, you can say that a > >system is incomplete because it has a propositional variable with no > >meaning and thus no proof of it or its negation. > > Yes, if the question were whether propositional logic was complete > the answer would be obviously not, because an atomic formula > is neither a tautology nor an anti-tautology. > > >That's not what we're talking about. > > Giggle. Translation: Let's not talk about the really really obvious > counterexamples to my assertions. Instead let's restrict discussion > to counterexamples that depend on non-trivial results in logic - > that way we'll still sound smart, even though what we said was > obviously wrong. > > Tee-hee. > > >C-B > > > >> ************************ > >> > >> David C. Ullrich > > > ************************ > > David C. Ullrich
From: Charlie-Boo on 9 Jan 2006 18:20
> >Daryl McCullough wrote & Charlie-Boo says... > >> Yes, intuitionistic propositional logic is a *particular* subset of > >> classical propositional logic, namely those that are provable using > >> intuitionistically valid rules of inference. > > > >That's it. That's my point. > > Your point was that you shouldn't use case analysis if you > are interested in finding out which propositional formulas > are intuitionistically valid? No, I never said to not use case analysis. This whole discussion has been the opposite. C-B > If so, I agree---you shouldn't > use case analysis. > > -- > Daryl McCullough > Ithaca, NY |