Regarding the question of translating the verbal descriptions of definitions and theorems into propositional logic

Question

I am studying discrete mathematics and recently trying to describe mathematical definitions or theorems in the form of propositional calculus or predicate calculus. I am not sure if my approach is correct.

For example, for a many-to-one function, the definition is that there exist two different elements in the domain mapping to the same element in the codomain.

So I thought to describe it like this:

Let $ f : A \to B $ be a function, and define the proposition P as:

$ P \equiv(f \text{ is a many-to-one function})\iff (\exists x, y \in A, (x \ne y) \implies (f(x) = f(y))) $

To ensure this proposition is correct, I thought of a method using truth tables.

Let

$ P \equiv T $ , $ (f \text{ is a many-to-one function}) \equiv T $

So

$ \exists x, y \in A, (x \ne y) \implies (f(x) = f(y)) \equiv T $

Then look at the truth table of the conditional statement:

$ x \ne y $	$f(x) = f(y) $	$ (x \ne y) \implies (f(x) = f(y)) $
T	T	T
T	F	F
F	T	T
F	F	T

Then I found a problem: when $ x \ne y $ and $ f(x) = f(y) $ are both F, the proposition is still true. This obviously does not fit the definition of a function, so I discarded this proposition.

I tried another expression:

$ (f \text{ is a many-to-one function}) \iff (\exists x, y \in A, ((x \ne y) \land (f(x) = f(y)))) $

But I still couldn't find where the problem is, so this is my final conclusion.

Recently, I have been studying these logical propositions and following similar steps as above. I am curious if there is any mistake in this approach.

Answer 1

To fully formalize your definition of $P$ in predicate logic, you might consider something like:

$~~~~~\forall f: \forall d: \forall c: [\forall a:[a\in d \implies f(a)\in c]\\ ~~~~~\implies [P(f,d,c) \iff \exists a: \exists b: [a\in d ~\land ~b\in d ~\land [a\neq b ~\land~ f(a)=f(b)]]]]$

(Note that last '$\land$'.)