From: george on 9 Nov 2007 10:30 On Nov 8, 11:59 pm, Newberry <newberr...(a)gmail.com> wrote: > He clearly believes that the we know PA/ZFC There is no such thing as PA/ZFC. PA is one thing. ZFC is another. > to be consistent with the > same certainty as any mathematical theorem The theorem that PA is consistent is provable in ZFC. It is NOT provable from/in PA. That ZFC is consistent has never been proven. It is certainly not provable from ZFC. Bothering to try to prove it in anything stronger is pointless; you would just have the same question about whether that stronger theory was vs. wasn't consistent. > i.e. we can prove G. "G" is NOT *one* thing. There is a DIFFERENT G for every (sufficiently rich) recursive axiom-set. You canNOT prove G(PA) in PA. You canNOT prove G(ZFC) in ZFC. > So the question arises how we can construct a machine that can do the same. > obviously not by emulating PA/ZFC. First-order logic is complete. It has inference rules. You just construct a machine that applies the inference rules repeatedly. There are some treatments with as few as one rule. And there *is* a way of doing this that you could think of as "emulating ZFC". Or emulating anything else for that matter. The point being that the axioms from which you are going to derive this theory are just one more INPUT to the machine.
From: george on 9 Nov 2007 10:31 On Nov 9, 7:17 am, aatu.koskensi...(a)xortec.fi wrote: > Yes, PA is obviously consistent. Come on. The Gentzen proof is not obviously understandable. N doesn't obviously exist at all.
From: george on 9 Nov 2007 10:34 AK > > > > Yes, PA is obviously consistent. On Nov 9, 8:00 am, abo <dkfjd...(a)yahoo.com> wrote: > Conclusive! Obvious! Who could doubt what one learned as a young boy > in Sunday school? I rated that 5 stars. Which I really don't like having to do for people with whom I've had bitter arguments.
From: george on 9 Nov 2007 10:35 On Nov 9, 8:20 am, Herman Jurjus <hjur...(a)hetnet.nl> wrote: > aatu.koskensi...(a)xortec.fi wrote: > > Yes, PA is obviously consistent. > > So what? So N is a model of it, so G is true, so a whole buncha stuff. Pick one. I don't think AK will care as much as Newberry will.
From: Daryl McCullough on 9 Nov 2007 16:47
Newberry says... >He clearly believes that the we know PA/ZFC to be consistent with the >same certainty as any mathematical theorem i.e. we can prove G. So the >question arises how we can construct a machine that can do the same. >obviously not by emulating PA/ZFC. Well, here's an attempt at describing an informal metatheory that captures a lot of human metatheoretic reasoning: 1. Every axiom of ZFC is true. 2. For every statement Phi in the language of ZFC, Phi <-> Phi is true. 3. If T is any theory in the language of ZFC, and every axiom of T is true, then every theorem of T is true. This informal theory can prove Con(ZFC) and Con(ZFC + Con(ZFC)), etc. And it's all perfectly mechanical; you can write a program to work out all the consequences of rules 1-3. Of course, we can give a name to this new theory: Let ZFC_1 = the collection of all statements in the language of ZFC that follow from rules 1-3. Then we can come up with yet another theory by modifying rule1: 1'. Every axiom of ZFC_1 is true. Then we could let ZFC_2 be the set of all consequences of rules 1', 2, and 3. etc. -- Daryl McCullough Ithaca, NY |