[FOM] The rule of generalization in FOL, and pseudo-theorems
Alessio Guglielmi
Alessio.Guglielmi at inf.tu-dresden.de
Tue Aug 31 15:45:59 EDT 2004
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
More information about the FOM
mailing list