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

[Kai Brünnler]

Dear Marcin,

You wrote:
> 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".

I was just referring to the problem that Sandy Hodges outlined:
> I would say that "0
> < a => (Exists y) a < y" is not a theorem - but even if we called it a
> theorem, the problem would not go away - we then have to deal with
> "theorems" which don't say anything, which are neither true nor false.

Further you wrote:
> [...] 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. 

No doubt. However, I was referring to the more specific problem above, 
which, btw, I didn't mean to belittle by calling it philosophical. My 
question was a genuine one, so let me clarify. I have a deductive system 
that works entirely on closed formulas and thus meets Sandy Hodges 
criterion. I like this property of the system, but I do so purely for 
aesthetical reasons. Are there other, more technical, reasons why this 
property is desirable?

-Kai
http://www.iam.unibe.ch/~kai/