From first-order logic to natural language

Question

I have this statement in FOL: $$∀x. (\mathrm{smart}(x) \lor ¬\mathrm{student}(x))$$ The natural language translation is$$ \text{All students are smart.} $$ I am not sure how this is concluded from FOL because it just says $x$ is either smart or not a student.

Can I convert the FOL as follows in order to conclude this statement? $$∀x. (\mathrm{smart}(x) \lor ¬\mathrm{student}(x))\\ ∀x. (¬\mathrm{student}(x) \lor \mathrm{smart}(x))\\ ∀x. (\mathrm{student}(x) → \mathrm{smart}(x)) $$

Answer 1

I am not sure how this is concluded from FOL because it just says x is either smart or not a student.

Correction, it says: everything is smart or not a student.

So clearly: if any thing is a student, then it must be smart.

Can I convert the FOL as follows in order to conclude this statement:

Yes. $\forall x~(\def\smart{\operatorname{smart}}\smart(x)\vee\neg\def\student{\operatorname{student}}\student(x))~\equiv~\forall x~(\student(x)\to\smart(x))$

Answer 2

Yes, you have to use the equivalence between :

$\lnot p \lor q$

and :

$p \to q$.

See : Material implication (rule of inference).

Answer 3

Let $\text{student(x)='x' is student}$

$\text{smart(x)='x' is smart}$

All student are smart can be written as-:

$\forall x (\text{student(x)} \rightarrow \text{smart(x)})$

on expanding it further,

$\forall x (\text{student(x)}^{'} +\text{smart(x)})$

as $p \rightarrow q =p^{'} +q$