EFQ

[Vaughan Pratt]

I confess to having some difficulty following the recent correspondence
between Neil Tennant, Arnon Avron, and Larry Paulson.  My difficulty has to
do with the words "true" and "valid", which I see being used in a context
where I'd expect "sound".

If terminology has changed since I started teaching algebraic logic at
Stanford in 1980, or if I was wrong back then, I'd appreciate being
straightened out.

My understanding is that a well-formed formula is *true* in a context
(environment) binding all its free variables to values such that the
formula then evaluates to "true", and is *valid* when it is true in all
relevant contexts.

An inference rule is sound when its conclusion is valid whenever all its
premises are valid.

These three notions generalize to modal logic by regarding quantifiers as
special modalities: (forall-x)  is [x:=?] while (exists-x) is <x:=?> where
x:=? is the action that assigns an arbitrary member of the domain to x and
[a] and <a> are the dual modalities of dynamic logic for action a.

If these are not the meanings of "true", "valid", and "sound" in modern
terminology, I'd appreciate knowing what the new definitions are and how to
use them.

Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220518/60db0aa5/attachment.html>