Prev: Question on a paper of Patton's
Next: How Can ZFC/PA do much of Math - it Can't Even Prove PA isConsistent (EASY PROOF)
From: Nam Nguyen on 4 Jul 2010 10:26 Jesse F. Hughes wrote: > Transfer Principle <lwalke3(a)lausd.net> writes: > >> If Aatu can say that PA is consistent, _period_, without any formal >> proof whatsoever, then why can't Nguyen believe that PA is >> inconsistent, _period_, without formal proof? > > Aatu said PA is consistent, _period_, without any formal proof? > I think that's how MoeBlee expressed what he believed as Aatu's views on the issue. Though not word for word, I believe Aatu's views are close to how MoeBlee described them.
From: Nam Nguyen on 5 Jul 2010 11:08 Aatu Koskensilta wrote: > "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes: > >> Aatu said PA is consistent, _period_, without any formal proof? > > There seems to be some confusion over my (perfectly standard as always) > take on these matters. Allow me to clarify. I know that PA is consistent > because I know how to produce a mathematical argument for that fact > which I fully understand -- in the sense that I grasp the key idea and > can explain all the technical details that go into its execution -- and > find compelling. The proof I have in mind has the following structure: > > 1. We give an inductive definition of a property T(x) of arithmetical > sentences. So, would T(x) be a formula in L(PA)? > > 2. We show that T("P") iff not T("~P"), that T("P & Q") iff T("P") and > T("Q"), and so on. > > 3. We conclude from this that T does not hold of any > contradiction. > > 4. We show that T holds of all the axioms of PA. > > 5. We show that the rules of inference of first-order logic preserve > T. > > 6. We conclude that no contradiction is formally derivable in PA. > > We can of course formalize this proof in any number of theories -- ACA, > ZFC, ... -- but this is just an incidental technical observation of no > immediate interest as far as consistency of PA is concerned. We may also > be interested in knowing exactly which set theoretic axioms are needed > e.g. to justify the sort of inductive definitions involved, and so > on. Again, this has no immediate connection to the question of > consistency of PA. > > As with any proof in ordinary mathematics we take in the above proof > many mathematical principles and modes of reasoning for granted. For > example, we apply induction to a property involving a predicate defined > by means of an infinitary inductive definition. Everyone must decide for > themselves whether they find such invocations evident, compelling, > legitimate mathematics. It's a brute fact of life that in ordinary > mathematics we do in fact take them for granted. > > In Usenet debates, and elsewhere too, people like to make much of and > pontificate tediously on who has or does not have the "burden of > proof". In reality, such "logical" rules of formal debate have about as > much to do with real arguments, persuasion, conversion, as the rules of > cricket. Whoever wants to convince someone else of something must of > course present arguments, questions, reflections, examples, > illustrations that have some real force to the receiving person, > regardless of whether they make a "positive claim" according to some > rulebook of debating. I don't have any real interest in convincing > anyone who does not take ordinary mathematics for granted of much > anything. I'm content with simply noting that the consistency of PA is a > triviality given what we in fact usually take for granted in > mathematics. If someone tells me they find the usual modes of reasoning > horribly dubious or unclear, even after careful explanation and > meticulous elucidation, I simply shrug and move on. >
From: Nam Nguyen on 5 Jul 2010 11:22 Aatu Koskensilta wrote: > "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes: > >> Aatu said PA is consistent, _period_, without any formal proof? > > There seems to be some confusion over my (perfectly standard as always) > take on these matters. Allow me to clarify. I know that PA is consistent > because I know how to produce a mathematical argument for that fact > which I fully understand -- in the sense that I grasp the key idea and > can explain all the technical details that go into its execution -- and > find compelling. The proof I have in mind has the following structure: > > 1. We give an inductive definition of a property T(x) of arithmetical > sentences. > > 2. We show that T("P") iff not T("~P"), that T("P & Q") iff T("P") and > T("Q"), and so on. > > 3. We conclude from this that T does not hold of any > contradiction. > > 4. We show that T holds of all the axioms of PA. > > 5. We show that the rules of inference of first-order logic preserve > T. > > 6. We conclude that no contradiction is formally derivable in PA. > > We can of course formalize this proof in any number of theories -- ACA, > ZFC, ... -- but this is just an incidental technical observation of no > immediate interest as far as consistency of PA is concerned. We may also > be interested in knowing exactly which set theoretic axioms are needed > e.g. to justify the sort of inductive definitions involved, and so > on. Again, this has no immediate connection to the question of > consistency of PA. > > As with any proof in ordinary mathematics we take in the above proof > many mathematical principles and modes of reasoning for granted. For > example, we apply induction to a property involving a predicate defined > by means of an infinitary inductive definition. Everyone must decide for > themselves whether they find such invocations evident, compelling, > legitimate mathematics. It's a brute fact of life that in ordinary > mathematics we do in fact take them for granted. Given this "modes of reasoning" is based on a "take ... for granted" basis, would you care to give some reflections on the (possible) weaknesses of the basis? > > In Usenet debates, and elsewhere too, people like to make much of and > pontificate tediously on who has or does not have the "burden of > proof". In reality, such "logical" rules of formal debate have about as > much to do with real arguments, persuasion, conversion, as the rules of > cricket. Whoever wants to convince someone else of something must of > course present arguments, questions, reflections, examples, > illustrations that have some real force to the receiving person, > regardless of whether they make a "positive claim" according to some > rulebook of debating. I don't have any real interest in convincing > anyone who does not take ordinary mathematics for granted of much > anything. I'm content with simply noting that the consistency of PA is a > triviality given what we in fact usually take for granted in > mathematics. If someone tells me they find the usual modes of reasoning > horribly dubious or unclear, even after careful explanation and > meticulous elucidation, I simply shrug and move on. Given that FOL formal system definition permits a system with infinitely many non-logical symbols, and which is outside the scope of say GIT, are you saying you'd "simply shrug and move on" when, e.g., people ask you to defend or criticize the possible (in)completeness of such system? Why restrict the scope of FOL analysis/discussion to only _individual_ preferences, while FOL understanding is supposed to be general and universal?
From: Nam Nguyen on 5 Jul 2010 11:29 Aatu Koskensilta wrote: > > In Usenet debates, and elsewhere too, people like to make much of and > pontificate tediously on who has or does not have the "burden of > proof". In reality, such "logical" rules of formal debate have about as > much to do with real arguments, persuasion, conversion, as the rules of > cricket. Whoever wants to convince someone else of something must of > course present arguments, questions, reflections, examples, > illustrations that have some real force to the receiving person, > regardless of whether they make a "positive claim" according to some > rulebook of debating. But in real life debate or argument , say in a court, people don't talk about the name "Godel", inaccessible cardinalities, LST, finfinitely many non-logical symbols, to say a few. We do!
From: Nam Nguyen on 5 Jul 2010 13:15
Nam Nguyen wrote: > Aatu Koskensilta wrote: > >> >> In Usenet debates, and elsewhere too, people like to make much of and >> pontificate tediously on who has or does not have the "burden of >> proof". In reality, such "logical" rules of formal debate have about as >> much to do with real arguments, persuasion, conversion, as the rules of >> cricket. Whoever wants to convince someone else of something must of >> course present arguments, questions, reflections, examples, >> illustrations that have some real force to the receiving person, >> regardless of whether they make a "positive claim" according to some >> rulebook of debating. > > But in real life debate or argument , say in a court, people don't > talk about the name "Godel", inaccessible cardinalities, LST, finfinitely > many non-logical symbols, to say a few. > > We do! Honestly, my intention here isn't to argue about the ordinary mathematics we, I included, do virtually all the times. The issue is when I tried: - to understand the difficulty of the arithmetical truth values of formulas such as GC, cGC, ... - to formalize SR, AI I could NOT escape certain _hard_ questions about the very reasoning processes and methods of reasoning we've taken for granted. And I don't think that's just one person's issue. If you don't see any value in the above statement, just to turn the table around and try to _formalize_ a formal system in which statements about, say, SR would hold and you'd see the exact steps, exact difficulties one has to go through. Mathematics is universal in many respects, but one of which is that if there are problems _everyone_ can repeat the steps that would lead to the problems! There's no sense to try escaping them and not to confront them, in order to attempt making mathematics better. FWIW. |