Re: What is a proof, exactly?
From: Jasper Stein (J.J.Stein.Stein_at_cs.cs.ru.ru.nl.nl)
Date: 12/03/04
- Next message: Rod: "semi-infinite number"
- Previous message: José Carlos Santos: "Re: need proof!!!"
- In reply to: Ryan Reich: "Re: What is a proof, exactly?"
- Next in thread: Han de Bruijn: "Re: What is a proof, exactly?"
- Reply: Han de Bruijn: "Re: What is a proof, exactly?"
- Reply: Jesse F. Hughes: "Re: What is a proof, exactly?"
- Messages sorted by: [ date ] [ thread ]
Date: Fri, 03 Dec 2004 10:53:25 +0000
Ryan Reich wrote:
>> - What is the status of "=" (equality) with respect to proofs? Is there
>> a
>> difference between "meaning of" and "definition of"? Is "=" defined or
>> does it only have a (logical) meaning? Can we equate any two mathematical
>> objects?
>
> Well, first-order logic does give a preferential status to that symbol
> over the other relational symbols, in that it appears in the axioms and is
> not up for interpretation.
This, in combination with other posts reminds me of something. I was raised
on Dirk van Dalen's "Logic and Structure", where he states that there are
languages of 1st order logic where "=" doesn't appear, although AFAIR he
gives no examples.
But now discussion on set theory and specifically the axiom of
extensionality makes me wonder about the status of = in ZF. Extensionality
is (Ax Ay: x=y <=> (Az: zex <=> zey)). Does this define = in terms of e?
That is: what is the language of set theory, does it have 2 relations (e
and =) or 1 (only e)? In the latter case, is = a defined notion (by
extensionality) or is it a logical thing which is only used in this axiom
to axiomatize e? In that case, are the logical = and the relation symbol =
two different things?
(As to the question about your class' notion of "truth" - every model comes
with an interpretation of the various constant, function and relation
symbols of the language; a sentence of the language is true if it is true
in all models (according to their respective interpretations))
> logically from the axioms or deduction. There is another way to insert
> interpretations into logic, which is as a "model" of a set of logical
> statements, namely a set in which each logical symbol corresponds to a
> function or relation or element of the set, so that a logical sentence is
> translated into a composition of these things concatenated with logical
> connectives like -> or "for all", and this sentence is either true or
> false (or totally undecidable, of
> course)...but again, this judgement is made by a person. Mathematical
I don't quite get what you mean here. Could you expand, please?
>> - Once we defined X as above, we can make additional definitions Y, Z,
>> ...
>> depending on X. Can we also make definitions depending on Thm? On prf?
>> Can you comment on the definition of the reciprocal ($x \to
>> \frac{1}{x}$), which seems to depend not only on $x$ but also on a
>> 'theorem' stating that $x \neq 0$? Does it also depend on a proof of such
>> a theorem? How?
>
> In what way does the definition of X allow us to make additional
> definitions?
Well, this is common, isn't it? We define what a ring is, and then we can
prove that if there is a unit element (some definitions of ring don't
require one) for its muliplication, then it's unique. Then one can define
what a division ring (aka. skew field) is, and if we have that we can
define what a field is (namely a commutative division ring).
Similarly one can define x to be some real number and f a function on the
reals, and then define y := f(x), depending on f and x.
(By the way, do you consider these to be two different kinds of
definitions?)
> In the sense that the existence of X is a logical statement
> with logical consequences, this is perhaps true (of course, that's not a
> first-order
> concept). Another way to look at it is that Y and Z depend on certain
> logical non-axioms in addition to the axioms, and if X satisfies those
> axioms then, having convinced ourselves that X is our universe of the day,
> we will accept Y
> and Z as well. That is a first order statement, and it really just says
> that
> the any model of Y's axioms is also a model of X's.
I'm not sure I follow what you're saying here.What do you mean by "X is our
universe of the day"? I meant X to be just some mathematical object: a real
number, a graph, or a category perhaps. These are not universes in any way
I'm aware of...?
I also presume you mean to say that if the existence of object X requires
axioms A1...Ai then we also have to accept objects Y and Z if their
existence follows from these same A1...Ai?
> However, the actual nature of Prf is irrelevant, since its existence is
> the verification that Thm is provable, and conversely the provability of
> Thm is (by
> definition) the existence of Prf. And we can deal with Thm.
Okay. So if Prf exists on the same level as X and Thm, could we define a new
object Y:=f(prf)? Let's say Y:=1 if prf uses induction and Y:=0 otherwise?
[about the 4colour theorem:]
> wrote it all out then humans would have confidence that humans could
> reproduce the proof, and since as I've indicated that I belive, proofs are
> eventually based on human ideas about how to determine truth.
Okay, some systems already do that. They spew out a proof (encoded in a
lambda term) of what they think is true. But these proofs are on the level
of formal proofs: every reasoning step is minutely described, and so they
become very big very soon. Even writing out the proof of n+k=k+n requires
tens of lines - okay, it's a pretty-printed lambda term with lots of
whitespace, but still it's a lot. So if you don't trust computers by
themselves, and humans cannot check these proofs, what must we think of
them?
> If a tree falls in a forest, and no one witnesses it in any way, did it
> fall? I
> would say yes. But theorems aren't trees; if a logical statement is
> consistent with the axioms then (by the completeness theorem) there exists
^^^^^^^^^^
Okay, I saw your other post :-)
> a proof, and the
> production of that proof does not change its logical status. All it does
> is change our knowledge of it, and it's the part where we believe that the
> RH is true not because we'd like to, but because it has been shown to be
> the case by methods we also believe to be the perfect embodiment of our
> intuition, that is
> important to us. If aliens give us an incomprehensible proof it's no
> good; and if the four-color theorem's proof is incomprehensible, that's no
> good either.
> Even if it's true. Of course, if I understand it and you don't, I can
> feel free to use it (provided my understanding indicates it's true, of
> course), whereas you would warily agree that my manipulation of the
> logical symbols is correct, there is one spot in my proofs that needs
> further verification.
It is interesting to see that you appear to allow the human factor to play a
role. I wonder how wide-spread this belief is. Responses, anyone? I know
the official blurb that the human factor shouldn't play a role, but I don't
believe it, and neither do you, it seems.
I suppose that in some axiomatic systems there are theorems - well,
statements really - whose minimum-sized proof is too long to even write out
physically. What about these?
>> I suppose that's enough questions for the time being. Feel free to
>> include any pertinent thoughts and additional questions.
>
> Let the tearing down of my amateurish responses begin!
For amateurish responses I found them quite good...! Thanks!
Jasper
-- The problem with having an open mind is that people toss in garbage
- Next message: Rod: "semi-infinite number"
- Previous message: José Carlos Santos: "Re: need proof!!!"
- In reply to: Ryan Reich: "Re: What is a proof, exactly?"
- Next in thread: Han de Bruijn: "Re: What is a proof, exactly?"
- Reply: Han de Bruijn: "Re: What is a proof, exactly?"
- Reply: Jesse F. Hughes: "Re: What is a proof, exactly?"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
