Proof theory for finitely valid sentences (Q2772902)

The paper under review is concerned with the proof theory of finitely valid sentences. By the famous theorem of Trakhtenbrot, the set of finitely valid first-order sentences is not recursively enumerable. Thus there can be no finitary calculus generating this set. NEWLINENEWLINENEWLINEThe author introduces a neat infinitary rule of inference, the so-called finiteness rule (fin). He shows that the standard sequent calculus for first-order logic augmented by (fin) derives exactly the set of finitely valid sentences, and, moreover, it admits cut elimination. NEWLINENEWLINENEWLINEThe finiteness rule (fin) is further studied in the context of sequent calculi for simple type theory and transitive closure logic. The latter calculi augmented by (fin) are shown to be complete with respect to the set of finitely valid sentences of the corresponding logic, and cut elimination holds as well. NEWLINENEWLINENEWLINEIn the last part of the paper, the question of approximating finite validity in a recursively enumerable way is discussed, and some remarks concerning intuitionistic logic are made.