Consider the string $(∀x)(∀y)(f(x) = y → ((∀z)g(z) = f(x) ≡ (∀z)g(z) = y))$

Question

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.

Answer 1

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.

Answer 2

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:

Answer 3

(∀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))