
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
TABLE HEADS 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 CONS(A,B), HEAD(H,S), TAIL(T,S) and APPEND(A,B,C) 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

