'When Are Relations Neither True Nor False? [Logic]

Prev: geometry precisely defining ellipsis and how infinity is in the midsection #427 Correcting Math
Next: Accounting for Governmental and Nonprofit Entities, 15th Edition Earl Wilson McGraw Hill Test bank is available at affordable prices. Email me at allsolutionmanuals11[at]gmail.com if you need to buy this. All emails will be answered ASAP.

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