HDTenEightyP/NetNews huggingface dataset:
From: sjt@ukc.ac.uk (S.J.Thompson)
Newsgroups: sci.logic
Subject: Looking for proof checking/building software for teaching
Date: 23 Nov 92 20:06:46 GMT
Organization: Computing Lab, University of Kent at Canterbury, UK.

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

=======================================================================

Simon Thompson				e-mail:	sjt@ukc.ac.uk
Computing Laboratory			phone:	+44-227-764000 
University of Kent				  extn. 3820
Canterbury, Kent,			fax:	+44-227-762811
CT2 7NF, UK

=======================================================================
From: paul@mtnmath.UUCP (Paul Budnik)
Newsgroups: sci.logic
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Date: 21 Nov 92 16:49:29 GMT
Organization: Mountain Math Software, P. O. Box 2124, Saratoga. CA 95070

In article <TORKEL.92Nov20160605@lludd.sics.se>, torkel@sics.se (Torkel Franzen) writes:
>   You don't have to accept anything. You are free to develop whatever
> mathematics you like and put it forward for general consideration. What
> I am objecting to is only the idea that e.g. the distinction between
> countable and uncountable sets can be seen to be a "relative" one in
> the light of results in logic.

Everything in mathematics is "relative" to some formal system. To talk
about what is absolutely true independent of a foral system is philosophy
not mathematics. It is not something that can be derived from results
in logic. Perhaps I do not understand what you mean by relative. 

It would be awkward, but not necessarily unreasonable, to define a formal
system in which the reals are countable. One could add an axiom that allows
one to see from within the system that all the reals namable in the language
of the system are countable. This would have to be done with care so that
one could not use this model of oneself to construct paradoxes, but I do
not think there is any fundamental problem in doing this.

Paul Budnik
Newsgroups: sci.logic
From: klaus@hal.nta.no (Klaus Gaarder FNI)
Subject: Re: implication truth table
Organization: Norwegian Telecom Research
Date: Wed, 18 Nov 92 14:39:31 GMT

In article <1992Nov16.162733.1831@falcon.aamrl.wpafb.af.mil>, cmitchell@falcon.aamrl.wpafb.af.mil writes:
|> 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."
|> 

The easy way out is that you can do away with '->' if you don't like it, 
replace every occurence of 'A->B' with '((NOT A) OR B)', which has exactely the
same truth table interpretation. (This is because NOT and OR define a complete
set of logical connectives, where all the ususal truth functional connectives can
be defined in terms of NOT and OR, 'A AND B' is equivalent to 
NOT((NOT A) OR (NOT B)) (De Morgan) ). The reason the usual interpretation of
'->' looks weird, is as you note the coloquial notion of 'If ... then ...' as
having causal overtones, the mathematical notion being a model not necessarily
capturing these aspects. In e.g., so called 'modal' logic you will find other
notions of implication like 'A necessarily implies B' or 'if A then possibly B'
etc.

Klaus@NTR
-- 
    __o   
  _`\<,_  
 (*)/ (*) Claudio Caputti
+++++++++++++++++++++++++++++++++++++++^++++++++++++++++++++++++++++++++++++++
Free will - the result of chaotic amplification of quantum events in the brain.
------------------------------------------------------------------------------
From: martinc@hatteras.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic
Subject: Re: Why Logic?
Date: 17 Nov 92 20:17:35 GMT
Organization: UNC Department of Computer Science
In-reply-to: cotera@woods.ulowell.edu's message of 16 Nov 92 14:16:53 GMT

In article <1992Nov16.091653.1@woods.ulowell.edu> cotera@woods.ulowell.edu writes:

   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.

(Can we start a group for bozos who want to propose dusty old paradoxes
as if they were somehow something we hadn't all seen a thousand times
before?  Something like alt.logic.stupid-tricks?)
--
		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: guttman@circe.mitre.org (Joshua D. Guttman)
Subject: Re: Why Logic?
Organization: The MITRE Corporation, Bedford, MA 01730
	<1992Nov22.014208.6629@CSD-NewsHost.Stanford.EDU>
Distribution: world 
Date: Mon, 23 Nov 1992 15:40:06 GMT

pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
   guttman@circe.mitre.org (Joshua D. Guttman) writes:
   >cotera@woods.ulowell.edu writes:
   >
   >   Can anyone explain why we use logic? Unfortunately, any logical arguments to
   >   support logic, are unfortunately, invalid.
   >   --Ray Cote
   >
   >On the contrary, logical arguments may be not only valid, but also informative.
   >(etc.)

   This seems to fall far short of addressing the basic question of why we
   use logic.  Why not do all our thinking with just the equations of
   arithmetic?  Or the equations of binary relations under composition and
   converse as suggested by Tarski and Givant in "A Formalization of Set
   Theory without Variables."

Are you asking why we use a syntax of variables and predicates (or rather a
natural language grammar in which these can be discerned)?  Or are you asking
why a particular logic, quantified predicate logic, is more beneficial than
another, say purely equational logic?  

As for why we do not do all our thinking with equations of arithmetic, I'd
answer, because numbers are not the only things we want to think about, and
quantifier-free formulas are not the only ones we want to assert.  I have not
looked at Tarski/Givant.

As to why we use any sort of deductive reasoning, I'd answer, because we have
beliefs and we examine assumptions and we want to know what their consequences
are.  Indeed, it would hard to imagine that we could attribute beliefs to a
creature that did not trouble itself about their consequences.

	Josh
Newsgroups: sci.logic
From: frank@Cookie.secapl.com (Frank Adams)
Subject: Re: Logic and Mathematicians
Date: Mon, 23 Nov 1992 16:14:22 GMT
Organization: Security APL, Inc.

In article <1992Nov21.185205.3566@dorsai.com> mutation@dorsai.com (Florian Lengyel) writes:
>Computing processes seem too fundamental to me, too much a part of the
>way mathematics and meta-mathematics is conducted to begin with ...
>Computing processes, which include the computation of inferences, are  
>absolute, in other words, so they should not be suceptible to varying 
>interpretations of set theory that would lead to such grossly different 
>computational outcomes as P = NP under one interpretation and P <> NP 
>under another.

But non-standard interpretations of ZFC often have non-standard integers.
It is quite possible for an algorithm to "halt" in time n^K, where K is a
non-standard integer in such a model, but not to halt in time n^k for any
actual integer k.

If one could show P=NP in a model of ZFC (or more likely PA) which could be
shown to have non-standard integers, while showing P < NP in a model which
did not appear to require non-standard integers, that would be strong
evidence for P < NP.  Depending on the details, a proof (on the
meta-theoretic level) might even be possible.

It is also possible that P < NP, but that no proof is available in any
system we can accept.  More specifically, P < NP may be independent of ZFC,
but we will not be able to prove it.  This is possible for any unsolved
problem, of course, but it seems more likely for unsolved problems in
complexity theory (and even more so in computability and set theory) than in
most areas.
From: martinc@hatteras.cs.unc.edu (Charles R. Martin)
Newsgroups: sci.logic
Subject: Re: Why Logic?
Date: 19 Nov 92 03:12:01 GMT
	<MARTINC.92Nov17151735@hatteras.cs.unc.edu>
	<1992Nov18.144719.24323@nntp.nta.no>
Organization: UNC Department of Computer Science
In-reply-to: klaus@hal.nta.no's message of 18 Nov 92 14:47:19 GMT

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

   In article <MARTINC.92Nov17151735@hatteras.cs.unc.edu>, martinc@hatteras.cs.unc.edu (Charles R. Martin) writes:
   |> In article <1992Nov16.091653.1@woods.ulowell.edu> cotera@woods.ulowell.edu writes:
   |> 
   |>    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.
   |> 
   |> (Can we start a group for bozos who want to propose dusty old paradoxes
   |> as if they were somehow something we hadn't all seen a thousand times
   |> before?  Something like alt.logic.stupid-tricks?)

   This kind of response is what you expect from the dogmatic only, and
   being dogmatic is a simple reason NOT to use logic. 

There's a difference between being dogmatic and being deep.  Assume for
purposes of argument only that I was being deep: what did I mean then?

   Also your response suggest you don't like to think too hard about
   what you're doing, and why you're doing it.  It must be the power of
   commercials: "Just Do It!"

Wrong: just tired of re-seeing silly paradoxes that were old hat when
Jesus was a teenybopper.

   Your kind of flame is simply pathetic.

Nope, you just didn't understand 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
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: Fri, 20 Nov 1992 15:20:07 GMT
Organization: SAS Institute Inc.


In article <BEVAN.92Nov19195201@beluga.cs.man.ac.uk>, bevan@cs.man.ac.uk (Stephen J Bevan) writes:
|> In article <BxwzEo.Gv4@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
|> 
|>    |> What attributes do they [anthropology, sociology ... etc.]
|>    |> 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.  ... and that one attempts to formulate *empirical*
|>    theories in these disicplines all argue that they *are* sciences.
|>    [deleted]
|> 
|> Ok, here's my laymans translation of that :-
|> 
|> A science is any subject where practitioners trawl over data trying to
|> find a description can justify the data (and from which predictions
|> can be made about any future data).
|> 
|> Is that acceptable?

It's pretty close, I think, but incomplete.  I would expand it to include
an account of what a *theory* is, how the theory is related to the data,
and how theories are related to other theories.

|>    The degree to which (or the specific areas in which) computer science
|>    exhibits these characteristics is still pretty unclear to me.
|> 
|> Under my definition, I would venture that little of what goes on in a
|> CS dept. would be classed as a science (not even the example I gave
|> previously regarding routing).

This was the view with which I started.  And I still think that "little" is
correct.  How little, and how central, I'm not sure.
-- 
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: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: recursive definitions and paradoxes
Organization: Computer Science Department,  Stanford University.
Date: Fri, 20 Nov 1992 17:52:27 GMT

In article <1992Nov20.155725.11719@guinness.idbsu.edu> holmes@garnet.idbsu.edu (Randall Holmes) writes:
>>Russell's paradox denies the existence of the paradoxical set of all
>>sets.  Denial of an existential is a universal, and the universal
>>statement asserted by Russell's paradox is that every set has a
>>nonmember.  The universal set is "too big" by one element, having no
>>nonmember.  From that perspective size has everything to do with it.
>>-- 
>>Vaughan Pratt	  		A fallacy is worth a thousand steps.
>
>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.  If the Axiom of Separation is added to one's
>theory, the paradox has the consequence indicated.  In theories where
>the Axiom of Separation does not hold (like NFU) the paradox has
>different consequences.

Good point, I hadn't spent long enough thinking about the meaning of
David Gudeman's "What if you altered ZF to contain this axiom (and
introduction of definitions)?"  I guess this must entail dropping
Separation, right?
-- 
Vaughan Pratt	  		A fallacy is worth a thousand steps.
Newsgroups: sci.logic
From: torkel@sics.se (Torkel Franzen)
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Followup-To: sci.logic
Organization: Swedish Institute of Computer Science, Kista
	<363@mtnmath.UUCP>
Date: Thu, 19 Nov 1992 19:10:17 GMT

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.
From: cmenzel@tamsun.tamu.edu (Chris Menzel)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 23 Nov 1992 23:38:30 -0600
Organization: Texas A&M University, College Station, TX
NNTP-Posting-Host: tamsun.tamu.edu

In article <26884@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>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.  

Well I've looked in Fitch's book on Combinatory Logic, Curry's
mathematical logic text, and Barendregt's article in the Handbook of
Mathematical Logic on the untyped lambda calculus and can find no such
definition.  Fitch does refer to the type of definition you refer to
in the section of his book that immediately follows the section on
recursion, but calls them "self-referential" or "impredicative" or
something to that effect (I left the book in my office and can't
recall the exact term at the moment).  At any rate, as far as I could
see, the term 'recursive' is used only for recursive definitions in
the sense I gave above or for recursive functions in the usual sense.
Do you happen to have any references to support your usage?

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

How about, say, "impredicative" or "self-referential", for example?

>					David Gudeman
>gudeman@cs.arizona.edu

--Chris Menzel
  Philosophy Department
  Texas A&M University
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 20 Nov 92 17:30:34 GMT
Organization: U of Arizona CS Dept, Tucson

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.

]... 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.  Non-creative, eliminable definitions are
no more than abbreviations, and mathematics cannot be done with such a
sparse notion of definition.
-- 
					David Gudeman
gudeman@cs.arizona.edu
Newsgroups: sci.logic
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: Will a mathematician locked up in a little room be happy?
Originator: sasghm@theseus.unx.sas.com
Date: Mon, 16 Nov 1992 13:52:28 GMT
Organization: SAS Institute Inc.


In article <1326@kepler1.rentec.com>, andrew@rentec.com (Andrew Mullhaupt) writes:

|> Actually, even the most rarefied pure mathematician is not likely to be
|> happy with this arrangement, although it might be closer to his idea of
|> nirvana than what he presently occupies. History shows that communication
|> is essential for the bulk of good mathematics, (as far as I know no other
|> field is as addicted to its literature as mathematics). Hardy's criteria,
|> (good mathematics is _new_ _true_ and _interesting_), are not likely to be
|> much use in isolation. (_New_ and _Interesting_ seem obvious, but you have
|> to think a little about _true_...)

As I recall, Hardy also observed that the most work one could really
expect out of a mathematician was about four hours per day.  I believe
that the rest of the time (at least in Hardy's case) was to be devoted
to cricket.
-- 
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: recursive definitions and paradoxes
Originator: sasghm@theseus.unx.sas.com
Date: Fri, 20 Nov 1992 20:19:31 GMT
Organization: SAS Institute Inc.


In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> 
|> 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.  Non-creative, eliminable definitions are
|> no more than abbreviations, and mathematics cannot be done with such a
|> sparse notion of definition.

I have a vague recollection of a result that any recursive definition
is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
memory?).  At any rate, concerning the claim that mathematics cannot
be done with "such a sparse notion of definition", it is interesting
to inspect Chapters X and XI of Kalish and Montague where the theory
of commutataive ordered fields is definitionally extended to the theory
of real numbers which in turn is definitionally extended to the
theory of convergence.  A sketch is then given of how this can be
extended to the integral calculus (including an explicit definition
of the Riemann integral).  In passing, it is observed that the 'recursive
definition' of sigma (the summation operator) used in the theory can be
replaced by an explicit definition.  All this rests in part on the work
of Scott on arbitrary variabe binding operators.

Perhaps you really want to avoid talk of "definition" and simply speak
of "axiomatization".
-- 
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