Ich habe folgende Aussage:
Wenn x>=4, dann 2^x>=x^2

Diese Aussage stimmt wie sich leicht erkennen lässt nun will ich sie aber beweisen, und zwar nicht mit Induktion sondern zur Übung mit der Prädikatenlogischen Resolution:
Dazu zunächst einige Definitionen:

G(x,y) := x>=y
e(x,y) := x^y

V := der Allquantor
E := Existenzquantor
- := Negation
= := Äquivalenz
v := Disjunktion
^ := Konjunktion

Nun habe ich die Aussage nach diesen Definitionen in Prädikatenlogik umgeschrieben:

Vx( G(x,4) -> G( e(2,x), e(x,2)))

Um diese Aussage zu beweisen, muss ich die Allgemeingültigkeit dieser Formel zeigen, oder die Unerfüllbarkeit der Negation:

-Vx( G(x,4) -> G( e(2,x), e(x,2)))
= Ex-( G(x,4) -> G( e(2,x), e(x,2)))
= Ex-( -G(x,4) v G( e(2,x), e(x,2)))
= Ex( G(x,4) ^ -G( e(2,x), e(x,2)))
erfüll.Äq. (G(a,4) ^ -G( e(2,a), e(a,2))) Skolemkonstante a
= { {G(a,4)} {-G( e(2,a), e(a,2))} }

Hier kann ich ja nun nicht resolvieren, da ich keine Variablen mehr habe so dass Unifikation möglich wäre. D.h. ich kann keine leere Klausel resolvieren und damit wäre die ursprüngliche Aussage nicht gültig. Wo liegt der Fehler?

Bin selbst auf den Fehler gekommen. Wenn es allgemeingültig wäre, dann wäre es ja für jede Struktur gültig, also für jedes Universum und jede Interpretaion. Aber mein Universum sind ja nur die Natürlichen Zahlen und meine Interpretation ist ja auch festgelegt.
Gibt es denn irgendeine andere prädikatenlogische Methode die Gültigkeit in der Struktur zu zeigen, ohne es für alle Zahlen einzeln zu zeigen (was ja nicht geht, da das Universum unendlich ist)?

gültig ist die Formel ja nicht,

du meinst die Erfüllbarkeit zu zeigen in dem du eine Interpretation vorgibst und dort drin die Gültigkeit zeigst? (ok, dann ja doch bisschen gültig ;) )

da kannst du verwenden was die Mathematik hergibt:
durch die Interpretation gilt: die Formel ist gültig wenn [x>=4, dann 2^x>=x^2} mit den bekannten Rechenenregeln gilt,

und das ist ja nun nur noch ein mathematischer Beweis

Bin selbst auf den Fehler gekommen. Wenn es allgemeingültig wäre, dann wäre es ja für jede Struktur gültig, also für jedes Universum und jede Interpretaion. Aber mein Universum sind ja nur die Natürlichen Zahlen und meine Interpretation ist ja auch festgelegt.
Gibt es denn irgendeine andere prädikatenlogische Methode die Gültigkeit in der Struktur zu zeigen, ohne es für alle Zahlen einzeln zu zeigen (was ja nicht geht, da das Universum unendlich ist)?

Joahhh… Also, du kannst die Peano-Axiome formulieren, Exponenten über Multiplikation über Addition formulieren und Größer-Gleich-Beziehungen definieren… Das ganze müsste dir dann ein "gültig" liefern :-)

Also, um das mal anders zu formulieren:

Um mit Prädikatenlogik etwas zu beweisen brauchst du Axiome und Ableitungsregeln. Wenn du etwas über die Domäne der Mathematik sagen möchtest, brauchst du selbige für (einen adäquaten Teil der) Mathematik.