Torkel Franzen on truth
in [Logic]
|
From: Peter_Smith on 24 Nov 2007 18:42 On 24 Nov, 22:49, Newberry <newberr...(a)gmail.com> wrote: > We are interested in whether "PA is > consistent" is true. How did we arive at the knowledge of this truth? > Is the method we arrived at it formalizable? The issue was whether a particular argument that leads to a certain conclusion (the consistency of PA) is formalizable. The question of the "method" by which we hit on the argument in question is quite different. It may be mere luck that we hit on a proof: that doesn't affect the question of whether the proof, when discovered, is susceptible to formalization.
From: Newberry on 24 Nov 2007 20:26 On Nov 24, 3:42 pm, Peter_Smith <ps...(a)cam.ac.uk> wrote: > On 24 Nov, 22:49, Newberry <newberr...(a)gmail.com> wrote: > > > We are interested in whether "PA is > > consistent" is true. How did we arive at the knowledge of this truth? > > Is the method we arrived at it formalizable? > > The issue was whether a particular argument that leads to a certain > conclusion (the consistency of PA) is formalizable. Is it? > The question of the "method" by which we hit on the argument in > question is quite different. By "method" obviously I did NOT mean the method of arriving at proofs. I used "method" instead of "proof" to avoid certain connotations. > It may be mere luck that we hit on a proof: that doesn't affect the > question of whether the proof, when discovered, is susceptible to > formalization. I do not understand this. Let's first decide if the argument that leads to "No matter how long we generate theorems of PA we will never derive a contradiction" is true is formalizable. In particular we are interested in the argument that makes us certain that this is the case, not the formalization in ZFC. Not knowing if ZFC is consistent we do not know if the ZFC proof produces a truth or a falsehood.
From: Daryl McCullough on 26 Nov 2007 10:37 Newberry says... > >On Nov 24, 11:25 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> But to "prove" something means to derive it from a set of axioms. >> Proof is relative to a set of axioms, but *truth* is not. So >> whether PA is consistent or not is a matter of fact, independent >> of any axioms. But whether we can *prove* that fact depends on >> what axioms we are using. > >If the fact is independent of any axioms then I wonder what we need >the axioms for. The point of axioms is to show that the truth of a complex, not intuitively obvious statement follows from the truth of statements that you've already accepted. >Let's forget about proofs then. How do we determine if >"PA is consistent" is true? You have to look at what the axioms of PA *say*. The Peano axioms are about the natural numbers, which has an intuitive interpretation in terms of counting, pebbles, for instance. The successor operation corresponds to adding another pebble to a collection. If x was the number beforehand, then x+1 is the number afterwards. The addition operation corresponds to combining two collections of pebbles. If x is the number in the first collection, and y is the number in the second collection, then x+y is the number in the combined collection. The multiplication operation corresponds to the operation of lining up pebbles in rectangular arrays. If you have an array of x rows of pebbles, and y pebbles in each row, then you have x*y pebbles altogether. The axioms of PA are all intuitively true about this interpretation. We accept them as true because we can hardly conceive of how they can be false. But it's just a matter of firmness of intuitions. Our intuitions *could* be wrong, I suppose. But if we are wrong about something as simple as arithmetic, then I don't think that there is a single aspect of mathematics that would be salvageable. We might as well treat arithmetic as correct until we have good reason to believe otherwise. >> Because it follows from other things we believe. There is no >> absolute sense in which we know it (or anything else). It's >> just that the consistency of PA follows from our best theories >> of mathematics. > >Which theories? ZFC? We cannot prove that ZFC is consistent. So what? You can only prove things from axioms. Either those axioms are left unproved, or you have an infinite chain of axioms built on top of axioms, with no foundation. Those are the choices. >> >So which one is it? >> >A) We don't prove the correctness of those intuitions >> >B) it's perfectly well formalizable >> >> Both are true. The consistency of PA follows from ourive >> intuitions. Our intuitions are pretty much formalizable. >> But we can't prove the correctness of those intuitions. > >By formalization I mean a formal proof. That's what I mean, too. There is a formal proof of the consistency of PA. >We were discussing the fact >that no matter how long we generate theorems of PA we will never >derive a contradiction. How did we arrive at the knowledge that it is >true? You could take it to be an empirical fact, tested by centuries of experience. >Is the method by which we arrived at it formalizable? Yes. -- Daryl McCullough Ithaca, NY
From: LordBeotian on 26 Nov 2007 12:46 "Newberry" <newberryxy(a)gmail.com> ha scritto >> >So which one is it? >> >A) We don't prove the correctness of those intuitions >> >B) it's perfectly well formalizable >> >> Both are true. The consistency of PA follows from ourive >> intuitions. Our intuitions are pretty much formalizable. >> But we can't prove the correctness of those intuitions. > > By formalization I mean a formal proof. We were discussing the fact > that no matter how long we generate theorems of PA we will never > derive a contradiction. How did we arrive at the knowledge that it is > true? We have 2 methods: 1) We consider the issue from a sintactic point of view and prove it by transfinite induction (Gentzen). 2) We find a model for the axioms. > Is the method by which we arrived at it formalizable? Both 1 & 2 are formalizable in ZFC *BUT* we DON'T know that PA is consistent because we formalized it in ZFC (*), we instead DO know it by mere consideration of the intuitive not-formalized arguments 1 or 2 above. (*) Otherwise you could ask why should ZFC influence our belief given the fact that we don't even know if it is consistent.
From: george on 26 Nov 2007 17:46
On Nov 24, 12:43 pm, Newberry <newberr...(a)gmail.com> wrote: > "PA is consistent" means that in PA, for any P we will never derive P > & ~P no matter how long and in what order > we keep generating theorems. Exactly so. But the question is, WHAT axioms are you trying to prove this FROM? If you are trying to prove it from PA itself, then it is hopeless (unless PA is inconsistent, in which case it will allow you to prove both that it is consistent AND THAT IT ISN'T). > It is not relative to any axioms. This is entirely wrong. Whether something IS (or is not) a *valid* or *sound* STEP in a proof, and whether some stringing- together of such steps is or is not a proof, IS axiomatically definable, at least up to finitude. Whether something does or does not CONSTITUTE a proof (or proof-subtree) IS relative to axioms. There are DIFFERENT possible systems of logic and rules of inference. You DO NEED to specify the one you are using -- the one that defines "proof", as you define it -- axiomatically. In the first-order case this is sort of fundamentally guaranteed to fail because we intuitively require that proofs must be finite, and finitude is not first-order definable. But you need to clarify your other confusions before falling on *that* sword. > It either is the case or not. True, but which of these is the case *does* depend on the *meta*-theoretical axioms that you used in *your* logic's definition of "proof". > This is what we are interested in proving. Who "we", dumbass? The whole import of Godel's theorem is that this CAN'T be proved. |