From: Aatu Koskensilta on 1 Mar 2010 05:34 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 1 Mar 2010 08:24 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 1 Mar 2010 09:34 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 1 Mar 2010 09:35 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 1 Mar 2010 09:41
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 |