Why are only some universal quantifiers explictly defined?

[nordlow]

Is there a reason why only some universal quantifiers are defined explicitly in axioms such as

(=>
   (subAttribute ?ATTR1 ?ATTR2)
   (forall (?OBJ)
      (=>
         (property ?OBJ ?ATTR1)
         (property ?OBJ ?ATTR2))))

rather than making the univeral quantifier ?OBJ also be defined implicitly as

(=>
   (subAttribute ?ATTR1 ?ATTR2)
   (=>
      (property ?OBJ ?ATTR1)
      (property ?OBJ ?ATTR2))))

[apease]

It's really just a historical artifact in this case. Unquantified variables in an assertion are implicitly universally quantified and so one is logically equivalent to the other in this case

[nordlow]

Ok, thanks.

[arademaker]

Let me use the opportunity for raising an old issue: I believe that axioms with all variables explicitly quantified are more readable and more transparent.

TL;DR

Paraphrasing Adam in a more verbose way: if we make the ?OBJ variable also implicit quantified, we are assuming the logical equivalence between the two statements

(forall (?ATTR1 ?ATTR2)
   (=>
    (subAttribute ?ATTR1 ?ATTR2)
    (forall (?OBJ)
       (=>
    (property ?OBJ ?ATTR1)
    (property ?OBJ ?ATTR2)))))

(forall (?ATTR1 ?ATTR2 ?OBJ)
   (=>
    (subAttribute ?ATTR1 ?ATTR2)
    (=>
     (property ?OBJ ?ATTR1)
     (property ?OBJ ?ATTR2))))

Admittedly, this is the case, and it can be easily proved in natural deduction using http://leanprover.github.io:

constant U : Type
constants property subAttribute : U → U → Prop

example (h : ∀ attr1, ∀ attr2, 
             subAttribute attr1 attr2 → (∀ obj, property obj attr1 → property obj attr2)) :
   ∀ attr1, ∀ attr2, ∀ obj, 
   subAttribute attr1 attr2 → (property obj attr1 → property obj attr2) :=
 assume (a : U) (b : U) (c : U),
 assume h₁ : subAttribute a b, h a b h₁ c 

But, IMHO, with the explicit quantifiers, we don't have ambiguity, and the choice between the first axiom or the second one is a matter of deciding which one is clearer. Using implicit quantifications, we are introducing ambiguity. The axiom above with all variables implicitly quantified has many possible equivalent axioms with all variables made explicit. One for each possible way to interleave the forall with the sub formulas. The flat quantification of all variables in the outermost position of the axiom is not necessary the more understandable form for presenting it.

That is, logical equivalence is not the only aspect to consider. I believe that axioms should be written not only for the theorem provers but also for humans. Similiar of what Donald Knuth said for programs:

Let us change our traditional attitude to the construction of programs: Instead of imagining that our main task is to instruct a computer what to do, let us concentrate rather on explaining to human beings what we want a computer to do.

Consider another example. Suppose that we want to say that all humans have a mother. Both axioms below are equivalent and formalize this fact:

(forall (?A)
  (=> (human ?A) (hasMother ?A)))

(not (exists (?A)
  (not (or (not (human ?A)) (hasMother ?A)))))

Which one is more readable and direct related to its description in natural language?

For me, the first axiom below is much more evident in its intention than the second one.

(forall (?ATTR1 ?ATTR2)
   (=>
    (subAttribute ?ATTR1 ?ATTR2)
    (forall (?OBJ)
       (=>
    (property ?OBJ ?ATTR1)
    (property ?OBJ ?ATTR2)))))

(=>
   (subAttribute ?ATTR1 ?ATTR2)
   (=>
      (property ?OBJ ?ATTR1)
      (property ?OBJ ?ATTR2)))