Quick logic question

Suppose you add to the language of first-order logic a sentence operator L for which you stipulate that all instances of

(L(p -> q) & Lp) -> Lq

are valid and that validity is closed under prefixing L's:

if p is valid, then so is Lp.

For example, L could be the modal operator 'necessarily', or it could mean the same as '$m[1]'. If it means the same as '$m[1]', then

$m[1]

is invalid, since it translates as

$m[1].

So the principle of Universal Instantiation

$m[1] provided y is free for x in p

must be restricted (or we have to redefine 'free'). The following version, however, would be sound:

$m[1] provided y is free for x in p.

Is there anything L could mean that would invalidate this version? Or do the principles for L guarantee that it holds?

Comments

# on 07 May 2010, 23:24

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.

# on 08 May 2010, 23:06

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.

Add a comment

Please leave these fields blank (spam trap):

No HTML please.
You can edit this comment until 30 minutes after posting.