Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Interdeducibility of properties of an abstract consequence relation.
Replies: 11   Last Post: Mar 8, 2013 8:40 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: Interdeducibility of properties of an abstract consequence relation.
Posted: Mar 8, 2013 8:40 PM

On Mar 9, 11:09 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> Graham Cooper wrote:
>

> > On Mar 9, 5:46 am, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:

> > > Graham Cooper wrote:
>
> > > > > > On Mar 7, 9:21 am, Frederick Williams <freddywilli...@btinternet.com>
> > > > > > wrote:

>
> > > > > > > P9 If Sub(M,x,y,N), Sub(alpha,x,y,beta) and M |= alpha, then N |= beta.
>
> > > > Again I don't see what P9 is for.
>
> > > > formula1 [X/Y] =  formula2
>
> > > > is standard substitution syntax.
>
> > > My (or rather, Hermes's) notation Sub(alpha,x,y,beta) signifies that
> > > alpha, x, y and beta stand in a certain relation to one another.
> > > Furthermore that relation is carefully defined.  (If it isn't carefully
> > > defined _in my post_, then the fault is mine and I shall rectify it.)
> > > What does the "standard" definition mean?  Standard may be good,
> > > understandable is better.

>
> > You've never seen
>
> > f(X+1) [Y/X]  =   f(Y+1)  ?
>
> I'd like you to define the general case, as I did with Sub, or, rather,
> as Hermes did.
>

You didn't define anything.

* if alpha is atomic, Sub(alpha,x,y,beta) iff beta is obtained from
alpha by replacing all occurrences of x with y,
* Sub(~alpha,x,y,beta) iff there is a gamma such that
Sub(alpha,x,y,gamma) and beta is ~gamma,
* Sub((alpha & beta),x,y,gamma) iff there are alpha' and beta' such
that Sub(alpha,x,y,alpha'), Sub(beta,x,y,beta') and gamma is
(alpha' & beta'),
* Sub(Uz alpha,x,y,beta) iff one of:
** x is not free in Uz alpha and beta is Uz alpha,
** x is free in Uz alpha, y is not z, and there is a gamma for which
Sub(alpha,x,y,gamma) and beta is Uz gamma.

You just wrote : "replace all occurrences of X with Y"

and a bunch of trivial identities.

as if this somehow magically lets you see inside (ALL) formula to
quantify over the right bits!

------------

I invented my own predicate argument indexing system so there is no
recursive string parsing (of arguments of arguments of...)

nat [ succ X ]
nat X

REF TERM VAR
1 nat
21 succ
22 * X

Now I can Match the entire Query String
to all predicates in 1 SQL Query.

ie. match multiple terms to multiple terms without recursively
tracking which position in the predicate you are at.

AFTER the predicate is found, a counter is added to each variable name
as they are all new anyway.

nat [ succ X1 ]
nat X1

Then new variable bindings are pushed onto the stack, and the Tails
are recursively checked.

To process strings at a high level you could use
then get SUBSTRING, LEFTSTRING, RIGHTSTRING etc..

-------------

Dan has formalised in VB
how to process Quantified Logic Strings
he might be more able to refine Hermes definitions
into something workable.

-------------

My Prolog Logic system will use @ to prefix an ALL(X) variable

subset S1 S2
e @A S2
e A S2

setequals
subset S1 S2
subset S2 S1

That is my formal code for Axiom of Extensionality.

It will check all members of S1 are in S2
and then check all members of S2 are in S1

although I will be only be working on finite sets.

Now SUBSET(S1, S2) is an atomic method that discards quantifiers
altogether.

{X | XeS1} C { Y | p(Y) }

that's an *ALL(X)* in that subset sentence!

------------

You have a LONG WAY to go before you can define WFF( p )

and its of no use anyway!

Herc
--
www.BLoCKPROLOG.com

Date Subject Author
3/6/13 Graham Cooper
3/6/13 Frederick Williams
3/6/13 Graham Cooper
3/6/13 Frederick Williams
3/7/13 Graham Cooper
3/8/13 Graham Cooper
3/8/13 Graham Cooper