The “compacity theorem” for propositional or first order logic (of which one possible formulation is the “finiteness theorem”, which states that reaching a conclusion from an infinite set of assumptions can always be done from a finite subset of that set) is often seen as an essentially “semantical” theorem (reason why it is usually stated in terms of the “consequence relation”  or in terms of “validity” – instead of in terms of the “deducibility relation” – and IS proved via a topological argument).

Indeed, considered from the proof-theoretical framework, the finiteness property has no proper meaning nor interest : usual formal proofs being finite objects (typically finite trees), it is almost trivial to see that they only use a finite number of assumptions.

To investigate the proof-theoretical meaning of the finiteness theorem (as I will do in my talk), one thus must broaden the horizon, by considering infinite proofs.

We will do it, not by considering proof-trees where the rules themselves are of an infinite arity (as omega-logic does), but by considering infinite proof-trees with usual rules of finite arity, with an end (a conclusion), but with no beginning – the kind of proofs that could only be built by a prover who would be proving since ever (a special dedication to longstanding debates particularly developed in Rome ;-).

In a sense, that proof-theoretical version of the proof of the compacity theorem brings a deeper result than the semantical one : it not only says that an infinite set of valid/provable formulas always includes a finite set of valid/provable formulas, but also says that enjoying an infinite time at our disposal would not change our demonstrative capacity (giving thus a good reason to content ourselves with our finite proofs).
 
org: TORTORA DE FALCO Lorenzo