[FOM] The rule of generalization in FOL, and pseudo-theorems

[Alessio Guglielmi]

Dear Sandy,

there is a deep inference system, called SKS, which appears to be 
doing exactly what you're asking for. The generalisation rule is 
equivalently replaced by the rule

        (FA x) (A or B)
    ------------------------ .
    ( (FA x) A or (EX x) B )

(In deep inference, connectives and quantifiers are always defined by 
inference rules in duals pairs.) The system is quite elegant, and it 
never produces `theorems' of the kind you don't like. Moreover, the 
sequent system LK (as well as natural deduction systems) is in a 
straightforward correspondence to system SKS. In addition, system SKS 
enjoys all the proof theoretic properties one might want, for example 
the finite choice property, which is the deep inference equivalent of 
the subformula one; cut elimination, of course, and many others.

You can find this system in Kai Bruennler's thesis at 
<http://www.iam.unibe.ch/%7ekai/Papers/phd.pdf> (p. 25; you can also 
buy this book at Amazon 
<http://www.amazon.de/exec/obidos/ASIN/3832504486/qid=1077070232/sr=1-4/ref=sr_1_8_4/302-1943298-8085610>).

The same thesis gives a short introduction to deep inference, whose 
main web page is at 
<http://alessio.guglielmi.name/res/cos/index.html>. If you have 
questions and you want to get in touch with the people involved in 
deep inference, you can use the mailing list Frogs at 
<http://alessio.guglielmi.name/frogs/index.html>.

Best wishes,

-Alessio


At 13:29 -0700 30.8.04, Sandy Hodges wrote:
>If we wanted to say what a logical theory is, we might use this
>definition, taken from Wikipedia:
>
>[A] logical theory, ... consists of
>
>1) ...
>2) a set of axioms, ....
>3) a set of inference rules which allow one to prove theorems from
>axioms or earlier proven theorems.
>
>[...]
>
>What I am hoping for is a source to cite, in which first-order logic is
>presented in a way that does not require such psuedo-theorems as "0 < a
>=> (Exists y) a < y".  If anyone knows of a textbook or article that has
>a system for first-order logic that avoids such "theorems", I would
>appreciate knowing where it is.   I do want a system that is of the
>'natural deduction' sort - one that conforms to the definition given
>above: that a logical theory is a list of axioms and a list of rules.
>
>Thanks for any references or other comments:
>
>Sandy Hodges