Resolution and the consistency of analysis.
Peter B. Andrews · Notre Dame Journal of Formal Logic · 1974
In [2] we formulated a system /?, called a Resolution system, for refuting finite sets of sentences of type theory, and proved that with different sets of parameters, we henceforth assume ZJ has no parameters, and denote by CίA 1 , . .., A w ) a formulation of the system with parameters A 1 , . .., A w .If J/ is a set of sentences, J4^~g B shall mean that B is derivable from some finite subset of J4 in system £.The deduction theorem is proved in §5 of [5].We shall