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