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

[Marcin Mostowski]

Sandy Hodges writes about 'rule of generalization', which is the following

    F(a)
_____________
for all x, F(x)

The interpretation of the rule depends on what is a. It would be either an
individual constant or a variable.


In the first case this is not a correct deduction rule in usual sense.
A deduction rule is correct iff under each interpretation if all its
premises are true then also its conclusion is true.

In the second case you can make it a correct rule, e.g. by defining truth
relation for formulae with free variables as truth under all valuations.
However the solution has its disadvantages. Particularly you remove in this
way the deduction theorem because from the implication 

(for all x F(x)) implies (for all x G(x))

you cannot infer

for all x (F(x) implies G(x)).

However, reasonings with the scheme of 'rule of generalization' have some
advantages. We frequently justify universal statements in a sense "on
examples". This can be interpreted as applying 'rule of generalization'.

Besides very well known Gentzen's natural deduction system there is older
suppositional proof system of Stanis{\l}aw Ja{\'s}kowski. This system for
the sentential case was formulated in early twenties as an answer to the
problem put by Jan {\L}ukasiewicz at his seminar. The problem was give a
formal proof system describing mathematical proving practice. Later on, in
1935 Ja{\'s}kowski published the paper "On the rule of supposition", which
extended the system to first order logic.
The most striking difference between these two proof systems is that
Gentzen's proofs are trees but Ja{\'s}kowski's proofs are linear like real
written mathematical proofs. Currently this system is a core logical poof
system of one of the most developed computer supported proof system MIZAR.
The suppositional proof system has something like the 'rule of
generalization', but not as a deduction rule. This is a rule of
constructing proofs. The proof of a universal statement of the form

for all x, F(x)

can be done as follows:

take a new individual constant c, and prove F(c).

A very concise definition of the Ja{\'s}kowski's proof system can be found
in my paper "Quantifiers definable by second order means" in Quantifiers,
vol. 2 (ed. Krynicki ...), Kluwer 1995.

The definition of a logical theory (I would say rather a deduction system)
mentioned by Sandy Hodges seems to be too narrow. I would prefer the
following:

A deduction system is determined by a triple F, D, Prove, where F is a set
of sentences, D is a set of proofs and Prove is a binary relation between
elements of D and F. Additionally, I would require that all the three sets
are recursive.
Such a definition covers all known finitary systems as well concrete as
those more abstract.

Kai Bruennler writes "After checking with some of my colleagues here in
Bern it seems to me that "working logicians" do not share your concern
about calling formulas with free variables "theorems". Are you aware of any
technical (as opposed to philosophical) problems arising from that?"

I do not know what Kai Bruennler means by "philosophical problems". When
you study proof systems then your choice of the technical details depends
on the kind of theorems you would like to prove. However majority of people
using logic are not "working logicians". They are mathematicians and
computer scientists writing proofs. They need logical education among
others for this. Therefore it is not inessential of what kind of proof
systems you teach them. There is quite common practice between
mathematicians of differentiating real mathematical proofs and formal
proofs (see e.g. "Discrete Mathematics by Ross and Wright). The idea
standing behind of this difference is that formal proofs are better in the
sense being more conclusive. This is done frequently without giving any
explicit proof system conforming to the proofs called "formal". It would
suggest that same real mathematical proofs couldn't be presented as
"formal" proofs. Of course the idea is stupid. My opinion is that what they
call real mathematical proofs can be treated as "formal" proofs as well,
but in an essentially richer and complicated proof system. Nevertheless the
problem shows that a kind of proof systems which you sell to others (not
"working logicians") is essential and it is not only "philosophical"
problem.

Marcin Mostowski


_____________________

Marcin Mostowski
Department of Logic
Institute of Philosophy
Warsaw University