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 16 Dec 2005 23:07 G. Frege wrote: > On 16 Dec 2005 01:36:20 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > > > > *Any* proposition can be proven in intuitionistic logic if you start > > with the [assumption] P&~P. > > > No. That's false. But it is true that any proposition can be derived > as a /conclusion/ from the /premiss/ P & ~P. > > Comment: Obviously you are not very familiar with systems > of natural deduction. There assumptions can be "discharged". > Hence the do not count as premisses of the final argument. > > > > > The above "proof" is fundamentally flawed and *should not* be accepted > > as a valid proof of ~(P&~P). > > > Nonsense. The proof is completely valid. > > > > > [...] What you could do is to make a straightforward, bald assertion > > of ~(P&~P) without claiming to prove it. > > > In logic we would call such a statement an /axiom/ then. > > B u t we do not have to do that, since we can actually prove the > statement in the usual systems (calculi) of intuitionistic logic. > (See the other posts where several proofs in several different > systems [calculi] of intuitionistic logic have been posted.) > > > F. I wonder if anyone realizes what a waste of time this discussion is? You are arguing about the syntax of propositional calculus. What could be more trivial or less consequential? It's just case analysis. Doesn't Resolution alone suffice as the rules of inference? (That's what programmers often use, AFAIK.) It's almost a variant of people attacking the syntax of a proposal rather than addressing the substance of the idea. In that case, they seem to want to do anything to (1) attack the proposal, and (2) not have to do any work in the process. So they look for syntax errors and all they talk about is the syntax and how anyone who doesn't know the syntax shouldn't be trusted or taken seriously. Then they argue ad nauseum about the "true meaning" of symbols. There are plenty of mathematical results that have never been formalized. Why not address something new rather than something so mundane as propositional calculus? > -- > "I do tend to feel Hughes & Cresswell is a more authoritative > source than you." (D. Ullrich) Gad! That is hopeless!
From: Torkel Franzen on 17 Dec 2005 01:14 "Charlie-Boo" <chvol(a)aol.com> writes: > You are arguing about the syntax of propositional calculus. This is a misunderstanding on your part. The argument concerns the semantics of constructive logic. The rule of ex falso quodlibet may reasonably be held to be constructively problematic; hence the relevance of the observation that ~(A<->~A) is provable in minimal logic.
From: Charlie-Boo on 17 Dec 2005 01:40 Torkel Franzen wrote: > "Charlie-Boo" <chvol(a)aol.com> writes: > > > You are arguing about the syntax of propositional calculus. > > This is a misunderstanding on your part. The argument concerns the > semantics of constructive logic. The rule of ex falso quodlibet may > reasonably be held to be constructively problematic; hence the > relevance of the observation that ~(A<->~A) is provable in minimal > logic. ~(A<->~A) is a propositional calculus wff, you're talking about proving it, and all propositional calculus proofs are simply case analysis (examining a finite set of possiblities), which I believe is completely implemented by resolution. Are any of the proofs being discussed not instances of propositional calculus wffs that can be proven by examining the truth tables (i.e. case analysis)? These different systems are merely different syntaxes to represent case analysis. C-B
From: sradhakr on 17 Dec 2005 01:52 G. Frege wrote: > On 16 Dec 2005 01:36:20 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > > > > The above "proof" is fundamentally flawed and *should not* be accepted > > as a valid proof of ~(P&~P). > > > Nonsense. The proof is completely valid. > While I am confused about lots of stuff concerning intuitionistic logic. "discharging an assumption" us NOT my point of confusion here. At the outset, note that I am NOT attacking the little details of your formal system. When I say that the proof is "not valid",I should clarify that I am finiding fault with it given the intuitionistic philosophy, i.e., the intuitionistic conceptions of truth, proof and negation. I have seen Daryl McCullough's post and your further elaboration of another proof of ~(P&~P) and I still have the same difficulty. Let me make one last attempt to make you see what my objection is. My understanding is that ALL proofs of ~(P&~P) in inutionism have to start with the hypothesis P&~P and claim that this is absurd. this is mandated by the intuitionistic conception of negation. The first issue is what, precisely, is the "absurdity"? I assert that the ONLY absudity that one can demonstrate is that an *arbitrary* proposition would result if one allows P&~P to stand. Remember that one cannot claim that P&~P is absurd in a pre-existing Platonic universe; that is not allowed by the intutionistic philosophy. Since truth=provability according to intuitionistic philosophy, one can interpret "~(P&~P)" as "A proof of P&~P is impossible", or equivalently, "A proof of P and a proof of ~P is impossible". So the outline of an intuitionistic proof of ~(P&~P) would be as follows. (1) Suppose, to the contrary, that P&~P, i.e., suppose that "Both P and ~P are provable".. (2) The said proof of P&~P can be converted into the proof of an arbitrary proposition Q.. (3) Therefore a proof of P&~P cannot exist. Hence, ~(P&~P). Here is my objection. One can alter (3), equivalently in intuitionistic logic, to the following: (3)* Therefore, it is provable that a proof of P&~P cannot exist, and ~(P&~P) follows The problem with deducing (3)* from (2) is as follows. One can interpret (3)* as asserting the existence of one particular ;proof that follows from an application of EFQ in step (2). I.e., one can interpret step (2) as "an arbitrary proposition Q has been proven" and step (3)* as following trivially from this interpretation. You can yell yourself hoarse that it ain't so, the assumption (1) has been discharged before concluding (3),, etc. But it seems to me that the formal outline of the proof is substantially the same in both cases. At least they are *too* similar for comfort. Regards, RS
From: Torkel Franzen on 17 Dec 2005 02:02
"Charlie-Boo" <chvol(a)aol.com> writes: > ~(A<->~A) is a propositional calculus wff, you're talking about proving > it, and all propositional calculus proofs are simply case analysis > (examining a finite set of possiblities), which I believe is completely > implemented by resolution. This is just to say that you know nothing about constructive logic. |