Proving since ever ? The compacity theorem revisited from a proof-theoretical perspective

Mercoledì 27 Ottobre ore 14:30, Jean-Baptiste Joinet, IRPhiL (Université Jean Moulin Lyon 3) & IHPST (CNRS/université Panthéon-Sorbonne), terrà il seminario di Logica e Informatica Teorica dal titolo "Proving since ever ? The compacity theorem revisited from a proof-theoretical perspective".

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).

Il seminario avrà luogo presso il Dipartimento di Matematica e Fisica
Largo San Leonardo Murialdo 1 - Aula 311
Oppure, cliccare sul seguente Link identifier #identifier__141034-1Link 
Link identifier #identifier__87901-1Link identifier #identifier__129240-2Link identifier #identifier__53071-3Link identifier #identifier__151294-4