How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent (EASY PROOF)
in [Logic]
|
Prev: equivalence
Next: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent (EASY PROOF)
From: MoeBlee on 29 Jun 2010 11:36 On Jun 29, 5:29 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > The fact that a model implies consistency is what is missing from ZFC, > so that is not a proof in ZFC. NO. ZFC proves that if a theory has a model then the theory is consistent. Do you REALLY not know how to see that for yourself? Have you even taken a MOMENT to see how to prove it? MoeBlee
From: Chris Menzel on 29 Jun 2010 11:26 On Tue, 29 Jun 2010 03:57:02 -0700 (PDT), Charlie-Boo <shymathguy(a)gmail.com> said: > On Jun 27, 9:40 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu> wrote: >> On Sun, 27 Jun 2010 17:14:02 -0700 (PDT), Charlie-Boo >> <shymath...(a)gmail.com> said: >> >> >> > > ZF, for example, proves Con(PA) which, of course, PA does not >> >> > > (assuming its consistency). >> >> > > > You have to assume PA is consistent? >> >> > > You have to ask? >> >> > Yes or no, please. >> >> Yes. (You *really* had to ask?) > > In Godel's proof that his system cannot prove its own consistency, he > uses the caveat "assuming it is consistent". But he is not talking > about PA at that point. He is talking about a system with a variable > for the set of axioms, which includes consistent systems and > inconsistent systems. Thus the "assuming it is consistent". > > Many unsophisticated people mistakenly refer to "assuming PA is > consistent", not knowing that Godel was talking about sets of axioms > outside of PA's. Sorry, but you are entirely mistaken. > PA itself is consistent, as is easily proved based on the simple fact > that the axioms and rules preserve truth. > > There is no "assuming PA is consistent", Chris Menzel - it is provably > consistent. It is indeed, except any such proof, when formalized, will be in a system stronger than PA itself and hence one whose consistency can only be proved in a stronger system still. The qualification "assuming PA is consistent" is simply an allusion to this Goedelian fact. It's not an expression of doubt. I, like most people, have no doubts about PA's consistency. But the only justification one can offer is that its axioms -- or the axioms of a stronger system in which PA's consistency is proved -- seem to be self-evident.
From: MoeBlee on 29 Jun 2010 11:42 On Jun 29, 6:57 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Without the axiom of infinity we can't prove that if a theory has no > model it is inconsistent. Indeed, we can prove in ZF-Inf+~Inf that some > consistent theories have no model. Under the ordinary definition of 'theory' (T is a theory <-> T is a set of sentences closed under entailment), and with the usual kind of languages and systems we're talking about here, in ZF-Inf~~Inf, we prove "there does not exist a theory". Of course, under some possible wider definition of 'theory' (so that there are theories that aren't infinite (i.e. are not an infinite set of sentences)), then something else may hold about theories. MoeBlee > > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, dar ber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: MoeBlee on 29 Jun 2010 11:43 On Jun 29, 7:34 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Transfer Principle <lwal...(a)lausd.net> writes: > > 1. Is there a proof in ZF-Inf+~Inf that every set is finite? > > It appears I once posted a proof. It relies, in an essential way, if I > recall correctly, on the axiom of replacement. Right. I reposted it yesterday. MoeBlee
From: MoeBlee on 29 Jun 2010 11:48
On Jun 29, 7:58 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Charlie-Boo <shymath...(a)gmail.com> writes: > > How about when you said that Gentzen proved PA consistent using ZFC? > > No one ever proves anything using ZFC in the sense of producing formal > derivations. Rather, they prove mathematical theorems using mathematical > principles formalized in ZFC. By certain elementary considerations we > know the formalizations of such theorems are formally derivable in ZFC. One quibble: There are people who do produce (even if only exercises) displays of certain formal ZFC derivations, as well as those who generate such derivations with computer programs, etc. Other than that, I think what you wrote is a well stated needed summary that should be part of a standing FAQ: Ordinarily, mathematicians "prove mathematical theorems using mathematical principles formalized in ZFC. By certain elementary considerations we know the formalizations of such theorems are formally derivable in ZFC." MoeBlee |