```Date: Mar 6, 2013 5:37 PM
Author: Graham Cooper
Subject: Re: Interdeducibility of properties of an abstract consequence relation.

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 forarguments>> 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)   <-   Xor(X, Y)    <-   YYou Still can't formulate an AXIOM that refers to arguments, unlessyour 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 argumentsof 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 levelthere are simple variable renaming schemes that do away withsubstitutions.INFERENCES = 0For Each New Formula, increment and append INFERENCES to everyvariable name.e.g.Predicatevert( line ( pnt( X , Y ) , pnt( X , Z )))Goal?vert( line ( pnt( 1 , 1 ) , pnt( 1, 5 )))  ?Matchvert( line ( pnt( X1 , Y1 ) , pnt( X1 , Z1 )))X1 = 1Y1 = 1X1 = 1Z1 = 5SUCCESS!> 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 ParallelComputers?Variables have arbitrary names just as each formula may be arbitraryitself.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 referenceSets without worrying about which parameter to index  Qx p(...x...)e( A, nats )  <->   isNat( A )Axioms deal with the SET natswhich 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 |= betamight get P4.-----Most of them follow easily by lettingM = p1 & p2 & p3 ... & pnand using  M ->rather than M |=Herc--www.BLoCKPROLOG.com
```