I'm having some trouble understanding the article's formula; and honestly it's a little weird to see people complain about how trivial the proof is.
Both this article and the article it quotes introduce the "((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q))" formula with absolutely no additional explanation. I guess that's fine if the article are meant for people with a mathematics background, but at someone who has always struggled with post-high-school-maths... what the hell?
I understand what ∃, ∀, ⇔, and → represent ("there exists", "for all", "equivalent" and "implies", respectively), but I have no idea how to parse the entire formula. What are P and Q?
After multiple tries, I'm reading it as "saying that 'there exists a x such that P(x) is true' implies Q" being equivalent to "for all x, P(x) implies Q", with the idea that P and Q are arbitrary proposals or whatever the proper terms are... But still, just processing the logical reasoning in my head is tough.
On the other hand "some types implement traits, and if a function expects a trait impl you can only pass it types that implement that trait" feels absolutely clear to me. It might be that Rust is good at breaking down math concepts into the essentials you need for programming. Or it might be that formal Math notation is not for me.
Just a quick note, the symbol ⇔ is typically meant to stand for 'material implication' and would be better read as 'if and only if'. Or at least that is the 'normal' usage in the literature for intuitionistic logic. It doesn't really change your reading of it, but equivalent does not really capture the traditional meaning of material implication. It is more accurate to portray the logical sentence as valid with either implication in the first position. The two statements are not equivalent to each other, but the re-ordering of the implications would be, i.e.
P and Q are propositions. P takes one parameter and Q takes none. For example P(x) might be "x is odd". The term `P(x)` by itself refers to P(x) being true.
So `∃ x. P(x)` is read as "There exists an x for which P of x is true." or "There exists an x such that P of x is true."
So `((∃ x. P(x)) → Q)` is read as "If there exists an x such that P of x is true, then Q is true."
And `(∀ x. (P(x) → Q))` is read as "For all x, if P(x) is true then Q is true."
The `⇔` indicates that the left hand side is true if and only if the right hand side is true, or in other words that they're equivalent, which you can tell from the descriptions above that they are.
Or it might be that formal Math notation is not for me.
No, it just means that you haven't studied that notation. Like programming, being skilled at maths is not something you're just naturally gifted with. It has to be studied.
The proof of the proposition in question is "trivial" in the sense that a first course in formal logic is more than enough to fully understand it, and that there is really no extra trick involved, basically the proof is as straightforward as it could be.
I will agree that the article doesn't explain enough how the formula in question relates to type theory and Rust's type system in particular.
Thanks for the feedback, I should have spent more time connecting the logic statement to the equivalent rust syntax as you’re right the post has a weird audience problem otherwise. You either already know logic well enough that the proof is trivial, or it doesn’t make any sense.
Comments
I'm having some trouble understanding the article's formula; and honestly it's a little weird to see people complain about how trivial the proof is.
Both this article and the article it quotes introduce the "((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q))" formula with absolutely no additional explanation. I guess that's fine if the article are meant for people with a mathematics background, but at someone who has always struggled with post-high-school-maths... what the hell?
I understand what ∃, ∀, ⇔, and → represent ("there exists", "for all", "equivalent" and "implies", respectively), but I have no idea how to parse the entire formula. What are P and Q?
After multiple tries, I'm reading it as "saying that 'there exists a x such that P(x) is true' implies Q" being equivalent to "for all x, P(x) implies Q", with the idea that P and Q are arbitrary proposals or whatever the proper terms are... But still, just processing the logical reasoning in my head is tough.
On the other hand "some types implement traits, and if a function expects a trait impl you can only pass it types that implement that trait" feels absolutely clear to me. It might be that Rust is good at breaking down math concepts into the essentials you need for programming. Or it might be that formal Math notation is not for me.
Just a quick note, the symbol ⇔ is typically meant to stand for 'material implication' and would be better read as 'if and only if'. Or at least that is the 'normal' usage in the literature for intuitionistic logic. It doesn't really change your reading of it, but equivalent does not really capture the traditional meaning of material implication. It is more accurate to portray the logical sentence as valid with either implication in the first position. The two statements are not equivalent to each other, but the re-ordering of the implications would be, i.e.
((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) is equivalent to (∀ x. (P(x) → Q)) ⇔ ((∃ x. P(x)) → Q)
P and Q are propositions. P takes one parameter and Q takes none. For example P(x) might be "x is odd". The term `P(x)` by itself refers to P(x) being true.
So `∃ x. P(x)` is read as "There exists an x for which P of x is true." or "There exists an x such that P of x is true."
So `((∃ x. P(x)) → Q)` is read as "If there exists an x such that P of x is true, then Q is true."
And `(∀ x. (P(x) → Q))` is read as "For all x, if P(x) is true then Q is true."
The `⇔` indicates that the left hand side is true if and only if the right hand side is true, or in other words that they're equivalent, which you can tell from the descriptions above that they are.
No, it just means that you haven't studied that notation. Like programming, being skilled at maths is not something you're just naturally gifted with. It has to be studied.
The proof of the proposition in question is "trivial" in the sense that a first course in formal logic is more than enough to fully understand it, and that there is really no extra trick involved, basically the proof is as straightforward as it could be.
I will agree that the article doesn't explain enough how the formula in question relates to type theory and Rust's type system in particular.
Thanks for the feedback, I should have spent more time connecting the logic statement to the equivalent rust syntax as you’re right the post has a weird audience problem otherwise. You either already know logic well enough that the proof is trivial, or it doesn’t make any sense.