Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theorie

Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theories. System F, which is weaker than dependent type theory corresponds to higher-order logic. First-order logic actually doesn’t actually correspond to a popular type system, though the correspondence of course exists.