Provability
Victor Porton
more specific for P=NP problem)...
... how we can (or cannot) be sure that the hypotheses or its negation
is provable.
There are statements which are unprovable nor true nor false in ZFC.
For a specific example can we be sure that either P=NP or P!=NP is
provable?
--
Victor Porton - http://www.mathematics21.org
Robert Israel
> For famous hypothesis such as Millennium Prize problems (or to be yet
> more specific for P=NP problem)...
>
> ... how we can (or cannot) be sure that the hypotheses or its negation
> is provable.
We can't. In some cases we can do half of this: e.g. if the Riemann
hypothesis or Goldbach's conjecture happens to be false, then its
negation is provable. But if it is true, there is no guarantee that
there is a proof of that.
> There are statements which are unprovable nor true nor false in ZFC.
>
> For a specific example can we be sure that either P=NP or P!=NP is
> provable?
No. This is even worse than the Riemann hypothesis in that regard:
thus if P=NP there is a polynomial-time algorithm for solving an NP-complete
problem, but there might not be a proof that this algorithm works.
--
Robert Israel isr...@math.MyUniversitysInitials.ca
Department of Mathematics http://www.math.ubc.ca/~israel
University of British Columbia Vancouver, BC, Canada
Michael Press
<rbisrael.20071023142716$7f...@news.ks.uiuc.edu>,
Robert Israel <isr...@math.MyUniversitysInitials.ca>
wrote:
> Victor Porton <por...@narod.ru> writes:
>
> > For famous hypothesis such as Millennium Prize problems (or to be yet
> > more specific for P=NP problem)...
> >
> > ... how we can (or cannot) be sure that the hypotheses or its negation
> > is provable.
>
> We can't. In some cases we can do half of this: e.g. if the Riemann
> hypothesis or Goldbach's conjecture happens to be false, then its
> negation is provable. But if it is true, there is no guarantee that
> there is a proof of that.
>
> > There are statements which are unprovable nor true nor false in ZFC.
> >
> > For a specific example can we be sure that either P=NP or P!=NP is
> > provable?
>
> No. This is even worse than the Riemann hypothesis in that regard:
> thus if P=NP there is a polynomial-time algorithm for solving an NP-complete
> problem, but there might not be a proof that this algorithm works.
The notion of algorithm shares an important characteristic
with the notion of theorem. A computational method is not
an algorithm until we have accepted a proof of its efficacy.
--
Michael Press
David C. Ullrich
wrote:
Not according to the definition of "algorithm" I know.
Both of the following routines are algorithms. One of them
is an algorithm which gives the right answer to the
question "Is RH true?":
def SayYes:
return "yes"
def SayNo:
return "no"
I don't know which one gives the right answer, but
that doesn't change the fact that they are both
algorithms and one of them works.
************************
David C. Ullrich
Michael Press
<ibiuh39cpcljngark...@4ax.com>,
Neither of those procedures and associated assertions is
an algorithm, because you have not offered an accepted
proof.
An algorithm is a procedure that takes input and
terminates with a well-defined and asserted result.
That it does terminate with the asserted result must be
proven. Until we accept the proof, it is not an
algorithm. The notion of right answer is not part of
the definition of algorithm.
This is an algorithm that returns "yes".
procedure say_no
return "yes"
end procedure
Proof:
The procedure returns "yes" because the statement
`return "yes"' is the first executed statement and
therefore always executes.
QED
--
Michael Press
Marshall
>
> An algorithm is a procedure that takes input and
> terminates with a well-defined and asserted result.
> That it does terminate with the asserted result must be
> proven. Until we accept the proof, it is not an
> algorithm. The notion of right answer is not part of
> the definition of algorithm.
That definition is extremely narrow, and does not correspond
to any usage of the term that I can recall in many years
of being a programmer.
I'm not even sure I'd buy in to the "well-defined" part.
Having a "probabilistic algorithm" doesn't sound like
a contradiction in terms. In fact, Googling it just
now it gets a lot of hits. Neither does "proven correct,
proven terminating algorithm" sound redundant.
Marshall
Michael Press
<1193251799....@e34g2000pro.googlegroups.com>,
Marshall <marshal...@gmail.com> wrote:
I fail to see the utility in defining an algorithm
to be no more than a partial recursive function.
A theorem is not a theorem until it is proven.
What is your standard for implementing a method
into production code?
--
Michael Press
Marshall
To be fair, there is a world of difference between
the standards of ordinary commercial software and
the standards of rigor for a mathematical proof.
In general, the former is driven by marketplace
concerns, meaning whatever can be banged out
most quickly that works a majority of the time.
I think it was Scott McNealy that said that most
software has the shelf life of a banana. Whereas
math is for the ages.
I vaguely suppose that what is CS is called an
algorithm is more like what in math would be
called a formula.
Marshall
Robert Israel
Whether you see the utility or not is beside the point. The
fact is that standard terminology in mathematics and theoretical
computer science does consider a partial recursive function is to be "an
algorithm", and there is a difference between "algorithm A solves problem P"
and "we have a proof that algorithm A solves problem P". Similar
situations exist is most of classical mathematics: objects may have
certain properties even if there is no proof that they have those
properties.
Don Stockbauer
So the following has a "short shelf life?"
C Add A and B and print the answer
C = A + B
Print "A + B = " C
Don Stockbauer
<isr...@math.MyUniversitysInitials.ca> wrote:
> Michael Press <rub...@pacbell.net> writes:
> > In article
Remember that a proof is only valid within a system, and not all
systems are the general system.
Michael Press
<rbisrael.20071025044151$5f...@news.ks.uiuc.edu>,
Robert Israel <isr...@math.MyUniversitysInitials.ca>
wrote:
> Michael Press <rub...@pacbell.net> writes:
Few enough people think of an algorithm in the way I
do, A.A. Markov and Donald Knuth take an algorithm to
be more definite than a partial recursive function.
Knuth writes at length in ACP, 1.1. Here is a portion
quoted in Wikipedia.
1. Finiteness: "An algorithm must always terminate
after a finite number of steps ... a very finite
number, a reasonable number"
2. Definiteness: "Each step of an algorithm must be
precisely defined; the actions to be carried out must
be rigorously and unambiguously specified for each
case"
3. Input: "...quantities which are given to it
initially before the algorithm begins. These inputs are
taken from specified sets of objects"
4. Output: "...quantities which have a specified
relation to the inputs"
5. Effectiveness: "... all of the operations to be
performed in the algorithm must be sufficiently basic
that they can in principle be done exactly and in a
finite length of time by a man using paper and pencil"
Apparently, only I consider a proof to be part of an algorthm.
--
Michael Press
galathaea
i think the part of cs you refer
is the engineer's cs
the infrastructurists
who use it loosely
because such distinctions do not help their daily work
theoretical foundations of cs
often take the approach
as indicated michael
this is inherently a verificationist
or operationalist
approach to algorithmic properties
and mathematical properties in general
constructivists do not assign truth
until a sentence is proven
because of the curry-howard isomorphism
there is an isomorphism
between sentences and types
so this gives a type theory
this guarantees
functions definable in this type theory
are all computable
developing this as a foundation for computer science
has evolved considerably over the years
from rough BHK (brouwer-heyting-kolmogorov) types
to martin-lof types
to the more reflexive one's of artemov
constructivists in this tradition
do not derive ullrich's dichotomy
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar
galathaea
<isr...@math.MyUniversitysInitials.ca> wrote:
> Michael Press <rub...@pacbell.net> writes:
> > In article
although true in many other parts of math
that is not true in rigorous computer science
where properties are strongly operational
due to the inherent relation between syntax and semantics
(galois adjunction)
proof theory is also formulated
very often in this operational form
and generally
this is common when properties evolve in time
some theories of definition
have this built in
David C. Ullrich
wrote:
That's ridiculous.
>An algorithm is a procedure that takes input and
>terminates with a well-defined and asserted result.
>That it does terminate with the asserted result must be
>proven. Until we accept the proof, it is not an
>algorithm.
Ridiculous. You are confusing "is an algorithm"
with "has been proven to be an algorithm".
They're not the same thing. I claimed that those
two things were algorithms. They are. I didn't
claim to have given _proofs_ that they were
algorithms. (As though that was difficult...)
>The notion of right answer is not part of
>the definition of algorithm.
>
>This is an algorithm that returns "yes".
>procedure say_no
> return "yes"
>end procedure
>
>Proof:
> The procedure returns "yes" because the statement
> `return "yes"' is the first executed statement and
> therefore always executes.
>QED
************************
David C. Ullrich
David C. Ullrich
wrote:
>In article
><1193251799....@e34g2000pro.googlegroups.com>,
> Marshall <marshal...@gmail.com> wrote:
>
>> On Oct 24, 10:57 am, Michael Press <rub...@pacbell.net> wrote:
>> >
>> > An algorithm is a procedure that takes input and
>> > terminates with a well-defined and asserted result.
>> > That it does terminate with the asserted result must be
>> > proven. Until we accept the proof, it is not an
>> > algorithm. The notion of right answer is not part of
>> > the definition of algorithm.
>>
>> That definition is extremely narrow, and does not correspond
>> to any usage of the term that I can recall in many years
>> of being a programmer.
>>
>> I'm not even sure I'd buy in to the "well-defined" part.
>> Having a "probabilistic algorithm" doesn't sound like
>> a contradiction in terms. In fact, Googling it just
>> now it gets a lot of hits. Neither does "proven correct,
>> proven terminating algorithm" sound redundant.
>
>I fail to see the utility in defining an algorithm
>to be no more than a partial recursive function.
Nobody has claimed that you see the utility in that
definition. That _is_ the definition.
Do you really think that if you don't see the utility
in a certain definition it follows that it cannot
in fact be the definition of whatever? Is that a
special property of you in particular, or is it
true that a definition is not a definition unless
_everyone_ sees the utility in it?
>A theorem is not a theorem until it is proven.
>What is your standard for implementing a method
>into production code?
************************
David C. Ullrich
galathaea
> On Wed, 24 Oct 2007 20:58:57 -0700, Michael Press <rub...@pacbell.net>
> wrote:
>
>
>
> >In article
there is no _the_ definition
everyone has the right to definition
michael's happens to be one of the more useful definitions
which is why it is used quite commonly
> >A theorem is not a theorem until it is proven.
> >What is your standard for implementing a method
> >into production code?
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea
> On Wed, 24 Oct 2007 17:57:05 GMT, Michael Press <rub...@pacbell.net>
> wrote:
>
>
>
> >In article
> > David C. Ullrich <ullr...@math.okstate.edu> wrote:
>
> >> On Tue, 23 Oct 2007 23:01:05 GMT, Michael Press <rub...@pacbell.net>
> >> wrote:
>
> >> >In article
it is your approach that is considered ridiculous
by many a foundationalist
unverifiable truth assignments
have long been held suspect
by many schools of thought
stoic logicians challenged just such approaches
for an example of early objections
but the challenges are quite widespread
unverifiable properties cannot be assigned a useful meaning
MoeBlee
> Marshall <marshall.spi...@gmail.com> wrote:
> > On Oct 24, 10:57 am, Michael Press <rub...@pacbell.net> wrote:
>
> > > An algorithm is a procedure that takes input and
> > > terminates with a well-defined and asserted result.
> > > That it does terminate with the asserted result must be
> > > proven. Until we accept the proof, it is not an
> > > algorithm. The notion of right answer is not part of
> > > the definition of algorithm.
>
> > That definition is extremely narrow, and does not correspond
> > to any usage of the term that I can recall in many years
> > of being a programmer.
>
> > I'm not even sure I'd buy in to the "well-defined" part.
> > Having a "probabilistic algorithm" doesn't sound like
> > a contradiction in terms. In fact, Googling it just
> > now it gets a lot of hits. Neither does "proven correct,
> > proven terminating algorithm" sound redundant.
>
> I fail to see the utility in defining an algorithm
> to be no more than a partial recursive function.
Utility is a separate question.
> A theorem is not a theorem until it is proven.
A sentence S is a theorem of a set of sentences G iff there is a proof
of S from G.
But what does "until" mean in this context?
MoeBlee
galathaea
constructivists almost universally seat properties in time
i am sure you have seen BHK semantics
moe
do you understand why constructivists
reject ullrich's dichotomy?
MoeBlee
> On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
> > > A theorem is not a theorem until it is proven.
>
> > A sentence S is a theorem of a set of sentences G iff there is a proof
> > of S from G.
>
> > But what does "until" mean in this context?
>
> constructivists almost universally seat properties in time
I'm not expert on the subject, but I recognize that certain
constructivists have notions that might be thought of, more or less
loosely, as temporal. However, it seems to me that in intuitionistic
mathematics, this can be formalized without a literal temporal
component.
> i am sure you have seen BHK semantics
> moe
Yes. Personally though (and I don't hold this to be controlling of
anyone else's understanding or even necessarily a permanent notion of
my own), I tend to view the BHK as an informal motivation that is then
formalized by actual mathematical semantics.
> do you understand why constructivists
> reject ullrich's dichotomy?
Due to my own personal unfamiliarity with Ullrich's notation, I don't
opine on the example Ullrich gave. But more generally, are you saying
that there is a definitely articulated constructivst notion of
'algorithm' that includes that something is not an algorithm until
proven to be an algorithm? If so, would you recommend a book or
article that I can read about that?
MoeBlee
MoeBlee
> michael's happens to be one of the more useful definitions
> which is why it is used quite commonly
Where is it common to define 'algorithm' to include that something is
not an algorithm unless proven to have certain properties as opposed
to just stipulating that it has those properties?
I mean, ordinarily we take the defintion to be of the form:
X is an algorithm iff X has such and such properties.
But, if I understand you correctly, you're saying:
X is an algorithm iff it is proven that X has such and such
properties.
So where do I find this definition in the constructivist literature?
MoeBlee
MoeBlee
> constructivists do not assign truth
> until a sentence is proven
Whatever is to be said about that, I don't see it follows that a
DEFINITION needs to include a provability clause.
If I say "X is a spofalosh iff X is croomalakish", then, fair enough
if you want to say that "X is a spofalosh" is true depending on a
proof that X is croomalakish. But I don't see how that entails that I
have to make the definitition "X is a spofalosh iff it's been proven
that X is croomalakish", especially since doesn't that lead to an
infinite regress as the next step now is that "X is a spofalosh" is
true depending on a proof that there's a proof that X is croomalakish?
MoeBlee
LauLuna
By 'provable' you don't seem to mean 'provable within some formal
system' but 'provable by human reason'.
There is an issue about philosophy of mathematics involved here. From
a Platonistic point of view it's perfectly possible that some facts
concerning mathematical objects result unknowable for human reason,
since mathematical facts are objective facts and don't depend on the
power of human reason.
But the more constructivist our point of view is, the less sensible
the claim seems that there can be mathematical facts out of the
potential reach of human reason.
Regards
galathaea
> On Oct 25, 10:35 am, galathaea <galath...@gmail.com> wrote:
> > On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
>
> > > > A theorem is not a theorem until it is proven.
>
> > > A sentence S is a theorem of a set of sentences G iff there is a proof
> > > of S from G.
>
> > > But what does "until" mean in this context?
>
> > constructivists almost universally seat properties in time
>
> I'm not expert on the subject, but I recognize that certain
> constructivists have notions that might be thought of, more or less
> loosely, as temporal. However, it seems to me that in intuitionistic
> mathematics, this can be formalized without a literal temporal
> component.
anything that can be formalised
can be formalised in a completely meaningless game of symbols
constructivists
from before brouwer
have made the point that math is a physical process
and that any computation
calculation
application of rule sets in steps
exists temporally
and have argued that any description of mathematics
that is to have _meaning_
must likewise describe these temporal processes
brouwer made much of math being a mental phenomenon
and used kantian arguments to connect this process with time
later constructivists
have allowed mathematics any computational existence
abstracted from the mind
and have used the temporality of computation
to make the connection more operational
kripke models
the most common semantic setting for heyting algebras
are inherently temporal
for the same reason the semantic interpretation of "possibility"
is inherently temporal
> > i am sure you have seen BHK semantics
> > moe
>
> Yes. Personally though (and I don't hold this to be controlling of
> anyone else's understanding or even necessarily a permanent notion of
> my own), I tend to view the BHK as an informal motivation that is then
> formalized by actual mathematical semantics.
that has been a common description over the years
but it is much less true since the work of martin-lof and artemov
there are obstructions that make it impossible
for a full valuation to be treated in BHK
so it has been often assumed the semantics could only be informal
but that is an error in mistaken existentials
it is sufficient for semantics
that a skolemised realisation exist
this was the importance of artemov's theory
in completing the formalisation of BHK
> > do you understand why constructivists
> > reject ullrich's dichotomy?
>
> Due to my own personal unfamiliarity with Ullrich's notation, I don't
> opine on the example Ullrich gave. But more generally, are you saying
> that there is a definitely articulated constructivst notion of
> 'algorithm' that includes that something is not an algorithm until
> proven to be an algorithm? If so, would you recommend a book or
> article that I can read about that?
i am unfamiliar with a specific singling out of "algorithm"
since constructivists tend to have strongly operational views
on all properties
for a good summary paper
that stresses in multiple places
the verificationist programme michael press has mentioned
see
http://www.cs.gc.cuny.edu/%7Esartemov/publications/RusMatSurveys.ps
almost any book on constructivism
though
will point out that constructivists do not accept
forAll sentences A
either A or not-A must be true
required by ullrich's construct
tertium datur
most references on constructivism will explain why this position is
taken
often
they will even use an example
old books sometimes used fermat's conjecture
many now use goldbach
there is a reason these examples are almost universally of this form
and why they will by nature change over the years
it has everything to do with time
galathaea
making statements and evaluating statements are two different
activities
and i am being rigorous in this statement
ie. "evaluating" means the models theoretic assignment of truth
valuations
at some level
there is an actual activity occurring
instead of a formal statement of acceptable actions that may occur
there is just action occurring
just because one can analyse analyses and analyse those analyses
furthur
does not mean one is actually doing that at any time
there is a potential infinite regression
just as there is always with metamathematical analyses
but it is not usually the case that there is such an infinite
analysis
the normatives don't regress
they exist only at the level of physical action
in other words
i am not talking syntax and definitions here
i am talking semantics
if syntax is what you object to
perhaps you may have disagreement with michael
but that was not how i interpreted the statements made
galathaea
i meant to point out chapter 4
"the semantics of judgement forms"
in the book here
www.cs.chalmers.se/Cs/Research/Logic/book/book.pdf
on martin-lof type theory
which also goes into this in a little detail
Robert Israel
It seems to me that it should be the other way 'round: it's harder to prove
something constructively than to prove it classically. Unless you're
redefining "mathematical fact" as "something that can be proven".
MoeBlee
> On Oct 25, 11:38 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > On Oct 25, 10:35 am, galathaea <galath...@gmail.com> wrote:
> > > On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
>
> > > > > A theorem is not a theorem until it is proven.
>
> > > > A sentence S is a theorem of a set of sentences G iff there is a proof
> > > > of S from G.
>
> > > > But what does "until" mean in this context?
>
> > > constructivists almost universally seat properties in time
>
> > I'm not expert on the subject, but I recognize that certain
> > constructivists have notions that might be thought of, more or less
> > loosely, as temporal. However, it seems to me that in intuitionistic
> > mathematics, this can be formalized without a literal temporal
> > component.
I'm writing this response primarily in the interest of not allowing it
to seem as if my questions have been addressed by your post that seems
to take my points as much more naive than they are, as, at this point,
I'm not hopeful that much worth can came from our exchanges now.
> anything that can be formalised
> can be formalised in a completely meaningless game of symbols
My point was that while I understand that one might describe the
temporal notion as part of the intutive motivation, one can work in
the formalized mathematics without then using anything about time
itself. In particular, it's still not been shown that a notion of time
is required to define 'theorem'. Indeed, for example, I don't see a
notion of 'time' mentioned in the definition of 'proof in the
intuitionisitic predicate calculus'. What I do see is a perfectly
explicit mathematical definition.
> constructivists
> from before brouwer
> have made the point that math is a physical process
> and that any computation
> calculation
> application of rule sets in steps
> exists temporally
> and have argued that any description of mathematics
> that is to have _meaning_
> must likewise describe these temporal processes
>
> brouwer made much of math being a mental phenomenon
> and used kantian arguments to connect this process with time
>
> later constructivists
> have allowed mathematics any computational existence
> abstracted from the mind
> and have used the temporality of computation
> to make the connection more operational
Whatever may be the case about that, you haven't answered my request
to be directed to a specific definition of 'algorithm' that mentions
not only the ordinary attributes of algorithms but also that it is
provable that a thing has those attributes. Your just mentioning
various constructivist theses and notions does not answer the
question.
> kripke models
> the most common semantic setting for heyting algebras
> are inherently temporal
> for the same reason the semantic interpretation of "possibility"
> is inherently temporal
Whatever "inherently" means here, the point I was getting at is that
one can take Kripke models to be perfectly exact formal mathematical
objects and that to work with them one would do well to appreciate the
intuitive motivation (which I can understand being described as
'temporal') but in the actual mathematics one does not need to invoke
any principles regarding time whatsoever.
And again, whatever the case about this, we've still not seen here a
reference to such definitions of 'theorem' that mention time.
> > > i am sure you have seen BHK semantics
> > > moe
>
> > Yes. Personally though (and I don't hold this to be controlling of
> > anyone else's understanding or even necessarily a permanent notion of
> > my own), I tend to view the BHK as an informal motivation that is then
> > formalized by actual mathematical semantics.
>
> that has been a common description over the years
> but it is much less true since the work of martin-lof and artemov
I admit that eventually I need to inform myself of such work, so I
can't comment now. Still, my comment was stated to be personal. As I
understand, the BHK notion is formalized by, for example, certain
methods of models that are perfectly mathematical.
> there are obstructions that make it impossible
> for a full valuation to be treated in BHK
> so it has been often assumed the semantics could only be informal
> but that is an error in mistaken existentials
I don't know what you mean by "mistaken existentials", but it was my
own point that, as far as I understand, BHK need NOT be merely
informal.
> it is sufficient for semantics
> that a skolemised realisation exist
>
> this was the importance of artemov's theory
> in completing the formalisation of BHK
>
> > > do you understand why constructivists
> > > reject ullrich's dichotomy?
>
> > Due to my own personal unfamiliarity with Ullrich's notation, I don't
> > opine on the example Ullrich gave. But more generally, are you saying
> > that there is a definitely articulated constructivst notion of
> > 'algorithm' that includes that something is not an algorithm until
> > proven to be an algorithm? If so, would you recommend a book or
> > article that I can read about that?
>
> i am unfamiliar with a specific singling out of "algorithm"
> since constructivists tend to have strongly operational views
> on all properties
Then I really don't follow you. We were talking about definitions of
'algorithm'; then you raised the matter of constructivism; now you
demur to connect constructivism with a defintion of 'algorithm'.
> for a good summary paper
> that stresses in multiple places
> the verificationist programme michael press has mentioned
> see
>
> http://www.cs.gc.cuny.edu/%7Esartemov/publications/RusMatSurveys.ps
Thanks for that link. I'll read it. It looks like something I can
learn from.
> almost any book on constructivism
> though
> will point out that constructivists do not accept
>
> forAll sentences A
> either A or not-A must be true
> required by ullrich's construct
>
> tertium datur
>
> most references on constructivism will explain why this position is
> taken
>
> often
> they will even use an example
>
> old books sometimes used fermat's conjecture
> many now use goldbach
>
> there is a reason these examples are almost universally of this form
> and why they will by nature change over the years
Look, constructivst views of the law of excluded middle are not at
issue with me. I'm very familiar with that. And, Ullrich's example is
not at issue with me, as I already mentioned that I'm not commenting
upon it specifically. What I did say is that I'd like to see where
such definitions of 'theorem' and 'algorithm' appear. Your reiterating
that the law of excluded middle is not accepted in most (all?)
constructivism does not answer the question as to where one might find
such definitions of 'algrorithm' and 'theorem'.
> it has everything to do with time
MoeBlee
MoeBlee
Whatever may be about that, I don't see that it shows how it is
entailed that a definition ITSELF of 'algorithm' must include in its
definiens that it is provable that a thing has the required properties
that are mentioned in the rest of the definiens.
> there is a potential infinite regression
> just as there is always with metamathematical analyses
> but it is not usually the case that there is such an infinite
> analysis
Not just potential. I don't see how you can avoid it, just as I
illustrated.
> the normatives don't regress
> they exist only at the level of physical action
>
> in other words
> i am not talking syntax and definitions here
What? Now I really don't follow you. The discussion was about
DEFINITIONS. My remarks were about DEFINITIONS.
> i am talking semantics
>
> if syntax is what you object to
> perhaps you may have disagreement with michael
> but that was not how i interpreted the statements made
What I said was plain, simple, and clear. I don't know why you are
confused about it.
MoeBlee
Michael Press
<aev0i3hj03i7tn8mr...@4ax.com>,
David C. Ullrich <ull...@math.okstate.edu> wrote:
No, it is _a_ definition. There is more than one
definition in play.
>
> Do you really think that if you don't see the utility
> in a certain definition it follows that it cannot
> in fact be the definition of whatever?
No, why do you ask?
> Is that a
> special property of you in particular, or is it
> true that a definition is not a definition unless
> _everyone_ sees the utility in it?
Rhetorical question?
--
Michael Press
Michael Press
<1193339665....@i13g2000prf.googlegroups.com>,
MoeBlee <jazz...@hotmail.com> wrote:
> On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
>
> > michael's happens to be one of the more useful definitions
> > which is why it is used quite commonly
>
> Where is it common to define 'algorithm' to include that something is
> not an algorithm unless proven to have certain properties as opposed
> to just stipulating that it has those properties?
Given a prime p, a natural number b,
and n a quadratic non-residue modulo p
there is a computation that purports
to find x such that xx = a (mod p).
You program the computation in a computer
and it does indeed provide a square root
modulo p each time it runs. Good enough for you?
> I mean, ordinarily we take the defintion to be of the form:
>
> X is an algorithm iff X has such and such properties.
>
> But, if I understand you correctly, you're saying:
>
> X is an algorithm iff it is proven that X has such and such
> properties.
>
> So where do I find this definition in the constructivist literature?
I do not know.
--
Michael Press
Michael Press
<1193332439.5...@v29g2000prd.googlegroups.com>
,
MoeBlee <jazz...@hotmail.com> wrote:
I was speaking loosely. A proof is part of a theorem.
--
Michael Press
Marshall
> On Oct 24, 11:28 pm, Marshall <marshall.spi...@gmail.com> wrote:
> >
> > I think it was Scott McNealy that said that most
> > software has the shelf life of a banana. Whereas
> > math is for the ages.
>
>
> C Add A and B and print the answer
>
> C = A + B
>
> Print "A + B = " C
What is that, BASIC? Didn't everyone stop using that, like,
decades ago?
Marshall
Michael Press
Michael Press
<1193333756.4...@v29g2000prd.googlegroups.com>
,
galathaea <gala...@gmail.com> wrote:
> On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
>
> > > A theorem is not a theorem until it is proven.
> >
> > A sentence S is a theorem of a set of sentences G iff there is a proof
> > of S from G.
> >
> > But what does "until" mean in this context?
>
> constructivists almost universally seat properties in time
I seem to think as constructivists do in this circumstance;
but I have not read the literature, nor do I think of myself
as holding a named position.
--
Michael Press
galathaea
> On Oct 25, 12:54 pm, galathaea <galath...@gmail.com> wrote:
> > On Oct 25, 11:38 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > On Oct 25, 10:35 am, galathaea <galath...@gmail.com> wrote:
> > > > On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > > > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
>
> > > > > > A theorem is not a theorem until it is proven.
>
> > > > > A sentence S is a theorem of a set of sentences G iff there is a proof
> > > > > of S from G.
>
> > > > > But what does "until" mean in this context?
>
> > > > constructivists almost universally seat properties in time
>
> > > I'm not expert on the subject, but I recognize that certain
> > > constructivists have notions that might be thought of, more or less
> > > loosely, as temporal. However, it seems to me that in intuitionistic
> > > mathematics, this can be formalized without a literal temporal
> > > component.
>
> I'm writing this response primarily in the interest of not allowing it
> to seem as if my questions have been addressed by your post that seems
> to take my points as much more naive than they are, as, at this point,
> I'm not hopeful that much worth can came from our exchanges now.
go fuck yourself
you sanctimonious ignorant piece of shit
i did nothing to you but try to answer your questions
you draw first blood
and then pretend a reactionary pose?
great way to back down from a position
and still try to save face...
> > anything that can be formalised
> > can be formalised in a completely meaningless game of symbols
>
> My point was that while I understand that one might describe the
> temporal notion as part of the intutive motivation, one can work in
> the formalized mathematics without then using anything about time
> itself. In particular, it's still not been shown that a notion of time
> is required to define 'theorem'. Indeed, for example, I don't see a
> notion of 'time' mentioned in the definition of 'proof in the
> intuitionisitic predicate calculus'. What I do see is a perfectly
> explicit mathematical definition.
yes
as i said:
anything that can be formalised
can be formalised in a completely meaningless game of symbols
you are apparently starting to show
a complete lack of understanding
of the distinction of semantics and syntax
do _you_ have a different theory of meaning?
i actually thought you knew these basic objects of model theory
seeing as you are often telling people (like zuhair)
to go read a textbook
why don't you?
> > constructivists
> > from before brouwer
> > have made the point that math is a physical process
> > and that any computation
> > calculation
> > application of rule sets in steps
> > exists temporally
> > and have argued that any description of mathematics
> > that is to have _meaning_
> > must likewise describe these temporal processes
>
> > brouwer made much of math being a mental phenomenon
> > and used kantian arguments to connect this process with time
>
> > later constructivists
> > have allowed mathematics any computational existence
> > abstracted from the mind
> > and have used the temporality of computation
> > to make the connection more operational
>
> Whatever may be the case about that, you haven't answered my request
> to be directed to a specific definition of 'algorithm' that mentions
> not only the ordinary attributes of algorithms but also that it is
> provable that a thing has those attributes. Your just mentioning
> various constructivist theses and notions does not answer the
> question.
i directed you to places that shows the origin
of _all_ statements given an operationalist evaluation
do you object to the more general framework?
seriously
your comment makes it sound like you have
no grasp of the concept of quantifiers
you say you want to see "theorem of X" used where it needs proof
(yet seem to not be aware that that is the bhk semantics)
you say you want to see "algorithm for Y" vary over time
(program verification languages often use
temporal specification logics like ltl and ctl)
this is a deep topic and requires much exposition
does that sound familiar?
> > kripke models
> > the most common semantic setting for heyting algebras
> > are inherently temporal
> > for the same reason the semantic interpretation of "possibility"
> > is inherently temporal
>
> Whatever "inherently" means here, the point I was getting at is that
> one can take Kripke models to be perfectly exact formal mathematical
> objects and that to work with them one would do well to appreciate the
> intuitive motivation (which I can understand being described as
> 'temporal') but in the actual mathematics one does not need to invoke
> any principles regarding time whatsoever.
and i showed i could not understand your point
by agreeing that all formalisation can be meaningless...??!
> And again, whatever the case about this, we've still not seen here a
> reference to such definitions of 'theorem' that mention time.
although this is pretty common throughout the field
so i'd have hoped you'd have "picked up a textbook" to get it
artemov writes in the paper i linked:
" Such a reading of modality naturally appears in dynamic and
temporal logics aimed at describing computational processes,
the states of which usually form a (possibly branching)
Kripke structure. "
so yes
"we" have seen here just such a reference
but i've mentioned bhk too...
really
moe
i have not seen such a lack of content in your posts before
(though i have seen belligerence)
so what gives?
you really have _never_ seen a semantics
that requires proof before a statement is considered true?
you've never seen the _reasons_ for tertium datur?
> > > > do you understand why constructivists
> > > > reject ullrich's dichotomy?
>
> > > Due to my own personal unfamiliarity with Ullrich's notation, I don't
> > > opine on the example Ullrich gave. But more generally, are you saying
> > > that there is a definitely articulated constructivst notion of
> > > 'algorithm' that includes that something is not an algorithm until
> > > proven to be an algorithm? If so, would you recommend a book or
> > > article that I can read about that?
>
> > i am unfamiliar with a specific singling out of "algorithm"
> > since constructivists tend to have strongly operational views
> > on all properties
>
> Then I really don't follow you. We were talking about definitions of
> 'algorithm'; then you raised the matter of constructivism; now you
> demur to connect constructivism with a defintion of 'algorithm'.
seriously
at this point i am starting to suspect
you are either much less capable than i had surmised from previous
posts
or something crawled up your ass
and you now can't stop yourself from arguing
i made the connection
when you ask:
how is 4 even?
and i reply:
all integers of the form 2x are even
it really is answering your question
no matter how hard you squint your eyes or shake your head
or whatever you are doing to skip over it
michael press gave an operational definition of algorithm
to call something an algorithm for a particular task
you must have a verification that the task gets accomplished
others thought it a strange way to treat algorithms
whereas to me it was quite natural
operationalism and constructivism are intimately related
so i brought up why it was natural
and common
> > for a good summary paper
> > that stresses in multiple places
> > the verificationist programme michael press has mentioned
> > see
>
> >http://www.cs.gc.cuny.edu/%7Esartemov/publications/RusMatSurveys.ps
>
> Thanks for that link. I'll read it. It looks like something I can
> learn from.
>
>
>
> > almost any book on constructivism
> > though
> > will point out that constructivists do not accept
>
> > forAll sentences A
> > either A or not-A must be true
> > required by ullrich's construct
>
> > tertium datur
>
> > most references on constructivism will explain why this position is
> > taken
>
> > often
> > they will even use an example
>
> > old books sometimes used fermat's conjecture
> > many now use goldbach
>
> > there is a reason these examples are almost universally of this form
> > and why they will by nature change over the years
>
> Look, constructivst views of the law of excluded middle are not at
> issue with me. I'm very familiar with that.
obviously not well enough
to understand it's operationalist origins
or how the computational foundations it is built from
are framed in a temporal (dynamic) ontology
there is a lot of depth here
and it appears you are dismissing shallowly
> And, Ullrich's example is
> not at issue with me, as I already mentioned that I'm not commenting
> upon it specifically. What I did say is that I'd like to see where
> such definitions of 'theorem' and 'algorithm' appear. Your reiterating
> that the law of excluded middle is not accepted in most (all?)
> constructivism does not answer the question as to where one might find
> such definitions of 'algrorithm' and 'theorem'.
this is where you seem to get dangerously avoidant
you appear to claim knowledge of bhk semantics
but have not seen that a system
where a theorem is true when it has been proven?
go read a fuckin' book you cranky crackpot!
" It does not make sense to think of truth or falsity
of a mathematical statement independently of our knowledge
concerning the statement. A statement is true if we have a
proof of it, and false if we can show that the assumption
that there is a proof for the statement leads to a
contradiction. " - famous math guys in a famous book somewhere
you claim to be well aware of the intuitionist reasons for tertium
datur
can you express those reasons
without reference to progressive states of knowledge?
can you state the reasons with a static notion of truth?
> > it has everything to do with time
listen moe
you need to check yourself
i came into this thread to point out
that michael press's position is very common
for someone who has attacked others for posting without knowing
you are demonstrating to the entire world
( well - that fraction that reads usenet
and happens to check this post
and has the appropriate background
and... well you get the qualification)
that you yourself do the same thing
that's fine
how else are you gonna learn, right?
but understand that you will not get away with innuendo
that you are doing the world a favor
by sighing heavily and implying that i am unwilling to explain deeper
i am sorry the burden of things to learn weighs heavy on you
i remember one series of posts
where you were entertaining some of zuhair's foundations
and then after a lot of exchanges
you became exasperated and stated you felt your time was wasted
that nothing you had posted had been listened to
because you were back to square one
well i've mentioned artemov to you before
you properly admitted at the time
you weren't familiar with the field
(one of the reasons i did not expect your pity party intro
because, despite some past aggression, you seemed more humble)
but if you would have been interested
you may have found the huge field of constructivist semantics
you may have learned of various principles of omniscience
and how they are rejected by various forms of constructivism
you may have found choice sequences
and heard mumblings of some deep connection with time
and something about husserl
and you come here
_expecting_ not to learn anything from the conversation?
you even post your feelings!
remember what you kept telling zuhair
that's right
go read some fuckin' books...
start with the pair by troelstra and van dalen
David C. Ullrich
wrote:
>In article
><1193339665....@i13g2000prf.googlegroups.com>,
> MoeBlee <jazz...@hotmail.com> wrote:
>
>> On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
>>
>> > michael's happens to be one of the more useful definitions
>> > which is why it is used quite commonly
>>
>> Where is it common to define 'algorithm' to include that something is
>> not an algorithm unless proven to have certain properties as opposed
>> to just stipulating that it has those properties?
>
>Given a prime p, a natural number b,
>and n a quadratic non-residue modulo p
>there is a computation that purports
>to find x such that xx = a (mod p).
>You program the computation in a computer
>and it does indeed provide a square root
>modulo p each time it runs. Good enough for you?
Huh???????? That's nothing even remotely resembling
an answer to his question. Yes, you can write a program
that does that - how does your pointing this out say
anything about the definition of the word "algorithm"?
>> I mean, ordinarily we take the defintion to be of the form:
>>
>> X is an algorithm iff X has such and such properties.
>>
>> But, if I understand you correctly, you're saying:
>>
>> X is an algorithm iff it is proven that X has such and such
>> properties.
>>
>> So where do I find this definition in the constructivist literature?
>
>I do not know.
************************
David C. Ullrich
David C. Ullrich
wrote:
I doubt that it's as useful as you think.
The problem with the definition in terms of what we know
or what's been proved is that it screws up the _logic_.
For example:
Let A = {0}. Let B = {1}. Let S = {1} if the Riemann
hypothesis is true, S = {0} if RH is false.
Now S is either A or B (we don't know which). A is
certainly recursive, and B is certainly recursive.
So by the suggested definition we're in the curious
situation where A is recursive, B is recursive, S
is either A or B, but S is not recursive. That's
wacky.
> which is why it is used quite commonly
Oh? Give an example of where it's used. I've
never seen it anywhere except here.
>> >A theorem is not a theorem until it is proven.
>> >What is your standard for implementing a method
>> >into production code?
>
>-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
>galathaea: prankster, fablist, magician, liar
************************
David C. Ullrich
David C. Ullrich
wrote:
It is _the_ standard definition.
>> Do you really think that if you don't see the utility
>> in a certain definition it follows that it cannot
>> in fact be the definition of whatever?
>
>No, why do you ask?
Because you made that statement about not seeing
the utility of the definition in the middle of
a discussion of what the definition _is_. If
your answer to my question is "no" then it's
hard to see the relevance of your comment.
>> Is that a
>> special property of you in particular, or is it
>> true that a definition is not a definition unless
>> _everyone_ sees the utility in it?
>
>Rhetorical question?
************************
David C. Ullrich
MoeBlee
> On Oct 25, 3:47 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On Oct 25, 12:54 pm, galathaea <galath...@gmail.com> wrote:
> > > On Oct 25, 11:38 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > > On Oct 25, 10:35 am, galathaea <galath...@gmail.com> wrote:
> > > > > On Oct 25, 10:13 am, MoeBlee <jazzm...@hotmail.com> wrote:
> > > > > > On Oct 24, 8:58 pm, Michael Press <rub...@pacbell.net> wrote:
>
> > > > > > > A theorem is not a theorem until it is proven.
>
> > > > > > A sentence S is a theorem of a set of sentences G iff there is a proof
> > > > > > of S from G.
>
> > > > > > But what does "until" mean in this context?
>
> > > > > constructivists almost universally seat properties in time
>
> > > > I'm not expert on the subject, but I recognize that certain
> > > > constructivists have notions that might be thought of, more or less
> > > > loosely, as temporal. However, it seems to me that in intuitionistic
> > > > mathematics, this can be formalized without a literal temporal
> > > > component.
>
> > I'm writing this response primarily in the interest of not allowing it
> > to seem as if my questions have been addressed by your post that seems
> > to take my points as much more naive than they are, as, at this point,
> > I'm not hopeful that much worth can came from our exchanges now.
>
> go fuck yourself
> you sanctimonious ignorant piece of shit
'sanctimonious' hardly applies. As to ignorance, I'm honest about
mine. As to excrement, I'll get to that later.
Now, your post here is a HUGE and obnoxious strawman attack.
I've said already that I do NOT dispute that various schools of
mathematics use a notion of time. And I've said that I fully recognize
that, for example, intuitionism rejects the law of excluded middle.
I've said that these things are not in dispute with me. But the fact
that certain kinds of mathematics have a notion of time doesn't answer
my very simple, very straightforward question: Where can I see
defintions of 'algorithm' and 'theorem' such as mentioned in this
thread?
That I've said that referring to the general context of certain kinds
of mathematics and even certain mathematical formulations themselves
is not to provide examples of such definitions as mentioned is NOT me
disputing that the such general contexts and formulations exist and
are at play and are even vital to an understanding of mathematics and
philosophy of mathematics. And your twisting the discussion AS IF I
had made a dispute that such context and formulations exist is
obnoxious. I asked for examples of certain kinds of definitions. You
don't answer that question by browbeating me as if I dispute what I do
not dispute.
> i did nothing to you but try to answer your questions
> you draw first blood
> and then pretend a reactionary pose?
What "first blood"?
> great way to back down from a position
> and still try to save face...
I've not backed down from any position. You haven't even mentioned a
specific "position" that you claim I've "backed down from".
> > > anything that can be formalised
> > > can be formalised in a completely meaningless game of symbols
>
> > My point was that while I understand that one might describe the
> > temporal notion as part of the intutive motivation, one can work in
> > the formalized mathematics without then using anything about time
> > itself. In particular, it's still not been shown that a notion of time
> > is required to define 'theorem'. Indeed, for example, I don't see a
> > notion of 'time' mentioned in the definition of 'proof in the
> > intuitionisitic predicate calculus'. What I do see is a perfectly
> > explicit mathematical definition.
>
> yes
>
> as i said:
> anything that can be formalised
> can be formalised in a completely meaningless game of symbols
Now you're just going back around in a circle of what's already been
said.
> you are apparently starting to show
> a complete lack of understanding
> of the distinction of semantics and syntax
Empty claim.
> do _you_ have a different theory of meaning?
I'm not an advocate of a particular philosophy of meaning. But
ordinarily I do work with the usual mathematical formulations, usually
in classical mathematics, but investigating intuitionistic logic too,
and with an ambition to eventually learn as many other approaches as I
can too..
> i actually thought you knew these basic objects of model theory
> seeing as you are often telling people (like zuhair)
> to go read a textbook
>
> why don't you?
Your bellowing is empty. You've not mentioned any single point in
model theory that I am not taking into account for the purpose of this
discussion. (Which is not to say there's not a lot of model theory
that I don't know; just that you haven't pointed to any statement I've
made that overextends my knowledge.)
I asked for an example of a certain kind of definition. I've not
contested at all what may be the context of various mathematics.
> do you object to the more general framework?
I haven't objected to any general framework at all in this
discussion.
> seriously
> your comment makes it sound like you have
> no grasp of the concept of quantifiers
Again, an empty charge by you. You haven't mentioned any specific
quantifier confusion.
> you say you want to see "theorem of X" used where it needs proof
Actually, I just said I wanted to see an example of a certain kind of
definition.
> (yet seem to not be aware that that is the bhk semantics)
I recognize the general import of BHK. Meanwhile, I asked to see an
example of a certain kind of definition.
> you say you want to see "algorithm for Y" vary over time
No I didn't. Please don't put words in my mouth.
> (program verification languages often use
> temporal specification logics like ltl and ctl)
>
> this is a deep topic and requires much exposition
>
> does that sound familiar?
Wonderful. I haven't at all disputed that there are temporal logics
and all kind of things. What I did ask was to see a definition of a
certain kind.
> > > kripke models
> > > the most common semantic setting for heyting algebras
> > > are inherently temporal
> > > for the same reason the semantic interpretation of "possibility"
> > > is inherently temporal
>
> > Whatever "inherently" means here, the point I was getting at is that
> > one can take Kripke models to be perfectly exact formal mathematical
> > objects and that to work with them one would do well to appreciate the
> > intuitive motivation (which I can understand being described as
> > 'temporal') but in the actual mathematics one does not need to invoke
> > any principles regarding time whatsoever.
>
> and i showed i could not understand your point
> by agreeing that all formalisation can be meaningless...??!
I don't very much doubt that you don't understand my point. That's
about the best I can answer your question.
> > And again, whatever the case about this, we've still not seen here a
> > reference to such definitions of 'theorem' that mention time.
>
> although this is pretty common throughout the field
> so i'd have hoped you'd have "picked up a textbook" to get it
> artemov writes in the paper i linked:
I just asked for an example of certain kind of definition. Please just
tell me what textbook to look at, and I'll look for that book. But
just citing textbooks that discuss temporal notions in various ways
does not answer my question. I've never disputed at all that various
mathematics and various philosophies of mathematics use temporal
notions.
> " Such a reading of modality naturally appears in dynamic and
> temporal logics aimed at describing computational processes,
> the states of which usually form a (possibly branching)
> Kripke structure. "
>
> so yes
> "we" have seen here just such a reference
>
> but i've mentioned bhk too...
You have a reference to temporal considerations. I've never disputed
that. I granted, from the very mention of temporal notions, that they
are at play in certain mathematical thinking.
Meanwhile, I just asked for an example of a certain kind of defintion.
By my doing that and my pointing out that various discussions of
temporal notions are not defintions of 'algorithm' and 'theorem' such
as I asked about does not constitute that I dispute that temporal
notions are active in certain mathematical thinking.
I know of definitions 'theorem' in, say, intuitionistic logic that
don't mention time. Now, my saying what I just said does not consitute
that I deny that a notion of time is at play in any particuclar
mathematical thinking. Rather, merely that the defintitions THEMSELVES
don't mention time. So, I'm asking, what definitions of 'theorem'
mention time. And I haven't even disputed that such defintions exist!
I'm just asking to see one!
> really
> moe
> i have not seen such a lack of content in your posts before
> (though i have seen belligerence)
> so what gives?
The belligerance in this discussion stems from you, particulary in
your post here.
As to lack of content, of course there's not much content, since I'm
basically in the position of asking a question: Where can I find such
definitions?
> you really have _never_ seen a semantics
> that requires proof before a statement is considered true?
That's not at issue.
I asked to see a certain kind of definition of "THEOREM", one that
mentions time.
> you've never seen the _reasons_ for tertium datur?
Sheez, are you brain impaired or something? I know about the prominent
arguments for and against the law of excluded middle. I said I am
familiar with the rejection of the law of excluded middle by certain
kinds of mathematics. This matter is NOT EVEN AT ISSUE. That you STILL
act is if it were at issue with me is obnoxious.
> > > > > do you understand why constructivists
> > > > > reject ullrich's dichotomy?
>
> > > > Due to my own personal unfamiliarity with Ullrich's notation, I don't
> > > > opine on the example Ullrich gave. But more generally, are you saying
> > > > that there is a definitely articulated constructivst notion of
> > > > 'algorithm' that includes that something is not an algorithm until
> > > > proven to be an algorithm? If so, would you recommend a book or
> > > > article that I can read about that?
>
> > > i am unfamiliar with a specific singling out of "algorithm"
> > > since constructivists tend to have strongly operational views
> > > on all properties
>
> > Then I really don't follow you. We were talking about definitions of
> > 'algorithm'; then you raised the matter of constructivism; now you
> > demur to connect constructivism with a defintion of 'algorithm'.
>
> seriously
> at this point i am starting to suspect
> you are either much less capable than i had surmised from previous
> posts
> or something crawled up your ass
> and you now can't stop yourself from arguing
Empty insults again. You've made no case that I am off base.
Even YOU mentioned that you were responding regarding definitions. And
you raised the matter of constructivsm. Then you say you're NOT
familiar with a constructivst definition of 'algorithm'.
> i made the connection
>
> when you ask:
> how is 4 even?
> and i reply:
> all integers of the form 2x are even
>
> it really is answering your question
> no matter how hard you squint your eyes or shake your head
> or whatever you are doing to skip over it
That's a ridiculous analogy. I'm NOT asking how it might be entailed
that there is a temporal notion involved in a certain definition. I'm
just asking to see a defintion itself that mentions a temporal notion.
> michael press gave an operational definition of algorithm
>
> to call something an algorithm for a particular task
> you must have a verification that the task gets accomplished
>
> others thought it a strange way to treat algorithms
> whereas to me it was quite natural
>
> operationalism and constructivism are intimately related
> so i brought up why it was natural
> and common
(1) A definition of 'X is an algorithm' may be different from a
definition of 'X is an algorithm to complete task T'.
(2) I've not made any dispute as to what is natural or common in how
one treats certain notions. I just asked to see a certain kind of
definition. And I didn't even dispute that such a definition exists.
And I didn't even claim that a lack of the existence of one would
nullify the legitimacy of any general notions. I just asked to see a
certain kind of definition. And for that, speaking of excrement, you
pour yours on me.
I never disputed that anyone has a certain ontology.
> there is a lot of depth here
> and it appears you are dismissing shallowly
I've not dismissed that there is a temporal notion. I GRANTED in my
early responses to you that there is a temporal notion. And I never
claimed it not to be deep or important.
> > And, Ullrich's example is
> > not at issue with me, as I already mentioned that I'm not commenting
> > upon it specifically. What I did say is that I'd like to see where
> > such definitions of 'theorem' and 'algorithm' appear. Your reiterating
> > that the law of excluded middle is not accepted in most (all?)
> > constructivism does not answer the question as to where one might find
> > such definitions of 'algrorithm' and 'theorem'.
>
> this is where you seem to get dangerously avoidant
I have a perfect prerogative not to commit myself to positions I don't
wish to commit myself to, such as a position on Ullrich's specific
example. Nothing I've said requires such a commitment.
> you appear to claim knowledge of bhk semantics
> but have not seen that a system
> where a theorem is true when it has been proven?
I just asked to see a certain kind of definition.
> go read a fuckin' book you cranky crackpot!
Please just tell me what book DEFINES 'theorem' by mentioning time.
> " It does not make sense to think of truth or falsity
> of a mathematical statement independently of our knowledge
> concerning the statement. A statement is true if we have a
> proof of it, and false if we can show that the assumption
> that there is a proof for the statement leads to a
> contradiction. " - famous math guys in a famous book somewhere
I didn't ask about TRUTH and FALSEHOOD. I asked about THEOREM.
> you claim to be well aware of the intuitionist reasons for tertium
> datur
>
> can you express those reasons
> without reference to progressive states of knowledge?
Whether I can or not, does not go to the question of where I can find
a certain kind of definition.
> can you state the reasons with a static notion of truth?
>
> > > it has everything to do with time
>
> listen moe
>
> you need to check yourself
>
> i came into this thread to point out
> that michael press's position is very common
>
> for someone who has attacked others for posting without knowing
> you are demonstrating to the entire world
> ( well - that fraction that reads usenet
> and happens to check this post
> and has the appropriate background
> and... well you get the qualification)
> that you yourself do the same thing
Au contraire. I'm claiming NOT to know. I'm saying from the OUTSET, "I
don't know of such a definition. Would you please point me to one?"
> that's fine
> how else are you gonna learn, right?
>
> but understand that you will not get away with innuendo
> that you are doing the world a favor
> by sighing heavily and implying that i am unwilling to explain deeper
I have NOT implied that you are unwilling to EXPLAIN deeper. Rather, I
said that your arguments are not examples of a certain kind of
defintion.
> i am sorry the burden of things to learn weighs heavy on you
>
> i remember one series of posts
> where you were entertaining some of zuhair's foundations
> and then after a lot of exchanges
> you became exasperated and stated you felt your time was wasted
> that nothing you had posted had been listened to
> because you were back to square one
>
> well i've mentioned artemov to you before
>
> you properly admitted at the time
> you weren't familiar with the field
> (one of the reasons i did not expect your pity party intro
> because, despite some past aggression, you seemed more humble)
>
> but if you would have been interested
> you may have found the huge field of constructivist semantics
>
> you may have learned of various principles of omniscience
> and how they are rejected by various forms of constructivism
>
> you may have found choice sequences
> and heard mumblings of some deep connection with time
> and something about husserl
>
> and you come here
> _expecting_ not to learn anything from the conversation?
No, I come hoping to learn. But from your PARTICULAR form of
conversation with me here, I gave up that our exchanges would be
helpful.
> you even post your feelings!
Yes. Everyone has such a prerogative.
> remember what you kept telling zuhair
>
> that's right
> go read some fuckin' books...
>
> start with the pair by troelstra and van dalen
I've read some of that and of course would like to work through all of
both volumes some day. But, since I don't have the books with me, it
would help if someone would point to a definition there of the kind
previously mentioned. Otherwise, I don't need to be admonished as to a
need for a basic familiarity with certain constructivst notions, since
I am familiar with them and that they exist is not even at issue with
me, and as to need for more familiarity with the particulars of
constructivst mathematics, I am the FIRST to say that I need that.
MoeBlee
MoeBlee
> > > A theorem is not a theorem until it is proven.
>
> > A sentence S is a theorem of a set of sentences G iff there is a proof
> > of S from G.
>
> > But what does "until" mean in this context?
>
> I was speaking loosely. A proof is part of a theorem.
Fair enough. An ordinary definition of 'theorem' mentions 'proof' (or
something equivalent). Thanks.
MoeBlee
MoeBlee
>
> MoeBlee <jazzm...@hotmail.com> wrote:
> > On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
>
> > > michael's happens to be one of the more useful definitions
> > > which is why it is used quite commonly
>
> > Where is it common to define 'algorithm' to include that something is
> > not an algorithm unless proven to have certain properties as opposed
> > to just stipulating that it has those properties?
>
> Given a prime p, a natural number b,
> and n a quadratic non-residue modulo p
> there is a computation that purports
> to find x such that xx = a (mod p).
> You program the computation in a computer
> and it does indeed provide a square root
> modulo p each time it runs. Good enough for you?
I think I get your basic idea there. But I don't see that it answers
my question. But below you do answer it:
> > I mean, ordinarily we take the defintion to be of the form:
>
> > X is an algorithm iff X has such and such properties.
>
> > But, if I understand you correctly, you're saying:
>
> > X is an algorithm iff it is proven that X has such and such
> > properties.
>
> > So where do I find this definition in the constructivist literature?
>
> I do not know.
MoeBlee
galathaea
1) do you see how stupid it looks
to continuously ask someone to read a book?
there are hundreds of thousands
(maybe millions now?)
of worthwhile books to read
not everyone gets to them all
2) moeblee keeps saying:
"defines..definition..DEFINITION..DEFINES!!"
definitions are one of those things
like propositions
that have too many connotations to be of much use
(this is a quinean argument)
definitions provide a syntactic form for formal manipulation
while trying to convey enough semantics content
for the definition to obtain in intended ways
instead of definitions
i try (sometimes poorly) to focus on strings about properties
statements or sentences
for the syntactic content
and the model or interpretation for semantics
what to formulate in the syntax
though
to obtain proper semantics
depends upon the content of the semantics
the properties of the interpretation
and what is desired to be conveyed
you can't put everything from the semantics in
as tarski found with truth
so somebody who is using constructivist semantics
will not add to definitions details common to all constructivist
interpretations
but someone who is discussing to an audience not regularly using
such
can add some of the content of constructivist semantics
to the definitions they give
in order to convey the intended meaning
you keep asking for definitions
whereas i keep talking about semantics
do you realise that definitions are intended to convey meaning?
3) do you understand that
posting that you have little hope of getting anything from a
conversation
when someone has actually been spending time to explain
themselves
is just being an ass?
and a stupid one at that?
you had things to learn
even from zuhair
but your behavior is what pisses people off
that one's just fyi
MoeBlee
> 1) do you see how stupid it looks
> to continuously ask someone to read a book?
>
> there are hundreds of thousands
> (maybe millions now?)
> of worthwhile books to read
>
> not everyone gets to them all
What an absurd strawman! I didn't say to anyone "read ALL books".
Rather, I said "Read A book" or "Read some books" or other variations,
but never anytyihng so ridiculous as a challenge that a person must
have read any greater number of writings. And often I even suggested
SPECIFIC books that address the material that the person needs to
know.
> 2) moeblee keeps saying:
> "defines..definition..DEFINITION..DEFINES!!"
Because that was what the DISCUSSION itself came to be about as even
YOU made a claim as to definitions.
> definitions are one of those things
> like propositions
> that have too many connotations to be of much use
> (this is a quinean argument)
Whatever about connotations. We do know of general forms for
mathematical definitions.
> definitions provide a syntactic form for formal manipulation
> while trying to convey enough semantics content
> for the definition to obtain in intended ways
That is, to me at least, a novel idea.
> instead of definitions
> i try (sometimes poorly) to focus on strings about properties
> statements or sentences
> for the syntactic content
> and the model or interpretation for semantics
>
> what to formulate in the syntax
> though
> to obtain proper semantics
> depends upon the content of the semantics
> the properties of the interpretation
> and what is desired to be conveyed
>
> you can't put everything from the semantics in
> as tarski found with truth
>
> so somebody who is using constructivist semantics
> will not add to definitions details common to all constructivist
> interpretations
> but someone who is discussing to an audience not regularly using
> such
> can add some of the content of constructivist semantics
> to the definitions they give
> in order to convey the intended meaning
>
> you keep asking for definitions
> whereas i keep talking about semantics
YOU mentioned defintition YOURSELF.
And as to your semantics, I've not contested that you may do whatever
you like in your semantics. I asked a simple question about where to
find a certain kind of definition. That ended up with you, in your
previous post, raining all kinds of garbage on me.
> do you realise that definitions are intended to convey meaning?
What is "intended" depends on who is doing the intending. But, as I
can see developing, I don't share your general notion of a definition.
In the meantime, I had just asked to see a defintion. I didn't even,
at that point, stipulate what a definition IS or what criteia for a
definition. I just asked to see one of the kind being claimed to be
"common", so anyone could provide whatever example they wish, and with
whatever understanding they have of what a definition is, how a
definition works, or what is the intent of a defintion. MY notions of
those things are not in question.
> 3) do you understand that
> posting that you have little hope of getting anything from a
> conversation
> when someone has actually been spending time to explain
> themselves
> is just being an ass?
It would be if the circumstances didn't warrant it.
> and a stupid one at that?
>
> you had things to learn
> even from zuhair
> but your behavior is what pisses people off
>
> that one's just fyi
Who, aside from cranks and you, are these people? For whom do you
speak?
Lots of people piss of lots of other people for lots of different
reasons. YOU pissed ME off (mildly, and then significantly) Thats 'y'
in 'fyi' too.
MoeBlee
galathaea
> On Oct 26, 12:35 pm, galathaea <galath...@gmail.com> wrote:
>
> > 1) do you see how stupid it looks
> > to continuously ask someone to read a book?
>
> > there are hundreds of thousands
> > (maybe millions now?)
> > of worthwhile books to read
>
> > not everyone gets to them all
>
> What an absurd strawman! I didn't say to anyone "read ALL books".
> Rather, I said "Read A book" or "Read some books" or other variations,
> but never anytyihng so ridiculous as a challenge that a person must
> have read any greater number of writings. And often I even suggested
> SPECIFIC books that address the material that the person needs to
> know.
of course not
you know
at least it is clear now how poor your reasoning skills are
i never said read all books either
but i pointed out one can always find another one you haven't read
and so one
if one were such a jackass needing self-assuring
could continue to just have one over you
kinda like this one poster i've seen...
> > 2) moeblee keeps saying:
> > "defines..definition..DEFINITION..DEFINES!!"
>
> Because that was what the DISCUSSION itself came to be about as even
> YOU made a claim as to definitions.
that is what you
in your little world
made the discussion into
once you realised michael press could be making a legitimate point
you are not everyone
nor are you the arbiter of DISCUSSION
no matter how much you CAPITALISE
or use the names of fallacies fallaciously
yes _i_ supported michael's definition
i even posted more information
where immediately i pointed out
that he was carrying semantic details
commonly left to the interpretation itself
i even started detailing this relation
between syntax and semantics in definitions
and pointed out how it related to the operationalist programme
which was where _i_ had taken the discussion
somehow that offended you to no end
because you wanted a discussion
where you continuously chirp
"definition" and "defines"
in various states of capitalisations
in an ocd loop of self-gratification
you didn't like someone actually answering some of your questions
so you pretended not to see them
you avoided them
somehow
this culminated in you making the funny statement
"I didn't ask about TRUTH and FALSEHOOD. I asked about THEOREM."
which you absolutely felt was completely unrelated
to all that background noise i was making about bhk
so in the end
yes
you were left only without the definition in the form you wanted
(though i had given you forms you didn't want)
and were able to valiantly fight away any other discussion
that may have made interesting points you might learn from
bravo there
> > definitions are one of those things
> > like propositions
> > that have too many connotations to be of much use
> > (this is a quinean argument)
>
> Whatever about connotations. We do know of general forms for
> mathematical definitions.
but
of course
as your immense wisdom already understands
defining is not a process that can be formalised
yes
yes i did
since it's not a formal concept
i made the mistake where i posted about a vague concept
and tried to make clear where i thought vagaries lie
you
on the other hand
mistakenly felt you were taking a well-defined position
and bravely ignored any clarifications
> And as to your semantics, I've not contested that you may do whatever
> you like in your semantics. I asked a simple question about where to
> find a certain kind of definition. That ended up with you, in your
> previous post, raining all kinds of garbage on me.
it was quite cathartic
thank you
you drew first blood through demeaning
so i don't feel too bad about it
> > do you realise that definitions are intended to convey meaning?
>
> What is "intended" depends on who is doing the intending. But, as I
> can see developing, I don't share your general notion of a definition.
> In the meantime, I had just asked to see a defintion. I didn't even,
> at that point, stipulate what a definition IS or what criteia for a
> definition. I just asked to see one of the kind being claimed to be
> "common", so anyone could provide whatever example they wish, and with
> whatever understanding they have of what a definition is, how a
> definition works, or what is the intent of a defintion. MY notions of
> those things are not in question.
well
actually your notion of definition is entirely the point
because i did give references that point to operational semantics
and how in those approaches
meanings require verifications in the sense indicated
you objected only because these ideas of meaning
did not encapsulate into one easily digestible sentence
which is what you meant by definition
i continued to expand in this direction
while your obsessions started you repeating define in various contexts
upset that the definitions i provided did not fit your form
i should have realised earlier
that you actually felt you were making a rigorous request
and corrected that mistaken notion of yours
instead of letting you overboil to the point of demeaning
that was obviously my fault
> > 3) do you understand that
> > posting that you have little hope of getting anything from a
> > conversation
> > when someone has actually been spending time to explain
> > themselves
> > is just being an ass?
>
> It would be if the circumstances didn't warrant it.
>
> > and a stupid one at that?
>
> > you had things to learn
> > even from zuhair
> > but your behavior is what pisses people off
>
> > that one's just fyi
>
> Who, aside from cranks and you, are these people? For whom do you
> speak?
>
> Lots of people piss of lots of other people for lots of different
> reasons. YOU pissed ME off (mildly, and then significantly) Thats 'y'
> in 'fyi' too.
i tried the mutual learning thing with you
it wasn't i that gave up
sanctimonious was precisely the word i was looking for
G. Frege
wrote:
> MoeBlee
What a waste of time and effort, Moe!
And HERE time actually does matter...
F.
--
E-mail: info<at>simple-line<dot>de
Michael Press
<1193422884.5...@z24g2000prh.googlegroups.com>
,
MoeBlee <jazz...@hotmail.com> wrote:
> On Oct 25, 5:06 pm, Michael Press <rub...@pacbell.net> wrote:
> > In article
> > <1193339665.610429.38...@i13g2000prf.googlegroups.com>,
> >
> > MoeBlee <jazzm...@hotmail.com> wrote:
> > > On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
> >
> > > > michael's happens to be one of the more useful definitions
> > > > which is why it is used quite commonly
> >
> > > Where is it common to define 'algorithm' to include that something is
> > > not an algorithm unless proven to have certain properties as opposed
> > > to just stipulating that it has those properties?
> >
> > Given a prime p, a natural number b,
> > and n a quadratic non-residue modulo p
> > there is a computation that purports
> > to find x such that xx = a (mod p).
> > You program the computation in a computer
> > and it does indeed provide a square root
> > modulo p each time it runs. Good enough for you?
>
> I think I get your basic idea there. But I don't see that it answers
> my question. But below you do answer it:
My basic idea is the question
"What is good enough reason for you to implement a computation."
You are saying "stipulation", and to me that is
equivalent to proof by assertion or proof by
authority. That is not good enough for me.
I want mathematical proof before a computation
and assertion of its efficacy can be admitted
as an algorithm.
> > > I mean, ordinarily we take the defintion to be of the form:
> >
> > > X is an algorithm iff X has such and such properties.
> >
> > > But, if I understand you correctly, you're saying:
> >
> > > X is an algorithm iff it is proven that X has such and such
> > > properties.
> >
> > > So where do I find this definition in the constructivist literature?
> >
> > I do not know.
To which I add that I am not a constructivist
and have not read the literature.
--
Michael Press
MoeBlee
> On Oct 26, 12:56 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> > On Oct 26, 12:35 pm, galathaea <galath...@gmail.com> wrote:
>
> > > 1) do you see how stupid it looks
> > > to continuously ask someone to read a book?
>
> > > there are hundreds of thousands
> > > (maybe millions now?)
> > > of worthwhile books to read
>
> > > not everyone gets to them all
>
> > What an absurd strawman! I didn't say to anyone "read ALL books".
> > Rather, I said "Read A book" or "Read some books" or other variations,
> > but never anytyihng so ridiculous as a challenge that a person must
> > have read any greater number of writings. And often I even suggested
> > SPECIFIC books that address the material that the person needs to
> > know.
>
> of course not
>
> you know
> at least it is clear now how poor your reasoning skills are
>
> i never said read all books either
> but i pointed out one can always find another one you haven't read
> and so one
> if one were such a jackass needing self-assuring
> could continue to just have one over you
> kinda like this one poster i've seen...
But I DON'T hold it over people that I've read a book or books that
they haven't read on the MERE grounds of any particular book that
they've not read or on the grounds of the number of books I've read in
comparison. What I've said to people who spout ignorantly about a
subject is that they need to read SOME book on the subject, and that
is not toward any comparison with with ME but toward informing
themselves so that they'll see what is incorrect in their spouting.
I definitely do NOT condone, anyone, call him 'Mr. Poster X',
dismissing another poster on the MERE basis that Mr. Poster X has read
more books or even knows more about the subject.
> > > 2) moeblee keeps saying:
> > > "defines..definition..DEFINITION..DEFINES!!"
>
> > Because that was what the DISCUSSION itself came to be about as even
> > YOU made a claim as to definitions.
>
> that is what you
> in your little world
> made the discussion into
> once you realised michael press could be making a legitimate point
No, *I* didn't turn the discussion into that of definitions. The
discussion ALREADY was on the subject of definitions before I also
posted on the subject of discussions.
In fact, YOU addressed the subject of defintion before I even posted a
single word in this thread!
So, you are REALLY swinging wildly.
Anyway, there's nothing wrong with the subject of definitions.
Moreover, I have no interest in Michael Press not making legitimate
points.
> you are not everyone
> nor are you the arbiter of DISCUSSION
> no matter how much you CAPITALISE
> or use the names of fallacies fallaciously
I don't claim do be an arbiter of the discussion! Where do you come up
with this garbage?! YOU were the one who emphasized that I had kept
coming back to the subject of defintion. I just pointed out that I was
coming back to it because it had been in the center of discussion
(also, to add, that it was the only point I had addressed originally,
as most of the rest of your stuff about constructivism was not even at
issue with me, so that your browbeating was quite inppropriate in that
regard).
I am not AT ALL seeking for anyone not to discuss ANYTHING in the
world they want to discuss. You're completely whack to even suggest
otherwise.
And you haven't given any argument that I've used the name of a
fallacy incorrectly.
Man, you just keep piling up your garbage here.
> yes _i_ supported michael's definition
>
> i even posted more information
> where immediately i pointed out
> that he was carrying semantic details
> commonly left to the interpretation itself
>
> i even started detailing this relation
> between syntax and semantics in definitions
> and pointed out how it related to the operationalist programme
> which was where _i_ had taken the discussion
>
> somehow that offended you to no end
What the FREAK are you talking about?! I didn't say ANYTHING about
those remarks of yours offending me.
This is about the FOURTH time now that you've as much as put words in
my mouth. I've asked you not to do that. Please don't.
> because you wanted a discussion
> where you continuously chirp
> "definition" and "defines"
> in various states of capitalisations
> in an ocd loop of self-gratification
I didn't want any particular kind of discussion. Now you're putting
thoughts and motivations into me that I don't have. I'm happy to have
people discuss whatever they like. Meanwhile, though, and especially
since the subject of defintion had become important in the discussion,
I had certain points and questions I wished to make about it. Yeah, I
wanted to post a couple of points and ask a couple of questions, and
then to fend from YOUR posts in which you addressed me as if I were
disputing matters I hadnd't even disputed - yeah, that must make me a
real controlling a-hole.
> you didn't like someone actually answering some of your questions
> so you pretended not to see them
>
> you avoided them
AGAIN, you give the baseless charge. I've been addressing you left and
right. And then Michael Press gave his OWN response and I addressed
that too.
> somehow
> this culminated in you making the funny statement
> "I didn't ask about TRUTH and FALSEHOOD. I asked about THEOREM."
> which you absolutely felt was completely unrelated
> to all that background noise i was making about bhk
I didn't say anything about what was related to any noise, background
or otherwise.
The statement I made was not funny at all. It's right to the issue.
You kept browbeating me about constructivist notions of truth and
other matters that I didn't even contest, so I said the exact most
relevent thing: I haven't contested anything about constructist
notions of truth, rather I ASKED to see certain claimed defintions of
THEOREM.
> so in the end
> yes
> you were left only without the definition in the form you wanted
> (though i had given you forms you didn't want)
> and were able to valiantly fight away any other discussion
> that may have made interesting points you might learn from
Again your'e putting a LOAD of garbage in my mouth. Please stop that.
I didn't desire that any particular definition prevail. I ASKED to see
examples in the literature of alternatives. And I don't know what you
think is a defintion of 'theorem' that you think you gave.
And I don't "fight away" other discussion. You or anybody can disscuss
whatever you like as far as I'm concerned. I'd RATHER that there NOT
be moderation of these threads. But my also getting my two cents in or
many cents in, whatever, is not "fighting away" other discussion.
> bravo there
>
> > > definitions are one of those things
> > > like propositions
> > > that have too many connotations to be of much use
> > > (this is a quinean argument)
>
> > Whatever about connotations. We do know of general forms for
> > mathematical definitions.
>
> but
> of course
> as your immense wisdom already understands
> defining is not a process that can be formalised
That's a novel idea to me.
Then at least recognize that you're wrong to say that *I* initiated
the subject.
> since it's not a formal concept
> i made the mistake where i posted about a vague concept
> and tried to make clear where i thought vagaries lie
>
> you
> on the other hand
> mistakenly felt you were taking a well-defined position
> and bravely ignored any clarifications
I'm happy to accept any clarifications you have. What I wouldn't do
though is refrain from responding to your posts that were posed as if
I had taken issue with that which was not at issue with me.
> > And as to your semantics, I've not contested that you may do whatever
> > you like in your semantics. I asked a simple question about where to
> > find a certain kind of definition. That ended up with you, in your
> > previous post, raining all kinds of garbage on me.
>
> it was quite cathartic
> thank you
No, no thank you.
> you drew first blood through demeaning
> so i don't feel too bad about it
Based on how the discussion was going, I felt that the discussion
would not be productive and so I frankly said so.
> > > do you realise that definitions are intended to convey meaning?
>
> > What is "intended" depends on who is doing the intending. But, as I
> > can see developing, I don't share your general notion of a definition.
> > In the meantime, I had just asked to see a defintion. I didn't even,
> > at that point, stipulate what a definition IS or what criteia for a
> > definition. I just asked to see one of the kind being claimed to be
> > "common", so anyone could provide whatever example they wish, and with
> > whatever understanding they have of what a definition is, how a
> > definition works, or what is the intent of a defintion. MY notions of
> > those things are not in question.
>
> well
> actually your notion of definition is entirely the point
> because i did give references that point to operational semantics
> and how in those approaches
> meanings require verifications in the sense indicated
I asked for defintions of 'algorithm' and 'theorem'. I welcome learing
more about other approaches. But what you posted in the particular
exchanges with me was not a defintion of 'algorithm' or 'theorem' in
your posts then(if there is such a definition in those exchanges,
then, yes I don't have a metal detector to find them). Meanwhile you
continued to browbeat me as if I had contested matters that weren't
even at issue with me.
> you objected only because these ideas of meaning
> did not encapsulate into one easily digestible sentence
> which is what you meant by definition
You KEEP putting words in my mouth (or this time, thoughts in my
brain). I did NOT object on any such basis as you just mentioned.
> i continued to expand in this direction
> while your obsessions started you repeating define in various contexts
> upset that the definitions i provided did not fit your form
Again, you're putting ascribing to me thoughts I didn't have. I didn't
even specify a form.
> i should have realised earlier
> that you actually felt you were making a rigorous request
> and corrected that mistaken notion of yours
> instead of letting you overboil to the point of demeaning
> that was obviously my fault
It was your fault to play me for a fool. You're still doing it.
I was frank to say that I didn't think our discussion would be
productive. My intent was not to demean (though I grant that you're
not unreasonable to take it that way and that I underestimated the
power of the remark), but rather to set a needed context for my
continued participation posting back to your posts.
So whehter you're umbrage is justified by my remark that I had low
expectations for a productive exchange, or whether rather you've shown
yourself to be ludicrously thin-skinned about the remark, I'm not
sure. But it is clear that soon enough you went way into the deep end
of villification in response. As well as you're being dishonest by
continuing to put words in my mouth when I've asked you about four
times already not to do it.
> > > 3) do you understand that
> > > posting that you have little hope of getting anything from a
> > > conversation
> > > when someone has actually been spending time to explain
> > > themselves
> > > is just being an ass?
>
> > It would be if the circumstances didn't warrant it.
>
> > > and a stupid one at that?
>
> > > you had things to learn
> > > even from zuhair
> > > but your behavior is what pisses people off
>
> > > that one's just fyi
>
> > Who, aside from cranks and you, are these people? For whom do you
> > speak?
>
> > Lots of people piss of lots of other people for lots of different
> > reasons. YOU pissed ME off (mildly, and then significantly) Thats 'y'
> > in 'fyi' too.
>
> i tried the mutual learning thing with you
How very enlightened of you. Meanwhile, you spoke for "people", and I
don't know who you think you speak for other than yourself.
> it wasn't i that gave up
>
> sanctimonious was precisely the word i was looking for
It's not even in the ballpark.
MoeBlee
MoeBlee
> What a waste of time and effort, Moe!
Perhaps.
MoeBlee
MoeBlee
> MoeBlee <jazzm...@hotmail.com> wrote:
> > On Oct 25, 5:06 pm, Michael Press <rub...@pacbell.net> wrote:
> > > In article
> > > <1193339665.610429.38...@i13g2000prf.googlegroups.com>,
>
> > > MoeBlee <jazzm...@hotmail.com> wrote:
> > > > On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
>
> > > > > michael's happens to be one of the more useful definitions
> > > > > which is why it is used quite commonly
>
> > > > Where is it common to define 'algorithm' to include that something is
> > > > not an algorithm unless proven to have certain properties as opposed
> > > > to just stipulating that it has those properties?
>
> > > Given a prime p, a natural number b,
> > > and n a quadratic non-residue modulo p
> > > there is a computation that purports
> > > to find x such that xx = a (mod p).
> > > You program the computation in a computer
> > > and it does indeed provide a square root
> > > modulo p each time it runs. Good enough for you?
>
> > I think I get your basic idea there. But I don't see that it answers
> > my question. But below you do answer it:
>
> My basic idea is the question
> "What is good enough reason for you to implement a computation."
You've lost me. People may have different reasons for performing a
computation. I don't see how that bears on what we were discussing.
> You are saying "stipulation", and to me that is
> equivalent to proof by assertion or proof by
> authority.
But I wasn't talking about definition, not proof. I was talking about
definition. 'stipulation' was in that sense -of stipulative
definition. I haven't advocated that such things are decided by
authority. On the contrary, 'stipulative' allows anyone to stipulate
their own defintions.
> That is not good enough for me.
> I want mathematical proof before a computation
> and assertion of its efficacy can be admitted
> as an algorithm.
Again, I didn't claim that X is an algorithm simply by X having been
stipulated to be an algorithm (Or did you even think I meant that? I'm
not sure.) What I meant was that for a stipulative definition of the
predicate 'is an algorithm' we stipulate what properties something
must have to be an algorithm. And my question (and skepticism) regards
whether those properties should include that X is PROVEN to have the
remaining properties in the definiens.
> To which I add that I am not a constructivist
> and have not read the literature.
Of course, that's quite fair.
MoeBlee
Michael Press
<1193444539.7...@q5g2000prf.googlegroups.com>,
MoeBlee <jazz...@hotmail.com> wrote:
> On Oct 26, 4:15 pm, Michael Press <rub...@pacbell.net> wrote:
> > In article
> > <1193422884.564195.101...@z24g2000prh.googlegroups.com>
> > MoeBlee <jazzm...@hotmail.com> wrote:
> > > On Oct 25, 5:06 pm, Michael Press <rub...@pacbell.net> wrote:
> > > > In article
> > > > <1193339665.610429.38...@i13g2000prf.googlegroups.com>,
> >
> > > > MoeBlee <jazzm...@hotmail.com> wrote:
> > > > > On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
> >
> > > > > > michael's happens to be one of the more useful definitions
> > > > > > which is why it is used quite commonly
> >
> > > > > Where is it common to define 'algorithm' to include that something is
> > > > > not an algorithm unless proven to have certain properties as opposed
> > > > > to just stipulating that it has those properties?
I looked around and nobody seems to officially adopt such a definition.
In practice people who publish algorithms prove that they
work for the intended purpose, and usually prove time and space
requirements as well.
> > > > Given a prime p, a natural number b,
> > > > and n a quadratic non-residue modulo p
> > > > there is a computation that purports
> > > > to find x such that xx = a (mod p).
> > > > You program the computation in a computer
> > > > and it does indeed provide a square root
> > > > modulo p each time it runs. Good enough for you?
> >
> > > I think I get your basic idea there. But I don't see that it answers
> > > my question. But below you do answer it:
> >
> > My basic idea is the question
> > "What is good enough reason for you to implement a computation."
>
> You've lost me. People may have different reasons for performing a
> computation. I don't see how that bears on what we were discussing.
OK
> > You are saying "stipulation", and to me that is
> > equivalent to proof by assertion or proof by
> > authority.
>
> But I wasn't talking about definition, not proof. I was talking about
> definition. 'stipulation' was in that sense -of stipulative
> definition. I haven't advocated that such things are decided by
> authority. On the contrary, 'stipulative' allows anyone to stipulate
> their own defintions.
>
> > That is not good enough for me.
> > I want mathematical proof before a computation
> > and assertion of its efficacy can be admitted
> > as an algorithm.
>
> Again, I didn't claim that X is an algorithm simply by X having been
> stipulated to be an algorithm (Or did you even think I meant that? I'm
> not sure.) What I meant was that for a stipulative definition of the
> predicate 'is an algorithm' we stipulate what properties something
> must have to be an algorithm. And my question (and skepticism) regards
> whether those properties should include that X is PROVEN to have the
> remaining properties in the definiens.
OK.
--
Michael Press
David C. Ullrich
wrote:
>In article
><1193444539.7...@q5g2000prf.googlegroups.com>,
> MoeBlee <jazz...@hotmail.com> wrote:
>
>> On Oct 26, 4:15 pm, Michael Press <rub...@pacbell.net> wrote:
>> > In article
>> > <1193422884.564195.101...@z24g2000prh.googlegroups.com>
>> > MoeBlee <jazzm...@hotmail.com> wrote:
>> > > On Oct 25, 5:06 pm, Michael Press <rub...@pacbell.net> wrote:
>> > > > In article
>> > > > <1193339665.610429.38...@i13g2000prf.googlegroups.com>,
>> >
>> > > > MoeBlee <jazzm...@hotmail.com> wrote:
>> > > > > On Oct 25, 10:00 am, galathaea <galath...@gmail.com> wrote:
>> >
>> > > > > > michael's happens to be one of the more useful definitions
>> > > > > > which is why it is used quite commonly
>> >
>> > > > > Where is it common to define 'algorithm' to include that something is
>> > > > > not an algorithm unless proven to have certain properties as opposed
>> > > > > to just stipulating that it has those properties?
>
>I looked around and nobody seems to officially adopt such a definition.
>In practice people who publish algorithms prove that they
>work for the intended purpose,
Of course they do. If one is claiming that something is an algorithm
one should include a proof that it is in fact an algorithm, if that's
not obvious. If one is claiming that something is an algorithm that
solves a certain problem one should include a proof that it does
solve that problem, if that's not obvious.
None of which has anything to do with the _definition_ of the
word "algorithm".
Look. What's the definition of "even integer"? It is this:
(i) n is an even integer if n = 2k for some integer k.
It is not this:
(ii) n is an even integer if it has been proved that
n = 2k for some integer k.
(ii) is the definition of "something which has been
proved to be an even integer". Yes, if one publishes
a statement that something is an even integer one
usually includes a proof of that fact. The fact that
this proof is included does not imply that the definition
of "even integer" is (ii).
************************
David C. Ullrich
David C. Ullrich
>On Fri, 26 Oct 2007 00:19:14 GMT, Michael Press <rub...@pacbell.net>
>I mostly agree with Michael Press on this issue.
You're entitled to your opinion. It's wrong.
>I admit that I know very little about the theory of computation, and
>yet, I think I know an algorithm when I see one.
>
>Here's my (informal) concept ...
>
>A procedure does not qualify as "an algorithm" unless there is a
>specification of
>
>(1) What problem the algorithm is intended to solve.
>
>(2) The acceptable and/or required inputs.
>
>(3) The possible outputs.
>
>(4) How the algorithm works.
>
>(5) A proof that it correctly solves the intended problem.
And I imagine that you'd also say that something does not
qualify as an irrational number unless there is a proof
that it is irrational?
If you would not say that, why not?
If you _would_ say that: You might note that it follows that
there are only countably many irrational numbers. It also
follows that zeta(3) was not irrational 100 years ago,
but is now irrational.
>As far as I can see, anyone who actually implements, designs, or
>writes textbooks about algorithms takes all of the above aspects quite
>seriously, _especially_ aspect (1), and would regard a procedure with
>no specified goal as useless nonsense, not an algorithm.
Of course they do! Just as when someone publishes an assertion
that a given number is irrational they include a proof of this
fact. That has nothing to do with the _definition_ of "irrational
number".
>quasi
************************
David C. Ullrich
T.H. Ray
>
> > On Oct 23, 3:57 pm, Victor Porton <por...@narod.ru>
> wrote:
> > > For famous hypothesis such as Millennium Prize
> problems (or to be yet
> > > more specific for P=NP problem)...
> > >
> > > ... how we can (or cannot) be sure that the
> hypotheses or its negation
> > > is provable.
> > >
> true nor false in ZFC.
> > >
> > > For a specific example can we be sure that either
> P=NP or P!=NP is
> > > provable?
> > >
> > > Victor Porton -http://www.mathematics21.org
> >
> > By 'provable' you don't seem to mean 'provable
> within some formal
> > system' but 'provable by human reason'.
> >
> > There is an issue about philosophy of mathematics
> involved here. From
> > a Platonistic point of view it's perfectly possible
> that some facts
> > concerning mathematical objects result unknowable
> for human reason,
> > since mathematical facts are objective facts and
> don't depend on the
> > power of human reason.
> >
> > But the more constructivist our point of view is,
> the less sensible
> > the claim seems that there can be mathematical
> facts out of the
> > potential reach of human reason.
>
> It seems to me that it should be the other way
> 'round: it's harder to prove
> something constructively than to prove it
> classically. Unless you're
> redefining "mathematical fact" as "something that can
> be proven".
> --
This is true. There are existence proofs (Brouwer's
original proof for his fixed point theorem comes to mind)
that are tremendously useful and important, for which
a constructive proof may or may not ever materialize.
Tom
> Robert Israel
> isr...@math.MyUniversitysInitials.ca
> Department of Mathematics
> http://www.math.ubc.ca/~israel
> University of British Columbia Vancouver,
> BC, Canada
T.H. Ray
> unverifiable properties cannot be assigned a useful
> meaning
>
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> galathaea: prankster, fablist, magician, liar
>
No, this is easily counterexampled. E.g., Many conjectures
depend on the proven truth of the Riemann Hypothesis. One
can imagine that RH is an unprovable conjecture. That
would not render meaningless those conjectures which
depend on RH, in that the utility has already been
demonstrated.
Constructivism assumes that mathematics has meaning,
a priori. That is the main distinction between
constructivism and formalism.
Tom
Han de Bruijn
> LauLuna <laurea...@yahoo.es> writes:
>
>>On Oct 23, 3:57 pm, Victor Porton <por...@narod.ru> wrote:
>>
>>>For famous hypothesis such as Millennium Prize problems (or to be yet
>>>more specific for P=NP problem)...
>>>
>>>... how we can (or cannot) be sure that the hypotheses or its negation
>>> is provable.
>>>
>>>There are statements which are unprovable nor true nor false in ZFC.
>>>
>>>For a specific example can we be sure that either P=NP or P!=NP is
>>>provable?
>>
>>By 'provable' you don't seem to mean 'provable within some formal
>>system' but 'provable by human reason'.
>>
>>There is an issue about philosophy of mathematics involved here. From
>>a Platonistic point of view it's perfectly possible that some facts
>>concerning mathematical objects result unknowable for human reason,
>>since mathematical facts are objective facts and don't depend on the
>>power of human reason.
>>
>>But the more constructivist our point of view is, the less sensible
>>the claim seems that there can be mathematical facts out of the
>>potential reach of human reason.
>
> It seems to me that it should be the other way 'round: it's harder to prove
> something constructively than to prove it classically. Unless you're
> redefining "mathematical fact" as "something that can be proven".
Sometimes it's _easier_ to prove something constructively than to prove
it classically.
Han de Bruijn
Dave L. Renfro
>> It seems to me that it should be the other way 'round:
>> it's harder to prove something constructively than to
>> prove it classically. Unless you're redefining
>> "mathematical fact" as "something that can be proven".
Han de Bruijn wrote:
> Sometimes it's _easier_ to prove something constructively
> than to prove it classically.
No, this isn't true, because every constructive proof is
also a classical proof.
Dave L. Renfro
Dave L. Renfro
>>> It seems to me that it should be the other way 'round:
>>> it's harder to prove something constructively than to
>>> prove it classically. Unless you're redefining
>>> "mathematical fact" as "something that can be proven".
Han de Bruijn wrote:
>> Sometimes it's _easier_ to prove something constructively
>> than to prove it classically.
Dave L. Renfro wrote:
> No, this isn't true, because every constructive proof is
> also a classical proof.
However, it occurred to me just after I posted this that
forcing yourself to consider only constructive methods of
approach might, in some cases, lead you to a simpler proof
in those cases where there is a short constructive proof
which you might have overlooked if you weren't forced to
consider only constructive forms of reasoning.
Dave L. Renfro
galathaea
> > unverifiable properties cannot be assigned a useful
> > meaning
>
> > -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> > galathaea: prankster, fablist, magician, liar
>
> No, this is easily counterexampled. E.g., Many conjectures
> depend on the proven truth of the Riemann Hypothesis. One
> can imagine that RH is an unprovable conjecture. That
> would not render meaningless those conjectures which
> depend on RH, in that the utility has already been
> demonstrated.
i mentioned this in another thread
but i wanted to respond directly as well
i do not know why you think this a counterexample
if there is a constructive proof of the implication
then the implication is constructively true
the bhk semantics explicitly deal with
the meaning of implication
but just because the implication is meaningful
does not mean it is meaningful to assert RH
or to assert its implications
|- A->B
does not give us
|- A
or
|- B
> Constructivism assumes that mathematics has meaning,
> a priori. That is the main distinction between
> constructivism and formalism.
it does not need the a priori
or any kantian baggage
and in my opinion does best without it
that is precisely why i do not agree with intuitionism
constructivism only requires symbols have meaning
but are perfectly content in allowing that meaning
to be assigned a posteriori in linguistic formation
and only very primitive meanings are necessary
for quite elaborate constructions
eventually including turing completeness
tommy1729
> On Oct 25, 4:28 am, David C. Ullrich
> <ullr...@math.okstate.edu> wrote:
> > On Wed, 24 Oct 2007 17:57:05 GMT, Michael Press
> <rub...@pacbell.net>
> > wrote:
> >
> >
> >
> > >In article
> > ><ibiuh39cpcljngark7juncm853rda37...@4ax.com>,
> > > David C. Ullrich <ullr...@math.okstate.edu>
> wrote:
> >
> > >> On Tue, 23 Oct 2007 23:01:05 GMT, Michael Press
> <rub...@pacbell.net>
> > >> wrote:
> >
> > >> >In article
> > >>
> ><rbisrael.20071023142716$7...@news.ks.uiuc.edu>,
> > >> > Robert Israel
> <isr...@math.MyUniversitysInitials.ca>
> > >> > wrote:
> >
> > >> >> Victor Porton <por...@narod.ru> writes:
> >
> > >> >> > For famous hypothesis such as Millennium
> Prize problems (or to be yet
> > >> >> > more specific for P=NP problem)...
> >
> > >> >> > ... how we can (or cannot) be sure that the
> hypotheses or its negation
> > >> >> > is provable.
> >
> > >> >> We can't. In some cases we can do half of
> this: e.g. if the Riemann
> > >> >> hypothesis or Goldbach's conjecture happens
> to be false, then its
> > >> >> negation is provable. But if it is true,
> there is no guarantee that
> > >> >> there is a proof of that.
> >
> > >> >> > There are statements which are unprovable
> nor true nor false in ZFC.
> >
> > >> >> > For a specific example can we be sure that
> either P=NP or P!=NP is
> > >> >> > provable?
> >
> > >An algorithm is a procedure that takes input and
> > >terminates with a well-defined and asserted
> result.
> > >That it does terminate with the asserted result
> must be
> > >proven. Until we accept the proof, it is not an
> > >algorithm.
> >
> > Ridiculous. You are confusing "is an algorithm"
> > with "has been proven to be an algorithm".
> > They're not the same thing. I claimed that those
> > two things were algorithms. They are. I didn't
> > claim to have given _proofs_ that they were
> > algorithms. (As though that was difficult...)
> >
> > >The notion of right answer is not part of
> > >the definition of algorithm.
> >
> > >This is an algorithm that returns "yes".
> > >procedure say_no
> > > return "yes"
> > >end procedure
> >
> > >Proof:
> > > The procedure returns "yes" because the
> statement
> > > `return "yes"' is the first executed statement
> and
> > > therefore always executes.
> > >QED
>
> it is your approach that is considered ridiculous
> by many a foundationalist
what else did you expect from david ...
This is an algorithm that returns "yes".
procedure say_no
return "yes"
end procedure
algoritm to prove RH
by definition
say RH is true
because david says so
end algoritm
>
> unverifiable truth assignments
> have long been held suspect
> by many schools of thought
>
> stoic logicians challenged just such approaches
> for an example of early objections
> but the challenges are quite widespread
>
> unverifiable properties cannot be assigned a useful
> meaning
>
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> galathaea: prankster, fablist, magician, liar
>
regards
tommy1729
Keith Ramsay
|For famous hypothesis such as Millennium Prize problems (or to be yet
|more specific forP=NPproblem)...
|
|... how we can (or cannot) be sure that the hypotheses or its
negation
|is provable.
In none of the cases can we be sure yet, except of course
for the Poincare conjecture which has been proven.
A lot of famous conjectures have the property that if the
conjecture is false, a counterexample can in principle be
verified (using some standard axiom system). The Riemann
hypothesis is this way, for example. If zeta has a zero in
the wrong place, there's a calculation that would show that
it does. I can't swear to it, but I believe the Poincare
conjecture was like this before it was proven: a
counterexample could in principle be checked with a finite
calculation.
The Birch and Swinnerton-Dyer conjecture may not be
completely that way yet, but it's at least close. If there
is a counterexample, it's an elliptic curve (given by a
cubic equation y^2=x^3+ax+b where a and b are integers). One
has to confirm the order of the zero of a computable function
associated with the curve, which as with the zeta function
is possible in principle, and then show that the curve has
the "wrong number" of solutions of certain kinds. That last
part can probably be done in every case, but I'm doubtful
whether it's proven.
I don't know enough about the Hodge conjecture to know, but
I think it may also at least be close to the situation where
a counterexample would necessarily be demonstrable in a
familiar formal axiom system.
The problems having to do with Navier-Stokes and Yang-Mills
both have to do with the existence of solutions to PDEs.
Perhaps someone knows the status of such questions.
|There are statements which are unprovable nor true nor false in ZFC.
|
|For a specific example can we be sure that eitherP=NPorP!=NPis
|provable?
The P=NP problem has an amusing equivalent. First, as you
may know there are NP problems which have a kind of
"universal" property relative to the others, so that if one
of them is in P, then all of NP is in P too (the NP-complete
problems). Boolean satisfiability is a convenient example:
given a formula with variables combined by connectives "and",
"or", and "not", is it possible to substitute "true" or
"false" for the variables is such a way as to make the
formula evaluate to "true"?
P=NP is equivalent to the existence of an algorithm that
finds a solution within some polynomial time bound, if it
exists. Amusingly, we can write down an algorithm which does
this if any algorithm does. It's called a Levin universal
search. It enumerates possible searching algorithms A1,A2,...
and simulates them, giving them the problem as input,
spending approximately 1/2^n of its time simulating an
algorithm A_k if it takes n bits to represent A_k in a given
self-terminating language. By self-terminating, I mean that
the universal Turing machine that runs the program is able
to tell where the program ends just from the program itself.
If some algorithm A_t is a polynomial-time algorithm for
finding solutions to boolean satisfiability problems (when
they exist), then Levin's search is such an algorithm too.
It just takes 2^N times as long, where N is the number of
bits in A_t. This is impractical, but in principal the Levin
search will find a solution in polynomial time too, just
with a huge constant factor.
So P=NP can be rephrased as a question about how long the
Levin search might take to find solutions.
Each polynomial is bounded above by n^C + C for some integer
C. First take C0 to be bigger than the degree. Then increase
it enough to deal with the (finitely many) cases where
n^{C0}+C0 is less than the polynomial. For each case of the
problem where a solution exists, whose length is n, we can
ask, what is the smallest value of C such that the Levin
search finds a solution within n^C+C steps? If there is some
fixed C that is large enough for all cases, then P=NP. If
the needed value of C is unbounded, then P<>NP. Thus P=NP is
equivalent to some computable sequence of integers being
bounded.
There's no fixed formal system in which if a computable
sequence of integers is bounded, then the boundedness can
be proven in the system. If there is no upper bound, then in
a vague sense it's even further from true that the
unboundedness would necessarily be provable in a given system.
One has to prove that for each candidate bound, there exists
a problem with a solution that Levin search takes longer than
that bound to find.
Keith Ramsay
Keith Ramsay
On Oct 25, 4:07 pm, Robert Israel
<isr...@math.MyUniversitysInitials.ca> wrote:
|LauLuna <laureanol...@yahoo.es> writes:
[...]
|> There is an issue about philosophy of mathematics involved here.
From
|> a Platonistic point of view it's perfectly possible that some facts
|> concerning mathematical objects result unknowable for human reason,
|> since mathematical facts are objective facts and don't depend on
the
|> power of human reason.
|
|> But the more constructivist our point of view is, the less sensible
|> the claim seems that there can be mathematical facts out of the
|> potential reach of human reason.
|
prove
|something constructively than to prove it classically. Unless you're
|redefining "mathematical fact" as "something that can be proven".
Constructive and nonconstructive mathematics are different
enough as conceptual structures to make it tricky to make
comparisons of definitions between them like this.
When one sets out to exhibit a possible example of something
that's true but unprovable, nonconstructively, one allows
oneself constructions such as the following. Suppose we have
a collection {A_i}_{i in I} of statements which we know are
not all false, and which are mutually contradictory. Then we
say, using classical logic, that exactly one of them is true,
and we can go on to refer to "the one that's true". Obvious
examples would be {p, "p is false"} for various statements p.
The fact that one doesn't allow this kind of thing as a
construction of a statement (constructively) doesn't mean
that one is adopting an unusually narrow definition of "fact"
or "true". There's a sense in which one is being more strict,
but in a less heavy-handed way than if one simply redefined
"truth" to be "proven truth".
Classically, one describes the situation by saying things
like, "one of {p,q} is true but we don't know that either
can be proven". The same situation is described with
essentially the same factual content constructively by
saying "p and q are not both false, i.e. ~(~p & ~q), but we
don't know that 'p or q' holds". In a constructive system,
or just speaking informally of provability, the provability
of "p or q" is equivalent to either p being provable or q
being provable. This assertion that "one of p or q is true"
may seem like some remarkable new fact provided by classical
logic, but the essential content is the same as ~(~p & ~q)
(assuming we've dealt with any issues concerning the meaning
of p and q already).
I don't generally identify truth with provability, and I
don't see that it's done very often, perhaps because it's
just unnecessary, perhaps because it's not so helpful. It's
one of the issues related to the Brouwer-Heyting-Kolmogorov
(BHK) interpretation of the quantifiers, however. The way
implication, ->, is interpreted is that "p->q" is taken to
mean that there is a procedure for converting a proof of p
into a proof of q (and in some possibly vague sense we can
demonstrate that it works). If q = "p is provable", then
p->q is interpreted to mean that from a proof of p we can
produce a proof that p is provable (which we can, of course).
So by interpreting connectives this way, BHK has a way of
operating as if all the statements were identified with their
(intuitive) provabilities.
Keith Ramsay
T.H. Ray
> wrote:
> > > unverifiable properties cannot be assigned a
> useful
> > > meaning
> >
> > > -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> > > galathaea: prankster, fablist, magician, liar
> >
> > No, this is easily counterexampled. E.g., Many
> conjectures
> > depend on the proven truth of the Riemann
> Hypothesis. One
> > can imagine that RH is an unprovable conjecture.
> That
> > would not render meaningless those conjectures
> which
> > depend on RH, in that the utility has already been
> > demonstrated.
>
> i mentioned this in another thread
> but i wanted to respond directly as well
>
> i do not know why you think this a counterexample
>
It's clearly a counterexample to your claim.
"Unverifiable properties" applies to any assigned
value. Verifiability, in fact, is not a constructive
concept. To try and make it so begs the principle
of the excluded middle which AFAIK all constructive
schools reject.
> if there is a constructive proof of the implication
> then the implication is constructively true
>
> the bhk semantics explicitly deal with
> the meaning of implication
>
> but just because the implication is meaningful
> does not mean it is meaningful to assert RH
> or to assert its implications
>
> |- A->B
>
> does not give us
>
> |- A
>
> or
>
> |- B
>
You are discounting the three valued logic of
constructive proof, that includes "not proven."
> > Constructivism assumes that mathematics has
> meaning,
> > a priori. That is the main distinction between
> > constructivism and formalism.
>
> it does not need the a priori
> or any kantian baggage
> and in my opinion does best without it
>
Opinion noted.
> that is precisely why i do not agree with
> intuitionism
>
> constructivism only requires symbols have meaning
> but are perfectly content in allowing that meaning
> to be assigned a posteriori in linguistic formation
>
That requirement would destroy the distinction between
constructivism and formalism.
> and only very primitive meanings are necessary
> for quite elaborate constructions
> eventually including turing completeness
>
Even primitive meanings are a priori, are they not?
Whether they are assigned or not, is then moot.
Tom
tommy1729
> On Oct 25, 3:47 pm, MoeBlee <jazzm...@hotmail.com>
> wrote:
> > On Oct 25, 12:54 pm, galathaea
> <galath...@gmail.com> wrote:
> > > On Oct 25, 11:38 am, MoeBlee
> <jazzm...@hotmail.com> wrote:
> > > > On Oct 25, 10:35 am, galathaea
> <galath...@gmail.com> wrote:
> > > > > On Oct 25, 10:13 am, MoeBlee
> <jazzm...@hotmail.com> wrote:
> > > > > > On Oct 24, 8:58 pm, Michael Press
> <rub...@pacbell.net> wrote:
> >
> > > > > > > A theorem is not a theorem until it is
> proven.
> >
> > > > > > A sentence S is a theorem of a set of
> sentences G iff there is a proof
> > > > > > of S from G.
> >
> > > > > > But what does "until" mean in this context?
> >
> > > > > constructivists almost universally seat
> properties in time
> >
> > > > I'm not expert on the subject, but I recognize
> that certain
> > > > constructivists have notions that might be
> thought of, more or less
> > > > loosely, as temporal. However, it seems to me
> that in intuitionistic
> > > > mathematics, this can be formalized without a
> literal temporal
> > > > component.
> >
> > I'm writing this response primarily in the interest
> of not allowing it
> > to seem as if my questions have been addressed by
> your post that seems
> > to take my points as much more naive than they are,
> as, at this point,
> > I'm not hopeful that much worth can came from our
> exchanges now.
>
> go fuck yourself
> you sanctimonious ignorant piece of shit
>
> i did nothing to you but try to answer your questions
>
> you draw first blood
> and then pretend a reactionary pose?
>
> great way to back down from a position
> and still try to save face...
>
> > > anything that can be formalised
> > > can be formalised in a completely meaningless
> game of symbols
> >
> > My point was that while I understand that one might
> describe the
> > temporal notion as part of the intutive motivation,
> one can work in
> > the formalized mathematics without then using
> anything about time
> > itself. In particular, it's still not been shown
> that a notion of time
> > is required to define 'theorem'. Indeed, for
> example, I don't see a
> > notion of 'time' mentioned in the definition of
> 'proof in the
> > intuitionisitic predicate calculus'. What I do see
> is a perfectly
> > explicit mathematical definition.
>
> yes
>
> as i said:
> anything that can be formalised
> can be formalised in a completely meaningless game
> me of symbols
>
> you are apparently starting to show
> a complete lack of understanding
> of the distinction of semantics and syntax
>
> do _you_ have a different theory of meaning?
>
> i actually thought you knew these basic objects of
> model theory
> seeing as you are often telling people (like
> ke zuhair)
> to go read a textbook
>
> why don't you?
>
> st evaluation
>
> do you object to the more general framework?
>
> seriously
> your comment makes it sound like you have
> no grasp of the concept of quantifiers
>
> you say you want to see "theorem of X" used where it
> needs proof
> (yet seem to not be aware that that is the bhk
> hk semantics)
> you say you want to see "algorithm for Y" vary over
> time
> (program verification languages often use
> temporal specification logics like ltl and ctl)
>
> this is a deep topic and requires much exposition
>
> does that sound familiar?
>
> > > kripke models
> > > the most common semantic setting for heyting
> algebras
> > > are inherently temporal
> > > for the same reason the semantic interpretation
> of "possibility"
> > > is inherently temporal
> >
> > Whatever "inherently" means here, the point I was
> getting at is that
> > one can take Kripke models to be perfectly exact
> formal mathematical
> > objects and that to work with them one would do
> well to appreciate the
> > intuitive motivation (which I can understand being
> described as
> > 'temporal') but in the actual mathematics one does
> not need to invoke
> > any principles regarding time whatsoever.
>
> and i showed i could not understand your point
> by agreeing that all formalisation can be
> meaningless...??!
>
> > And again, whatever the case about this, we've
> still not seen here a
> > reference to such definitions of 'theorem' that
> mention time.
>
> although this is pretty common throughout the field
> so i'd have hoped you'd have "picked up a textbook"
> k" to get it
> artemov writes in the paper i linked:
>
> " Such a reading of modality naturally appears in
> dynamic and
> temporal logics aimed at describing computational
> al processes,
> the states of which usually form a (possibly
> ly branching)
> Kripke structure. "
>
> so yes
> "we" have seen here just such a reference
>
> but i've mentioned bhk too...
>
> really
> moe
> i have not seen such a lack of content in your posts
> before
> (though i have seen belligerence)
> so what gives?
>
> you really have _never_ seen a semantics
> that requires proof before a statement is
> is considered true?
>
> you've never seen the _reasons_ for tertium datur?
>
> > > > > do you understand why constructivists
> > > > > reject ullrich's dichotomy?
> >
> > > > Due to my own personal unfamiliarity with
> Ullrich's notation, I don't
> > > > opine on the example Ullrich gave. But more
> generally, are you saying
> > > > that there is a definitely articulated
> constructivst notion of
> > > > 'algorithm' that includes that something is not
> an algorithm until
> > > > proven to be an algorithm? If so, would you
> recommend a book or
> > > > article that I can read about that?
> >
> > > i am unfamiliar with a specific singling out of
> "algorithm"
> > > since constructivists tend to have strongly
> operational views
> > > on all properties
> >
> > Then I really don't follow you. We were talking
> about definitions of
> > 'algorithm'; then you raised the matter of
> constructivism; now you
> > demur to connect constructivism with a defintion of
> 'algorithm'.
>
> seriously
> at this point i am starting to suspect
> you are either much less capable than i had
> had surmised from previous
> posts
> or something crawled up your ass
> and you now can't stop yourself from arguing
>
> i made the connection
>
> when you ask:
> how is 4 even?
> and i reply:
> all integers of the form 2x are even
>
> it really is answering your question
> no matter how hard you squint your eyes or shake your
> head
> or whatever you are doing to skip over it
>
> michael press gave an operational definition of
> algorithm
>
> to call something an algorithm for a particular task
> you must have a verification that the task gets
> accomplished
>
> others thought it a strange way to treat algorithms
> whereas to me it was quite natural
>
> operationalism and constructivism are intimately
> related
> so i brought up why it was natural
> and common
>
> there is a lot of depth here
> and it appears you are dismissing shallowly
>
> > And, Ullrich's example is
> > not at issue with me, as I already mentioned that
> I'm not commenting
> > upon it specifically. What I did say is that I'd
> like to see where
> > such definitions of 'theorem' and 'algorithm'
> appear. Your reiterating
> > that the law of excluded middle is not accepted in
> most (all?)
> > constructivism does not answer the question as to
> where one might find
> > such definitions of 'algrorithm' and 'theorem'.
>
> this is where you seem to get dangerously avoidant
>
> you appear to claim knowledge of bhk semantics
> but have not seen that a system
> where a theorem is true when it has been proven?
>
> go read a fuckin' book you cranky crackpot!
>
> " It does not make sense to think of truth or falsity
> of a mathematical statement independently of our
> ur knowledge
> concerning the statement. A statement is true if we
> we have a
> proof of it, and false if we can show that the
> he assumption
> that there is a proof for the statement leads to a
> contradiction. " - famous math guys in a famous
> us book somewhere
>
> you claim to be well aware of the intuitionist
> reasons for tertium
> datur
>
> can you express those reasons
> without reference to progressive states of
> of knowledge?
>
> can you state the reasons with a static notion of
> truth?
>
> > > it has everything to do with time
>
> listen moe
>
> you need to check yourself
>
> i came into this thread to point out
> that michael press's position is very common
>
> for someone who has attacked others for posting
> without knowing
> you are demonstrating to the entire world
> ( well - that fraction that reads usenet
> and happens to check this post
> and has the appropriate background
> and... well you get the qualification)
> that you yourself do the same thing
>
> that's fine
> how else are you gonna learn, right?
>
> but understand that you will not get away with
> innuendo
> that you are doing the world a favor
> by sighing heavily and implying that i am unwilling
> to explain deeper
>
> he conversation?
>
> you even post your feelings!
>
> remember what you kept telling zuhair
>
> that's right
> go read some fuckin' books...
>
> start with the pair by troelstra and van dalen
>
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> galathaea: prankster, fablist, magician, liar
>
im not here to judge.
i just wanted to say galathaea is sexy when she is pissed :)
sexy math babe :D
neilist
<snip>
> what else did you expect from david ...
>
> This is an algorithm that returns "yes".
> procedure say_no
> return "yes"
> end procedure
>
> algoritm to prove RH
>
> by definition
>
> say RH is true
> because david says so
> end algoritm
Tommy, stop being childish. Your comments in this thread aren't math,
so shut up.