Abstract

1, . . . , n | ≈ ψ ? Here 1, . . . , n, ψ are premisses of some formal language, such as a propositional language or a predicate language. | ≈ is an entailment relation: the entailment holds if all models of the premisses also satisfy the conclusion, where the logic provides some suitable notion of ‘model’ and ‘satisfy’. Proof theory is normally invoked to answer a question of this form: one tries to prove the conclusion from the premisses in a finite sequence of steps, where at each step one invokes an axiom or applies a rule of inference