From: Nam Nguyen on
Jesse F. Hughes wrote:
> Transfer Principle <lwalke3(a)lausd.net> writes:
>
>> If Aatu can say that PA is consistent, _period_, without any formal
>> proof whatsoever, then why can't Nguyen believe that PA is
>> inconsistent, _period_, without formal proof?
>
> Aatu said PA is consistent, _period_, without any formal proof?
>

I think that's how MoeBlee expressed what he believed as Aatu's views
on the issue. Though not word for word, I believe Aatu's views are
close to how MoeBlee described them.
From: Nam Nguyen on
Aatu Koskensilta wrote:
> "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes:
>
>> Aatu said PA is consistent, _period_, without any formal proof?
>
> There seems to be some confusion over my (perfectly standard as always)
> take on these matters. Allow me to clarify. I know that PA is consistent
> because I know how to produce a mathematical argument for that fact
> which I fully understand -- in the sense that I grasp the key idea and
> can explain all the technical details that go into its execution -- and
> find compelling. The proof I have in mind has the following structure:
>
> 1. We give an inductive definition of a property T(x) of arithmetical
> sentences.

So, would T(x) be a formula in L(PA)?

>
> 2. We show that T("P") iff not T("~P"), that T("P & Q") iff T("P") and
> T("Q"), and so on.
>
> 3. We conclude from this that T does not hold of any
> contradiction.
>
> 4. We show that T holds of all the axioms of PA.
>
> 5. We show that the rules of inference of first-order logic preserve
> T.
>
> 6. We conclude that no contradiction is formally derivable in PA.
>
> We can of course formalize this proof in any number of theories -- ACA,
> ZFC, ... -- but this is just an incidental technical observation of no
> immediate interest as far as consistency of PA is concerned. We may also
> be interested in knowing exactly which set theoretic axioms are needed
> e.g. to justify the sort of inductive definitions involved, and so
> on. Again, this has no immediate connection to the question of
> consistency of PA.
>
> As with any proof in ordinary mathematics we take in the above proof
> many mathematical principles and modes of reasoning for granted. For
> example, we apply induction to a property involving a predicate defined
> by means of an infinitary inductive definition. Everyone must decide for
> themselves whether they find such invocations evident, compelling,
> legitimate mathematics. It's a brute fact of life that in ordinary
> mathematics we do in fact take them for granted.
>
> In Usenet debates, and elsewhere too, people like to make much of and
> pontificate tediously on who has or does not have the "burden of
> proof". In reality, such "logical" rules of formal debate have about as
> much to do with real arguments, persuasion, conversion, as the rules of
> cricket. Whoever wants to convince someone else of something must of
> course present arguments, questions, reflections, examples,
> illustrations that have some real force to the receiving person,
> regardless of whether they make a "positive claim" according to some
> rulebook of debating. I don't have any real interest in convincing
> anyone who does not take ordinary mathematics for granted of much
> anything. I'm content with simply noting that the consistency of PA is a
> triviality given what we in fact usually take for granted in
> mathematics. If someone tells me they find the usual modes of reasoning
> horribly dubious or unclear, even after careful explanation and
> meticulous elucidation, I simply shrug and move on.
>
From: Nam Nguyen on
Aatu Koskensilta wrote:
> "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes:
>
>> Aatu said PA is consistent, _period_, without any formal proof?
>
> There seems to be some confusion over my (perfectly standard as always)
> take on these matters. Allow me to clarify. I know that PA is consistent
> because I know how to produce a mathematical argument for that fact
> which I fully understand -- in the sense that I grasp the key idea and
> can explain all the technical details that go into its execution -- and
> find compelling. The proof I have in mind has the following structure:
>
> 1. We give an inductive definition of a property T(x) of arithmetical
> sentences.
>
> 2. We show that T("P") iff not T("~P"), that T("P & Q") iff T("P") and
> T("Q"), and so on.
>
> 3. We conclude from this that T does not hold of any
> contradiction.
>
> 4. We show that T holds of all the axioms of PA.
>
> 5. We show that the rules of inference of first-order logic preserve
> T.
>
> 6. We conclude that no contradiction is formally derivable in PA.
>
> We can of course formalize this proof in any number of theories -- ACA,
> ZFC, ... -- but this is just an incidental technical observation of no
> immediate interest as far as consistency of PA is concerned. We may also
> be interested in knowing exactly which set theoretic axioms are needed
> e.g. to justify the sort of inductive definitions involved, and so
> on. Again, this has no immediate connection to the question of
> consistency of PA.
>
> As with any proof in ordinary mathematics we take in the above proof
> many mathematical principles and modes of reasoning for granted. For
> example, we apply induction to a property involving a predicate defined
> by means of an infinitary inductive definition. Everyone must decide for
> themselves whether they find such invocations evident, compelling,
> legitimate mathematics. It's a brute fact of life that in ordinary
> mathematics we do in fact take them for granted.

Given this "modes of reasoning" is based on a "take ... for granted"
basis, would you care to give some reflections on the (possible)
weaknesses of the basis?

>
> In Usenet debates, and elsewhere too, people like to make much of and
> pontificate tediously on who has or does not have the "burden of
> proof". In reality, such "logical" rules of formal debate have about as
> much to do with real arguments, persuasion, conversion, as the rules of
> cricket. Whoever wants to convince someone else of something must of
> course present arguments, questions, reflections, examples,
> illustrations that have some real force to the receiving person,
> regardless of whether they make a "positive claim" according to some
> rulebook of debating. I don't have any real interest in convincing
> anyone who does not take ordinary mathematics for granted of much
> anything. I'm content with simply noting that the consistency of PA is a
> triviality given what we in fact usually take for granted in
> mathematics. If someone tells me they find the usual modes of reasoning
> horribly dubious or unclear, even after careful explanation and
> meticulous elucidation, I simply shrug and move on.

Given that FOL formal system definition permits a system with infinitely
many non-logical symbols, and which is outside the scope of say GIT, are you
saying you'd "simply shrug and move on" when, e.g., people ask you to defend
or criticize the possible (in)completeness of such system? Why restrict the
scope of FOL analysis/discussion to only _individual_ preferences, while FOL
understanding is supposed to be general and universal?
From: Nam Nguyen on
Aatu Koskensilta wrote:

>
> In Usenet debates, and elsewhere too, people like to make much of and
> pontificate tediously on who has or does not have the "burden of
> proof". In reality, such "logical" rules of formal debate have about as
> much to do with real arguments, persuasion, conversion, as the rules of
> cricket. Whoever wants to convince someone else of something must of
> course present arguments, questions, reflections, examples,
> illustrations that have some real force to the receiving person,
> regardless of whether they make a "positive claim" according to some
> rulebook of debating.

But in real life debate or argument , say in a court, people don't
talk about the name "Godel", inaccessible cardinalities, LST, finfinitely
many non-logical symbols, to say a few.

We do!
From: Nam Nguyen on
Nam Nguyen wrote:
> Aatu Koskensilta wrote:
>
>>
>> In Usenet debates, and elsewhere too, people like to make much of and
>> pontificate tediously on who has or does not have the "burden of
>> proof". In reality, such "logical" rules of formal debate have about as
>> much to do with real arguments, persuasion, conversion, as the rules of
>> cricket. Whoever wants to convince someone else of something must of
>> course present arguments, questions, reflections, examples,
>> illustrations that have some real force to the receiving person,
>> regardless of whether they make a "positive claim" according to some
>> rulebook of debating.
>
> But in real life debate or argument , say in a court, people don't
> talk about the name "Godel", inaccessible cardinalities, LST, finfinitely
> many non-logical symbols, to say a few.
>
> We do!

Honestly, my intention here isn't to argue about the ordinary mathematics we,
I included, do virtually all the times.

The issue is when I tried:

- to understand the difficulty of the arithmetical truth values of formulas
such as GC, cGC, ...

- to formalize SR, AI

I could NOT escape certain _hard_ questions about the very reasoning processes
and methods of reasoning we've taken for granted. And I don't think that's
just one person's issue.

If you don't see any value in the above statement, just to turn the table
around and try to _formalize_ a formal system in which statements about,
say, SR would hold and you'd see the exact steps, exact difficulties one
has to go through.

Mathematics is universal in many respects, but one of which is that if there
are problems _everyone_ can repeat the steps that would lead to the problems!

There's no sense to try escaping them and not to confront them, in order
to attempt making mathematics better. FWIW.