From: Aatu Koskensilta on
Newberry <newberryxy(a)gmail.com> writes:

> Does not seem like he has much to say. "evident from the nature of the
> concepts involved" seems like a contradiction in terms.

Why?

> He is asserting both that matehematics is synthetic a priori and
> analytic.

Shoenfield is not asserting anything about such matters. He's just
presenting a relatively straightforward observation.

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Alan Smaill on
Newberry <newberryxy(a)gmail.com> writes:

> On Mar 1, 2:25�am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
>> Newberry says...
>>
>> >On Feb 28, 5:59=A0pm, stevendaryl3...(a)yahoo.com (Daryl McCullough)
>> >wrote:
>> >Is the axiom of restricted comprehension manifestly true?
>>
>> I think so.
>>
>> >What if you derive counterintuitive consequences from these axioms that
>> >seemed manifestly true at first?
>>
>> I would be disappointed if that didn't happen.
>
> How does manifest truth morph into counter-intuition?

The intuition is that mathematics is full of beautiful surprises,
even when the axioms are consistent.

Well, that's my intuition. What's yours?


>>
>> --
>> Daryl McCullough
>> Ithaca, NY
>

--
Alan Smaill
From: James Burns on
Newberry wrote:
> On Mar 1, 2:25 am, stevendaryl3...(a)yahoo.com
> (Daryl McCullough) wrote:
>>Newberry says...

>>>Is the axiom of restricted comprehension manifestly true?
>>
>>I think so.
>>
>>>What if you derive counterintuitive consequences from
>>>these axioms that seemed manifestly true at first?
>>
>>I would be disappointed if that didn't happen.
>
> How does manifest truth morph into counter-intuition?

The details vary, but it seems to me to be an effect of
none of us being all-knowing.

By the way, one consequence (in the non-logical sense)
of manifest truth morphing into counter-intuition is
the use of logic itself. If intuition gave the same
results as logic, then there would be very little reason
to use logic, since intuition takes so much less effort.

Jim Burns

From: MoeBlee on
On Feb 26, 10:53 pm, Newberry <newberr...(a)gmail.com> wrote:
> On Feb 26, 12:46 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
> > On Feb 25, 8:58 pm, Newberry <newberr...(a)gmail.com> wrote:
>
> > > On Feb 25, 9:45 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
> > > > On Feb 25, 11:22 am, Newberry <newberr...(a)gmail.com> wrote:
>
> > > > > And we believe that PA is consistent because all its axioms are
> > > > > manifestly true?
>
> > > > They're clearly true to a lot of people. They seem clearly true to me.
> > > > Which axiom of PA doesn't strike you as true?
>
> > > > Meanwhile, in a theory such as Z, we prove that the axioms of PA are
> > > > true. Though, I don't argue that that, in itself, has much
> > > > epistemological force.
>
> > > > >     "All unicorns have two horns"
>
> > > > > manifestly true?
>
> > > > Given ordinary predicate logic, if the sentence is taken as
>
> > > > Ax((x is a horse & x has a horn) -> x has two horns)
>
> > > > then it is clearly true in any model in which there are no horses with
> > > > horns.
>
> > > "true in any model in which there are no horses with horns" is the
> > > same as "manifestly true"?
>
> > Okay, then my point is made in even greater force.
>
> If there are no unicorns in your model, what does the model tell you
> about unicorns?

If 'is a unicorn' is a (nickname for a) predicate symbol of the
language but the model maps the predicate (symbol) to the empty set,
then there are still various sentences in the language with 'is a
unicorn' in them. Most salient among them is the sentence, true for
this model, "There are no unicorns".

I don't know what point you think there is to your question.

MoeBlee

From: MoeBlee on
On Mar 1, 12:00 am, Nam Nguyen <namducngu...(a)shaw.ca> wrote:
> Aatu Koskensilta wrote:
> > Nam Nguyen <namducngu...(a)shaw.ca> writes:
>
> >> If you don't really know what system his proof is _in_ then you failed
> >> to know what it means when you said GIT proof is "entirely syntactic
> >> ... proof".
>
> > G del's proof isn't a formal proof in a formal system.
>
> And that's precise my position all along in this thread and in many others
> in the past: Godel Theorem is a meta theorem and _not a FOL theorem_
> (if there's any technical merit to it).

Why aren't you LISTENING? The proof that Godel himself gave was an
informal proof. But that proof (and, subsequently, proofs of Rosser's
even stronger result) may be given in such formal systems as Z set
theory, PA, and even PRA, and Aatu even alerts us that the proof can
be given in a formal PRA using a remarkably small fragment of the
logic.

So, the point is that if you doubt the reliability of PRA then what
WOULDN'T you doubt? If you challenge the reliability of this even
narrower PRA then what mathematical reasoning wouldn't you challenge?

> It's just there are posters who would directly or implicitly argue the
> opposite that Godel's proof is a FOL proof.

No, you didn't even READ Aatu's post. He explicitly mentioned that
results even stronger than Godel's original result ARE formalizable in
certain famous first order theories.

> For example, Frederick
> answered (by quoting Godel) that "P is essentially the system ..."
> when I asked him "So which formal system is that [Godel's] 'syntactic
> proof' in?". Or MoeBlee alluded so in saying Godel's proof could be
> carried out by FOL systems Z and PRA:
>
>    "Godel may not have had PRA specifically in mind at the time
>    (I think PRA was only subsequently stated as an explicit theory?),
>    but at least we do know how to formalize PRA. And if we cannot be
>    confident that PRA is consistent then I don't know what substantive
>    mathematical theory we could be confident as to consistency. In any
>    case, PRA may serve as a formal embodiment of what Godel referred
>    to as finitistic and intuitionistically unobjectionable (or whatever
>    exact phrase he used)."

Yes, and what Aatu wrote goes exactly in hand with that. And you still
have not addressed it.

> > it proceeds solely by way of reasoning about the
> > syntactic form of formal expressions, formal structure of derivations,
> > and so on, and doesn't involve e.g. model theoretic notions.
>
> Are you saying then the notions of "true", "false" can be entirely
> discarded? If the answer is yes, how do we safeguard this sole "way
> of reasoning" from it leading our reasoning to inconsistency, we knowing
> that this "way" is not the rigid formal system proof? If the answer is
> no, what does "truth" mean, we knowing that this isn't model theoretical
> truth?

No, Aatu is not claiming a generalization about discarding anything.
He's just pointing out that the particular approach Godel used (and
which may be formalized in a number of famous first order theories)
was to argue solely about syntax given certain quite ordinary
assumptions about natural numbers.

> > As with any
> > mathematical proof we can of course formalise the proof in any number of
> > formal systems:
>
> You seem to have lost me here.

I can see that you just typed up a whole bunch of stuff in reply to
Aatu before even reading the rest of his post, particularly this
juncture in it.

> Isn't formalizing a proof in a formal system
> essentially the same as deducing a formal system theorem, which as you said
> above isn't the case because "G del's proof isn't a formal proof in a formal
> system."?

Whatever you mean by "deducing a formal system", Aatu is just pointing
out to you that Godel's own particular presentation was informal but
that we can formalize it. What don't you understand about that? Ifmay
prove "If x is a subset of y and y is a subset of x, then x=y" in an
informal manner but I could also present it as a first order proof
from an axiom and definition in formal Z set theory. The same
principle applies to Godel's proof though, of course, the project of
formalizing it is just more complicated and longer. What don't you
understand about this?

> ? primitive recursive arithmetic or even weaker fragments
>
> > of arithmetic, Peano arithmetic, ZFC, Per Martin-L f's constructive type
> > theory, higher-order set theory with the axiom that the class of
> > ordinals is weakly compact, what have you.
>
> OK.

OK? Then why did you not just delete the earlier part of your post?

I strongly suggest you're more interested in shooting back replies to
Aatu than you are in UNDERSTANDING the information he's giving you.
Suggestion: Try reading his post all the way through BEFORE shooting
back your line by line replies.

> What about inconsistent formal systems, if all we really care is just
> a proof - any proof - for GIT?

Again, you're not LISTENING. From Aatu's remarks you can easily
discern that not only can we prove the incompleteness theorem in a
trivial manner (such as from inconsistent axioms) but also from axioms
and logic so very thin as to be virtually unassailable. PRA
(especially with the limited logic Aatu described) uses just plain
computational arithmetic. If you doubt such plain computational
arithmetic, then you might as well doubt ANYTHING in mathematics.

Again, results even STRONGER than Godel's version of the
incompleteness theorem may be proven from EXTREMELY conservative,
cautious, safe mathematical assumptions - virtually the bare
assumptions needed just to carry out ordinary arithmetic computations.

On the other hand, you claim even to doubt, e.g., the following:

1 1 0

is a different pattern from

1 1 1

(or whatever the exact example we discussed a couple of years ago).

So, of course, you could find reason to doubt anything I suppose.

MoeBlee