HDTenEightyP/NetNews huggingface dataset:
From: paul@mtnmath.UUCP (Paul Budnik)
Newsgroups: sci.logic,sci.physics
Subject: Re: Lowneheim-Skolem theorem (was: Continuos vs. discrete models)
Date: 17 Nov 92 17:39:47 GMT
Followup-To: sci.logic
Organization: Mountain Math Software, P. O. Box 2124, Saratoga. CA 95070

In article <COLUMBUS.92Nov16105941@strident.think.com>, columbus@strident.think.com (Michael Weiss) writes:
> In an earlier post, Paul Budnik writes:
>    This well known result is called the Lowenheim and Skolem theorem. The
>    idea of the proof is that a formal system is a computer program for enumerating
>    theorems. The names of all real numbers created by such a program are
>    obviously countable. Of course the mapping of these real numbers to names is
>    not definable within the the formal system and thus these reals cannot be
>    shown to be countable within the system.
> 
> This is not the correct statement of the Loewenheim-Skolem theorem.  Here is
> one formulation (the so-called "downward" Loewenheim-Skolem theorem):

I did not say that the above was a statement of the theorem, but that it was
the idea of the proof. I suspect that the `downward' L-S theorem is a 
generalization of what I was referring to.

>     Any model of a countable first-order theory has a countable elementary
>     submodel.  (By "countable theory", we mean one whose language is
>     countable.  "Elementary" means, roughly, that any assertion true of the
>     model is true also of the submodel.)
> 
> Budnik's statement about there being only a countable infinity of definable
> real numbers is correct, if by "definable" we mean "definable by a formula
> in a countable theory".  This fact is essentially trivial, since there are
> only a countable number of formulas in such a theory.

But all formal system have only a countable number of formulas. You and
many mathematicians may believe that there exists a Platonic heaven in
which all reals reside and that some formal systems include sentences
referring to each of these reals. That is a philosophical conjecture that
is open to question.

> ... 
> In short: there may be good reasons for radically changing the foundations
> of physics (and there may not-- pace, defenders of the status quo(ntum)!),
> but the Loewenheim-Skolem theorem is not one of them.

I do not think anyone is going to accept or reject a physical theory based
on L-S. I do think it provides a valuable perspective in thinking about these
issues. A formal system is a computer program for enumerating theorems.
Whether it is anything beyond that and whether the infinite totalities
it supposedly refers to exists is an open question. There is no physical
evidence for such objects. It is hard to understand what such physical
evidence might be.

Follow ups are directed to `sci.logic'.

Paul Budnik
Newsgroups: sci.logic
From: guttman@circe.mitre.org (Joshua D. Guttman)
Subject: Re: Why Logic?
Organization: The MITRE Corporation, Bedford, MA 01730
Distribution: world 
Date: Thu, 19 Nov 1992 17:07:34 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.
   --Ray Cote

On the contrary, logical arguments may be not only valid, but also informative.

For instance, to explain why we use classical first order logic (for many
important purposes), logical theorems such as soundness and completeness are
very relevant.  So are fancier theorems such as the non-enumerability of
consequence in 2nd order logic, or Lindstrom's theorem.  

Of course it depends what the argument is intended to accomplish.  A truly
illogical person (perhaps a child) must be trained, not convinced.  A logical
person who wants to gain insight into what he's doing and why can learn a lot
from mathematical logic.  

I believe that this point is originally due to Michael Dummett, "Justification
of Deduction", in _Truth_and_Other_Enigmas_.

	Josh
Newsgroups: sci.logic
From: holmes@garnet.idbsu.edu (Randall Holmes)
Subject: Re: recursive definitions and paradoxes
Organization: Boise State University
Date: Fri, 20 Nov 1992 15:57:25 GMT

In article <1992Nov19.215048.26539@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.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.
>-- 
>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.

Separation = for any set A and each formula P, {x E A | P} exists.


-- 
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: torkel@sics.se (Torkel Franzen)
Subject: Re: implication truth table
Organization: Swedish Institute of Computer Science, Kista
	<TORKEL.92Nov18100921@isis.sics.se> <Bxwzqs.H8L@unx.sas.com>
Date: Wed, 18 Nov 1992 16:57:59 GMT

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

   >Perhaps another way of putting this is that the usual truth-functional
   >interpretation of the material conditional is about the weakest
   >interpretation that satisfies all the "usual" rules of inference.

  "Material conditional" is a bit misleading here, since the rules I
mentioned are all intuitionistically valid. That is, the inference of
"if A then B" from "not A" is not dependent on any equivalence of
"if A then B" with "not A or B", which is often taken to be required by
the "material conditional".
From: alti@dcs.ed.ac.uk (Thorsten Altenkirch)
Newsgroups: sci.logic
Subject: Re: Types of type theory
Date: 16 Nov 92 19:47:49 GMT
	<ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
	<1992Nov13.123046.17412@husc3.harvard.edu>
Organization: LFCS, Edinburgh

In article <1992Nov13.123046.17412@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:

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

   I would prefer not to conflate intuitionism with constructivism;

Sorry, if I gave this impression. Although Type Theory (in the sense
of Martin-L"of) is constructive it is not necessarily intuitionistic,
i.e. we may accept Markov's principle.  This would be particularly
useful if you use Type Theory for program verification. However, all
the Type Theories I know are actually intuitionistic.

   otherwise
   your final remark is misleading, as the results of G\"odel and Tarski imply
   that any proof-theoretic conception of mathematical truth will fall short
   of the bivalence required by the classical reasoning.

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
(i.e. you decide to use only the equations of the call-by-value
\lambda calculus). 

I suppose the most famous person working in this direction is Girard
who last year wrote a paper entitled "A New Constructive Logic:
Classical Logic". However, I should also mention Parigot's "Free
Deductions" and Vilinsky's categorical account of continuations.
--

 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!
From: rar@csl.sri.com (Bob Riemenschneider)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 21 Nov 92 17:40:00
Organization: Computer Science Lab, SRI International, Menlo Park, CA.
NNTP-Posting-Host: birch.csl.sri.com
In-reply-to: sasghm@theseus.unx.sas.com's message of Fri, 20 Nov 1992 20:19:31 GMT

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

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

Beth's theorem ("Padoa's method is general"), a more-or-less immediate
consequence of the Craig interpolation lemma.  (No doubt Mr. Gudeman
will be unimpressed, however.)

                                                        -- rar
Newsgroups: sci.logic
From: wjcastre@magnus.acs.ohio-state.edu (W.Jose Castrellon G.)
Subject: Re: Why invalid?
Summary: Solution 
Organization: The Ohio State University,Math.Dept.(studnt)
Date: Wed, 18 Nov 1992 00:22:16 GMT

In article <1992Nov17.164246.18220@uklirb.informatik.uni-kl.de> ayala@uklirb.informatik.uni-kl.de (Mauricio Ayala R.) writes:

>Can anyone give me a counterexample of the following:
>
>Let T a consistent first order theory with equality which
>decidable set of quatifier-free logical consequences:
>
>  QF(T) = { B  |   t |= B, B quantifier-free }
>
>Let A be a T-consistent quantifier-free formula.
>Then (T,A) is also a consistent first order logic with
>equality and QF(T,A) is ALSO DECIDABLE.
>
>M. Ayala
>Universitaet Kaiserslautern
>FRG
>ayala@informatik.uni-kl.de
>

Solution follows.










Take the theory over the language with one constant  0 , one function  f(x) ,
one unary predicate  P(x), and a binary relation  R(x,y), as follows:

For all  x  R(0,f(x))
R(0,0)
and for each  n  in a non-recursive r.e. set, the axioms:

[ There exists an  x  such that  not R(0,x) ]  -->  [ P(n) ]

(where  n  is the abbreviation of  f(x)  applied  n  times to  0 )

Then one can check that the set of quantifier free sentences that are logical
consequences of this axioms is recursive.

However if one expands the language with one more constant  c , and add the
sentence   not R(0,c), then that set becomes non-recursive.  [if you dont allow
an expansion of the language, then it can be shown that there is no counter-
example].
From: bevan@cs.man.ac.uk (Stephen J Bevan)
Newsgroups: sci.logic
Subject: Re: What is Computer Science (was: Natural Kinds)
Date: 19 Nov 92 19:52:01 GMT
	<BEVAN.92Nov17144906@beluga.cs.man.ac.uk> <BxwzEo.Gv4@unx.sas.com>
Organization: Department of Computer Science, University of Manchester
In-reply-to: sasghm@theseus.unx.sas.com's message of 18 Nov 92 13:42:23 GMT

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?

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

bevan
Newsgroups: sci.logic
From: hbe@sonia.math.ucla.edu (H. Enderton)
Subject: Re: Looking for references on IF-THEN-ELSE connectives
Organization: UCLA Mathematics Department
Distribution: sci
Date: Sun, 15 Nov 92 18:32:08 GMT

In article <POSEGGA.92Nov13122538@margaux.ira.uka.de>
posegga@margaux.ira.uka.de (Joachim Posegga) writes:
>I am looking for references on ternary IF-THEN-ELSE connectives in
>logic. Church, for instance, treats expressions of the form [A,B,C],
>meaning "(B -> A) & (~B -> C)", in his book "Introduction to
>mathematical logic".
>Does anyone know of other papers/books on this? I am aware of Bauer &
>Wirsing (1991), Orlowska (1967 and 1969), and Shannon (1938).

A number of older works treating this ternary connective can be
found by looking in the JSL subject indexes (volumes 26 and 45)
under "conditioned disjunction."

---Herb Enderton    (hbe@math.ucla.edu)

Newsgroups: sci.logic
From: torkel@sics.se (Torkel Franzen)
Subject: Re: Do completed infinite totalities exist? Was: Lowneheim-Skolem theorem
Organization: Swedish Institute of Computer Science, Kista
	<365@mtnmath.UUCP>
Date: Fri, 20 Nov 1992 15:06:05 GMT

In article <365@mtnmath.UUCP> paul@mtnmath.UUCP (Paul Budnik) writes:

>This is an important and useful concept. Does this mean that we must accept
>that the set of all reals as a completed infinite totality? I do not think so.

  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.
Newsgroups: sci.logic
From: wjcastre@magnus.acs.ohio-state.edu (W.Jose Castrellon G.)
Subject: Re: Why invalid?
Organization: The Ohio State University,Math.Dept.(studnt)
Date: Sat, 21 Nov 1992 19:58:27 GMT


In article <Bxzvpx.Bp7@cantua.canterbury.ac.nz> wft@math.canterbury.ac.nz (Bill Taylor) writes:

>|> >Can anyone give me a counterexample of the following:
>|> >
>|> >Let T a consistent first order theory with equality which
>|> >decidable set of quatifier-free logical consequences:
>|> >
>|> >  QF(T) = { B  |   t |= B, B quantifier-free }
>|> >
>|> >Let A be a T-consistent quantifier-free formula.
>|> >Then (T,A) is also a consistent first order logic with
>|> >equality and QF(T,A) is ALSO DECIDABLE.
>
>|> Solution follows.
>|> 
>|> Take the theory over the language with one constant  0 , one function  f(x) ,
>|> one unary predicate  P(x), and a binary relation  R(x,y), as follows:
>|> 
>|> For all  x  R(0,f(x))
>|> R(0,0)
>|> and for each  n  in a non-recursive r.e. set, the axioms:
>|> 
>|> [ There exists an  x  such that  not R(0,x) ]  -->  [ P(n) ]
>|> 
>|> (where  n  is the abbreviation of  f(x)  applied  n  times to  0 )
>|> 
>|> Then one can check that the set of quantifier free sentences that are logical
>|> consequences of this axioms is recursive.
>|> 
>|> However if one expands the language with one more constant  c , and add the
>|> sentence   not R(0,c), then that set becomes non-recursive.  [if you dont allow
>|> an expansion of the language, then it can be shown that there is no counter-
>|> example].
>
>I don't quite get this comment. If the constant c is in the original language,
>but with no extra axioms, isn't the original theory still decidable for
>quantifier-free formulas ? And thus isn't the example now a counterexample
>of the type originally required ?
>

Bill, what happens is that with that extra constant in the language, some 
quantified sentences of the original language can have quantifier free logical
consequences:

(*)     [ There exists an  x  such that  not  R(0,x) ]  -->  [ P(n) ]

will imply the quantifier free sentence     

(**)    not R(0,c) -->  P(n)
[ only for the n's that satisfy  (*) ].

So if the set of quantifier free sentences of the theory in the new language 
(with no extra axioms, other than logical ones) were recursive, by looking at 
the sentences of the form (**) one could decide membership in the non-recursive
r.e. set we started with.  [ actually the reason to include the axiom R(0,0)
was to avoid this kind of situation for the constant  0 ]. [ By the way, a 
fellow student pointed out that in fact there are no counterexamples if we only
allow new relation symbols in the new language ].
Newsgroups: sci.logic
From: klaus@hal.nta.no (Klaus Gaarder FNI)
Subject: Re: Why Logic?
Organization: Norwegian Telecom Research
Date: Fri, 20 Nov 92 10:18:50 GMT

In article <MARTINC.92Nov18221201@hatteras.cs.unc.edu>
Date: 19 Nov 92 03:12:01 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?

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

Sorry, but I completely fail to see what's so deep about your comment, I also fail
to see what it has to with " re-seeing silly paradoxes".

I thus consider my response to your flame as valid as ever before.

Klaus@NTR
-- 
    __o   
  _`\<,_  
 (*)/ (*) Claudio Caputti
+++++++++++++++++++++++++++++++++++++++^++++++++++++++++++++++++++++++++++++++
Free will - the result of chaotic amplification of quantum events in the brain.
------------------------------------------------------------------------------
From: frank@Cookie.secapl.com (Frank Adams)
Subject: Re: recursive definitions and paradoxes
Date: Sat, 21 Nov 1992 23:05:30 GMT
Organization: Security APL, 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
>altered ZF to contain this axiom (and introduction of definitions)?  In
>the first place, you could immediately prove the existence of all sets
>that are already there.  And by adding some of the well-known machinery
>from recursion theory to prove Exist!... you could also talk about a lot
>of self-containing sets.  Wouldn't this theory be much more powerful
>than ZF?

Actually, no.  Unless I am much mistaken, this kind of definition is
eliminable.  If we have a definition X := E, we can rewrite a wff of
the form P(X) as (All X.((Ex! X.X=E) => X=E) => P(X)).

(This rewrite is a bit complicated, since it covers the case where X is not
uniquely defined.  The essential form is (All X.X=E => P(X)), which can be
used if Ex! X.X=E has been proved.)

Please try again.
Newsgroups: sci.logic
From: jon@cs.washington.edu (Jon Jacky)
Subject: Re: Programs for simple logic proofs:  where are they?
Summary: Otter and HOL are very nice, but probably not what the poster wanted
Keywords: Natural deduction, automatic theorem proving, Otter, HOL, Muffin
Organization: Computer Science & Engineering, U. of Washington, Seattle
Date: Mon, 16 Nov 92 18:32:10 GMT

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?

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

I think what the original post was asking for was a simple natural deduction
prover for propositional logic, where the problem statements and proofs look
much as they do in a logic textbook.   Do such things exist?  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.

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA



Newsgroups: sci.logic
From: klaus.gaarder@nta.no (Klaus Gaarder TFI)
Subject: Re: Why Logic?
Organization: Norwegian Telecom Research
Date: Wed, 18 Nov 92 14:24:34 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.
|> --Ray Cote

Simple: to get from 'true' statements about some universe of discourse to other
true statements of the same universe. Why this has turned out to be the preferred
way of doing science should be obvious.

Klaus
-- 
    __o   
  _`\<,_  
 (*)/ (*) Claudio Caputti
+++++++++++++++++++++++++++++++++++++++^++++++++++++++++++++++++++++++++++++++
Free will - the result of chaotic amplification of quantum events in the brain.
------------------------------------------------------------------------------
Xref: sparky sci.logic:2075 sci.physics:19074