XPost: comp.theory, sci.math
From: news.dead.person.stones@darjeeling.plus.com
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.)
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.
--- SoupGate-DOS v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
