Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Also, die ganze Methode der Polynomenordnung basiert hauptsächlich darauf, dass ich mir für jede

Operation in meiner Signatur, sagen wir endstellig, ein Polynom ausdenke.

Und zwar eins in so vielen Variablen wie die Stelligkeit angibt.

Also, mit N Variablen sagen wir x1 ist xn.

Und dann definiere ich für jeden Term t ein Polynom pt, was ich dann in offensichtlicher

Weise erhalte, nämlich durch rekursive Definition.

Ja, da haben wir letztes Mal eine rekursive Definition für angegeben, die besagt aber

schlicht und einfach, ersetze überall wo in dem Term so eine Operation vorkommt diese

Operation durch das Polynom, was ich mir dafür ausgedacht habe.

Gut, insgesamt hatte ich eine Polynomielle Interpretation mit typischen Buchstaben Script

A.

Die Polynome steht aus diesen Daten hier, also für jede Operation ein Polynom und einer

Teilmenge A von N.

Und ich sage ein Term ist in der Polynomordnung größer als S.

Genau dann, wenn die Polynome, die ich beidseits ausrechne, entsprechend vergleichbar sind

über diesen eingeschränkten Bereich auf den natürlichen Zahlen.

Wir haben am Ende der letzten Sitzung ein Beispiel gesehen, wo wir gemerkt haben, aha, nicht

manchmal, insbesondere muss man also typischerweise auf natürliche Zahlen bestimmter Mindestgröße

einschränken, damit man weiß, dass Variablen, die vorkommen, mindestens so groß sind wie

irgendwelche Konstanten, die man dann wegweist.

Also konkret in dem Falle musste halt die Variable x mindestens 2 sein oder größer

als 2, damit sie größer ist als eine konstante 2, die da auf der anderen Seite vorkommt.

Und solche Dinge bringt man in der Wahl dieses A unter.

So, da war noch technisch einiges offen und zwar insbesondere hatten wir, und zwar kurz

angedeutet, wie man so eine Polynomordnung verwendet, aber nicht warum so eine Polynomordnung

es am Ende dann auch tut.

Das analysieren wir jetzt noch mal zu Ende.

Insbesondere hatten wir in der Definition, was eine Polynomordnung ist, also was ich

da für Daten angeben muss, hatten wir insistiert, dass das Pf streng monoton sein soll.

Das analysieren wir noch mal ein bisschen weiter.

Wir nehmen uns also hier einen Polynom P in Variablen x1 bis xn.

Und wir sagen, das sei streng monoton, wenn eine rein syntaktische Eigenschaft zunächst

mal gilt.

Und zwar dann, wenn jede dieser Variablen xi in P auch tatsächlich vorkommt.

Es steht mir natürlich frei, als das P zunächst mal einfach eine Konstante zu wählen, ja,

also auch eine Konstante ist ein Polynom in Variablen x1 bis xn, die ich mich alle eben

zufällig mal entscheide, nicht zu verwenden.

Und das verbiete ich hier.

Also ich verlange, dass jede der Variablen, über denen P angeblich lebt, tatsächlich

in P vorkommt.

So, was heißt das formal?

Formal hatten wir ja so ein Polynom definiert, über einfach die Familie von Koeffizienten,

die es hat.

Für jedes Monom einen Koeffizienten.

Man muss also es eine solche Sequenz von Exponenten geben, i1 bis i n.

Das sind die Exponenten meiner Variablen im Monom.

So, das soll es geben für alle i.

Also, naja, xi kommt vor.

Ne, mach man doch nicht.