[FOM] A formal system which uses only sentences

[Arnon Avron]

In continuation to Sandy Hodges' question, I just recall a textbook
in which a Hilbert-type system of the type he requested (i.e. proofs
consists solely of sentences) is presented. This is the book
"An Outline of Mathematical Logic" by A. Grzegorczyk (Synthese Library,
vol. 70, Reidel Publishing company, 1974). The system is presented
in section I.6 of the book. It has the further advantage that by omitting
exactly one of the axioms (the axiom of nonemptiness of the domain)
we get a sound and complete (for sentences) system for free logic.

Note that since Grzegorczyk's system deals only with sentences,
the difference between the "truth" consequence relation
and the "validity" consequence relations is irrelevant here.

 Let me take the opportunity to make short comments about 
Marcos' message: 

1) What he calls local rules and  global rules 
were called in the past  (e.g. by Gabbay) "rules of derivation"
and "rules of proof", respectively. 

2) In my comments about internal variables I meant mainly
the rule of substitution (which makes sense only in the presence of 
internal variables). However, it is true that a similar distinction
is very relevant in Modal Logic too. In fact, in my 1991 paper 
"simple Conseqence Relations" (which I mentioned in my first
posting on this sybject) and in my contribution to Gabbay's
volume "What is a Logical Systems" I presented the two consequence
relations of modal logics, and call them too the "truth" consequence
relation and the "validity" consequence relation (but some friends
thought that using the same names in the context of FOL and of
propositional modal logic is somewhat confusing. I disagree).


Arnon Avron