Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9301250928.AA27774@ted.cs.uidaho.edu>
Date: Mon, 25 Jan 93 10:23:40 MET
From: schneide <schneide@de.uka.ira>
To: info-hol@edu.uidaho.cs.ted
Subject: Basic Rules

The philosophy of the HOL system is to have a rather small subset
of basic symbols and inference rules on which further operators
such as /\,\/,etc and derived rules can be defined. 

The HOL system uses as primitive symbols: = (equality), ==> 
(implication) and @ (Choice Operator). In [Andr76] another
calculus for higher order logic is presented whose language
is based only on equality and the choice operator. Implication
can be defined, e.g. as

 x ==> y   :=  [ x = [(\f.(f T T)) = (\f.(f x y))] 

Furthermore, the basic inference rules are not independent. For 
example REFL can be easily implemented by BETA_CONV and SUBST
as follows:

	|- [(\x.x)E] = E       |- [(\x.x)E] = E    
      -------------------------------------------
		       |- E = E

If implication is defined as above, the basic inference rules 
MP, DISCH, IMP_ANTISYM can be derived. As a consequence a 
smaller set of basic symbols and rules is obtained which is 
nevertheless as powerful as the used 8 rules. 

Now my question: Is there any special reason for using
these primitive operators and basic inference rules? And
if not, wouldn't it be reasonable to have a minimal set 
of basic rules? And if there are reasons for efficiency,
why don't we take REWRITE_RULE as a basic rule of inference,
since this rule is used very often.


References
[Andr76] P. Andrews, An introduction to mathematical logic and type
	 theory: To Truth through Proof, North-Holland, 1976.