The Math Forum

Search All of the Math Forum:

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

Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   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
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Mar 9, 11:09 am, Frederick Williams <>
> Graham Cooper wrote:

> > On Mar 9, 5:46 am, Frederick Williams <>
> > wrote:

> > > Graham Cooper wrote:
> > > > > > On Mar 7, 9:21 am, Frederick Williams <>
> > > > > > 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

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


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

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

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


Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.