HDTenEightyP/NetNews huggingface dataset:
From: mclean@itd.nrl.navy.mil (John McLean)
Subject: Re: Self-Reference and Paradox (was Re: Human i
Reply-To: mclean@itd.nrl.navy.mil
Organization: Information Technology Division, Naval Research Laboratory
Date: Tue, 17 Nov 1992 20:39:42 GMT

From daryl@oracorp.com (Daryl McCullough)
>In comp.ai.philosophy, we were discussing the meaningfulness of
>self-referential sentences, and I noticed that many people seem to
>think that such sentences are inherently invalid, or meaningless, or
>paradoxical.
>In my opinion, the problem with such sentences are not with their
>self-referential character, but with their use of an unrestricted
>notion of truth (or falsity).

Certainly the paradox is not due solely to self-reference.  There is
nothing paradoxical about the self referring sentence; "This sentence
has five words".  Your appeal to a restricted notion of truth is
essentially Tarski's solution.

From pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
>All I know of Kripke's work is a talk I heard by a third party about a
>semantic proposal by Kripke for a logic of Per Martin-Loef.  As I
>understood it Kripke had suggested interpreting "This sentence is
>false" as having the truth value "undefined"

It's been a long time since I read Kripke's paper on truth, but as
I remember, his basic way of assigning a truth value is as follows:

	1.  Assign truth values to simple sentences (e. g. "Snow is white"
	    is assigned true and "Snow is black" is assigned false).
	2.  Assign truth values that assert the truth or falsity of
	    sentences assigned truth values in the previous step (e. g.,
	    "`Snow is white' is true" is assigned true, "`Snow is white' is
	    false" is assigned false, etc.).
	3.  Continue.

This process produces a least fixed point.  A sentence is true if it
is assigned true in that fixed point, false if it is assigned false
in that fixed point, and ungrounded otherwise.  Note that all paradoxical
sentences are ungrounded.  However, some ungrounded sentences may not
be paradoxical, e. g., "This sentence is true".  A sentence is paradoxical
only if it cannot be assigned a truth value at any fixed point.

The difference between this solution and Tarski's is that whereas
Tarski has a separate, but completely defined, notion of truth at each
linguistic level of a language, Kripke has a single, but not completely
defined, notion of truth for the entire language.
 
John McLean

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

In article <1992Nov16.050846.15982@infodev.cam.ac.uk> gjm11@cus.cam.ac.uk (G.J. McCaughan) writes:
>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.)

This is exactly what I was thinking about.  There would also have to
be some algorithm that one could not prove to not be in P.  Would this
algorithm have to be "objectively" in P?

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


-- 
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: hbe@sonia.math.ucla.edu (H. Enderton)
Subject: Sacks Symposium, May '93
Organization: UCLA Mathematics Department
Date: Sun, 15 Nov 92 18:36:52 GMT

                        THE SACKS SYMPOSIUM

A conference in mathematical logic will be held May 13-16, 1993 at the
Massachusetts Institute of Technology in honor of Professor Gerald
Sacks on the occasion of his 60th birthday.  Invited speakers include:
Harvey Friedman, Robin Gandy, Leo Harrington, Eugene Kleinberg, Simon
Kochen, Georg Kreisel, Alistair Lachlan, Manuel Lerman, Alain Louveau,
Menachem Magidor, Yiannis Moschovakis, Anil Nerode, Dag Normann,
Richard Shore, Theodore Slaman, Robert Soare, Carol Wood, and Hugh
Woodin.  There will be sessions for contributed papers and an evening
banquet.  The conference will be supported by the NSF and local
universities, and will enjoy the participation of the Mid-Atlantic
Mathematical Logic Seminar (MAMLS) and the New England Set Theory
Seminar (NESTS).  Some financial assistance will be available to
students and recent Ph.D.'s.  Women and minorities are particularly
encouraged to apply.  Conference organizers: Sy Friedman
(sdf@math.mit.edu), Steve Homer (homer@cs.bu.edu) Aki Kanamori
(aki@math.bu.edu), and Ted Slaman (ted@zaphod.uchicago.edu).  For more
information or to be put on the mailing list, contact one of the
organizers.  To contribute a paper or to apply for financial
assistance, contact Sy Friedman.
From: turpin@cs.utexas.edu (Russell Turpin)
Newsgroups: sci.logic
Subject: Re: Why invalid?  (was:  Why logic?)
Date: 16 Nov 1992 13:41:30 -0600
Organization: CS Dept, University of Texas at Austin
NNTP-Posting-Host: peaches.cs.utexas.edu

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

Unfortunately, I have no notion of what Ray Cote means by
"invalid."  Perhaps he could explain this.  (Those who notice
that such explanation is meta-logical discussion get an A.)

Russell
From: rh@smds.com (Richard Harter)
Newsgroups: sci.logic
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Date: 22 Nov 92 07:47:40 GMT
Reply-To: rh@ishmael.UUCP (Richard Harter)
Organization: Software Maintenance & Development Systems, Inc.

In article <TORKEL.92Nov21195445@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:

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

Perhaps the distinction is quite simple, but I fail to see it.  In
particular I fail to see why there isn't an implicit formal system
in the concept of "uncountable".  Unless one accepts the notion of
the absolute uncountable, uncountability is always relative to s
system and a model for the system, is it not?
-- 
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,sci.math
From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Logic and Mathematicians
Organization: Computer Science Department,  Stanford University.
Date: Mon, 16 Nov 1992 19:30:17 GMT

In article <1992Nov16.165221.5725@guinness.idbsu.edu> holmes@garnet.idbsu.edu (Randall Holmes) writes:
>This is exactly what I was thinking about.  There would also have to
>be some algorithm that one could not prove to not be in P.  Would this
>algorithm have to be "objectively" in P?

P consists of sets, not algorithms.  A slow algorithm says nothing
about the complexity of the set it accepts.
-- 
Vaughan Pratt	  		A fallacy is worth a thousand steps.
From: bevan@cs.man.ac.uk (Stephen J Bevan)
Newsgroups: sci.logic
Subject: Re: What is Computer Science (was: Natural Kinds)
Date: 17 Nov 92 14:49:06 GMT
	<BEVAN.92Nov11113345@hippo.cs.man.ac.uk> <Bxt9GA.Iyp@unx.sas.com>
Organization: Department of Computer Science, University of Manchester
In-reply-to: sasghm@theseus.unx.sas.com's message of 16 Nov 92 13:28:58 GMT

In article <Bxt9GA.Iyp@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:

   In article <BEVAN.92Nov11113345@hippo.cs.man.ac.uk>, bevan@cs.man.ac.uk (Stephen J Bevan) writes:
   |> What are "etc." in this case?  I'm still waiting to see any mention of
   |> a "science" that isn't (IMHO) a "natural science".

   Well, there are some who consider the social sciences (anthropology,
   sociology, psychology) to be sciences.

But why?  What attributes do they possses that makes them a "science"
that computer science (sic) does not have?  (Maybe we need somebody
who considers them as a science to answer this question).

   [geology example deleted as IMHO it is a "natural" science]

   [description of routing problem deleted]

   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.

Maybe you missed my previous message; this is the second time I've
used this example in this context.

bevan
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 20 Nov 92 17:46:33 GMT
Organization: U of Arizona CS Dept, Tucson

In article  <1992Nov19.215048.26539@CSD-NewsHost.Stanford.EDU> Vaughan R. Pratt writes:
]In article <26788@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
]>But consider the paradoxical definitions
]>
]>  S := {{},R}
]>  R := {x E S : ~(x E x)}                                (8)
]>
]>where the definition of R has exactly the same form as the definition of
]>Russell's paradoxical set (replacing S with the universal set).  But
]>here, S is a set with only two elements!  Given such a clear example of
]>Russell's paradox by quantifying over a finite set, I don't see how
]>anyone can still claim that Russell's paradox is somehow caused by a
]>universal set that is "too big".  Size has nothing to do with it, the
]>only consideration is how it is defined.  Clearly in this example the
]>problem is an ill-founded mutual recursion between the two set
]>definitions.
]
]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.

Your argument, depending as it does on universals, cannot account for
the finite paradox I present above (nor can it account for a host of
other logical and "linguistic" paradoxes).  Therefore, if you insist
on this explanation of Russel's paradox, you require two different
explanations for two very similar paradoxes.  I can explain both of
them at once.  Doesn't this give my explanation more credibility?

My explanation of the paradoxes (I claim) applies universally to _all_
the common paradoxes of logic --including the so-called linguistic
paradoxes.  I've actually gone through a large subset of them to
verify this.  In each case, I could find no way to write the paradox
without some form of recursion, and in each case, my axiom of
definition (or its equivalent) would render the paradox harmless.
Isn't this "unified paradox theory" better than a set of theories that
requires different explanations for different paradoxes?
-- 
					David Gudeman
gudeman@cs.arizona.edu
Organization: Masters student, Philosophy, Carnegie Mellon, Pittsburgh, PA
Newsgroups: sci.logic
Date: Sat, 21 Nov 1992 14:20:43 -0500 
From: Asmawi Mohamad <am5j+@andrew.cmu.edu>
Subject: Recursive Functions

I am taking a course in logic this semester, and currently looking for
a good introductory text in recursive function that include some discussion
about the application of RF in computability.  Does anyone out here knows
about the availability of books about this?

Thanks a lot
Newsgroups: sci.logic
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Subject: Re: recursive definitions and paradoxes
Originator: sasghm@theseus.unx.sas.com
Date: Thu, 19 Nov 1992 21:37:13 GMT
Organization: SAS Institute Inc.


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) '='?  If the
"Axiom of Definition" is being proposed for discussion, we really
need some more axioms for ':=', since at the moment it appears only
on the left-hand side of one conditional axiom and otherwise has
some informal semantics (it is said to be a "definition") attached
to it.  The standard approach, of course, is to introduce definitions
into theories by using the usual '=' and '<->'.

It is quite correct to observe that "we have to be careful what we
take to be a definition".  There is a fairly widely known *theory*
of definition in which certain criteria must be satisfied in order
for a formula to be a definition (actually, things are probably
better put in terms of "definitional extensions" of theories).
I can't put my hands on specific references at the moment, but the
names of Patrick Suppes and Quine come to mind.  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.  (Certain of the paradoxes failed in
the system of my dissertation because it could be shown that the
proposed "definition" of the truth predicate required did not
constitute a definitional extension of the theory.)

At any rate, it seems that any discussion should take place within
the context of the theory (or at least *a* theory, and then why
not the usual one?) of definition.
-- 
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
From: sasghm@theseus.unx.sas.com (Gary Merrill)
Newsgroups: sci.logic
Subject: Re: Recursive Functions
Date: 23 Nov 92 15:50:04 GMT
Organization: SAS Institute Inc.
Originator: sasghm@theseus.unx.sas.com


In article <gf3ck=e00WB5IVcUsC@andrew.cmu.edu>, am5j+@andrew.cmu.edu (Asmawi Mohamad) writes:
|> I am taking a course in logic this semester, and currently looking for
|> a good introductory text in recursive function that include some discussion
|> about the application of RF in computability.  Does anyone out here knows
|> about the availability of books about this?
|> 
|> Thanks a lot

I like (and have taught from) _Computability and Logic_ by Boolos
and Jeffrey.
-- 
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
From: plummer@cs.swarthmore.edu (David Barker-Plummer)
Newsgroups: sci.logic
Subject: Re: Programs for simple logic proofs:  where are they?
Date: 16 Nov 92 23:07:04 GMT
Organization: Swarthmore College, Swarthmore, PA

In article <1992Nov16.183210.9769@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes:

JJ> 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?

JJ> I saw two responses to this post, recommending Otter and HOL.  I think they
JJ> made it clear that they were probably not what Mike Brown was looking for.
JJ> The Otter and HOL versions of this very simple proof don't look a whole lot
JJ> like Mike's very clear presentation.  I've read the book about Otter and 
JJ> learned/used a little of HOL; they are both powerful research systems, with
JJ> all that entails.

JJ> I think what the original post was asking for was a simple natural
JJ> deduction prover for propositional logic, where the problem
JJ> statements and proofs look much as they do in a logic textbook.
JJ> Do such things exist?  The nearest thing I have read about is
JJ> "Muffin: A Proof Assistant", a chapter by Richard C. Moore in
JJ> Jones and Shaw, CASE STUDIES IN SYSTEMATIC SOFTWARE DEVELOPMENT,
JJ> Prentice Hall International, 1990. I recall the chapter saying
JJ> something about Muffin being made available.  I wonder if anyone
JJ> is using it.

Andrews' system, ack I can't remember its name right now, allws you to
construct proofs in exactly the standard natural deduction
presentation of the original poster's example.  Contact Peter Andrews
at CMU.  Of course, the underlying logic of this prover is typed
higher order logic, and is significantly more powerful (and hence
harder to understand) than the simple example would suggest.

Another system that comes to mind is MacLogic developed by Roy Dychoff
at St. Andrews University (rd@cs.st-and.ac.uk).  I am not sure of the
availability, but this is the sort of system I would choose for
teaching natural deduction to neophytes.

-- Dave
From: cmenzel@tamsun.tamu.edu (Chris Menzel)
Subject: Re: recursive definitions and paradoxes
Organization: Texas A&M University, College Station
Date: Fri, 20 Nov 1992 21:08:03 GMT

In article <26788@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>A "recursive definition" of a name X is a sentence of the form
>
>  X := E
>
>where E is an expression that contains X as a free variable.  Naively we
>might associate with such definitions the axiom
>
>  X := E => X = E
>
>To express what a definition means.  (We also need some syntactic rules
>to allow the introduction of definitions so that the same name is not
>used for different purposes.)
>
>Here are some examples of recursive definitions:
>
>(1) x := x + 1
>(2) x := x * 2
>(3) x := 1/x
>(4) x := x * 1

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.  (The
legitimacy of such definitions in set theory is of course a theorem to
be proved; I believe von Neumann was both the first to see this and
the first to provide the requisite proof.  Levy's Basic Set Theory
has a nice, detailed proof in ZF.)  Unless I'm really missing
something, the above are not recursive definitions in this sense, nor
is the definition of the Russell set.

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

--Chris Menzel
  Philosophy Department
  Texas A&M University
From: alti@dcs.ed.ac.uk (Thorsten Altenkirch)
Newsgroups: sci.logic
Subject: Re: Types of type theory (Errata)
Date: 16 Nov 92 22:42:20 GMT
	<ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
	<1992Nov13.123046.17412@husc3.harvard.edu>
	<ALTI.92Nov16194749@tanera.dcs.ed.ac.uk>
Organization: LFCS, Edinburgh

In article <ALTI.92Nov16194749@tanera.dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:

   Certainly, but this just means that you have to give up something to
   get classical reasoning AND propositions as types. I am not an expert
   in this area but as I understand it: You may have a computational
   interpretation of type theory if you 'fix' your evaluation strategy
		     ^^^^^^^^^^^
Should read: classical logic

   (i.e. you decide to use only the equations of the call-by-value
   \lambda calculus). 

Sorry.
--

 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:2074 sci.physics:19073