Conference rusure::math

    I'll see if I can find a list of the standard axioms/deductive rulse
    for the first order predicate calculas with quantification.  It is
    worth noting, right off the bat, that the first expression implies
    the second.  This is because of the theorem:

	    (X --> Y) ==> (X*Z --> Y)

    Where "a ==> b" is read "b can be deduced from a".  So working
    completely "inside" the quantifier, adding the extra terms to the
    conjunction adds no information.

    You can think of the universal quantifier as an infinite conjunction
    so, your first expression may be thought of as:

	(Unimp( a1 ) --> Iit( a1 )) * (Unimp( a2 ) --> Iit( a2)) * ...

    With the "a's" covering every entity in the universe of discourse.
    You can then use the above deductive prinicple on each term of the
    infinite conjunction to get the appropriate terms, then translate
    back to the universal quantification form (with a change in variable)
    to get your second expression.

    (The existential quantifier may, of course, be thought of as an
    infinite disjunction).

				    Topher

Is

For_all( x ): (Fen=0) * Fi( x ) --> fdf( x )

is equivalent to

(Fen=0) --> [ For_all( x ): fi( x ) --> fdf( x ) ]

?

I'd guess so.

    I was trying to remember the rules for deduction with quantification
    last night and as I remember it, they are:

	D1: P(a) ==> (Exists x)(P(x))
	D2: P ==> (All x)(P)
	D3: (Exists x)(P) ==> P
	D4: (All x)(P(x)) ==> P(a)

    To use these, you essentially use the first two to add quantifiers
    and the second two to remove them.

    Example from .2 (rephrased a bit):

	1) (All x)(A * P(x) --> Q(x))		    Hypothesis
	2) (All x)(~A + ~P(x) + Q(x))		    Def -->; DeMorgan's
	3) (All x)(A --> (P(x) --> Q(x))	    Assoc +; Def -->
	4) (All x)(A --> (All y)(P(x) --> Q(x)))    D2
	5) A --> (All y)(P(y) --> Q(y))		    D4
	6) A --> (All y)(All x)(P(y) --> Q(y))	    D2
	7) A --> (All x)(P(x) --> Q(x))		    D4; QED

    Step 5 probably makes you a bit uncomfortable, but its legitimate, as
    long as you observe the naming rules (which I didn't formalize as much
    as a really formal treatment would).  You can only substitute the
    "specific" value of y if "y" means the same thing everywhere it is
    substituted.

					    Topher

re .3

Thanks, I will copy the list and hang it up on my wall.

In case you are wondering where the problem came from, I'm rewriting
a portion of a processor spec to untangle some apparently correct but
unenlightening verbiage that's caused confusion among the software
community.

I've taken three convoluted rules and collapsed them into two simpler
ones, using the rewriting rules given here, and some semantics not visible
here.  So predicate logic really does have everyday(?) applications.

    For informal work, your best bet is to use the "infinite conjunction"
    non-formalism.  For example once we get to:

	(All x)(A --> (P(x) --> Q(x))

    we mentally convert it to:

	(A --> (P(a1) --> Q(a1)) * (A --> (P(a2) --> Q(a2))) * ...

    then apply the theorem (A --> B) * (A --> C) ==> (A --> (B*C))
    "recursively" to get:

	A --> ((P(a1) --> Q(a1)) * (P(a2) --> Q(a2)) * ...)

    which is:

	A --> (All x)(P(x) --> Q(x)); QED

    that way you just use the rules for conjunction and disjunction.

					Topher

    In _Godel, Escher, Bach_, Hofstadter gives:
    
    Specification:  If u is a variable in X and "All u: X" is a theorem,
    then X is a theorem and so is the result of replacing every occurrence
    of u in X with a term that does not contain any variable quantified in
    X.
    
    Generalization:  If X is a theorem in which u is a free variable, then
    "All u: X" is a theorem, except that this is not allowed in a "fantasy"
    in which u is a variable that appeared in the fantasy's premise.
    
    (A fantasy is an embedded derivation in which some statement has been
    assumed as a premise without proof.  When the fantasy is closed, the
    statement that the premise implies the conclusion becomes a theorem.)
    
    Interchange:  If u is a variable, then "All u: ~" and "~ Exists u:" are
    interchangeable.  That is, those strings can be interchanged wherever
    they occur within any theorem.  "~" is negation.
    
    Existence:  If X is a theorem and Y is the result of replacing any or
    all occurences of a term in X with a variable u that does not otherwise
    occur in X, then "Exists u: Y" is a theorem.
    
    Also, I question D3 in response .3.  Observe that it permits
    
    	(Exists x)(P) ==> P ==> (All x)(P).
    
                                                
    				-- edp

>>    Also, I question D3 in response .3.  Observe that it permits
>>    
>>    	(Exists x)(P) ==> P ==> (All x)(P).

	Correct ... from (Exists x)(P(x)) you can conclude that
	there is something out there that has property P, but it
	may be a very special element and it can certainly be the
	case that your general run of the mill x doesn't satisfy P.

	In some expositions of the first order predicate calculus
	when you have (Exists x)(P(x)) you can introduce a new
	constant b and assert P(b).  Look again at the restriction
	on Generalization in .-1 and think of the constant b as a
	variable that you are not ever allowed to quantify over.

	Dan

RE: .6 (edp)

    OK, obviously I have to be explicit about my conventions (which are
    common ones in actual, semi-formal, work).

    1) In this system there are *no* unbound variables.  There is, however,
       *implicit* universal quantification.  Predicates are implicitly
       quantified with non-universal quantification, i.e.,:

		    (All P in {Predicate})(...)

       which is equivalent to:

		    (All P)(P in {Predicate} --> (...))

       Implicitly quantified variables are distinguished from specificly
       named instances lexographically and by common sense (this being only
       semi-formal).  (I believe that the only reason that free variables
       are included in QFOPC (First Order Prepositional Calculus with
       Quantification) is because in FOPC (i.e., without quantification)
       you cannot treat free variables as implicitly universally
       quantified, and it is handy for foundational work to make QFOPC as a
       strict extension to FOPC).

    2) If a relevant variable is not mentioned as an argument to a
       predicate it doesn't occur in that predicate.

    Therefore, for the comment:

>    Also, I question D3 in response .3.  Observe that it permits
>    
>    	(Exists x)(P) ==> P ==> (All x)(P).

    the deduction is permitted because it is correct:  For a universe
    of discourse of cucumbers:

	From: "There exists a cucumber, x, such that it is raining today";
	One can deduce: "It is raining today" (since there the cucumber is
	    irrelevant).
	From which one can further deduce: "For all cucumbers, x," (also
	    readable as "for whatever cucumber you choose to call "x")
	    "it is raining today."

    This is not the same as the (mis)deduction.

	From: "There exists a cucumber, x, such that x is over 10 inches
	    long";
	One can(not) deduce: "x is over 10 inches long" (not syntactically
	    correct, unless you have "jumped" implicitly to the next step
	    since unbound variables are not permitted).
	From which one can fur can further deduce: "All cucumbers are over
	    10 inches long"

    That would have to be written:
    
	# (Exists x)(P(x)) ==> P(x) ==> (All x)(P(x))

    3. A name can have at most one meaning at any point in a proof or
    formula.  You cannot quantify over the same "variable name" in a
    nested fashion, nor over a name used as the name of a specific thing
    within the deductive system (i.e., you cannot say (All 13), or
    (All father-of(,))

    My purpose was to provide a minimal, complete (up to mathematical
    induction) rules for standard quantification against which "suspicions"
    could be checked in practice, not to provide a formal, rigorous,
    foundational system (I'm providing clarification of intent since there
    perhaps was confusion, not complaining about criticism).  There are
    many alternate such systems, and a lot that could be made more
    rigorous.

				    Topher

RE: .6 (edp)

    The one clearly "different" basic rule in the GEB rule set (other than
    those created by the different and greater degree of formalization), is
    the one labeled interchange.  I thought it worth demonstrating that
    this is a theorem in the system in .3

	1) (All x)(P(x))			    Hypothesis
	2) (All x)(~(~P(x)))			    Double negation.
	3) (All x)(~((Exists y)(~P(x))))	    D1
	4) ~(Exists y)(~P(y))			    D4

    This makes it plausible that they are of equivalent power (ignoring,
    once again differences in formalism).

					    Topher

    Copi wrote the standard introductory text (several actually) on Formal
    Logic, and they do cover what you are talking about so far.  If you
    want to read up on it (I cannot find my text right now.) I'd suggest
    going to the library and looking for Logic books under his name.
    
    --  Barry

The most extensive reference I know of is:

	Edward Cohen
	Programming in the 1990's
	Sprimger-Verlag  1990
	ISBN 0-387-97382-6


The following uses the DEC Technical character set:

*>
For symmetric and associative binary operators op we write the
quantified version of op as

		(�1mOP�0mi : R : T)

OP is a quantifier, formed by a capitalized and bold/underlined  op
i  is a list of dummies (bound variables)
R  is called the range, and is a boolean expression
T  is called the term, and has the same type as op

We usually omit a range of true:

		(�1mOP�0mi :: T) = (�1mOP�0mi : true : T)

Function application is denoted by an infix period, i.e.  
 F.x rather than F(x) .

In the following Z is a function that does not depend on the dummies,
and other letters are, in general, functions of the dummies.

term rule:	(�1mOP�0mi : R : P op Q) = (�1mOP�0mi : R : P) op (�1mOP�0mi : R : Q)

range rule:	(�1mOP�0mi : P � Q : T) = (�1mOP�0mi : P : T) op (�1mOP�0mi : Q : T)

		provided op is idempotent  or  P.i � Q.i for all i .

generalized 
distributivity: (�1mOP�0mi : R : Z � T) = Z � (�1mOP�0mi : R : T)

		provided that � distributes over op 
	   and (the range is non-empty  or  the unit of op is the zero of �)

empty range:	(�1mOP�0mi : false : T) = unit of op

		provided that op has a unit

constant term:	(�1mOP�0mi : R : Z) = Z

		provided that op is idempotent and the range is non-empty

dummy transformation:
		(�1mOP�0mi : R.i : T.i) = (�1mOP�0mj : R.(f.j) : T.(f.j) )

		provided that function f is invertible (a bijection).

		If f is the identity function, then we have:

renaming the dummy:  (�1mOP�0mi : R.i : T.i) = (�1mOP�0mj : R.j : T.j)

nesting:	(�1mOP�0mi : P.i : (�1mOP�0mj : Q.i.j : T.i.j) ) =
		(�1mOP�0mi,j : P.i � Q.i.j : T.i.j)

1-point rule:	(�1mOP�0mi : i = Z : T.i) = T.Z

for � and �:

Trading:	(�1mޛ0mi : R : T) � (�1mޛ0mi :: �R � T)
	   also (�1mޛ0mi : R � S : T) � (�1mޛ0mi : R : S � T)

		(�1mߛ0mi : R : T) � (�1mߛ0mi :: R � T)

Instantation:	(�1mޛ0mi :: f.i) � f.x

		f.x � (�1mߛ0mi :: f.i)

De Morgan:	 (�1mߛ0mi : R :  T) � �(�1mޛ0mi : R : �T)
		�(�1mߛ0mi : R : �T) �  (�1mޛ0mi : R :  T)


for min and max:  (�1mMIN�0mi : R : -T) = -(�1mMAX�0mi : R : T)

for numerical quantification:

		(�1mN�0mi : R : T) = (�1m+�0mi : R � T : 1)

		(�1mN�0mi : R : T) = (�1m+�0mi : R : n.T) 

		where	n.x = 0 if x � false
		 	      1 if x � true