what difference between propositions and `if` statement of program

Question

Consider a proposition, $$\forall x\in\mathbb{R}~(x^2<0\implies x=23)\tag{1}$$ Due to vacuous truth, Obviously it's a true proposition, However I have confused by it when transform this proposition to a program. Such as:

if(x² < 0){
  return 23;
}

We know the statement will never be executed, because x² always greater or equal than zero, I don't know, Does a mathematics proposition can be transformed to if statement in program, if my transformation is wrong, how to transform this proposition?

TABLE

A   B   T/F
___________
T | T | T
T | F | F
F | T | T
F | F | T

Answer 1

You are confusing two uses of the combination "if.....then". In math it is a connective, a way of linking two sentences into one sentence. We define that in "if A then B" if A is false the compound sentence is true. In programming "if A then B" means "if A is true, do B, and if A is false do not do B". These are not at all the same.

Programming languages like FORTRAN and Python also have a completely different meaning for the equals sign. It is normal to write $I=I+1$ except in Python you use lower case. The equals sign is not what mathematicians use it for, it is a direction to compute the right hand side and store that in the address indicated by the left hand side. The left side has to be essentially a single variable.

In English, whether you consider "if A then B" to be true when A is false is ambiguous. If I say "If 2+2=5 then the moon is made of green cheese." is that true, false, or nonsense? I think most people would opt for nonsense. In English "if ..... then" has a sense of the first causing the second. In math it is clearly true.

Meanings change due to context.

Answer 2

The material implication symbol $\implies$ (which is sometimes called the "if" symbol) is pretty much totally unrelated to if-statements in computer programming.

In classical logic (the kind of logic that mathematicians use 95% of the time, perhaps), the statement $p \implies q$ is simply an abbreviation of $(\neg p) \lor q$. It means exactly that, no more, no less.

So, the correct way to translate $x^2 < 0 \implies x = 23$ into computer code would be something like this:

function my_predicate(x) {
    let p = (x² < 0);
    let q = (x == 23);
    return ((!p) || q);
}

Then the sentence $\forall x\in\mathbb{R}~(x^2<0\implies x=23)$ is equivalent to the assertion that the function my_predicate is equivalent to the function always_true, as defined like so:

function always_true(x) {
    return true;
}