Church uses Hilbert-style formulations for his logics based on lambda-calculus (Church 1932, 1933, 1940). That was the standard approach in mathematical logic at the time. I don’t know whether Church was familiar with Gentzen’s work, but it’s clear that Church is not using natural deduction nor sequent calculus in these papers.
1 Like