HDTenEightyP/NetNews huggingface dataset:
From: alti@dcs.ed.ac.uk (Thorsten Altenkirch)
Newsgroups: sci.logic
Subject: Re: Types of type theory
Date: 13 Nov 92 13:15:46 GMT
Organization: LFCS, Edinburgh

In article <1992Nov12.144654.7493@ucthpx.uct.ac.za> gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:

   dzik@access.digex.com (Joseph Dzikiewicz) writes:
   : I have come across two uses of the term "type theory" in logic that seem
   : to be referring to different things.

   ...

   Type theory *is* higher-order logic, where the types are used to
   avoid the paradoxes. One version -- the one Andrews explains --
   is Church's Simple Theory of Types. There are others -- the Ramified
   Theory of types (Ramsey) and the original, Russell's type theory.

   The Simple Theory of Types is just Predicate Calculus 
   enriched with typed lambda calculus. 

There is still another type of type theory for which the most famous
example is Martin-L"of's Type Theory. Here types and propositions are
identified, i.e. a proposition is the type of its proofs. This may
seem unusual but it leads to a very elegant formalisation of
mathematical concepts. This sort of Type Theory is inherently
intuitionistic because every proof has to have a constructive content.
(I should mention that there is some work going on in extending this
to classical reasoning).

--

 Thorsten Altenkirch         	And there's a hand, my trusty fiere,
 Laboratory for Foundations  	   And gie's a hand o' thine,
 of Computer Science 	      	And we'll tak a right guid-willie waught
 University of Edinburgh     	   For auld lang syne!
Xref: sparky sci.logic:1984 sci.philosophy.meta:2477
From: Robert.Vienneau@launchpad.unc.edu (Robert Vienneau)
Newsgroups: sci.logic,sci.philosophy.meta
Subject: Feyerabend, Kuhn, Lakatos, and Popper one school? (was re: Natural Kinds)
Date: 10 Nov 92 18:21:03 GMT
Article-I.D.: samba.1992Nov10.182103.28535
Followup-To: sci.logic,sci.philosophy.meta
Organization: University of North Carolina Extended Bulletin Board Service

In article <BxIA0y.2F9@unx.sas.com> Gary Merrill writes:
> [All sorts of stuff]

Gary, what are you arguing about?

You have made a couple of statements about a list of philosophers that I
proposed as a beginning list of important philosophers of science,
namely Feyerabend, Kuhn, Lakatos, and Popper. You have said they are
representative of a single "school" or "tradition." You have
characterized them as all reacting against positivism.

I have asserted that this characterization of this group as being of a
single school is indefensible. I have tried to point out sepearate
influences on separate philosophers among these four. I have tried to
indicate how there's more to at least some of these than a mere reaction
against positivism. (Note that the points at issue here are not whether
they are individually right or wrong, whether they are of importance or
not, or whether positivism is correct or not (although we have brought
up these questions to a very limited extent)).

Have you defended your position? Have you retracted it? No, all you have
done is respond with insults. I admit that I have not been particularly
polite, although I think you took some comments I made jestingly in a
different light. I have been candid about the gaps in my reading, and I
am going to look up your essay.

And your insults do not even reflect what I posted:

>...That you apparently wish to judge the contemporary state of
>philospohy of science on the basis of this and ignorance of more
>recent samplings speaks for itself.

Where have I offered to "judge the contemporary state of" anything? At
best, I may have given a few impressionistic comments.

                                                Robert Vienneau

P.S. On the subject of importance, your comments do make me wonder. I
assume that if Karl Popper is important anywhere, it is in the
philosophy of science. I accept frequency of referencing as a quick
rough and ready measure of influence. So your comment,

>...(By
>the way, I just looked throuth *two* sets of proceedings of the Philosophy
>of Science Association to nail down dates on Popper and could not find
>a *single* reference to him in *any* of the bibliographies.  Is this a
>measure of "stature"?)

does cause me some cognitive dissonance. Anybody else want to offer an
opinion?
--
   The opinions expressed are not necessarily those of the University of
     North Carolina at Chapel Hill, the Campus Office for Information
        Technology, or the Experimental Bulletin Board Service.
           internet:  laUNChpad.unc.edu or 152.2.22.80
Newsgroups: sci.logic,sci.philosophy.meta
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: Natural Kinds (was re: Are all crows black?)
Originator: sasghm@theseus.unx.sas.com
Date: Mon, 9 Nov 1992 13:30:47 GMT
Organization: SAS Institute Inc.


In article <1992Nov8.210316.5922@dcs.qmw.ac.uk>, arodgers@dcs.qmw.ac.uk (Angus H Rodgers) writes:

|> 
|> In your own mind, it may not be a putdown. But this is a dangerously
|> Pickwickian manouevre, because the trouble with calling maths "purer"
|> and "better" than science is that it plays into the hands of those who
|> would conclude that it is therefore "useless" -- and withdraw funding!
|> It pays to be pragmatic. :-)

Ah yes.  The ultimate academic bugaboo:  funding.  Everything (even your
taxonomy of cognitive disciplines) must be a slave to funding.

|> Seriously, it's worth asking *why* the title of science is considered
|> so honorific, and then (and not before that) asking whether maths (or
|> computation) does or does not deserve that title.

But what title is *that* title.  Is it the title of being *useful* or
the title of being *science*.  Even the hobgoblins of funding don't
treat these as equivalent.

|>    Computer science is the science of discrete processes. The
|>    automatic computing machine -- which is one kind of discrete
|>    process, possessing a universal property which enables it
|>    in principle to simulate any other such process -- is
|>    conventionally taken to stand (both metonymically and
|>    synecdochally) for the whole field. So the problem with
|>    the phrase "computer science" lies not in the word "science",
|>    but in the word "computer": the tool has eclipsed its object.
|> 
|> Or, again:
|> 
|>    Computer science is discrete applied mathematics. But this
|>    is not to say that the discrete mathematics needed for the
|>    applications always exists before the applications do. So
|>    computer science is not applied discrete mathematics; the
|>    qualifiers do not commute.
|> 
|> (Comments? Flames? Alternatives? - Myself, I'm not sure whether
|> the adjective "complex" should somehow also be worked into the 
|> definition(s).)

I don't have a problem with this.  But notice that it makes
CS a subdiscipline of mathematics -- and it still lacks significant
distinguishing features of the genuine sciences.  It also suggests
that there is (or ought to be) a distinction between CS and
software engineering along the lines of the distinction between
(say) applied (or even pure) mathematics and civil engineering.
But this does not seem to be the case.  And it isn't obvious
that it should be.
-- 
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: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: Impredicativity - was: Russell's Paradox
Organization: Boise State University
Date: Fri, 6 Nov 1992 19:21:18 GMT

In article <TORKEL.92Nov5210509@lludd.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <1992Nov5.170354.29866@guinness.idbsu.edu> holmes@garnet.idbsu.edu
> (Randall Holmes) writes:
>
>   >Neither A nor B can be shown to represent a unique object in ZFC-.
>
>  Of course not! The question I was commenting on was whether it
>is provable in ZF without foundation that if there is a function f
>defined on the natural numbers satisfying f(n)={n,f(n+1)}, then there
>is a set x such that x={1,x}, and my answer was that in all likelihood
>this is not so.

You were right; it is easy to construct an interpretation of ZFC- +
VCP (nothing is an iterated element of itself) + existence of
non-well-founded sets.

-- 
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,alt.uu.future
From: jbaez@riesz.mit.edu (John C. Baez)
Subject: Re: Are all crows black? => Logic as an essential subject?
Organization: MIT Department of Mathematics, Cambridge, MA
Date: Fri, 6 Nov 92 02:48:02 GMT

In article <1992Nov5.182513.25397@lclark.edu> higa@lclark.edu (Keith Higa) writes:
>In article <1992Nov4.170813.27890@CSD-NewsHost.Stanford.EDU> 
>pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
>>I have very mixed feelings about this.  Freshman math at Gunn High
>>(where my 14 year old goes) started out this year with a couple of
>>weeks of propositional logic before getting into geometry etc.  My
>>intuitive feeling was that she got much less useful math out of the
>>logic than out of the geometry.  On the other hand logic is fundamental
>>to thought, and even if humans don't reason propositionally it is good
>>to at least be aware of a logical system that they could plausibly
>>reason in, albeit clumsily.
>
>My logic professor brought up the story of Bertrand Russell.  I think
>(correct me if I'm wrong), that he and a co-author set out to prove that
>all math was based on logic, and it took them two volumes to logically
>prove that 1+1=2.

There were, however, some interesting lemmas.

Xref: sparky sci.logic:1987 sci.philosophy.meta:2490 sci.math:14737
From: pstevens@cage.gssec.bt.co.uk (Perdita Stevens)
Newsgroups: sci.logic,sci.philosophy.meta,sci.math
Subject: Re: Will a mathematician locked up in a little room be happy?
Date: 10 Nov 92 18:08:38 GMT
	<Bx998I.KpK@unx.sas.com> <1992Nov6.024607.6831@galois.mit.edu>
Organization: BT Glasgow Systems and Software Engineering Centre, Scotland.


   Gary Merrill writes:

   >You can take a mathematician and lock him in his little office with just
   >some writing materials and he will (a) be pretty happy, and (b) be able
   >and willing to do anything of a mathematical nature.  Even a committed
   >*theoretical* physicist will be very distressed under such circumstances
   >since he has not way to determining whether his theories (however abstract)
   >are *good* ones.

Or her ...

In article <1992Nov6.024607.6831@galois.mit.edu> jbaez@riesz.mit.edu (John C. Baez) writes:

   >I hope you have not tried this experiment, because I don't think I, at
   >least, would stay happy for long in this little office.  

but I might ... bliss ... when can I start ?? :-) :-) :-)

Seriously, I think one has to restrict the original statement to talk
about pure mathematicians, and I'm sure many of them would disagree
much of the time. I think this has to do with the social nature of human
beings and the need to bounce ideas off people, and have them bounce
theirs off you, as a way of getting ideas; for the same reason
teaching is a valuable aid to research. The point is well made that it
is *valid* to consider doing such a thing to a pure mathematician, even
if it isn't the most *efficient* way for one to work. (The same
perhaps applies to some kinds of writers?)

Perdita Stevens, 
representation theorist turned software engineer,
definitely not speaking for my employer.
From: cxm7@po.CWRU.Edu (Colin Mclarty)
Newsgroups: sci.logic
Subject: Re: Types of type theory
Date: 12 Nov 1992 19:30:25 GMT
Organization: Case Western Reserve University, Cleveland, OH (USA)
Reply-To: cxm7@po.CWRU.Edu (Colin Mclarty)
NNTP-Posting-Host: slc5.ins.cwru.edu


In a previous article, dzik@access.digex.com (Joseph Dzikiewicz) says:

>I have come across two uses of the term "type theory" in logic that seem
>to be referring to different things.
>
	Yes, there are two different sense of "type"-- no doubt 
relatable on some level but I don't know of any reason toe relate
them.  
	The name "type theory" always means the first, i.e. 
higher order logics.
From: torkel@sics.se (Torkel Franzen)
Newsgroups: sci.logic
Subject: Re: Impredicativity - was: Russell's Paradox
Date: 5 Nov 92 09:08:28 GMT
	<1992Nov4.073717.22625@CSD-NewsHost.Stanford.EDU>
	<1992Nov4.134534.17092@husc3.harvard.edu>
	<1992Nov5.004725.8252@CSD-NewsHost.Stanford.EDU>
Organization: Swedish Institute of Computer Science, Kista

In article <1992Nov5.004725.8252@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.
Stanford.EDU (Vaughan R. Pratt) writes:

   >Again, I'm not in the market to be talked out of Replacement, or talk
   >anyone out of it.  Foundation on the other hand seems as pointless as
   >the cumulative hierarchy: each needs the other and neither seems to be
   >much use to the rest of mathematics.

  The point of the cumulative hierarchy is that it gives an interpretation of
ZF, as Zermelo lucidly explains in his 1930 article. The whole business
of "Down with foundation!", "Oppose unnatural self-membership!",
"Give me replacement or give me death!" as it has appeared here is
completely bogus. If you want to introduce a new set theory or a new
interpretation of existing set theory, by all means do so if you can.
What I am interested in is whether or not you can explain what
you are talking about, as has been done with the "standard" theory of
non-well-founded sets (in that case by giving a model of the theory in ordinary
mathematics).
Newsgroups: sci.logic
From: dzik@access.digex.com (Joseph Dzikiewicz)
Subject: Types of type theory
Organization: Express Access Online Communications, Greenbelt, MD USA
Date: Tue, 10 Nov 1992 23:34:10 GMT

I have come across two uses of the term "type theory" in logic that seem
to be referring to different things.

In one, Type Theory seems to relate to the rules for higher-order-logics
(ie, second order logic and up).  This is discussed in Peter Andrews'
book "An Introduction to Logic and Type Theory: To Truth through Proof."
I have also seen it referred to as "Church's Type Theory."

In the other, types are sets of formulas in first order logic.  This
is discussed in some detail in Chang and Keisler's book "Model Theory."

Am I correct in thinking that these are two different things with the same
name, or are they the same thing presented differently by two
different groups of authors?

Any enlightenment would be greatly appreciated.

Joe Dzikiewicz

Xref: sparky sci.logic:1963 sci.philosophy.meta:2411
From: arodgers@dcs.qmw.ac.uk (Angus H Rodgers)
Newsgroups: sci.logic,sci.philosophy.meta
Subject: Re: Natural Kinds (was re: Are all crows black?)
Date: 8 Nov 92 21:03:16 GMT
Organization: Computer Science Dept, QMW, University of London

In <Bx8yvo.6ty@unx.sas.com>
sasghm@theseus.unx.sas.com (Gary Merrill) writes:

>But one of my major points is that calling a discipline "not a science"
>is *not* (necessarily) a put down.  Hence my remark that "science" is
>often used primarily for its "honorific" value.  Both Zeleny and I
>have urged (and offered evidence) that mathematics is not (generally)
>considered to be a *science*.  Yet I believe that both of us regard
>it as somehow "purer" and in some sense "better" than a science:
>more fundamental, stricter criteria of adequacy, etc.

In your own mind, it may not be a putdown. But this is a dangerously
Pickwickian manouevre, because the trouble with calling maths "purer"
and "better" than science is that it plays into the hands of those who
would conclude that it is therefore "useless" -- and withdraw funding!
It pays to be pragmatic. :-)

Seriously, it's worth asking *why* the title of science is considered
so honorific, and then (and not before that) asking whether maths (or
computation) does or does not deserve that title.

My own humble opinion -- even humbler since reading Vaughan Pratt's
list of questions :-) -- is that taking the title of a science is a
claim to the possession of (in a loose sense) verifiable truths about
the real world. (But I'm repeating myself; and I haven't studied enough
philosophy to refine the definition much further.)

To make this post a bit more interesting, I'll venture a definition of
"computer science". I've tested (!) this against Vaughan Pratt's list
of questions, and it seems to bear up, or at least not to look too 
silly to be worth mentioning:

   Computer science is the science of discrete processes. The
   automatic computing machine -- which is one kind of discrete
   process, possessing a universal property which enables it
   in principle to simulate any other such process -- is
   conventionally taken to stand (both metonymically and
   synecdochally) for the whole field. So the problem with
   the phrase "computer science" lies not in the word "science",
   but in the word "computer": the tool has eclipsed its object.

Or, again:

   Computer science is discrete applied mathematics. But this
   is not to say that the discrete mathematics needed for the
   applications always exists before the applications do. So
   computer science is not applied discrete mathematics; the
   qualifiers do not commute.

(Comments? Flames? Alternatives? - Myself, I'm not sure whether
the adjective "complex" should somehow also be worked into the 
definition(s).)
--
Angus H. Rodgers  (PhD student), | arodgers@dcs.qmw.ac.uk  
Dept. of Computer Science, Queen | [ +44 | 0 ] 71 975 5241   
Mary & Westfield College,  Mile  | "But what is contact? No two points
End Rd., London E1 4NS, England  | are in contact." -- A.N. Whitehead.
Organization: Freshman, MCS general, Carnegie Mellon, Pittsburgh, PA
Newsgroups: sci.logic,comp.ai.philosophy,comp.robotics,comp.databases.theory,comp.theory
Date: Sat,  7 Nov 1992 20:32:04 -0500 
From: Mark Alan Lang <Elistan+@CMU.EDU>
Subject: Re: Human Computers....

Excerpts from netnews.comp.robotics: 7-Nov-92 Human Computers.... by
Eskinder Sahle@csgrad.cs pl.na nasa slab. 
> Hello all:

	Hi there!
  
> I need some help....  I'm looking for examples in fiction literature
> of super sophisticated communicative computers a la HAL. That is,
> computers that talk and communicate like humans.  I'm not so much 
> interested in those instances where it's a robot that cannot be
> distinguished from a human being as in computers sounding human without
> being almost totally human-like....  .
>  
> Thanks in advance.
> Ahmed 

	You might want to check out a book called _When H.A.R.L.I.E Was One,
Release 2.0_ by David Gerrold.  Very good as both a science-fiction
story and as a speculative paper about the future of computers, IMHO.

-----------------------------------------------------------------------
|  Mark Lang                       |  ml5t+@andrew.cmu.edu            |
|  elistan+@cmu.edu                |  elistan@drycas.club.cc.cmu.edu  |
-----------------------------------------------------------------------

Newsgroups: sci.logic
From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Foundation, a.k.a. Regularity (was re: Impredicativity - was: Russell's Paradox.)
Keywords: foundation (regularity) => cumulative hierarchy
Organization: Computer Science Department,  Stanford University.
Date: Thu, 5 Nov 1992 17:31:31 GMT

In article <1992Nov5.112036.17130@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:
>Vaughan, I shall presume to fill in for Randall by pointing out that
>Schoenfield formulates the Regularity Axiom on p. 326 of the Handbook,
>whereas Takeuti & Zaring describe the same axiom on p. 18 of the first
>edition of their book.  While I am happy to see someone else follow my
>preferred practice of reading into a text whatever one wants to find
>therein, I really wish you would check your sources before wasting the
>time of your audience with this pointless prevarication.

Yes, you're absolutely right, I don't know why I thought it wasn't
there.  I retract what I said about Regularity (Foundation) being
omitted, very sorry.  (This is turning out to be an excellent way for
me to get rid of my misconceptions about set theory.  I hope people
don't object to strongly to my occasional slipups of this kind in this
forum.  Short of investing a lot more time checking everything, the
only alternative I see is for me not to post anything about things I'm
not expert in.)

>This informal procedure can be made rigorous as follows.  The form of
>FA that I find most useful for these purposes is the Axiom Schema of
>Restriction,

Oops, that should have been Regularity.  (Bill's calling it AF was
equally confusing for me, making me think of AntiFoundation.)
-- 
Vaughan Pratt				There's no truth in logic, son.
From: rh@smds.com (Richard Harter)
Newsgroups: sci.logic
Subject: Re: Impredicativity - was: Russell's Paradox
Date: 8 Nov 92 07:41:20 GMT
Reply-To: rh@ishmael.UUCP (Richard Harter)
Organization: Software Maintenance & Development Systems, Inc.

In article <1992Nov6.193134.17283@guinness.idbsu.edu> holmes@garnet.idbsu.edu (Randall Holmes) writes:

>The open sentence "x is not an element of x" is in fact true or false
>for each x, in any reasonable set theory.  But it does not define a
>set.  The reason it does not define a set is that _if it defined a
>set_ there would be a problem with substituting some particular x (the
>extension of this property) into the sentence.  There is in fact no
>instance in either ZFC or NFU in which "~x E x" fails to be true or
>false for some x; in ZFC, it is _always true_, and in NFU it is
>sometimes true and sometimes false.

This is the classical approach to dealing with the paradoxes, i.e. to
claim that there are open sentences whose extensions are not sets.
However one can also take the view that "x is a member of y" is not
a proper relationship.  In other words it is not the case that for
all x,y either T(x a member of y) or F(x a member of y).  I have come
to have the opinion that the paradoxes establish that membership is
not a two valued function, and more generally, truth is not a predicate.

-- 
Richard Harter: SMDS Inc.  Net address: rh@smds.com Phone: 508-369-7398 
US Mail: SMDS Inc., PO Box 555, Concord MA 01742.    Fax: 508-369-8272
In the fields of Hell where the grass grows high
Are the graves of dreams allowed to die.
Newsgroups: sci.logic,alt.uu.future
From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Are all crows black? => Logic as an essential
Organization: Computer Science Department,  Stanford University.
Date: Sat, 14 Nov 1992 03:28:08 GMT

In article <1e1cnoINN74a@columbia.cs.ubc.ca> kean@cs.ubc.ca (Alex Kean) writes:
>>>> ....
>>>>too many people graduating as it is without knowing the difference
>>>>between "All men are mortal/Socrates is a man -> Socrates is mortal" and
>>>>"All men are mortal/Socrates is mortal -> Socrates is a man".
>>
>
>... the first form of inference as we know is deduction,
>and the second form is actually know as abduction.

All men are mortal/Madonna is mortal -> Madonna is a man.  Guess she
was abducted.
-- 
Vaughan Pratt	  		A fallacy is worth a thousand steps.
Newsgroups: sci.logic