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 6:57 PM

On Mar 7, 9:21 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> Please don't change the groups posted to. It's clearly a sci.logic
> question.
>
>
>
>
>
>
>
>
>
> Graham Cooper wrote:
>

> > 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,
>
> Indeed so, commas and brackets are often used but they are avoidable.
> For an explanation of "my" choice of language conventions, see the last
>
>
>
>
>
>
>
>
>

> > 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.
>
> Nothing in my post has got anything to do with axioms.  It's about
> something else.  See the word "abstract" in the subject header, see the
> "Note,..." sandwiched between ***** and ***** below.
>
>
>
>
>
>
>
>
>

> > 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.
>
> It enables me to state P9 below.
>
>
>
>
>
>
>
>
>
>
>

> > 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.
>
> Might it?  I wouldn't mind seeing the details.
>

> > Most of them follow easily by letting
>
> Follow from what?  The question is to do with some (maybe) following
> from the others.  'Follow' except in the context of 'follow from ...' I
> don't understand.
>

> > M = p1 & p2 & p3 ... & pn
>
> M need not be finite.
>

> > and using  M ->
> > rather than M |=

>
> This is the last paragraph I referred to above.  As I remarked in my OP,
> P1-P9 (and thus the preceding gubbins) comes from a text.  I am
> currently reading that text.  Were I reading something else I might have
> written a different post, as it is my post reflects (to some degree) the
> contents of that text.  So your suggestion that I might do something
> else altogether gets me nowhere.  Nevertheless, thank you for your
> interest.
>
> --
> When a true genius appears in the world, you may know him by
> this sign, that the dunces are all in confederacy against him.
> Jonathan Swift: Thoughts on Various Subjects, Moral and Diverting

syntax) and quoting verbatim.

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