Wolfgang Schwarz

One fun example is a substitution operator: read [z/x] as an operator (written to the right of its argument) which is equivalent to the usual function on formulas. It's easy to check that it's "normal" in the sense of your two properties. But it clearly doesn't validate the last principle in general; e.g.:

$latex \forall x \, (Fx)[z/x] \to (Fy)[z/x]$ is $latex \forall x \, Fz \to Fy$, which is equivalent to $latex Fz \to Fy$.

A bit more pedestrianly, if L is interpreted as a modal operator over variable domains then the principle fails, since y may not exist.

Hey Jeff,

thanks! I'm actually playing around with counterpart-theoretic
semantics for modal logic here, without "very serious actualism", as
you would call it. Maybe you've thought about this as well:

In counterpart-theoretic modal logic, both (Free) Universal
Instantiation and Leibniz' Law have to be restricted. For example, one
could stipulate that x is free in A only if x does not occur in the
scope of a modal operator in A. With this restriction, FUI and LL are
sound, but if you then combine the principles of Free Logic with K,
the resulting system is incomplete. You also need something like

(*) x=y \to \Box A \to \Box A[y//x]

or perhaps

(**) \forall x \Box A \to E!y \to \Box A[y/x].

without the added restriction. The problem is that the restrictions on
FUI and LL are too strong: they ignore the fact that variables are
"directly referring" in counterpart semantics. So there should be less
restrictive versions of LL and FUI from which (*) can be derived. For
example, one could redefine substitution in both principles so that
A(x)[y/x] is \exists z (z=y \land A(y)). But I can't get (*) with this
version either. Perhaps I just didn't try enough?

Any thoughts would be much appreciated; I'm sure you see through all this much better than I.