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 7:02 PM

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

Making SUBS a predicate has no purpose and neither does formalising
variable renaming in Quantified logic.

As opposed to Lambda Calculus where substituting [Y/X] is used in the
computation.

Herc

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