While implementing the deductive system of both the Calgary and Cambridge for LogicPenguin (which is nearly complete), I noticed a couple oddities.
The Cambridge version lists a restriction on $∀I$ and $∃I$. It says that the variable introduced must not already occur in the statement generalized upon.
The Calgary (and Mangus's original) list no restriction at all.
Both are wrong if a quantifier with a certain variable within the scope of another quantifier with the same variable is allowed syntactically.
The Calgary version allows the inference from $∃xRxa$ to $∃x∃xRxx$, which, at least given the normal way of treating double-binding, is semantically equivalent to $∃xRxx$, which should not be provable from $∃xRxa$. (Just as an example, there are others.)
The Cambridge rule, however, is too restrictive, since it is impossible to prove something like $∀x(Fx → ∃xFx)$, which is semantically valid.
Looking at the Cambridge recursive syntactic formation rules for formulas of FOL, it looks like it disallows both vacuous binding and double binding, so maybe this isn't really a problem for it. (Though the restriction then seems redundant since the result wouldn't even be well-formed.)
However, the Calgary version needs some kind of fix. Either the syntactic rules have to change, or there needs to be a restriction on the rules, something like "c must not occur within the scope of a quantifier $∃x$ or $∀x$ already in $A(...c...c...)$."