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

> I mean, if we don't actually know something isn't kind of prudent that
> we just say we don't know that something? (And I was blamed for being
> a crank?)

What we take to be known in mathematics is to some extent a matter of
opinion. In ordinary mathematics it's a triviality that PA is provably
consistent. Those who regard the principles and modes of reasoning taken
for granted in ordinary mathematics as dubious will of course have to
inspect the proof for themselves and make up their own mind.

--
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
Nam Nguyen <namducnguyen(a)shaw.ca> writes:

> Huh? You didn't say anything in that conversation and silently let him
> "represent" your views and if his "representing" goes wrong that would
> be my fault, no explanation needed?

I said nothing about anything being your fault.

--
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
Nam Nguyen <namducnguyen(a)shaw.ca> writes:

> Hopefully by now you'd understand why in the other thread I asked why
> in debates you've tended to:
>
>> think you're infallible and above the rigorousness of mathematical
>> reasoning?

No. Why do you think I think I'm infallible and "above the rigorousness
of mathematical reasoning"?

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Nam Nguyen on
David Libert wrote:
> Nam Nguyen (namducnguyen(a)shaw.ca) writes:
>> Aatu Koskensilta wrote:
>>> Nam Nguyen <namducnguyen(a)shaw.ca> writes:
>>>
>>>> MoeBlee wrote:
>>>>
>>>>> And, in that regard, I have said all along that there is no
>>>>> finitistic proof of the consistency of PA.
>>>> So you've agreed that there's no formal proof for PA's consistency and that
>>>> if you go by formal proof only then you don't have knowledge of PA's
>>>> consistency.
>>> There are many formal proofs of the consistency of PA. None of them are
>>> finitistic.
>> So it doesn't seem you used the phrase "formal proof" in the standard
>> way that textbook (e.g. Shoenfield's) would use. In that standard
>> usage, a formal proof is a (finite) syntactical proof of a FOL formal
>> system theorem.
>>
>> Given that standard definition of "formal proof", would you agree with
>> my statement above that:
>>
>> >> there's no formal proof for PA's consistency and that if you go by
>> >> formal proof only then you don't have knowledge of PA's consistency.
>>
>> ?
>
>
> This discussion seems to me to be reducing to what people often call
> (in common language, not the technical logical sense), semantics, ie
> definitions of words. Namely what do we mean by "know" or
> "really know" or "formal proof" .
>
> My edition of Shoenfield is copyright 1967. All page numbers I reference
> below are for that edition.
>
> On page 4 Shoenfield defines the theorems of a formal system, namely
> the usual involving axioms and rules and conclusion.
>
> Earlier on this same page 4 he defines a formal system as havin axioms and
> rules of inference. This simply says axioms, with no further specification.
>
> On page 22 Shoenfield writes:
>
> "We can now define the class of formal systems which we are going to study.
> A first-order theory, or simply a thoery, is a formal stysten T such that
>
> i) the language of T us a first order language;
>
> ii) the axioms of T are the logical axioms of L(T) and certain further axioms,
> called the nonlogical axioms;"
>
>
> There is a iii) I omot about rules of inference.
>
> An important part of logic is to be able to have applied theories.
>
> If all we ever did with logic was pure logic, all we could talk avout is =
> and substitution instances of propostional logic on other predicates.
>
> And indeed, Shoenfield like any other logic book spends a lot of time discussing
> applied theories.
>
> So Shoenfield talked about theorems for formal theories, and later he spelled
> out these formal theories include nonlogical axioms.
>
> And this is what I have always understood to be the standard definition,
> not just Shoenfield but every text and every course I have seen.
>
> A formal proof is a sequence of statements with the conclusion at the end,
> every statement following from previous statements by a rule of inference,
> or being an axiom, an axiom being a logical axiom or a nonlogical axiom.
>
> If you think that formal proofs must only be in pure logic, and all you are
> telling us is pure logic does not prove Con(PA), all of us I am sure have
> known that for years. I do know that I have.

I do appreciate what you've said in this paragraph. All I've been asking
others here is just a firm confirmation of such: we can't prove consistency
by the most rigorous regime of proof in FOL, namely rules of inference and
axioms. Once that is confirmed then I'd be able to expand my certain
exposition(s) further. But no one up to now has "formally" confirmed such matter
(and most of the time some of them actually went on the "attack" rather than
dwelling deep into analysis of the issue, iirc).

>
> For myself, and I think a reasonable reading of the pther people here,
> we never meant to be claiming that pure logic has a formal proof of Con(PA).

I believe I understood and understand that. The key thing though I think
they ignored (perhaps unintentionally, perhaps unintentionally) is that
my motivation has been examining the possible _incompatibilities_
between the most rigorous method (syntactical inference by the
rules) and the most "liberal" method, semantics interpretation.

If we can identify these incompatibilities of different methods of
reasoning then we'd know the strength and weaknesses of mathematical
reasoning which is to Shoenfield is method oriented. Then I think
we'd be in a better position to improve FOL reasoning in order
to cope with a) existing problems or b) the never ending demand
to use mathematics as a means to express sciences.

>
> Instead we regard Con(PA) as accepted by the normal canons of mathematics,
> and many of us, including me, feel that ZFC or ZF or whatever is one reasonable
> codification of that.

My aim isn't meant to persuade people to ignore such "feeling". FWIW,
I too am using ZFC many times to have some intuitions into some "pet projects"
of my own (such as formalizing some biological concepts). The point though
is I've been arguing for a formal codification of what is impossible to
know. Instead of presenting a clear cut reason why such "reverse" codification
be impossible, others somehow just ignored my invitation to sincerely give
such codification a fair and impartial consideration, to say the least.

>
> We say we consider that we know Con(PA) as a mathematical statement by the
> normal standards of mathematical knowledge, and this fact itself can be
> illuminated by ZF |- Con(PA).
>
> And ZF provability is by a first order applied system, as Shoenfield
> discusses. In fact on page 239 he evens begins a description of ZF.

I _tend_ to believe Q, PA, ZF(C) be consistent. But if Quinne himself
could be wrong about ML, then from the reasoning point of view there's always
such a dangling sword in the form of "F /\ ~F" that *potentially* could
still be there. I believe we have to balance between intuition and rigid
logic. If we discard the former it's difficult to do mathematics, if we
ignore the later, we could send spaceships off orbits, manufacture medication
with severe side effects, alter DNA sequences with unintended and unimaginable
consequences. So to speak, intuition and logic have to "dance" together, imho.

> So the technical work in logic defining what a proof is applies to this
> case. And so we do apply it. As is justified by Shoenfield's own words
> above. Anyway, if there is some problem with ZF being a formal system why
> does Shoenfield have a chapter on it?

We have to assume we know something to move on and I'm OK with that. And
it's not unusual for a textbook to gloss over or assume something, from what
limited reading I've had. But if we _borrow_ a knowledge then we have to
realize it's a borrowed knowledge. And I'd think the more impartial on what
we feel we be entitled to know vs what we're only endowed to know, the better
we can improve how we conduct mathematical reasoning.

>
> So you dispute our mathematical knowledge by saying know means really know,
> and relaly know means having a formal proof, and formal proof means over
> pure logic only with no nonlogical axioms.

I beg to disagree. Formal proofs apply to non-logical theorems as well.

>
> But you are just changing our claims to something we never meant.

Again, I'd disagree here. What I think others have overlooked is FOL reasoning
actually condones more that one way to "prove" knowledge: a rigorous way and an
intuitional way. And what I've been saying that we should view the situation
in a high level bird-eye view so that we know what-is-what, so to speak. And
I think it's meant to be that way, the way the late President Reagan said in
"Trust but Verify": we trust our intuition but if necessary we'll verify that
with the rigorousness proofs through rules of inference. If for whatever the
reason we couldn't the verification then the trusted is always an un-verified
hence a guarded trust only. Naturally.

***

And that's just my high-level of the situation. In details I do have a few
technical reasons that would reveal unsettling reasons why the compatibility
between intuition and rigor of syntactical proof is very much questionable.
But due to the time constraint, let me defer presenting the reasons in the next
post(s).


--
----------------------------------------------------
There is no remainder in the mathematics of infinity.

NYOGEN SENZAKI
----------------------------------------------------