is this formula provable in predicate logic? ⊢ (∀x)(∀y)(f(x1) = y1 → ((∀z)g(z) = f(x1) ≡ (∀z)g(z) = y1)) "Can you prove ⊢ (∀x)(∀y)(f(x1) = y1 → ((∀z)g(z) = f(x1) ≡ (∀z)g(z) = y1)) in predicate logic? explain."
I'm saying no, but I'm not sure why. Is it because it's not a tautology? and how would Godel's incompleteness theorems come to play here?
Please help, thanks.
 A: In first order logic, there are validities in addition to tautologies. These statements are statements that are true in every possible interpretation, and just not being a tautology isn't enough to tell you if it's a valid statement or not. Gödel's incompleteness theorems suggest that for every system that's powerful enough to represent arithmetic, there are statements that are undecidable... that is the truth value might be true in a particular model but not be a theorem of the formal system, but that doesn't say that validity is undecidable directly.
Church's theorem does however. That's the answer to the Entscheidungsproblem, the question on whether there's an algorithm to decide the validity of a first order statement. Church answered this in the negative for statements that are sufficiently complex.
I can't say for sure in your particular statement, since the statement looks a bit ambiguous, with quantifiers not matching any variables, and syntactic identity symbol being used where I think biconditional is meant. However if I take your statement to be this one in prenex normal form:
$\forall$x$\forall$y$\forall$z$\forall$u : ((f(x) = y) $\implies$ (g(z) = f(x)) $\iff$ (g(u) = y))
Then we can say some things about it. First, it is decidable since the only dyadic predicate is equality. This means we can determine whether it's a valid statement though several ways. We can negate the statement and use resolution. If we come up with the empty clause, it's a contradiction and hence it's unsatisfiable. The negation of an unsatisfiable statement is a valid statement. If you run out of rules, you've saturated the search and proven it satisfiable. 
But satisfiable doesn't mean valid. A formula can be satisfiable and it's negation can be satisfiable as well, and what that means is there are models for each instance. This opens another way to find out if the statement is provable or not: finite model generation. I think that since the statement has only equality and monadic functions that if there's a model of it the model is finite so we can generate interpretations of the statement to see if it applies. If there's a finite model for the statement and the negation of the statement, the statement is unprovable also.
You can prove, through saturation of resolution or finite model generation that the statement isn't logically valid. It is satisfiable though.
