[FOM] FOM EXISTENTIAL IMPORT

[John Corcoran]

FOM EXISTENTIAL IMPORT
Frege, Russell, Quine, Cohen, Nagel and other logicians have discussed
the logical relations between universal sentences such as 'every number
has P', Ax P(x), and "the corresponding existential" 'some number has
P', Ex P(x).  Equally discussed is the more interesting between
universalized conditionals such as 'every number that has S has P', Ax
(S(x) --> P(x)), and "the corresponding existentialized conjunction"
'some number that has S has P', Ex (S(x) & P(x)). This discussion takes
the class of numbers as the universe of discourse, i.e., as the range of
the individual variables.  As usual, S(x) and P(x) are formulas having
only x free. Some logicians use a special terminology: a universalized
conditional sentence has existential import if it implies "the
corresponding existentialized conjunction".  In classical logic the
issue of which such sentences have existential import is easily answered
by what has been called the Classical Existential Import Theorem: In
order for 'Every number that has S has P', Ax (S(x) --> P(x)), to have
imply 'Some number that has S has P', Ex (S(x) & P(x)), it is necessary
and sufficient for 'Some number has S', Ex S(x), to be tautological
(logically true).
Q0.1. Where in the literature is the Classical Existential Import
Theorem stated or discussed?
Q0.2. Who if anyone is credited with it?
This theorem holds in all (non-modal) classical logics: monadic logic,
first-order, first-order with identity, second-order, and the rest.
To make use of this theorem in a given logic it would be useful to know
more about the class of existential tautologies in that logic, i.e., the
class of logically true existential sentences of that logic, especially
the existentializations of non-tautological formulas such as Ey x = (y
+y).  One thing that is clear is that in the language of Robinson
Arithmetic there are infinitely many pairwise non-equivalent open
formulas whose existentializations are tautological.
Q1. Where in the literature are existential tautologies discussed?
Q2. What is known about the mathematical properties of these classes? 
The following questions are about non-classical logics.
Q3. In standard free-logic, what is a necessary and sufficient condition
for 'every number that has S has P', Ax (S(x) --> P(x)), to imply 'some
number that has S has P', Ex (S(x) & P(x))?
Q4. The same question for intuitionistic logic.
Q5. The same question for other logics.
My own investigations have led to the following little lemma.
Existential Tautology Lemma: Every non-empty definable set of natural
numbers is definable by a formula whose existentialization is
tautological.
Q6. Where in the literature is the Existential Tautology Lemma or
something more general stated or discussed?
Thanks to M.Brown and A. Urquhart 
-