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 7, 2013 4:26 PM

On Mar 7, 9:21 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> Graham Cooper wrote:
> > there are simple variable renaming schemes that do away with
> > substitutions.

>
> > INFERENCES = 0
>
> > For Each New Formula, increment and append INFERENCES to every
> > variable name.

>
> > e.g.
>
> > Predicate
> > vert( line ( pnt( X , Y ) , pnt( X , Z )))

>
> > Goal?
> > vert( line ( pnt( 1 , 1 ) , pnt( 1, 5 )))  ?

>
> > Match
> > vert( line ( pnt( X1 , Y1 ) , pnt( X1 , Z1 )))

>
> > X1 = 1
> > Y1 = 1
> > X1 = 1
> > Z1 = 5

>
> > SUCCESS!
>
> > > Sub(M,x,y,N) means that for every alpha in M there is a beta in N such
> > > that Sub(alpha,x,y,beta) and every formula in N can be obtain thus from
> > > one in M.

>
> > Set at a time variable renaming?
>
> > Again I don't see what the utility is.
>
> It enables me to state P9 below.
>

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

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

Making Sub(..) a predicate still doesn't formalise the Quantifier
syntax

Try writing

WFF( p ) as a predicate

ProofByInduction( p(n) ) as a predicate

ProofByContradiction( p ) as a predicate

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

In my Shorthand for |-

Axiom1 & Axiom2 & Axiom3 & .... Axiomn -> Theorem1

it's quite neat in that a false axiom gives you a false theory!

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