Consider the string $(∀x)(∀y)(f(x) = y → ((∀z)g(z) = f(x) ≡ (∀z)g(z) = y))$ Is this well-formed formula a tautology?
I am having trouble finding examples to help me work through these types of problems. I was hoping someone could help me out.
I think, using abstraction, this can be written as:
$$(∀x)(∀y)(p → (q ≡ q_1))$$
which can be further abstracted to a simple boolean variable such as $p_1$.
Which I say is not a tautology.
But then I am asked:
Can you prove $$(∀x)(∀y)(f(x) = y → ((∀z)g(z) = f(x) ≡ (∀z)g(z) = y))$$ in predicate logic? If so, give a proof, if not, explain why.
I know that if the above were a tautology, then the above would be immediately provable. But if it is not a tautology, what do I say?
Can I say it is not provable because it is not a tautology and therefore not an axiom... I don't know what to say here.
Thanks in advance for any help or thoughts.
 A: The formula is a valid formula of First-order logic with equality.
Here is the derivation:
1) $f(x)=y$ --- premise
2) $(∀z)(g(z)=f(x))$ --- assumed [a]
3) $g(z)=f(x)$ --- from 2) by Universal instantiation
4) $g(z)=y$ --- from 1) and 3) bt transitivity of equality
5) $(∀z)(g(z)=y)$ --- from 4) by Generalization

6) $(∀z)(g(z)=f(x)) \to (∀z)(g(z)=y)$ --- from 2) and 5) by Conditional Proof (i.e. Implication introduction)

In the same way, assuming $(∀z)(g(z)=y)$ we derive : 

7) $(∀z)(g(z)=y) \to (∀z)(g(z)=f(x))$.

Thus, we derive, by Bi-conditional introduction :

8) $(∀z)(g(z)=y) \leftrightarrow (∀z)(g(z)=f(x))$

and finally we conclude with:


9) $(∀x)(∀y)[(f(x)=y) \to ((∀z)(g(z)=y) \leftrightarrow (∀z)(g(z)=f(x)))]$ --- from 19 and 8) by Conditional introduction (discharging the premise) and Generalization twice.


Having proved it, by soundness of the calculus, we conclude that the formula is valid.
A: Assuming your $x_1$ is just $x$, and $y_1$ is just $y$, the statement is valid.
Your abstraction does indeed not show this, however, since your $p$ abstracts away from the crucial identity $f(x) = y$ that makes this a valid statement.
Here is a proof in Fitch:

A: (∀x)(∀y)(f(x)=y→((∀z)g(z)=f(x)≡(∀z)g(z)=y)
(∀x)(∀y)(f(x)=y)→(∀x)(∀y)((∀z)g(z)=f(x)≡(∀z)g(z)=y)  (Theorem)
(∀x)(∀y)(f(x)=y)  |--  (∀x)(∀y)((∀z)g(z)=f(x)≡(∀z)g(z)=y)  (deduction theorem)
Using a ping pong argument:
(∀x)(∀y)(f(x)=y)  |--  (∀x)(∀y)((∀z)g(z)=f(x)→(∀z)g(z)=y)
(∀x)(∀y)(f(x)=y)  |--  (∀x)(∀y)(∀z)g(z)=f(x)→(∀x)(∀y)(∀z)g(z)=y (Theorem)
(∀x)(∀y)(f(x)=y),(∀x)(∀y)(∀z)g(z)=f(x)|-- (∀x)(∀y)(∀z)g(z)=y (deduction)
(∀z)(∀x)(∀y)(f(x)=y),(∀x)(∀y)(∀z)g(z)=f(x)|-- (∀x)(∀y)(∀z)g(z)=y (axiom)
(1) (∀z)(∀x)(∀y)f(x)=y      (Hypothesis)
(2) (∀x)(∀y)(∀z)g(z)=f(x)   (Hypothesis)
(3) f(x)=y                  (Specialization (1))
(4) g(z)=f(x)               (Specialization (2))
(5) y=g(z)                  (Transitivity (3) and (4))
(6) (∀x)(∀y)(∀z)g(z)=y      (Generalization x,y,z dnof in (1) or (2))
(∀x)(∀y)f(x)=y  |--  (∀z)(∀x)(∀y)g(z)=y → (∀x)(∀y)(∀z)g(z)=f(x)
(∀x)(∀y)f(x)=y,(∀z)(∀x)(∀y)g(z)=y  |-- (∀x)(∀y)(∀z)g(z)=f(x) (deduction)
(∀z)(∀x)(∀y)f(x)=y,(∀z)(∀x)(∀y)g(z)=y |-- (∀x)(∀y)(∀z)g(z)=f(x) (axiom)
(1) (∀z)(∀x)(∀y)f(x)=y    (Hypothesis)
(2) (∀z)(∀x)(∀y)g(z)=y    (Hypothesis)
(3) f(x)=y                (Specialization (1))
(4) g(z)=y                (Specialization (2))
(5) g(z)=f(x)             (Transitivity (3) and (4))
(6) (∀x)(∀y)(∀z)g(z)=f(x) (Generalization x,y,z dnof in (1) or (2))
