[FOM] Valid rules versus valid formulas

[Arnon Avron]

As a part of his reply to my message on the incomplete logic 
needed for mathematics, Harvey Friedman has asked:

> > to my best knowledge, although the set of valid formulas
> > of ancestral logic is not r.e., nobody has ever suggested
> > a valid rule of it which is not derivable in this proof system,
> > and  again I think that it is an important research question to
> > find one.
> 
> Is your use of the word "rule" here importantly different than just
> saying that nobody has suggested a natural valid sentence of ancestral
> logic which is not provable in the commonly associated proof system?

The immediate reason I was talking about rules is that I am 
usually thinking in terms of Gentzen-type calculi, and in such
calculi rules play the major role (unlike Hilbert-type systems,
which usually employ a very small set of rules, and the crucial
question is what axioms or axiom-schemas should be adopted). 
However, I do think that talking about rules is importantly 
more general then talking just about valid sentences,
or valid formulas, or even valid axiom-schemas.

   Logics are developed in order to be *applied*, and when 
a logic is applied in some area, it might make a lot of difference
whether some rule is included in it or not, even if the
inclusion of that rule does not change the set of valid formulas.
This is obvious in case no deduction theorem of any sort is
available. (A trivial example: Kleene's 3-valued logic
has no valid formulas at all, but still it is very useful
for certain applications, because it does have a rich set
of valid rules.) However, it is true even if deduction theorems 
are available. Take for example classical FOL itself. 
Some books present formal systems for it which include
the generalization rule. Some other prefer
a presentation which employ MP as the unique rule. The set
of valid formulas of FOL is the same in all, but not
the consequence relation. Thus without the generalization rule
(or an additional substitution rule) one cannot infer
p(c) from p(x) (where x is a variable). This suits e.g. the
reasoning applied in high school for dealing with a set of equations
(or inequalities), but not for the reasoning applied there
for deriving identities from other identities. 

Finally, in the case of a logic for which the compactness theorems fails
(like ancestral logic, which was the subject of those postings) I do 
take into account the possibility of finding an effective valid rule 
(perhaps even with an infinite number of premises!)
that cannot be translated into any valid formula or axiom schema.

Arnon