XPost: comp.theory, sci.math
From: polcott333@gmail.com
On 1/5/2026 11:04 AM, Mike Terry wrote:
> On 04/01/2026 22:13, 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.
>
> Yes, that can happen. It's known as ω-incompleteness. That's where we
> have
> ⊢ p(1)
> ⊢ p(2)
> ⊢ p(3)
> ...
> but not
> ⊢ ∀n p(n)
>
> There is a related phenomenon which is much more severe, which we have
> ⊢ p(1)
> ⊢ p(2)
> ⊢ p(3)
> ...
> and additionally
> ⊢ ¬∀n p(n)
>
> This is called ω-inconsistency. (Any inconsistent theory will also be
> ω-inconsistent, but it's possible for a consistent theory to be ω-
> inconsistent, so they are not equivalent concepts.)
>
∀n ∈ ℕ (n < 4 → p(n))
>
>
> So ω-incompleteness is saying our theory lacks some Theorems we would
> like [regarding universal quantification for certain properties p],
> while ω-inconsistency is much worse, actually saying that some n exists
> such that ¬p(n) holds, despite p(1), p(2),... all holding. [Clearly
> such an n can't be a (standard) natural number.]
>
> I'm not really up on all this, but seem to (randomly!) recall:
> 1. ω-incompleteness is fairly common (not too worrying)
> 2. Godel's proof of GIT needed the assumption that his base system P was
> /ω-consistent/, which is a stronger condition than just consistency.
> 3. A few years after GIT was published, someone published an improved
> proof,
> along the same lines but "tweaked" so it required only that P is /
> consistent/,
> rather than ω-consistent. (So nowadays when people discuss GIT
> they typically
> don't even mention ω-consistency.)
>
>
> > 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.
>
> Not sure if you're joining the proofs or the statements p(n) with an &
> operator. Well, you can't join proofs with '&', so you must mean
> allowing infinitely long sentences like
>
> p(0) & p(1) & p(2) &...
>
> Or you could concatenating the proofs to make an infinitely long proof,
> or both, I get where you're going.
>
> Yeah, those sorts of ideas have all been studied, but it's not as simple
> as you make out.
>
> OK, so we string together an infinite number of proofs for p(1), p(2),
> p(3)... and/or we have an infinitely long conjunction as above, but how
> would that (of itself) actually prove ∀n p(n) ?
>
> Just from what's been said, it /wouldn't/, because we can build models
> where all your infinitary stuff above happens, AND ∀n p(n) is actually
> still false, and we wouldn't want to be proving false statements.
> We're missing something /in our logical calculus/ that encapsulates the
> idea that our domain is /only/ n=0,1,2,3... (i.e. the natural numbers)
> So to actually prove ∀n p(n), as well as /allowing/ infinitary proofs in
> some fashion, we'd also need to add /further/ infinitary logical
> deduction rules somehow reflecting that our base domain is /only/ N.
> (Just /saying/ "N is our preferred model" doesn't change things.)
>
>
> > 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.
>
> Yes that's common. For example there are common systems where for all
> (natural numbers) m,n we can prove
>
> ⊢ + = +
>
> typically using induction over m,n (in the meta-system). [ means the
> numeral for n in our system, i.e. <3> is typically SSS0, and so on].
> However it can fail to be the case for our sytem that
>
> ⊢ ∀m∀n m + n = n + m
>
> Mike.
>
--
Copyright 2026 Olcott
My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable.
This required establishing a new foundation
--- SoupGate-DOS v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
