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 6, 2013 5:37 PM

On Mar 7, 6:56 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> Frederick Williams wrote:
> > [blah]
>
> This is slightly improved (oh really?):
>
> Let there be a countable stock of predicates each of some arity n
> (n = 0, 1, 2, ...), and an infinite but countable stock of variables.
> ~, &, U, ( and ) are used autonomously.
>
> An atomic formula is a predicate followed by a number of variables equal
> to the predicate's arity.  Just what predicates and variables are
> doesn't matter much, but one can tell that a string of them is or is not
> an atomic formula, and if it is an atomic formula, just which atomic
> formula it is.  So, for example, if P is a predicate of arity two, the
> variable _won't_ include b and bb because then Pbbb would be ambiguous.
> This kind of fussy detail won't be mentioned further.

it's pretty standard to use a delimiter, or data structure for
arguments

>
> A formula is any one of the following:
>
> * alpha, where alpha is an atomic formula,
> * ~alpha, where alpha is a formula,
> * (alpha & beta), where alpha and beta are formulae,
> * Ux alpha, where x is a variable and alpha is a formula.
>
> If x is a variable, Ux is called a quantifier. (alpha -> beta)
> abbreviates ~(alpha & ~beta)
>
> Below alpha, beta, ... (maybe decorated with primes) are formulae; and
> x, y, ... are variables.
>
> 'x occurs free in alpha' is defined as follows:
> * each occurrence of a variable in an atomic formula is a free
>   occurrence,
> * x occurs free in ~alpha iff x occurs free in alpha,
> * x occurs free in (alpha & beta) iff x occurs free in alpha or in beta,
> * x occurs free in Uy alpha iff x occurs free in alpha and x is not y.
>
> An occurrence of a variable that is not free is said to be bound.
> Clearly a variable that is bound is bound because of some quantifier.
> Such a variable is said to be in the scope of that quantifier.

Axioms refer to formula's as variables.

or(X , Y) <- X
or(X, Y) <- Y

You Still can't formulate an AXIOM that refers to arguments, unless
your syntax is more convoluted again!

ALL(a, b, c....)
P(x,y, a, b, c, ...)
A(x) .... P....

where a, b, c might me sub arguments of sub arguments of sub arguments
of P.

>
> Let M be a set of formulae. 'x occurs free in M' means x occurs free in
> at least one member of M.  Below M, N, ... are sets of formulae (not
> excluding the empty set).
>
> Informally, Sub(alpha,x,y,beta) means 'beta is derived from alpha by
> substituting y for x in all places where x is not in the scope of Ux'.
> 'in the scope of' was defined only so that that informal explanation of
> Sub(alpha,x,y,beta) could be given.  I think the phrase has no further
> use so far as this post is concerned.  Precisely:
>
> * 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.
>

this is very fine grain low level

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. Molecular Parallel
Computers?

Variables have arbitrary names just as each formula may be arbitrary
itself.
What is the point of changing all X,Y,Zs in a dozen formula to P,Q,Rs?

When you use a Set Specification Axiom then you can then reference
Sets without worrying about which parameter to index Qx p(...x...)

e( A, nats ) <-> isNat( A )

Axioms deal with the SET nats
which has an implicit parameter.

>
> Now consider a relation |= between sets of formulae and formulae having
> the following properties.
>
> P1 If alpha in M then M |= alpha.
> P2 If M |= alpha then M union N |= alpha.
> P3 If {alpha} |= beta and {beta} |= gamma, then {alpha} |= gamma.
> P4 If M |= alpha and N |= beta, them M union N |= (alpha & beta).
> P5 If M |= (alpha -> beta) and N |= alpha, then M union N |= beta
> P6 M |= (alpha -> beta) iff M union {alpha} |= beta.
> P7 Ux alpha |= alpha.
> P8 If x is not free in M union {beta} and if M union {alpha} |= beta,
>    then M union {Ux alpha} |= beta.
> P9 If Sub(M,x,y,N), Sub(alpha,x,y,beta) and M |= alpha, then N |= beta.
>
> Now to my question: can any of P1 through to P9 be deduced from the
> others?
>
> Note, I make no reference to axioms, interpretations or truth, |= is
> just what this posts says it is.  (Except for typos. :-)
>

Use (alpha -> beta) abbreviates ~(alpha & ~beta)

P5 If M |= (alpha -> beta) and N |= alpha, then M union N |= beta

might get P4.

-----

Most of them follow easily by letting

M = p1 & p2 & p3 ... & pn

and using M ->
rather than M |=

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