Interpretation of knowledge in first order logic

I don't quite understand how to correctly interpret knowledge in First Order Logic.

Here is what I think about the different building blocks of FOL:
- Function: input: term(s) -> output: term
- Predicate: input: term(s) -> output: true/false
- Term: Function(Term,..) | Constant | Variable -> A term is like an object NOT a truth value
- Sentence: Predicate(Term(s)) | Term -> A sentence is like a complex predicate which evaluates to true/false once you replace the free variables with real objects

Is my understanding correct so far?

Now, I want to build a knowledge base in order to check later whether a fact is entailed in the knowledge base or not.

This is where I am confused.

Here is a simple fact:
All professors are male.
Version 1: ∀x prof(x) => male(x)
Version 2: ∀x prof(x) ∧ male(x)

Regarding version 1:

Interpretation

For me, the first one read as: "Every x who is a professor is automatically male." When x is not a professor the premise is false therefore you can conclude whatever you want. False => True/False. It's basically a free pass for every object which is not a prof. Is this correct? I guess it doesn't matter as it was not the idea to constraint other objects except professors.

Fact checking/Inference

When I later want to check a fact, e.g. Sarah is female and a professor. I would insert Sarah for x and see that the implication is wrong and thus the new fact is not satisfied by the knowledge base. Is this correct?

Regarding version 2:

Interpretation

The second one reads as: "Every x who is a professor and also male." Then it stops without a conclusion. Here something like ∀x (prof(x) ∧ male(x)) => True seems to be missing. This is also confusing. Is it even possible to represent the fact not using an implication?

Fact checking/Inference When I later want to check a fact, e.g. Sarah is female and a professor. I would insert Sarah for x, prof(x) ∧ male(x) would be false as male(Sarah) is false. This looks correct. Are both versions correct after all?

Could someone help me understand how to correctly represent/interpret sentences in the knowledge base?

• Quite correct... maybe is better to say that terms like constants are "names" for objects. – Mauro ALLEGRANZA Jan 3 at 11:48
• For "All professors are male" the correct symbolization is Version 1: $∀x (Prof(x) \to Male(x))$. If $x$ is not a $Prof$, don't worry, but if $x$ is a $Prof$ then it follows that it must be a $Male$. – Mauro ALLEGRANZA Jan 3 at 11:49
• "All professors are male" is falsified by a $Prof$ that is not a $Male$. Version 2, instead : $\forall x (Prof(x) \land Male(x))$ is falsified also by a $Male$ that is not a $Prof$, and this is not waht we want. – Mauro ALLEGRANZA Jan 3 at 11:53