HDTenEightyP/NetNews huggingface dataset:
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Newsgroups: sci.logic
Subject: Re: What is Computer Science (was: Natural Kinds)
Date: 18 Nov 92 13:42:23 GMT
Organization: SAS Institute Inc.
Originator: sasghm@theseus.unx.sas.com


In article <BEVAN.92Nov17144906@beluga.cs.man.ac.uk>, bevan@cs.man.ac.uk (Stephen J Bevan) writes:
|> In article <Bxt9GA.Iyp@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
|> 
|>    In article <BEVAN.92Nov11113345@hippo.cs.man.ac.uk>, bevan@cs.man.ac.uk (Stephen J Bevan) writes:
|>    |> What are "etc." in this case?  I'm still waiting to see any mention of
|>    |> a "science" that isn't (IMHO) a "natural science".
|> 
|>    Well, there are some who consider the social sciences (anthropology,
|>    sociology, psychology) to be sciences.
|> 
|> But why?  What attributes do they possses that makes them a "science"
|> that computer science (sic) does not have?  (Maybe we need somebody
|> who considers them as a science to answer this question).

The classical answer here is straightforward and centers around the
use of the hypothetico-deductive method and deductive-nomological
explanations.  One may argue (and I certainly would at least in
some cases) that these are ill-applied in various social sciences,
but the fact that they *are* a central part of the methodology, and
the fact that the gathering and analysis of empirical evidence
plays a central role in theory acceptance/rejection, and the fact
that one attempts to formulate *empirical* theories in these
disicplines all argue that they *are* sciences.

For a brief but reasonable treatment of the fundamental issues,
some good little books are

	Philosophy of Natural Science (Carl Hempel)
	Philosophy of Social Science (??? I forget the author)
	Philosophy of Biological Science (David Hull)

all part of a series published by Prentice-Hall.

The degree to which (or the specific areas in which) computer science
exhibits these characteristics is still pretty unclear to me.
-- 
Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm
Newsgroups: sci.logic
From: fokp@vccsouth26.its.rpi.edu (Ben Fok the "lemming")
Subject: letter
Keywords: letter
Reply-To: fokp@rpi.edu
Organization: Rensselaer Polytechnic Institute, Troy, NY.
Date: Mon, 16 Nov 1992 00:04:09 GMT


everybody's roomate got letter but nobody recieved any letter.
Why?


Newsgroups: sci.logic,sci.math
From: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: Logic and Mathematicians
Organization: Boise State University
Date: Mon, 16 Nov 1992 16:49:12 GMT

In article <1992Nov15.191744.17481@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:
>In article <1992Nov15.220359.21971@guinness.idbsu.edu>
>holmes@garnet.idbsu.edu (Randall Holmes) writes:
>
>>In article <1992Nov14.141234.26280@email.tuwien.ac.at>
>>zach@csdec1.tuwien.ac.at writes:
>
>>>In article <1992Nov12.204959.17389@husc3.harvard.edu>,
>>>zeleny@husc10.harvard.edu (Michael Zeleny) writes:
>
>MZ:
>>>>I offer Post's problem as a counterexample.  Also, it doesn't seem
>>>>that there could be a solution for "P =? NP" that would render the
>>>>problem silly in retrospect.
>
>RZ:
>>>Oh yes: Prove P=NP is independent of ZFC. It actuall HAS
>>>been shown independent in some weak arithmetics.
>
>Funny, I would have thought independence to be indicative of
>foundational profundity, rather than triviality.
>
>>>-- 
>>>Richard Zach                         Technische Universitaet Wien
>>>[zach@csdec1.tuwien.ac.at]     Abteilung fuer Formale Logik 185.2
>
>RH:
>>Wouldn't that actually answer the question?
>
>Only from the standpoint of a formalist.

No, I think it might answer it from a realist standpoint, but I'm
having trouble chasing quantifiers around in my head; I can't tell
without sitting down and thinking about it, and I have things to do...
I was hoping that someone would know the answer.


>
>>-- 
>>The opinions expressed		     --Sincerely,
>>above are not the "official"	     M. Randall Holmes
>>opinions of any person		     Math. Dept., Boise State Univ.
>>or institution.			     holmes@opal.idbsu.edu
>
>cordially,
>mikhail zeleny@husc.harvard.edu
>" -- I shall speak bluntly, because life is short."


-- 
The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@opal.idbsu.edu
Newsgroups: sci.logic
From: gavan@elc.mth.uct.ac.za (Gavan Tredoux)
Subject: Re: implication truth table
Date: Thu, 19 Nov 92 19:56:42 GMT
Organization: University of Cape Town
X-Newsreader: Tin 1.1 PL4

mclean@itd.nrl.navy.mil (John McLean) writes:
: From cmitchell@falcon.aamrl.wpafb.af.mil ()
: >My question is: WHY is the implication relation defined as it is?

[some reasons]

There are logics that don't allow this paradox of
material implication - relevance logics, where the antecedent
and consequent have to be relevant to each other for the
implication to hold. Of course there are a million and one
ways of doing this.

Primary strength of classical logic: there's only one.

Gavan Tredoux
UCT
From: cmitchell@falcon.aamrl.wpafb.af.mil
Newsgroups: sci.logic
Subject: implication truth table
Date: 16 Nov 92 16:27:33 EST
Organization: USAF AL/CFH, WPAFB, Dayton, OH

Greetings -

I'm doing a first course in real analysis and have a question about
the implication relation.

I've asked 3 professors and checked 3 text books so far and have no
satisfying answer.

Truth Table for `A implies B' (If A Then B):

	A	B	->
	F	F	T
	F	T	T
	T	F	F
	T	T	T

Consider the following sentence:
	IF it is sunny tomorrow, THEN I will go to the ball game.

My expectation was that:
	if   it is not sunny,
	then I would have no way of determining the truth of the implication.

My question is: WHY is the implication relation defined as it is?

My best speculations so far are:

	1- because it gives us an internally consistent system.
	   (this seems like the easy way out to me, but what do
	    I know?)

	2- my expectation (above) seems to have a temporal assumption
	   within it (a kind of cause and effect?).
	   this would seem contrary to the spirit of what is intended
	   when a mathematician speaks in terms of IF-THEN, but I can
	   get no farther with this line of reasoning on my own.

	3- there are simply differences between the language of Math
	   and the language of English and mathematicians have agreed
	   to speak Math to one another.
	   I suppose this would hearken back to number 1.

	4- the accepted definition allows implications like
	   A->B->C  to have an intuitively satisfying interpretation.
	   (again this seems arbitrary rather than reasoned).


Thanks in advance for any responses.

-- 

"The opinions and views expressed here are strictly my own and do not 
necessarily reflect the official position of either the U.S. Air Force 
or its contractors."

Newsgroups: sci.logic
From: torkel@sics.se (Torkel Franzen)
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Organization: Swedish Institute of Computer Science, Kista
	<369@mtnmath.UUCP>
Date: Sat, 21 Nov 1992 18:54:45 GMT


   >Everything in mathematics is "relative" to some formal system. To talk
   >about what is absolutely true independent of a formal system is philosophy
   >not mathematics.

  The distinction is quite simple. "Provability in T" is an example of a
concept that has a formal system as a parameter, "uncountable" is an
example of a concept that has no formal system as a parameter, whether
explicit or implicit.

  "Absolute truth" has nothing to do with this. It's just a matter of what
we say and mean in mathematics. The notion that "everything in mathematics is
relative to some formal system", on the other hand, is the expression of
some philosophical doctrine.
Newsgroups: sci.logic
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: recursive definitions and paradoxes
Originator: sasghm@theseus.unx.sas.com
Date: Fri, 20 Nov 1992 19:12:21 GMT
Organization: SAS Institute Inc.


In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
|> ]
|> ]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> ]
|> ]|> I propose for discussion the
|> ]|> 
|> ]|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
|> ]|> 
|> ]|> where "Exist! x" means "there exists a unique x such that".  What if you
|> ]
|> ]I have not *carefully* read the rest of this posting.  However, on
|> ]the face of it, it appears that this "axiom of definition" is quite
|> ]suspect.  I'm not sure what
|> ]
|> ]	X := E
|> ]
|> ]means.  If it is really intended to represent a *definition* of X,
|> ]then why is the new axiom necessary? What exactly is the symbol
|> ]':=' meant to express beyond (or short of) '='?
|> 
|> The symbol '=' alone does not point out what variable is being
|> defined, but ':=', (which is defined formally by its usage) does.  I
|> did not discuss the rules for introducing X := E because they seemed
|> uninteresting.  It is clear that you need syntactic rules to avoid
|> naming conflicts and that rules must cover a range of clauses in a
|> proof.  That is, a definition has a scope that includes more than just
|> the clause in which it is introduced.  Clearly, no axiom or normal
|> rule of inference is adequate to specify this.

"Defined formally by its usage"?? "They seemed uninteresting"?
Things are particularly confusing since in the proposed Axiom of Definition
it appears that what is "defined" in

	X := E

is a 0-place operation symbol (X) (i.e., a term).  What does it mean to
provide a recursive definition for such an expression?  If ':=' is a
binary relation symbol, it would be nice to have some clue concerning the
properties of the relation in question.  This is not uninteresting, but
essential.

As it is, all we have is the proposed Axiom of Definition, which we can
take as a *partial* formalization of ':='.  This is not enough.

For example, it is possible to think of the Axiom of Definition as being
proposed in a free logic where '=' has the usual semantics according to
which

	x = y

is true just in case x and y both denote and have the same extension,
but where ':=' has the semantics that

	x := y

is true just in case either both denote and have the same extension *or*
both are denotationless.  The Axiom of Definition is sound under such
an interpretation (given the usual interpretation of the quantifiers).
I am sure that this is not your intention, but nothing you say appears
to rule it out.

Either a little more precision and formalization or, failing that, some
specific examples of such "definitions" would be an aid to the understanding.
-- 
Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm
Newsgroups: sci.logic
From: ian@nasser.eecs.nwu.edu (Ian Sutherland)
Subject: Re: Lowneheim-Skolem theorem
Organization: EECS Department, Northwestern University
Date: Mon, 23 Nov 1992 22:36:55 GMT

In article <367@mtnmath.UUCP> paul@mtnmath.UUCP (Paul Budnik) writes:
>In article <1992Nov20.140159.4770@sun0.urz.uni-heidelberg.de>, gsmith@l
auren.iwr.uni-heidelberg.de (Gene W. Smith) writes:
>> "Uncountable" means no one-to-one relation with the integers
>> can be given.  This does not refer to a formal system.
>
>Unless you have a formal system in which to determine what constitutes
>a one-to-one relationship you are not doing mathematics.

If this is so Mr. Budnik, then what do you call the activities of all
those people in math departments all over the world who don't even know
the STATEMENT of the Lowenheim-Skolem theorem?  I.e., probably most
working mathematicians who are not logicians?  You may call it
"philosophy", but the rest of the world calls it "mathematics".  The
people that do this "mathematics" which you insist is "philosophy"
don't look at formal systems to tell them what constitutes a one-one
relationship.  You can say that they're operating without foundations
(they'd probably be glad to agree!), or you can say they're just a
bunch of Platonists, but it is an abuse of language to insist that
they're doing "philosophy".
-- 
Ian Sutherland
ian@eecs.nwu.edu

Sans Peur
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 21 Nov 92 17:58:05 GMT
Organization: U of Arizona CS Dept, Tucson

In article  <1992Nov20.210803.5903@tamsun.tamu.edu> Chris Menzel writes:
]
]It seems to me, David, that you cause unnecessary confusion by calling
]these and, as you do later in your post, the definition of the Russell
]set recursive definitions.  By my lights, the usual understanding is
]that a recursive definition is one in which a function f is defined on
]a well-founded relation R such that for each object b in the field of
]R, f(b) is defined in terms of f(x) for x such that xRb.

This is a limited form of recursion, not the general form that is used
in the lambda calculus and combinatory calculus.  In general a
function definition

  f(x) := E

(where ':=' is usually an equals with a triangle, a dot, or another
bar over it) is recursive if f appears on the right-hand side.  Such a
definition is taken to define the function that satisfies the equation

  f(x) = E

Of course in general there are many such functions, so to get a unique
solution we assume that the above definition defines f as the least
fixed point of the function F defined by

  F(f) := \x.E

In the days of Peano there was no fixed point theory, and even
induction was suspect, so recursion was severely restricted.  And
since the domain (the natural numbers) is totally ordered the result
is that Peano's recursive definitions define unique functions even
without taking the least fixed point (I think).  But restricted forms
of recursion are more properly named with the restriction, as in
"primitive recursion".  As I recall, there are several versions of
Peano arithmetic, each with a slightly different restriction on what
counts as a legal recursive definition.

]Since you say at the beginning of your note what *you* mean by a
]recursive definition, my comment here is essentially a quibble that
]doesn't address the substance of your remarks.  But if you are in fact
]using such a deeply entrenched term in a nonstandard fashion, you
]would seem to be a lot better off calling the notion you've defined
]something else.

I think this just is a difference in cultures (so I'm glad I had a
chance to clarify this).  My notion of recursion should be quite
familiar to anyone who knows the modern work in the lambda calculus.
Within the tradition I am familiar with, I can't imagine what else you
would call a definition X := E where X occurs in E and the sentence is
taken to define X as the unique solution to X = E.  As you observed
yourself, X can be viewed as a zero-adic function, in which case this
is real functional recursion.

I prefer to generalize in the other direction though, saying that
recursive definitions always define names rather than function
symbols, and that

  f(x) := E

is just a convenient form of the more basic

  f := \x.E

which is just a convenient form of the even more basic

  Def f . f = \x.E
-- 
					David Gudeman
gudeman@cs.arizona.edu
From: brendan@cs.uq.oz.au (Brendan Mahony)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 23 Nov 92 01:26:54 GMT
Reply-To: brendan@cs.uq.oz.au

In <1992Nov20.155725.11719@guinness.idbsu.edu> holmes@garnet.idbsu.edu (Randall Holmes) writes:

>This is inaccurate.  Russell's paradox proves nothing except that
>there is no set which has exactly the sets which are not elements of
>themselves as members.

Come on Russel's `paradox' tells us that if we assume
 
	(RS \in RS) or \lnot (RS \in RS)
 
we are in lots of trouble.
   
--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."
From: paul@mtnmath.UUCP (Paul Budnik)
Newsgroups: sci.logic
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Date: 20 Nov 92 16:40:54 GMT
Organization: Mountain Math Software, P. O. Box 2124, Saratoga. CA 95070

In article <TORKEL.92Nov19201017@lludd.sics.se>, torkel@sics.se (Torkel Franzen) writes:
> In article <363@mtnmath.UUCP> paul@mtnmath.UUCP (Paul Budnik) writes:
> 
>    >I think we can learn a lot more
>    >about the notion of a real number from such research than we can
>    >from proving theorems related to the continuum hypothesis.
> 
>   I have no objection to your inventing whatever mathematics you are
> capable of, on the basis of any ideas whatever. My negative comments
> are directed only at the notion that results in logic "show" that second
> order non-finitary concepts are not well-defined, or that we can do
> without them.

I have not claimed that these concepts are either not well defined or that
results in logic show we can do without them. My objection is a philosophical
one and centers on the assumption that mathematics requires quantification
over the reals be based on non-finitary concepts. You cannot define
the ordinal of the recursive ordinals without quantifying over the reals.
This is an important and useful concept. Does this mean that we must accept
that the set of all reals as a completed infinite totality? I do not think so.
I think the notion of an arbitrary path in a recursively enumerable tree is
meaningful even though I think the set of all reals is not.

Paul Budnik
Xref: sparky sci.logic:2160 sci.philosophy.meta:2682
From: ard@cs.bham.ac.uk (Antoni Diller)
Newsgroups: sci.logic,sci.philosophy.meta
Subject: Re: Feyerabend, Kuhn, Lakatos, and Popper one school? (was re: Natural Kinds)
Date: 23 Nov 92 18:08:21 GMT
Organization: School of Computer Science, University of Birmingham, UK

In article <1992Nov12.145454.7709@ucthpx.uct.ac.za> gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:
>
>In particular, Kuhn Lakatos and Popper have *rather* a lot in common.
>It's just that Popper doesn't think so. In fact Lakatos always
>presented himself as a Popperian (Popper declined the honour) while
>Kuhn cites Popper as a major influence (Popper reacted vehemently).
>
>Gavan Tredoux
>UCT 

There are close links of all sorts between these philosophers.  If you
read Kuhn's early work, like ``The Copernican Revolution'', he there
is more Popperian than Popper, putting forward what later came to be
known as naive falsificationism.  Lakatos's notion of a scientific research
programme is very similar to the earlier Popperian notion of a
metaphysical research programme.  The more I read Popper the more I
think that these other philosophers have very little original to offer.
One of the probles has been that Popper has written vastly more than
he has published, though he has lectured on this new material.  I guess
a lot will appear when he dies.


Antoni Diller
Newsgroups: sci.logic
From: hardy@elc.mth.uct.ac.za (Hardy Hulley)
Newsgroups: sci.logic
Subject: Re: Looking for proof checking/building software for teaching
Date: 23 Nov 92 23:43:10 GMT
Article-I.D.: ucthpx.1992Nov23.234310.28222
Organization: University of Cape Town
X-Newsreader: Tin 1.1 PL4

sjt@ukc.ac.uk (S.J.Thompson) writes:
: I am looking for software to support teaching propositional and predicate
: logic at undergraduate level. Specifically, I would like software for the
: IBM PC or for Sun workstations which support the interactive construction of
: proofs. I will post a summary of responses, assuming I receive any, to the
: net.
: 
: Many thanks
: 
: Simon Thompson
 
Last year we wrote a very simple Predicate Calculus proof-checker which runs
on top of Cambridge University's HOL theorem prover. We had exactly the same
idea as you have - we got undergraduate students to construct their proofs
in the system, and the proof-checker then checked the validity of these proofs.

The HOL software runs beautifully on a Sun workstation, and writing a system
especially for Predicate Calculus is a simple exercise.

Hardy Hulley

Lab. for Formal Aspects and Complexity in Computer Science
University of Cape Town



 
Newsgroups: sci.logic
From: frank@Cookie.secapl.com (Frank Adams)
Subject: Re: recursive definitions and paradoxes
Date: Mon, 23 Nov 1992 19:58:09 GMT
Organization: Security APL, Inc.

In article <26841@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
>]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
>]|> I propose for discussion the
>]|> 
>]|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
>]|> 
>]|> where "Exist! x" means "there exists a unique x such that".  What if you
>]
>]... Definitions must
>]satisfy such criteria as non-creativity (you can't prove something
>][in "old" notation] by using the definition that you couldn't
>]without it) and eliminability (the defined notation must be eliminable
>]in *all* contexts).  The fact that the above axiom is being suggested
>]seems to imply that the proposed "definition" does not satisfy the
>]criterion of eliminability...
>
>Exactly.  Actually, my notion of definition does not satisfy either of
>the two notions you mention.  Recursive definitions are creative and
>non-eliminable, and for that reason they have to be protected with an
>axiom that limits their use.

This statement is at best misleading.  The proposed notion of definition,
with the axiom given, *is* eliminable (and hence non-creative), as I have
noted in another posting.  *Without* the axiom given, it is of course also
eliminable -- you can prove something about X given X := E iff you can
prove it about a free variable X.  Only with the naive axiom of definition
is it not eliminable -- and then it is inconsistent.

There are other axioms which could be added which would make this kind of
definition non-eliminable, and David may have some such in mind.  No such
have been presented, however.
Newsgroups: sci.logic
From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: implication truth table
Organization: Computer Science Department,  Stanford University.
Date: Thu, 19 Nov 1992 22:30:28 GMT

In article <1992Nov19.195642.15296@ucthpx.uct.ac.za> gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:
>mclean@itd.nrl.navy.mil (John McLean) writes:
>: From cmitchell@falcon.aamrl.wpafb.af.mil ()
>: >My question is: WHY is the implication relation defined as it is?
>
>[some reasons]
>
>There are logics that don't allow this paradox of
>material implication - relevance logics, where the antecedent
>and consequent have to be relevant to each other for the
>implication to hold. Of course there are a million and one
>ways of doing this.
>
>Primary strength of classical logic: there's only one.

This is true for intuitionistic logic as well, which has only one
implication up to logical equivalence.  A->B is the weakest
interpretation of this implication for which modus ponens remains
sound, that is, the weakest C such that A&C |- B.  Assuming only the
cut rule and A|-A, this uniquely determines A->B up to logical
equivalence, where logical equivalence of A and B means A|-B and B|-A.
This definition may seem less paradoxical than the classical definition
of A->B as "~A or B".
-- 
Vaughan Pratt	  		A fallacy is worth a thousand steps.
Newsgroups: sci.logic
From: wft@math.canterbury.ac.nz (Bill Taylor)
Subject: Re: Why Logic?
Organization: Department of Mathematics, University of Canterbury
Date: Wed, 18 Nov 1992 01:55:29 GMT


|>    Can anyone explain why we use logic? Unfortunately, any logical arguments to
|>    support logic, are unfortunately, invalid.
|> 
|> Because if you don't use logic we'll kill you.

This may actually have happened once !!!!!


From that grand old corny western, "Gunfight at O.K. Coral".....

Doc:   Where's your logic, Wyatt ?
Wyatt: To hell with logic; that's my brother lying there !