From: Aatu Koskensilta on
Nam Nguyen <namducnguyen(a)shaw.ca> writes:

> You should have told me so years ago. Now I feel "unfortunate" that I
> bought Shoenfield's "Mathematical Logic" to loose my precious time
> learninng formal systems and FOL proofs! (Kind of kidding, of course!)

There are some formal proofs in Shoenfield's _Mathematical Logic_ but
mostly we find just loads of ordinary mathematical proofs of theorems
about formal provability, formal proofs, formal systems, models,
recursive functions, definable sets of naturals, axiomatic set
theory. Here by "ordinary mathematical proof" is meant a piece of
mathematical reasoning (in mathematical English) from basic mathematical
principles -- the principle of mathematical induction, basic properties
of addition and multiplication, ... -- establishing some conclusion.

> You seem to have lost me here. 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."?

I can't really see what it is you find difficult to understand. G�del's
proof is not a formal proof, as is apparent on even a brief glance at
the paper, but we can formalise it to give a formal proof in a suitable
formal system, such as primitive recursive arithmetic. In this it is no
different from any proof in mathematics. That the proof doesn't involve
e.g. any model theoretic considerations we ascertain simply by
inspecting the proof and the relevant definitions. Again, I suggest you
consult a standard text such as Girard's _Proof Theory and Logical
Complexity_.

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on
Aatu Koskensilta <aatu.koskensilta(a)uta.fi> writes:

> Here by "ordinary mathematical proof" is meant a piece of mathematical
> reasoning (in mathematical English) from basic mathematical principles
> -- the principle of mathematical induction, basic properties of
> addition and multiplication, ... -- establishing some conclusion.

I seem to have quite unnecessarily introduced an element of
idealisation. Allow me to rectify: an ordinary mathematical proof is a
piece of mathematical reasoning (expressed in natural language augmented
with mathematical notation and jargon) establishing the truth of some
mathematical statement by indicating in a way appropriate for the
intended audience how the conclusion follows from axioms or previously
proven mathematical results. About axioms Shoenfield has this to say:

For what reason do we accept the axioms? We might try to use
observation here; but this is not very practical and hardly in the
spirit of mathematics. We therefore attempt to select as axioms certain
laws which we feel are evident from the nature of the concepts
involved.

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Newberry on
On Mar 1, 5:24 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Aatu Koskensilta <aatu.koskensi...(a)uta.fi> writes:
> > Here by "ordinary mathematical proof" is meant a piece of mathematical
> > reasoning (in mathematical English) from basic mathematical principles
> > -- the principle of mathematical induction, basic properties of
> > addition and multiplication, ... -- establishing some conclusion.
>
> I seem to have quite unnecessarily introduced an element of
> idealisation. Allow me to rectify: an ordinary mathematical proof is a
> piece of mathematical reasoning (expressed in natural language augmented
> with mathematical notation and jargon) establishing the truth of some
> mathematical statement by indicating in a way appropriate for the
> intended audience how the conclusion follows from axioms or previously
> proven mathematical results. About axioms Shoenfield has this to say:
>
>  For what reason do we accept the axioms? We might try to use
>  observation here; but this is not very practical and hardly in the
>  spirit of mathematics. We therefore attempt to select as axioms certain
>  laws which we feel are evident from the nature of the concepts
>  involved.

Does not seem like he has much to say. "evident from the nature of the
concepts involved" seems like a contradiction in terms. He is
asserting both that matehematics is synthetic a priori and analytic.
He does not bother to say explicitly which one it is.

If you take the position that mathematics is analytic i.e. the axioms
are implicit definitions then you realize how hollow the manifet truth
theory is. Are definitions true? You do not have to believe that
mathematics is analytic but if you take the manifest truth position
then you have to refute that mathematics is analytic. Torkel Franzen
did not bother to say which one was it either.

Let us suppose that mathematics is synthetics a priori (which it is
not) and we somehow comprehend the truths. If this is so why do we
need any derivation system at all?



>
> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, dar ber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

From: Newberry on
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?
>
> --
> Daryl McCullough
> Ithaca, NY

From: Newberry on
On Mar 1, 2:27 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
> Newberry says...
>
> >The way you put it, it sounds like my primary objective is to make a
> >distinction between the two sentences above for some strange reason.
> >Actually the distinction is a consequence of outlawing
> >     (x)((2 > x > 4) -> ~(x < x + 1))
> >and solving the Liar paradox.
>
> Disallowing this statement or that statement is not *solving* the
> liar paradox.

Outlawing
~(Ex)(Ey)(P'xy & Q'y) (1)
does solve the paradox.

> It's creating a system in which it cannot be expressed.

You mean cannot be derived?

> But that's *already* the case in the language of arithmetic. So I
> don't understand the point of your proposed restriction.

Let me explain the point.
a) the sentences that cannot be derived are neither true nor false
b) the derivation of
~(Ex)P'xm'
does not result in a contradiction. [m' is the Goedel number of (1).



>
> --
> Daryl McCullough
> Ithaca, NY