A purely existential first-order sentence ∃x⃗ φ(x⃗) (with φ quantifier-free) is provable iff a finite disjunction ⋁_i φ(t⃗_i) of ground instances is propositionally valid. Herbrand 1930. Reduces first-order validity to an effectively…
A purely existential first-order sentence ∃x⃗ φ(x⃗) (with φ quantifier-free) is provable iff a finite disjunction ⋁_i φ(t⃗_i) of ground instances is propositionally valid. Herbrand 1930. Reduces first-order validity to an effectively…