Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.

Topic: Eliminating Quantifiers For Dummies! A(x) E(y) ALL(t)EXIST(u)EaAb ..
Replies: 50   Last Post: Jan 28, 2012 11:25 AM

 Messages: [ Previous | Next ]
 Marshall Posts: 1,928 Registered: 8/9/06
Re: Eliminating Quantifiers For Dummies! A(x) E(y) ALL(t)EXIST(u)EaAb ..
Posted: Jan 23, 2012 11:21 PM

On Jan 23, 7:52 am, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Jan 23, 10:23 am, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>
>
>
>
>
>
>
>
>

> > Jack Campin <bo...@purr.demon.co.uk> writes:
> > >> > There is a decision procedure for equality of terms in the first
> > >> > order theory of Abelian groups (and for a lot of other subtheories
> > >> > of the first order theory of groups).

>
> > >> > Express the same problem in your language and there isn't one.
>
> > >> Why not?  If there's a decent translation of the original statements
> > >> into statements in the DC version of abelian group theory, and DC is
> > >> complete, then there's still a decision procedure for the translated
> > >> statements.

>
> > >> No decision procedure for arbitrary statements in DC, I agree.
>
> > > The problem is identifying which expressions in DC are suitable
> > > inputs for a decision procedure (rewrite rule system, say).  You're
> > > only going to be able to do that if you know enough to reconstruct
> > > their equational forms.  If you don't even recognize the existence
> > > of a first-order group theory sublanguage in your calculus, this is
> > > going to be difficult.

>
> > As long as you have a decent translation, then the image of that
> > translation gives you the statements you are interested in.
> > I can't see any serious issue in describing such a translation --
> > in fact there are steps in that direction elsewhere in the thread.

>
> > >  The examples DC has given include no more
> > > than assertions of membership in a single carrier set, and they
> > > can just be thrown away, but in principle things can get much more
> > > complicated.

>
> > Yes, in principle -- but that complication doesn't affect the
> > decidability of the validity of the translated inputs.  (The set theory
> > needed would be minimal anyway, presumably)

>
> Sorry, no set theory at all for Jack! In his first-order group theory,
> Jack will not even admit "0 in G." No "elements of a set." No
> underlying sets and no implicit domains of  quantification. His first-
> order group theory is to be completely untainted by ANY set-theoretic
> considerations whatsoever, right, Jack? Am I wrong? I really hope so.

And that's not all! Jack also doesn't have any group-theoretic
considerations in his set theory!

Hey, how come DCProof doesn't have any image editing tools
in it? Not even a simple pencil drawing tool. Why is that?

Marshall

Date Subject Author
1/23/12 Alan Smaill
1/23/12 Dan Christensen
1/23/12 Dan Christensen
1/24/12 Frederick Williams
1/24/12 Dan Christensen
1/24/12 Rotwang
1/24/12 Dan Christensen
1/25/12 Rotwang
1/25/12 Ki Song
1/25/12 Dan Christensen
1/25/12 Rotwang
1/26/12 Dan Christensen
1/26/12 Tony Bones Orlow
1/26/12 Frederick Williams
1/26/12 Tony Bones Orlow
1/26/12 Frederick Williams
1/26/12 Tony Bones Orlow
1/26/12 William Hale
1/26/12 Tony Bones Orlow
1/26/12 William Hale
1/26/12 Tony Bones Orlow
1/26/12 MoeBlee
1/26/12 Dan Christensen
1/26/12 MoeBlee
1/26/12 Dan Christensen
1/26/12 MoeBlee
1/26/12 Dan Christensen
1/27/12 MoeBlee
1/26/12 Tony Bones Orlow
1/26/12 Dan Christensen
1/27/12 Tony Bones Orlow
1/27/12 Dan Christensen
1/27/12 Tony Bones Orlow
1/27/12 Frederick Williams
1/27/12 MoeBlee
1/27/12 Tony Bones Orlow
1/27/12 Tony Bones Orlow
1/27/12 MoeBlee
1/27/12 MoeBlee
1/27/12 MoeBlee