'When Are Relations Neither True Nor False?
in [Math]
|
From: Newberry on 1 Mar 2010 00:10 On Feb 28, 5:59 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > >On Feb 26, 4:10=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> Unrestricted comprehension, which says if Phi(x) is a formula > >> with one free variable, then there is a set y such that forall > >> x, > > >> x is an element of y > >> <-> > >> Phi(x) > > >> This is clearly not true in the case Phi(x) is the formula > >> "x is an element of x". > > That should be "x is not an element of x". > > >Looks like you discovered that it was not manifestly true only AFTER > >you derived a contradiction. > > Well, the discovery happened long before I was born, so it's hard to > know whether I would have believed Frege's axiom to be "manifestly > true" had I been unaware of Russell's paradox. Is the axiom of restricted comprehension manifestly true? What if you derive counterintuitive consequences from these axioms that seemed manifestly true at first?
From: Nam Nguyen on 1 Mar 2010 01:00 Aatu Koskensilta wrote: > Nam Nguyen <namducnguyen(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). It's just there are posters who would directly or implicitly argue the opposite that Godel's proof is a FOL proof. 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)." > It is an ordinary > mathematical proof, presented originally in mathematical German. But in the name of precise mathematics, and mathematical reasoning, what would we mean by "ordinary mathematical proof"? For example, is the ordinary proof of "x<y \/ x=y \/ y<x" of length 1? or greater than 1? Or in the collection of "ordinary proofs" would one be able to find a proof for GC, or "there are infinitely many counter examples of GC"?. etc... > When > people say it's entirely syntactic they're not claiming it's a formal > proof -- we meet precious few formal proofs in mathematics, fortunately! 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!) > -- but rather that 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? > 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. 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."? ? 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. What about inconsistent formal systems, if all we really care is just a proof - any proof - for GIT?
From: Daryl McCullough on 1 Mar 2010 05:25 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. -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 1 Mar 2010 05:27 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. It's creating a system in which it cannot be expressed. But that's *already* the case in the language of arithmetic. So I don't understand the point of your proposed restriction. -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 1 Mar 2010 05:33
Nam Nguyen says... >Aatu Koskensilta wrote: >> Nam Nguyen <namducnguyen(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). That's not what Aatu said. He said that it isn't a *formal* proof. What that means is that it is not a sequence of statements such that each statement is either an axiom or follows from previous statements by rules of inference. >It's just there are posters who would directly or implicitly argue the >opposite that Godel's proof is a FOL proof. 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: And that's certainly true. Godel's theorem could be carried out in Z. -- Daryl McCullough Ithaca, NY |