HDTenEightyP/NetNews huggingface dataset:
From: kean@cs.ubc.ca (Alex Kean)
Newsgroups: sci.logic
Subject: Re: Are all crows black? => Logic as an essential
Date: 13 Nov 1992 15:11:52 -0800
Organization: Computer Science, University of B.C., Vancouver, B.C., Canada
NNTP-Posting-Host: columbia.cs.ubc.ca

In article <1992Nov12.231756.17396@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:
>>> ....
>>>Let's not put Will off of syllogistic logic, though, please.  There are
>>>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".
>
>AK:
>>I have not graduated yet, what is the difference?
>
>Validity.  (This is truly depressing.)
>

Very true. In fact, the first form of inference as we know is deduction,
and the second form is actually know as abduction. It is correct that
abduction is not truth preserving, nevertheless, it is a form of inference
used widely in our everyday life. My curiosity for posting stamps from 
my interest on abduction, the non-truth preserving inference, but is used
commonly enough *as if it is truth preserving*.


>AK:
>>Best Regards,
>
>Have you considered a career in feminist computer science?
>

I have not graduated yet, what is feminist computer science?

Best Regards,

Alex Kean <kean@cs.ubc.ca>

Department of Computer Science           
University of British Columbia
6356 Agricultural Road,
Vancouver, British Columbia
Canada V6T 1Z2

Tel: +1 (604)-822-3061
Fax: +1 (604)-822-5485



Newsgroups: sci.logic,sci.philosophy.meta,sci.math
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, 9 Nov 1992 13:50:43 GMT
Organization: SAS Institute Inc.


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

|> To me computer science is about four interactions: information and
|> time, computation and communication, models and reality, and
|> perspective and users.  Discreteness is neither emphasized nor
|> deemphasized in this view, the integers and the reals are both
|> important in CS.

Do you see CS as having any immediate empirical content in the
manner of physics, chemistry, biology, etc.?  If so, could you
describe this a bit?  (I concede that "immediate empirical
content" is not very precise, but I think we know what is 
intended.)  It seems pretty clear that given your view of the
nature of CS, it really has nothing to do with actual physical
machines, but rather more properly deals with "machines" in the
logical (mathematical) sense (Turing machines, for example).

Your view of CS is a coherent one, but I'm not sure
how widely received it would be.  Simply as a matter of your
own personal opinion, do you think this view is widely shared
(in both academia and industry), or do you offer it rather along
the lines of "What CS *should* be"?  Do you wish to subsume
so-called "software engineering" under CS, or would you treat
it differently as a distinct applied discipline?
-- 
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: jg@cl.cam.ac.uk (Jim Grundy)
Subject: Re: Programs for simple logic proofs:  where are they?
Reply-To: jg@cl.cam.ac.uk
Organization: Cambridge Hardware Verification Group
Date: Thu, 12 Nov 1992 12:06:07 GMT

In article <4804@equinox.unr.edu>, mjb@dws014.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)
|> 
|> I have looked around, but can't find a program for this.
|> (I tried archie searches for many keywords and didn't find a program)
|> 
|> Is there a program out there that will do these proofs?
|> 
|> Thanks
|> --
|> Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"

You can do this in the HOL theorem prover (several ways).

* 1: Backward Proof.

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
"Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e (MP_TAC (ASSUME "P:bool"));;
OK..
"P ==> Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e (ACCEPT_TAC (ASSUME "P ==> Q"));;
OK..
goal proved
. |- P ==> Q
.. |- Q

Previous subproof:
goal proved
() : void

#quit ();;
Bye.
$

* 2: Forward Proof

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#top_print print_all_thm;;
- : (thm -> void)

#let th1 = ASSUME "P ==> Q";;
th1 = P ==> Q |- P ==> Q

#let th2 = ASSUME "P:bool";;
th2 = P |- P

#let th3 = MP th1 th2;;
th3 = P ==> Q, P |- Q

#quit ();;
Bye.
$

* 3: Let HOL do a backward proof for you.

$ hol


===============================================================================
         HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
===============================================================================

#set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
"Q"
    [ "P" ]
    [ "P ==> Q" ]

() : void

#e RES_TAC;;
OK..
goal proved
.. |- Q

Previous subproof:
goal proved
() : void

#quit ();;
Bye.
$

===============================================================================
Jim Grundy               
University of Cambridge | Phone: +44 223 334760            | This space has
Computer Laboratory     | Fax:   +44 223 334678            | been intentionally
New Museums Site        | Telex: CAMSPLG 81240             | left blank for
Pembroke Street         | email: jg@cl.cam.ac.uk           | formatting
Cambridge  CB2 3QG      |                                  | purposes.
UNITED KINGDOM          |                                  |
===============================================================================
Newsgroups: sci.logic
From: jlavi@cs.joensuu.fi (Jarkko Lavinen)
Subject: Re: Programs for simple logic proofs: where are they?
Organization: University of Joensuu
Date: Thu, 12 Nov 1992 10:37:23 GMT

mjb@dws014.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)
Isn't this just what a theorem prover does? You could try for example
Otter which is available in ANL.

----- OTTER 2.2, July 1991 -----
The job began on cs, Thu Nov 12 12:32:19 1992
The command was "otter".

set(binary_res).
set(factor).
assign(stats_level,1).

list(usable).
1 [] -P | Q.
2 [] P.
end_of_list.

list(sos).
3 [] -Q.
end_of_list.

given clause #1: (wt=1) 3 [] -Q.
** KEPT: 4 [binary,3,1] -P.

----> UNIT CONFLICT at   0.01 sec ----> 5 [binary,4,2] .

Level of proof is 1, length is 1.

---------------- PROOF ----------------

1 [] -P | Q.
2 [] P.
3 [] -Q.
4 [binary,3,1] -P.
5 [binary,4,2] .

------------ end of proof -------------

So You just insert premises in axioms and deny the conclusion, theorem
prover then finds a contradiction. You can find the software
from 140.221.10.1 = anagram.mcs.anl.gov.

>Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"
From: martinc@hatteras.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic
Subject: Re: Are all crows black? => Logic as an essential subject?
Date: 13 Nov 92 19:32:21 GMT
	<MARTINC.92Nov12021908@hatteras.cs.unc.edu>
	<1duqtpINNjl1@columbia.cs.ubc.ca>
Organization: UNC Department of Computer Science
In-reply-to: kean@cs.ubc.ca's message of 12 Nov 92 23:55:37 GMT

In article <1duqtpINNjl1@columbia.cs.ubc.ca> kean@cs.ubc.ca (Alex Kean) writes:

   In article <MARTINC.92Nov12021908@hatteras.cs.unc.edu> martinc@hatteras.cs.unc.
   >
   >Let's not put Will off of syllogistic logic, though, please.  There are
   >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".
   >

   I have not graduated yet, what is the difference?

Please god, tell me he's kidding.

On the off chance you're not kidding, let's try another example: if I
say "all trees are green" and I look at a green shirt, can I conclude
that since it's green, it must be a tree?
--
		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
Newsgroups: sci.logic
From: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: Impredicativity - was: Russell's Paradox
Organization: Boise State University
Date: Thu, 5 Nov 1992 17:03:54 GMT

In article <TORKEL.92Nov5103134@isis.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <Bx81Ho.9HL@cantua.canterbury.ac.nz> wft@math.canterbury.ac.nz 
>(Bill Taylor) writes:
>
>   >A = { 1 , { 2 , { 3 , { 4 , {.....}}}}}
>   >B = { 1 , { 1 , { 1 , { 1 , {.....}}}}}
>   >Can B above, be obtained from A above, by ZF methods.
>
>  The question is vague in several respects, but the most likely
>answer is no. A, to put this into formal ZF terms, is, let us say, the
>range of a function f defined on the natural numbers, where
>f(n)={n,f(n+1)} for all n.  Assuming the existence of such a function
>in ZF (without foundation) does not in any obvious way (and hence not
>at all, by the argument from experience) imply the existence of a set
>x such that x={1,x}.  In particular, Replacement by itself is no help
>since to get x using replacement, we need to define a function h by
>h(n)=G(f(n)), where G({a,b})={1,G(b)}, and there is no way of defining
>G in ZF (without foundation) so that this is provable. In other words:
>Replacement allows us to make infinite "substitutions" in sets, but to
>make infinite substitutions in non-well-founded sets we need a
>corresponding non-well-founded recursion principle.
>
>  Of course, even if this is correct it doesn't follow that accepting
>A and rejecting B makes any sense. Or in other words: it doesn't help
>explain what mathematical objects, if any, you have in mind.

Neither A nor B can be shown to represent a unique object in ZFC-.
You are being hypnotized by your notation.  

There _can_ be sequences of sets xi and yi such that xi = {i,x[i+1}
and yi = {1,x[i+1]}  in ZFC-.  There can be many of each!  Thus A may
ambiguously denote many objects, and B may denote many objects -- nor
need an object denoted by B be an element of itself (it may contain a
_different_ object of the form B).

Aczel's AFA has a "strong extensionality" consequence which asserts
that there can be at most one object of the form A and at most one
object of the form B, in addition to its "non-well-foundedness"
consequence which asserts that there is at least one of each.

-- 
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: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: Impredicativity - was: Russell's Paradox
Organization: Boise State University
Date: Fri, 6 Nov 1992 19:31:34 GMT

Re Gudeman:

Your criterion for an acceptable property is wrong.

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.

My appeal to particular set theories is merely to point out that this
situation is coherent and belies your criterion for a property to be a
"real" property.  Some perfectly well-defined open sentences which
have truth values no matter what is substituted into them cannot have
extensions or intensions.  Once again, there is no problem with
self-membership or non-self-membership holding of particular objects;
there simply is no "object" which is the extension of
"self-membership" or "non-self-membership".  And this does not mean
that the objects in the universe are not unambiguously divided between
the self-members and the non-self-members; there is no ambiguity, no
gray area between them.  But there cannot be a set of the
non-self-members.

-- 
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
From: martinc@grover.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic
Subject: Re: Computer Science vs. Software Eng. (was re: Natural Kinds)
Date: 13 Nov 92 20:58:44 GMT
	<1992Nov12.222503.15918@vax5.cit.cornell.edu>
Followup-To: sci.logic
Distribution: sci
Organization: UNC Department of Computer Science
In-reply-to: horj@vax5.cit.cornell.edu's message of 13 Nov 92 03:25:03 GMT

In article <1992Nov12.222503.15918@vax5.cit.cornell.edu> horj@vax5.cit.cornell.edu (Eric Scheirer) writes:

   There are, empirically, at least three major ways of detecting bugs:

     1. Use the program until it fails to work.  

     2. Try to construct a lot of test cases during development.

     3. Try to prove the program correct (in the Gries sense) before coding it,
	and fail.

   Certainly, it would be possible to construct an argument that these 
   methods correspond to "science", "engineering", and "math" respectively.

It's an interesting thought, but I'm afraid you're mistaken.  Consider
the analogy with bridge-building that gets bandied about a lot -- an
engineer building a bridge certainly uses mathematical analysis to check
the idealiZed mathematical bridge against the specifications for that
bridge.  Similarly, a software engineer should (and someday will!) use
mathematical proof techniques to check the idealized program expressed
as a program text against the program's specifications.


--
		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
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:18:00 GMT

In article <1992Nov5.174527.22908@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
>In article <1992Nov5.164251.29649@guinness.idbsu.edu> holmes@garnet.idbsu.edu (Randall Holmes) writes:
>>You do not "weaken" FA to AFA; ZFC- + FA and ZFC- + AFA are both
>>stronger than ZFC-, but neither is stronger than the other.
>
>I guess this must be another of my misconceptions.  My general
>impresssion was that AFA was automatically true under FA, by virtue of
>the latter saying that only "unwound" graphs were permitted, and that
>every chain on the unwinding had to terminate.  So what's an example FA
>situation contradicting AFA?
>-- 
>Vaughan Pratt				There's no truth in logic, son.

AFA asserts the existence of a set (only one) which is its own sole
element; FA asserts the impossibility of such a set.

-- 
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: mclean@itd.nrl.navy.mil (John McLean)
Subject: Re: Natural Kinds (was re: Are all crows bl
Reply-To: mclean@itd.nrl.navy.mil
Organization: Information Technology Division, Naval Research Laboratory
Date: Fri, 6 Nov 1992 20:48:54 GMT

From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt):
>In article <1992Sep23.094901.1@sscvx1.ssc.gov> doctorj@sscvx1.ssc.gov writes:
>>pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
>>How about: Physics is science, while math is not.  By science, I mean 
>>the sequence:
>>  1: Look at the existing data and formulate a theory which explains it.
>>  2: Use that theory to predict new results.
>>  3: Perform experiments (ie, collect more data) to test the theory.
>>  4: Go to 1.
>>Math does not follow this sequence.  It does not contain falsifiable theories
>>in the way that physics does.
>>...
>>This use of the word "experiment" is ill conceived.  Computer calculations 
>>are not experiments.  Neither are slide rule or hand calculations.
>
>Let me not dispute your sequence here, but rather opine:
>
>(A) Math is perfectly capable of following your sequence.
>
>(B) Hypotheses can be falsified in math.
>
>(C) Falsification isn't all it's cracked up to be in either math or
>physics.

I have to admit that I'm a bit unclear who is saying what in the
above exchange, but let me make two comments.

First, I largely agree with claims (A)-(C) and recommend reading
Lakatos' multi-part article "Proofs and Refutations" which
originally appeared in the British Journal of the Philosophy of
Science and was later reprinted as a book.

Second,  although I largely agree with (A)-(C), I think that math and
physics do differ in degree.  What sequence (1)-(4) leave out is proof
in the sense of derivation.  Physical theories are usually established
by inference to the best explanation and are not usually derived from
other theories.  (Note I say "not usually".  Many important statements
of physics are derived from theories.  E=mc^2 comes to mind if I
remember my freshman mechanics course correctly.)  Mathematical
statements are usually justified by derivation or by finding a
counterexample to its negation (which can also be viewed as a
derivation).  Nevertheless, when evaluating axioms, one often
experiments with their consequences and makes what resembles an
empirical judgement about the truth of the axioms.  Witness the
discussion on set theory.

Let me go out on a limb and say that the emphasis on derivation in
mathematics is why mathematicians spend so much time looking at
derivationally elegant, but nevertheless false, sets of axioms.  For
example, Euclidean geometry is still extensively studied although
Einstein showed that it is not true.  (My doubt about this last
observation is that one could say that physicists do the same when they
study Newtonian mechanics and that the underlying reason is the same in
both cases: both Newtonian mechanics and Euclidean geometry provide
useful approximations to the way the world is.)

John McLean

Newsgroups: sci.logic,sci.philosophy.meta
From: solovay@math.berkeley.edu (Robert M. Solovay)
Newsgroups: sci.logic
Subject: Re: Impredicativity - was: Russell's Paradox.
Date: 5 Nov 1992 09:06:36 GMT
Organization: U.C. Berkeley Math. Department.
NNTP-Posting-Host: math.berkeley.edu

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

>It should be pointed out that neither of the two axiomatizations of ZF
>(that I took as definitive of ZF for my bet that ZF will be shown
>inconsistent by 2012) mention FA.  These were the axiomatizations of
>Takeuti and Zaring in their book "Introduction to Axiomatic Set
>Theory", and of Schoenfield in his article in Barwise's "Handbook of
>Mathematical Logic."  I selected these only because of their
>accessibility, not because they omitted FA.  In fact I do not know of
>an equally accessible axiomatization of ZF that includes FA (we
>amateurs are appallingly ignorant).  Randall, you're the one appealing
>to FA here, can you suggest a suitably accessible axiomatization that
>includes it?  It would come in handy for future reference.
>

>Vaughan Pratt				There's no truth in logic, son.

	Foundation is definitely considered one of the standard axioms
of ZF. Try Kunen, Set Theory:An introduction to Independence Proofs,
for example.

	Bob Solovay
	solovay@math.berkeley.edu
Xref: sparky sci.logic:2017 alt.uu.future:270
From: martinc@hatteras.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic,alt.uu.future
Subject: Re: Are all crows black? => Logic as an essential subject?
Date: 12 Nov 92 07:19:08 GMT
	<1992Nov8.193612.16707@lclark.edu> <BxGFw2.AJv@cck.coventry.ac.uk>
	<1992Nov11.225953.231@galois.mit.edu>
Followup-To: sci.logic
Organization: UNC Department of Computer Science
In-reply-to: jbaez@riesz.mit.edu's message of 11 Nov 92 22:59:53 GMT

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

   In article <BxGFw2.AJv@cck.coventry.ac.uk> esz001@cck.coventry.ac.uk (Will Overington) writes:

   >Can I ask please, is syllogisms and the like what sci.logic is about,
   >or am I missing something fundamental.

   Syllogisms are what logicians were up to in the Middle Ages, and there's
   a lot of interesting stuff that has happened since.  (Actually logicians
   were already doing lots of other stuff in the Middle Ages.)  In the late
   1800's a study of the "foundations of mathematics" and logic began which
   led to a lot of spectacular results in this century, such as Goedel's
   theorems.  For a tour of logic you could do worse than to take a peek at
   the entries about logic in the Encyclopedia of Philosophy.  And you can
   read sci.logic to see what sorts of things people argue about.

Let's not put Will off of syllogistic logic, though, please.  There are
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".

And while they're at it, they could learn about the classical fallacies.
--
		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