Talk:Herbrand's theorem

Latest comment: 1 year ago by 2601:646:9D81:2C30:C1BA:9B11:122E:E809 in topic Statement Section is wrong

mergefrom Herbrand theory

edit

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)Reply


Corollary

edit

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)Reply

Source? Taemyr (talk) 01:02, 23 November 2008 (UTC)Reply
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)Reply

Cites for generalizations?

edit

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)Reply

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

edit

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 (talkcontribs) 16:03, 5 June 2022 (UTC)Reply

Statement Section is wrong

edit

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