HDTenEightyP/NetNews huggingface dataset:
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: Are all crows black? => Logic as an essential subject?
Originator: sasghm@theseus.unx.sas.com
Date: Mon, 16 Nov 1992 14:11:48 GMT
Organization: SAS Institute Inc.


In article <1992Nov9.153536.3892@ariel.ec.usf.edu>, mccolm@darwin.math.usf.edu. (Gregory McColm) writes:

|> "Proof theory", which is based on the idea of having some 
|> hypotheses and using rules of inference to generate 
|> conclusions, all within some artificial language, has 
|> Aristotle's syllogisms as the oldest example.  200 yrs ago, 
|> Kant said that Logic had not progressed since Aristotle, 

This is, of course, incorrect (gasp!  Kant wrong?).  A look at
the late medievals suffices to show some significant differences
to Aristotle.  Even before that there were some improvements.
Note, for instance, that the common example (also given in this
thread) of

	All men are mortal.
	Socrates is a man.
	Therefore, Socrates is mortal.

is not in fact an *Aristotlean* syllogism, but a Galenic syllogism.
(It is the presence of the *particular* term 'Socrates' that is
at issue here.)

|> and it wasn't until Boole, DeMorgan, & co., that Logic 
|> began its modern adventure:  what happened was the appearance 
|> of abstract algebra.  A lot of sci.logic is on the modern 
|> systems (eg, Peano's Predicate Calculus under Goedel's rules 
|> of inference) which are still quite Aristotilean.

The late medievals knew (and argued at some length) that Aristotle's
logic was inadequate.  (See in particular Jean Buridan's _Sophisms
on Meaning and Truth_.)  Unfortunately, although they had some quite
sophisticated ideas and some very good contributions at the semantic
level, they never developed a good notation for formalization.
-- 
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: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: What is Computer Science (was: Natural Kinds)
Originator: sasghm@theseus.unx.sas.com
Date: Mon, 16 Nov 1992 13:28:58 GMT
Organization: SAS Institute Inc.


In article <BEVAN.92Nov11113345@hippo.cs.man.ac.uk>, bevan@cs.man.ac.uk (Stephen J Bevan) writes:
|> In article <BxGBsJ.8qG@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
|>    Do you see CS as having any immediate empirical content in the
|>    manner of physics, chemistry, biology, etc.?
|> 
|> 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.  Then there is geology, which
has its own problems of methodology (though surely this is a "natural
science" as well).

|> As for empirical content, what about the example of routing via
|> simmulated annealing?  There is no way to check this is any good
|> without experimenting (i.e. writing the code for the router and trying
|> it on as many boards as you can find).  As I noted before you may not
|> consider this CS as a computer was only used to prove the method
|> worked (ignoring the fact that routing has an obvious application in
|> the design of computers).  However, if you do have this view, I would
|> be interested to know under what banner you felt this work lay.

Well, this is exactly the sort of thing I have been fishing for --
but note how long it has taken someone to suggest such an example
rather than purely formal/mathematical methodologies.  (Note also
that it appears to fit a previous suggestion of mine concerning
an analogy between programs and theories.)
-- 
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
Xref: sparky sci.logic:2050 sci.math:15007
From: zeleny@husc10.harvard.edu (Michael Zeleny)
Newsgroups: sci.logic,sci.math
Subject: Re: Logic and Mathematicians
Date: 16 Nov 92 00:17:43 GMT
Organization: The Phallogocentric Cabal

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.

>-- 
>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."
From: martinc@grover.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic
Subject: Re: Why Logic?
Date: 20 Nov 92 15:57:01 GMT
	<MARTINC.92Nov18221201@hatteras.cs.unc.edu>
	<1992Nov20.101850.7674@nntp.nta.no>
Organization: UNC Department of Computer Science
In-reply-to: klaus@hal.nta.no's message of 20 Nov 92 10:18:50 GMT

In article <1992Nov20.101850.7674@nntp.nta.no> klaus@hal.nta.no (Klaus Gaarder FNI) writes:

    Sorry, but I completely fail to see what's so deep about your
   comment.


I don't doubt it.
--
		Charles R. Martin/(Charlie)/martinc@cs.unc.edu
     Dept. of Computer Science/CB #3175 UNC-CH/Chapel Hill, NC 27599-3175
	    3611 University Dr #13M/Durham, NC 27707/(919) 419 1754
     "Oh God, please help me be civil in tongue, pure in thought, and able
      to resist the temptation to laugh uncontrollably.  Amen." -- Rob T
From: timc@cs.man.ac.uk (Tim Clement)
Newsgroups: sci.logic
Subject: Re: Programs for simple logic proofs:  where are they?
Keywords: Natural deduction, automatic theorem proving, Otter, HOL, Muffin
Date: 17 Nov 92 14:18:26 GMT
Organization: Dept Computer Science, University of Manchester, U.K.

In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:
>In article <4804@equinox.unr.edu> mjb@dws020.unr.edu (Mike Brown) writes:
>>I am looking for programs that will do proofs like:
>>			Prove: Q            \
>>	1 P then Q	Premis               > The problem
>>	2 P		Premis              /
>>	3 Q             1, 2, Modus Ponens  >  The program's proof
>>
>>(The proofs do get more involved)
>>
>>Is there a program out there that will do these proofs?
>
>The nearest thing
>I have read about is "Muffin: A Proof Assistant", a chapter by Richard C. Moore
>in Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT, Prentice
>Hall International, 1990. I recall the chapter saying something about Muffin
>being made available.   I wonder if anyone is using it.
>

Muffin developed into "mural", a WIMP interface proof assistant for
natural deduction proofs (i.e. proofs much like the example above).
As a proof assistant, it leaves the user to decide that Modus Ponens
is the rule to apply (although there are various forms of assistance
for the choice).  Full details are in "mural: a formal development
support system" by C.B.Jones et al, Springer 1991.  ISBN 3-540-19651-X.

mural is generally available at modest cost.  It is a large SmallTalk
image, so can only be supplied to people with an appropriate SmallTalk
license (hence no FTP).  For details, contact richard@cs.man.ac.uk
(non-educational users) or br@inf.rl.ac.uk (universities and similar
bodies).

Tim Clement
Newsgroups: sci.logic
From: reintjes@infonode.ingr.com (Peter Reintjes)
Subject: Paradoxical Slogan
Keywords: paradox liars
Organization: Intergraph Corporation, Huntsville, AL.
Date: Wed, 18 Nov 1992 01:28:32 GMT


I saw the following slogan on the side of an oil
truck today. I thought I would put it to this group
to classify it for me.

   Young Oil Company  "We Deliver more than we Promise"

If you interpret their slogan as some sort of
a promise. Is the statement:  true,  false,  an
example of the 'Liars Paradox',  a type error, or what?

Actually,  I posted this more for amusment than anything.
I'm not trying to apply logic to the field of advertising.

                - Peter Reintjes  pbr@quine.sofla.ingr.com
Newsgroups: sci.logic
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
From: wft@math.canterbury.ac.nz (Bill Taylor)
Date: Tue, 24 Nov 1992 02:17:51 GMT
Organization: Department of Mathematics, University of Canterbury

In article <TORKEL.92Nov22115549@echnaton.sics.se>, torkel@sics.se (Torkel Franzen) makes an good point that "uncountable" seems to have a clear cut
meaning to most working mathematicians, independent of whatever formal system
they may (seem to) be working in (if any). He makes an excellent analogy with
the concept of "complete", in some detail, pointing out that the same applies.

While there may be some room for debate, he presents a very robust and appealing
case.  But then he also goes on to say, in distinction, 

|> On the other hand,
|> such concepts as "formally undecidable" or "definable" do have formal systems
|> as explicit and implicit parameters, and are understood, explained, and used
|> on that understanding.

While I agree totally that this is so with "formally undecidable", I'm not so
sure about the other.

"Definable", when used technically, does of course mean precisely "with respect
to a formal system"; but then Paul Budnik's point was that (precisely speaking)
this is also true for "uncountable".  But Torkel Franzen was making the point
that "uncountable" also corresponds to a clear-cut mathematical idea that is
independent of any formal system; and I suggest that "definable" is similar.

I suspect that many working mathenmaticians have a vague but firmly held idea
that there are certain identifiable "definable" things in some platonic sense,
just as much as there are uncountable things.  While they may not be able to
give quite such a good account of them as they could of uncountable, they might
make a fair stab at it, if pressed.  It would almost certainly be based on the
simple idea of sets being given in (unrestricted-looking) comprehension terms
   { x | P(x) } .

Of course the property P can only be made precise within a formal system.
But then, as said above, the same remark applies to uncountable.

Does this idea ring any bells with anyone else; that "definable" may have some
meaning in mathematical "reality" (independent of a formal system); that is
*at least as much* as does "uncountable".  
 ~~~~~~~~~~~~~~~~
------------------------------------------------------------------------------
              Bill Taylor              wft@math.canterbury.ac.nz
------------------------------------------------------------------------------
             Quantum particles: the dreams that stuff is made of.
------------------------------------------------------------------------------
Xref: sparky sci.logic:2158 sci.physics:19487
From: paul@mtnmath.UUCP (Paul Budnik)
Newsgroups: sci.logic,sci.physics
Subject: Re: Lowneheim-Skolem theorem (was: Continuos vs. discrete models)
Date: 23 Nov 92 16:38:49 GMT
Followup-To: sci.logic
Organization: Mountain Math Software, P. O. Box 2124, Saratoga. CA 95070

In article <1992Nov22.230633.12855@galois.mit.edu>, jbaez@riesz.mit.edu (John C. Baez) writes:
> In article <1992Nov22.002703.5865@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
> >In article <368@mtnmath.UUCP> paul@mtnmath.UUCP (Paul Budnik) writes:
> 
> >>The discussion on L-S has apparently misled you. I believe that the
> >>space-time manifold is discrete, i. e. not continuous. There are many
> >>ways to discriminate between a continuous and discrete model and this
> >>has nothing to do with countability.
> >
> >So why this raging debate about how many reals, then?
> 
> Typically, issues which have no practical significance generate more
> raging debates on sci.physics than those which do.

The question of how many reals, is significant
even though it does not have a direct effect on the
mathematics that physicists use. The way mathematicians extend logic
today is by postulating the existence of large cardinals.
These abstractions are so far removed from the computational roots of
mathematics that there is no intuitive basis for deciding between them.
However these large cardinal axioms have combinatorial implications.
For example they allow us to decide the halting problems for a wider
class of Turing Machines. It is my contention that if one focused
on understanding these combinatorial implications and forgot about the
Platonic heaven of completed infinite totalities, real progress could
be made in extending logic.

Follow ups are directed to `sci.logic'.

Paul Budnik
Newsgroups: sci.logic,alt.uu.future
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: Are all crows black? => Logic as an essential subject?
Originator: sasghm@theseus.unx.sas.com
Date: Mon, 16 Nov 1992 13:41:11 GMT
Organization: SAS Institute Inc.


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

It's interesting to see someone who is not a "professional" specialist
in history of logic take such an interest in a topic such as syllogictic
reasoning.  I'm a bit surprised you didn't mention Lukasiewicz's book.
(perhaps you don't care for the perspective?).

|> De Morgan was the first and last mathematician to take a really serious
|> look at syllogisms.  The battle with Hamilton prompted Boole to write
|> up his thoughts on the subject of logic, and within thirty years the
|> research potential of syllogisms had died, replaced by Boolean logic as
|> interpreted by Peirce, Jevons, Schroeder, and others.  The 24
|> syllogisms continued to be taught sporadically for another century,
|> indeed my first encounter with logic was when my high school swimming
|> coach lent me his freshman logic text, which confined itself to
|> syllogisms!

Peirce, it should be pointed out, did quite a bit of work in what might
be called "inductive" syllogisms as a formalization of his inductive
logic.

|> I do not know of tight bounds for the complexity of syllogistic
|> reasoning, can someone supply these?  I would expect it to be decidable
|> in polynomial time, since it should be straightforward to eliminate
|> premises sequentially and deterministically.  Note that Carroll's forms

I would expect a great deal of similarity here to the properties of
monadic predicate logic since syllogistic is (representable as) a
sub-system of that.  Indeed, the primary weakness in syllogistic
reasoning is the inability to express dyadic (and hence more complex)
relations.  As a consequence, it is hard to do foundations of mathematics
via syllogisms since you can't seem to express arithmetic relations.

-- 
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,sci.math
From: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: Logic and Mathematicians
Organization: Boise State University
Date: Sun, 15 Nov 1992 22:03:59 GMT

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:
>|> 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.
>
>Oh yes: Prove P=NP is independent of ZFC. It actuall HAS
>been shown independent in some weak arithmetics.
>
>-- 
>Richard Zach                         Technische Universitaet Wien
>[zach@csdec1.tuwien.ac.at]     Abteilung fuer Formale Logik 185.2

Wouldn't that actually answer the question?


-- 
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: jhhardy@silver.ucs.indiana.edu (J. Hardy)
Subject: Re: Programs for simple logic proofs: where are they?
Organization: Indiana University
Date: Tue, 17 Nov 1992 13:46:46 GMT

In <IMG.92Nov17114848@hope.aisb.ed.ac.uk> img@aisb.ed.ac.uk (Ian Green) writes:


>If you're looking for an interactive system, you might try FOL or
>its derivative, GETFOL.  Contact Fausto Giunchiglia, at fausto@irst.it or
>fausto@dist.unige.it for more info.  Weyhrauch80 describes FOL.

>	-ian

>@article(Weyhrauch80,
>        Author = {Weyhrauch, Richard W.},
>         Title = {Prolegomena to a Theory of Mechanized Formal Reasoning},
>          Year = {1980},
>       Journal = AI,
>        Volume = {13},
>         Pages = {133--170})

As I recall there are several programs that do FOL proofs in a natural
deduction system for the Mac and for IBM-clones.  The ones I'm
thinking of aren't theorem provers, but are more like proof checkers.
I know that Tarski's World (by Barwise and Etchemendy) is available both
for the macintosh and for windows.  If that's the sort of thing you're looking
for then there are several others also (tho I can't at the moment recall the
titles).  Someone was demo'ing an IBMish program at the last APA conference
I attended.

If that's the sort of thing you're looking for then you might ask on
philos-l.  I seem to recall that a list of such programs circulated there not
too long ago.

jim hardy

Newsgroups: sci.logic,sci.math
From: mutation@dorsai.com (Florian Lengyel)
Subject: Re: Logic and Mathematicians
Organization: The Dorsai Embassy +1.718.729.5018
X-Newsreader: Tin 1.1 PL4
Date: Mon, 16 Nov 1992 22:22:20 GMT

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.

Would the construction of two models of ZFC,
  the first, in which P = NP holds
  the second, in which P <> NP holds
call for two models of computation that would violate the polynomial-time
Church's thesis, if not Church's thesis itself?

In the first model, the notion of computation would have an interpretation
which would not be polynomially equivalent to the notion of computation in the
second model. If you believe Church's thesis, the independence proof would
establish that these two notions of computability encompass exactly the
same class of functions. So the encoding of a polynomial time NP-complete 
algorithm in the first model as an algorithm in the second model would not 
be polynomial time.

If you believe the polynomial-time version of Church's thesis, this situation
cannot occur (assuming that polynomial-time means the same thing in both
models). 

A formalist might say: "P = NP is independent of the axioms of set theory,
I cannot derive P = NP or P <> NP from ZFC, therefore the question is
'settled'", but only if the formalist would willfully overlook the
construction of the computable functions and their complexity classes
according to the first and second models, at least one of which would
(it appears to me) involve a non-standard notion of computation.

But I must admit that these possibilities strike me as counterintuitive,
because of my sense that such an independence proof would violate the
polynomial time form of Church's thesis.

: 
: >-- 
: >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."

Ordinally,

-- 
MUTATION@DORSAI.COM
FLORIAN@NEOTERIC.COM
Xref: sparky sci.logic:2052 sci.math:15021
From: gjm11@cus.cam.ac.uk (G.J. McCaughan)
Newsgroups: sci.logic,sci.math
Subject: Re: Logic and Mathematicians
Date: 16 Nov 92 05:08:46 GMT
Organization: U of Cambridge, England

In article <1992Nov15.191744.17481@husc3.harvard.edu>, zeleny@husc10.harvard.edu (Michael Zeleny) writes:

> 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.

The following isn't very profound, but I had to think it out to work out
who was right on this one. I'm posting it mostly to save other people the
trouble of doing it themselves. :-)

If P=NP is independent of ZFC, then ZFC does not prove P=NP, so you can't
write down an algorithm for (say) the travelling salesman problem and prove
it's in P using only ZFC. I suppose there might be an algorithm that you
could write down but that you couldn't prove (in ZFC) to be in P. (A bit
like with Goodstein's theorem, where there's an "algorithm" you can write
down but you can't prove it terminates unless you use something stronger
than PA.)

So no, it wouldn't actually answer the question. If any "plausible"
extension of ZFC proved P=NP, then there would be an algorithm for (e.g.)
travelling salesman that was "plausibly" in P. What if it were done with,
say, a forcing argument? Suppose P=NP holds in some generic extension of V.
Then ... I don't know; I can't think about forcing at 5am. Oh well.

-- 
Gareth McCaughan     Dept. of Pure Mathematics & Mathematical Statistics,
gjm11@cus.cam.ac.uk  Cambridge University, England.    [Research student]