Flattening quantification over relations

Question

I already asked this question in stack overflow here and somebody suggested to post it here. I repeat the question again:

I have a Relation f defined as $f: A \to B × C$. I would like to write a first-order formula to constraint this relation to be a bijective function from A to B × C?

To be more precise, I would like the first order counter part of the following formula (actually conjunction of the three):

$$\begin{align} \forall a: A,\exists! bc : B × C, f(a)=bc & \qquad\text{$f$ is function}\\ \forall a_1,a_2: A, f(a_1)=f(a_2) → a_1=a_2 & \qquad\text{$f$ is injective}\\ \forall bc : B × C, \exists a : A, f(a)=bc & \qquad\text{ $f$ is surjective} \end{align} $$

As you see the above formulae are in Higher Order Logic as I quantified over the relations. What is the first-order logic equivalent of these formulae if it is ever possible?

Thanks

Answer 1

First of al in logic $ B \times C$ is just an other set.

so lets assume

• Ax is true iff $ x \in A$
• Bx is true iff $ x \in B \times C$
• Rxy is true iff $ f(x) = y $

then your relations become

$f(x)$ is a function: $ \forall x (Ax \to ( \exists y (By \land Rxy \land \forall z ((Bz \land Rxz) \to y = z )))) $

$f(x)$ is injective: $ \forall x y z ((Ax \land Ay \land Bz \land Rxz \land Ryz ) \to x = y) $

the last one you can do yourself

GOOD LUCK