Re: Creating a "toy" OO/AO language...
- From: "Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx>
- Date: Fri, 2 Nov 2007 10:17:29 +0100
On Thu, 01 Nov 2007 17:37:05 -0000, Mark Nicholls wrote:
On 1 Nov, 16:46, "Dmitry A. Kazakov" <mail...@xxxxxxxxxxxxxxxxx>
wrote:
On Thu, 01 Nov 2007 15:58:21 -0000, Mark Nicholls wrote:
given the axioms of R is it, or is it not possible to prove that for
all x,y there exists a number z s.t. x<z<y without having to
exhaustively list the examples?.....clearly.
I don't buy proofs of existence, as I said.
you don't buy the continuity of the real line? do you then reject
calculus?
No, I don't.
BTW, since when calculus became a proof of existence of a result? Don't we
all already know that sin(x) exists? (:-))
Any other proof will be
equivalent to listing examples. This or that way, you need *all* examples.
Either you get them through your belief in something *equivalent* (like
well-ordering, or induction, or whatever), or else you construct them.
(oracle vs. machine)
i.e. I don't need to enumberate the integers to know that if you give
me one, I can find one bigger....I'll just prove from the axioms of
the integers.
You didn't prove it, but rather ensured by a choice of an appropriate set
of axioms, like the axiom of induction.
you gave me the axioms by talking about sine.
No, that was the point. I asked you for the language we are speaking.
before that you asked for a specification for sine.
Yes, but the answer given was not in the target language, thus it was
illegal.
the language is the one usually associated with R, i.e. '+','-','\'
Right, but this language is not understood. No programming language may
have +:RxR->R as known in mathematical analysis. The whole point was that
neither of non-trivial real operations can be defined or specified beyond
triviality without a reference to infinity. You need a source of infinity
in your target language. If you have it, that would be equivalent to having
or enumerating R, because then that source could be used to do that thing.
The
language of mathematical analysis indeed defines sine. But the computer
speaks a different one. Further, you cannot accurately model mathematical
analysis in a computer.
you cannot create a model of mathematical anaysis, but you can create
a model that models proof theory, and then use the axioms of the
theory of analysis to prove things about mathematic analysis, it's not
especially new, proof checkers have existed for donkeys years.....I
need only show an implementation to be correct given the premises....I
do not then need to exhaustively test every example.
Yes, you can, but this system will be sufficiently weak, so that you will
need infinite inference chains, like one to prove that the last figure of
pi is 7. (:-))
I can prove things about R...but I am incapable of calculating
anything in R in general.....do I need write down pi, before I can use
it?
That depends on how do you want to use it. What about pi**pi? Note that the
number of real-valued functions is even larger than R itself. You gain
nothing by doing things symbolically, because whatever finite symbolism
you'd take that would not give you all R.
R is not 'defined' by it's values,
?? R *is* a set of its values. Period.
that is just a set.....no operators, no axioms.....it's useless....a
bag of meaningless labels.....you can do nothing with it.
1+1=?
its meaningless...'+' is not defined on just a set....this is not the
R I recognise as the one in mathematical analysis....I wished it
was...the books would be much shorter.
Clearly operations are defined on the values of R. In mathematics we cannot
have real values without operations. Whether you have defined + on a set
called R, or only can do it, even, if you don't know if you could, but
somebody else knows, or can show that you can ... etc ad infinitum, that
all is equivalent to existence of + on R.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.
- Follow-Ups:
- Re: Creating a "toy" OO/AO language...
- From: Mark Nicholls
- Re: Creating a "toy" OO/AO language...
- References:
- Re: Creating a "toy" OO/AO language...
- From: Mark Nicholls
- Re: Creating a "toy" OO/AO language...
- From: Dmitry A. Kazakov
- Re: Creating a "toy" OO/AO language...
- From: Mark Nicholls
- Re: Creating a "toy" OO/AO language...
- From: Dmitry A. Kazakov
- Re: Creating a "toy" OO/AO language...
- From: Mark Nicholls
- Re: Creating a "toy" OO/AO language...
- From: Dmitry A. Kazakov
- Re: Creating a "toy" OO/AO language...
- From: Mark Nicholls
- Re: Creating a "toy" OO/AO language...
- Prev by Date: Re: Creating a "toy" OO/AO language...
- Next by Date: Re: Creating a "toy" OO/AO language...
- Previous by thread: Re: Creating a "toy" OO/AO language...
- Next by thread: Re: Creating a "toy" OO/AO language...
- Index(es):
Relevant Pages
|
Loading