XPost: comp.theory, sci.math
From: tristan.wibberley+netnews2@alumni.manchester.ac.uk
On 05/01/2026 01:48, Jeff Barnett wrote:
> On 1/4/2026 3:50 PM, Richard Damon wrote:
>> On 1/4/26 5:13 PM, Jeff Barnett wrote:
>>> On 1/4/2026 11:55 AM, Mike Terry wrote:
>>>> On 02/01/2026 17:54, Richard Damon wrote:
>>>>> On 1/2/26 12:24 PM, Mike Terry wrote:
>>>>>> On 02/01/2026 15:25, Richard Damon wrote:
>>>>>>> On 1/2/26 1:14 AM, Tristan Wibberley wrote:
>>>>>>>> On 02/01/2026 04:45, Richard Damon wrote:
>>>
>>>>>> Similarly, the word "proof" can be informal (simply an argument
>>>>>> that convinces people of the truth of a statement), or refer to
>>>>>> the "proof calculus" of the formal system being discussed. Most
>>>>>> authors I've come across seem to use "proof" more or less
>>>>>> informally and for clarity choose another word for whatever
>>>>>> sequence of syntactic "proof steps" the formal system specifies.
>>>>>> Often "derivation" is used, and that seems intuitive to me, so I
>>>>>> try to always use that term here, and using "proof" for more
>>>>>> general mathematial arguments, e.g. proving that the G statement
>>>>>> is "true" using some meta-theory.
>>>>>
>>>>> The issue is that "derivation" doesn't actually imply a finiteness,
>>>>> which is a necessity of "proof".
>>>>
>>>> Where do you get that idea? Are you thinking "derivation" is just
>>>> an informal word? I'm using it in the technical sense previously
>>>> explained.
>>>>
>>>> Within a formal system there will be a set of rules which define
>>>> what a valid "derivation" looks like. These would ensure that such
>>>> derivations are finite. (I'm sure someone at some time has made a
>>>> special study of "infinite proofs", but that is off the beaten
>>>> track.) As explained in my previous post, I'm using "derivation" as
>>>> the technical term for whatever passes as a "formal proof conforming
>>>> to the requirements of the proof calculus of the system". This is
>>>> so that the idea does not get muddled with your more general kind of
>>>> proof = "convincing argument in some meta-theory".
>>>
>>> There are examples of the following situations that I remember from
>>> discussions with logicians circa. 60 years ago. Assume we have a
>>> simple axiomatic system that allows us to express some facts about
>>> what we believe to be natural numbers. Call the objects in a model of
>>> the system N and we wish to prove, in our little system, that for all
>>> n in N p(n). Now it turns out that for any n in N we can write a
>>> simple finite proof of p(n) but are (provably in a larger or meta
>>> system) not able to prove the universally quantified statement in the
>>> little system. Well actually .... if you wrote a proof, in the little
>>> system, for each n in N and joined them with and "&" operator you
>>> would prove the quantified statement albeit with an infinity proof.
>>> In a little larger system, perhaps with an induction axiom, or a meta
>>> system it might be trivial to prove the whole thing with a finite
>>> effort.
>>
>>
>> The issue how can you know or show that you can make such a proof for
>> all n within the system?
>
> Some of the facts in the above are knowable in more powerful systems and
> can only be appreciated from that viewpoint.
> > IF you can break the infinite number of n into a finite number of cases,
>> then you can built a finite proof based on those cases.
>
> If that were true in the examples I was shown, then none of the rest
> would follow and I wouldn't have posted what I did.
>
>> The problem is that the normal definition of "proof" requires it to be
>> finite, as proofs are supposed to SHOW to a person that the statement
>> is true, and we can't handle such an infinite series.
>
> That is simply not true. Period. If I recall correctly, the book
> "Zermelo's Axiom of Choice -- Its Origins, Development and Influence" by
> Gregory H. Moore, talks about infinite proofs in a few places. (My copy
> of the book is 40+ years ago and was unholy expensive. You can now get a
> paperback copy for $13.99 at US Amazon.con.) Where, other then in silly
> USENET, dose it say that all proofs in all formal systems must be
> finite? Serious question. Maybe this is a point that you and Peter can
> agree on, but don't implicate innocent bystanders.
Natural induction is finite, eg:
it's true for 0
if it's true for n then it's true for f(n).
Some, as Gödel's Axiom I.3, might have an axiom that takes the "it" of
the above induction and implies that forall n "it" is so of f(n).
Ah, but is that right? for every system? suppose we are able to do
inference under the quantifier and then get it back out.
I don't know the terminology here, f(n) might be said to be an object of
the system but not the infinite f(f(f(...))) yet forall quantification
could be used to make crazy deductions because of the self-reference it
/describes/ even though it doesn't /exemplify/ one.
I distrust Gödel's I.3 for that reason until I know more.
> Logicians qualified to discuss and develop theories of and using
> infinitary proofs do not have such problems. (I'm using the term
> "qualified logician" to distinguish an individual from myself and other
> want-a-bees participating in these idiotic discussions.)
They are not idiotic, they are the learning process. Even a book listing
correct facts is not good enough because being able to repeat facts that
you cannot understand enough to check is just a job for a computer - it
is programming, not learning.
You have used the term "qualified" essentially undefined. What's the
point of that? Mere politics? Isn't there enough of that here already?
The chief quality of a qualified logician is doubt. Anyone without doubt
is no logician. I disqualify anyone without doubt.
> there are at least 20 want-a-bees
They're conventionally called "learners", "pupils", "students" etc. I
know there is a popular movement for the derision of the attempt to
become educated but I prefer not to have it come to me.
I will agree some of us learners are trying to dominate the others by
pretending to be professors but sometimes learners had professors that
taught them wrong (even though that would still conventionally make them
qualified) including making it seem less of a challenge and a smaller
matter than it really is.
We're 2 generations dead from the last wave of confusion and discussion
among English-speaking academics for these foundational matters - expect
many people that have declarations of qualification that are wildly
[continued in next message]
--- SoupGate-DOS v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
