Talk:Herbrand's theorem

mergefrom Herbrand theory

Suggested merge: The Herbrand theory page does not seem to say anything much more than this page, thus I suggest a merge. But perhaps there is more to the theory than this individual theorem? I don't know ... linas (talk) 23:13, 4 June 2008 (UTC)

Corollary

I think we could add the following corollary: Every universal and model complete theory in a language has definable Skolem functions, which are given by terms in that language on finitely many definable pieces. Manta (talk) 12:03, 22 November 2008 (UTC)

Source? Taemyr (talk) 01:02, 23 November 2008 (UTC)

I have seen it used in several places. For instance, van den Dries, Lou; Macintyre, Angus; Marker, David: The elementary theory of restricted analytic fields with exponentiation. Ann. of Math. (2) 140 (1994), no. 1, 183--205, Corollaries 2.15 and 4.7. Manta (talk) 14:58, 24 November 2008 (UTC)

Cites for generalizations?

A work of Dale Miller is cited for the first, but what about the other two? 31.50.156.46 (talk) 18:41, 6 July 2019 (UTC)

Section "Statement" is either false or over-complicated.

In the theorem statement there is no constraints on the sequence of terms t_i,j. Either the specification is missing, saying what are the terms and if they are of specific shape. Otherwise, because the terms are not said to be different from each other - the theorem is equivalent to a formulation when only single sequence t_1,j needs to exist. — Preceding unsigned comment added by Zaabson (talk • contribs) 16:03, 5 June 2022 (UTC)

Statement Section is wrong

The statement indexes the terms $t_{ij}$ with $1\leq i\leq k$ and $1\leq j\leq n$. The bounds for $i$ should allow for any finite number but reuses $k$, the number of existential quantifiers, instead. Maybe use a new bound $r$ instead, i.e. $1\leq i\leq r$? — Preceding unsigned comment added by 2601:646:9D81:2C30:C1BA:9B11:122E:E809 (talk) 07:07, 17 July 2023 (UTC)