From: Newberry on
On Jun 22, 11:16 am, George Greene <gree...(a)email.unc.edu> wrote:
> On Jun 21, 12:10 am, Newberry <newberr...(a)gmail.com> wrote:
>
> > We better get this straight. Thie is from Wikipedia:
>
> > "for any consistent, effectively generated formal theory that proves
> > certain basic arithmetic truths, there is an arithmetical statement
> > that is true,[1] but not provable in the theory" (Kleene 1967, p.
> > 250).
>
> Unfortunately, Newberry continues,
>
> > I do not know how Kleene would prove that in ANY conceivable theory
> > capable of arithmetic with a plausible interpretation there are
> > unprovable truths.
>
> KLeene would NOT prove that, since Kleene DID NOT SAY that.
> What Kleene DID say was that for any EFFECTIVELY GENERATED formal
> theory,
> there were unprovable (i.e. UN-effectively-generatable) truths.
> He did NOT say that this was for "any conceiveable" theory.
>
> Well, I hope that clears THAT up.

I do not know how Kleene would prove that in ANY conceivable
EFFECTIVELY GENERATED theory capable of arithmetic with a plausible
interpretation there are unprovable truths.

> Of course, there are those of us who think that "un-effectively-
> generatable formal theory"
> IS A CONTRADICTION IN TERMS (what MAKES a theory "formal" is that you
> CAN
> generate it), but standard technical parlance is that ANY old "full"
> set of consequences
> (even if there is no effective way of filling it out) is a theory.
> "True" "natural" first-order arithmetic is such a "theory".

From: Aatu Koskensilta on
Barb Knox <see(a)sig.below> writes:

> That is again just flat wrong. Tarski's work on semantical truth was
> current at the time of Goedel's work. Goedel intentionally wanted a
> purely syntactic demonstration, not one that relied on semantic truth.
> Goedel knew perfectly well what makes a mathematical statement
> semantically true in the modern sense. His incompleteness theorems
> are simply not about that.

You've got your history a bit mixed-up here. The incompleteness theorems
predate Tarski's work on truth. G�del was, as Hao Wang reports, led to
the incompleteness theorems in attempt to reduce the consistency of
analysis to consistency of arithmetic, using a truth predicate. He
realized that arithmetical truth is not arithmetically definable, but
provability in a formal theory is.

> Even though popularisations of Goedel's results discuss them in terms of
> "truth", the results themselves do not.

It might be a good idea for you to find Torkel Franz�n's old G�del page
in the web archives.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: George Greene on
On Jun 23, 12:48 am, Newberry <newberr...(a)gmail.com> wrote:
> I do not know how Kleene would prove that in ANY conceivable
> EFFECTIVELY GENERATED theory capable of arithmetic with a plausible
> interpretation there are  unprovable truths.

"Effectively generated" is well-defined.
You just use the definition; THAT'S how you prove it.
Godel proved it first; there was not much left for anyone to add
except the formal statement of what it meant to be "effectively
generatable",
which is itself related to Church's Thesis.

"ANY conceivable" and "effectively generatable" are just NOT
compatible.
"Effectively generatable" puts some clear limitations on the theory.
What is conceivable withOUT that constraint is going to be very broad,
but even so, proving something for "any and everything" is a lot
simpler
than you seem to think. You do NOT have to take into account all the
infinite
complexity of "everything": you in fact do the opposite: you just
throw ALL THAT AWAY
because a result that is going to apply TO EVERYthing canNOT CARE
about any of that
detail.

From: Newberry on
On Jun 23, 2:22 pm, George Greene <gree...(a)email.unc.edu> wrote:
> On Jun 23, 12:48 am, Newberry <newberr...(a)gmail.com> wrote:
>
> > I do not know how Kleene would prove that in ANY conceivable
> > EFFECTIVELY GENERATED theory capable of arithmetic with a plausible
> > interpretation there are  unprovable truths.
>
> "Effectively generated" is well-defined.
> You just use the definition; THAT'S how you prove it.

The issue is the definition of truth.

> Godel proved it first; there was not much left for anyone to add
> except the formal statement of what it meant to be "effectively
> generatable",
> which is itself related to Church's Thesis.
>
> "ANY conceivable" and "effectively generatable" are just NOT
> compatible.
> "Effectively generatable" puts some clear limitations on the theory.
> What is conceivable withOUT that constraint is going to be very broad,

Obviously I meant any conceivable within that constraint.

> but even so, proving something for "any and everything" is a lot
> simpler
> than you seem to think.  You do NOT have to take into account all the
> infinite
> complexity of "everything": you in fact do the opposite: you just
> throw ALL THAT AWAY
> because a result that is going to apply TO EVERYthing canNOT CARE
> about any of that
> detail.

From: George Greene on

> On Jun 23, 2:22 pm, George Greene <gree...(a)email.unc.edu> wrote:
> >"Effectively generated" is well-defined.
> > You just use the definition; THAT'S how you prove it.

On Jun 23, 11:32 pm, Newberry <newberr...(a)gmail.com> wrote:
> The issue is the definition of truth.

No, DUMBASS, the issue IS NOT the definition of truth.
ALL the definitions of truth have in common that everything that is
provable is true (if the theory is consistent). The question was
whether
the truths could get MORE COMPLICATED and go BEYOND that.
It turns out that THEY CAN, so coming up with A MORE complicated
definition of truth IS NOT going to change that! That's only going to
make this result MORE TRUE, under ANY definition of truth.


> > "ANY conceivable" and "effectively generatable" are just NOT
> > compatible.
> > "Effectively generatable" puts some clear limitations on the theory.
> > What is conceivable withOUT that constraint is going to be very broad,
>
> Obviously I meant any conceivable within that constraint.

But the whole point is, there ISN'T much of anything conceivable
EXCEPTT TURING MACHINES, within that constraint!
The other candidates (lambda-calculus, e.g.,) ARE PROVABLY
equivalent!