There need to be restrictions on ∀I and ∃I

[frabjous]

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...)$."

[rzach]

Yes, the original forallx did not allow $\forall x(Fx \to \exists x Fx)$ in the syntax. I made that change in forallx:YYC to align it with the OLP syntax. I think in practice it basically never comes up since you wouldn't ask students to prove $\forall x(Fx \to \exists x Fx)$ but rather $\forall x(Fx \to \exists y Fy)$. But yeah that's a mistake, thanks!

[rzach]

PS at least carnap.io does it right, i.e., it doesn't accept the first inference...

[frabjous]

Because of its roots in Hardegree's system and how that book states its similar rules, the current version of Logic Penguin enforces these rules the other way around, i.e., the line you already have is required to be an instance of the line you get, replacing all free occurrences of the variable in the line you get with the same name (which they might already include). It should handle both cases correctly.

The problem is that wording the rule that way is confusing to students, since they naturally think about substitutions in the result, not in what they already have. I understand why you use notations like $A(...x...x...)$ and $A(...x...c...)$ but they're not as precise as something like $A[c/x]$ where this means what $A$ becomes when $c$ is substituted for all free occurrrences of $x$, even if there aren't any. By experience, I know intro students understand your kind of notation better than the the more precise variation, however, so I'm not against it.

LogicPenguin (optionally) allows a rule panel to pop up with all the rules and students can fill in justifications by clicking on the rule in the panel. At the moment, I'm just trying to make sure the rules are stated at least as accurately as possible.

Vacuous binding and double binding are both annoying things to have to account for, and never useful or necessary, and I understand why some people might choose to exclude them from the syntax. But if they are allowed, a proof checker needs to treat them in accordance with the semantics.

[rzach]

Ok maybe I'm an idiot but I can't come up with an example of an invalid inference if $\forall$I isn't restricted.

However, I do have to restrict $\forall$ E, since right now the replacement of $x$ in $A(\dots x\dots x\dots)$ is defined as "replace all occurrences of $x$" not "all free occurrences" so we technically allow $\forall x\forall x A(x,x) \vdash \forall x A(c,x)$ which is bad.

[frabjous]

I interpreted the change is the schemas in $∀E$ to mean all free occurrences. I guess that was just being charitable, but by all means make the wording tighter.

The example I gave for restricting ∃I is also invalid for ∀I even if "a" isn't in an undischarged premise/assumption. Let the domain be integers and interpret R as less-than. From there being something less than any arbitrary "a" does not mean that everything is such that something is less than itself.

If that doesn't maybe this one will convince you?

1. $∀y∃x ¬x=y$   (a plausible if contingent premise)

2. $∃x ¬x=a$   (∀E 1)

3. $∀x∃x ¬x=x$   (∀I 2 ???)

4. $∃x ¬x=x$   (∀E 3)

Some monists might be happy, but …

[rzach]

Duh, thank you.

[rzach]

Kinda regretting I allowed vacuous quantification in the syntax now, but I made my bed so I guess I have to lie in it.

[rzach]

I think I've fixed it -- by defining the notation for substitution/replacement more carefully, so that the main text basically stays the same. But added a couple of paragraphs that show how you have to be careful in cases with overlapping quantifiers binding the same variables. (Since they only come into play if you use such sentences in examples, and you'd be a mean instructor if you did, I figured it's best to explain it separately for the attentive/curious students but not make the main exposition more convoluted by adding restrictions.)

[frabjous]

Seems good enough. Probably only matters to students actively trying to break things.

Incidentally, the code for supporting most of the forallx systems, including Calgary, for LogicPenguin is mostly complete but could use some bug checking. I'll send you a link you can use to play around via email.

I did put a restriction on these rules in its pop-up rule panel.

[rzach]

Thanks!