I am a math noob. These questions will likely sound dumb so I apologize ahead of time. But I like to code, and I've been getting into lisp languages. Someone wrote an introductory summary to Gödel foundations of mathematics/incompleteness theorem written in variation of lisp they called PM-Lisp (principia mathmatica lisp).
Article can be seen here: https://stopa.io/post/269
I found the article really fascinating but had trouble following through all of it. The first Issue I had was the definition of equals "="
(def = (and (when A B) (when B A)))
which was built atop the when symbol in the list of symbols:
I think I was confused about the when function... I was at first thinking of when as when in clojure which is essentially just a macro for (if .. do ..)
(macroexpand '(when 1 2 3 4)) (if 1 (do 2 3 4))
but that is not what it seems to do in PM-Lisp take the example of = definition:
(def = (and (when A B) (when B A)))
If this were the same functionality clojure it would be testing the truthyness of the evaluation of each when expression
so If I had (and (when 3 5) (when 5 3)) it would evaluate to (and 5 3) which would evaluate to 3 which is truthy.
So that got me stuck in the article. But it seems that when is more like a test/assertion... (when x z) saying for all values of x ... z is implied (i.e. the same way one mathematical rule implies another). Though I'm not sure what the author means by "A implies B"
I'm going to reread this article and try to understand better.
As per comments above, "when" is the Conditional connective (aka: Material implication) formalizing "if..., then...".
If so, the example regarding the definition of "equal" must be about the Bi-conditional: $(A \equiv B) =_{\text {def} }(A→B)∧(B→A)$, that is defined this way into Principia Mathematica.
The example "(not (= 0 1))" reads in usual logical symbols: $¬(0=1)$, while "(or (= 0 1) (not (= 0 1)))" reads $(0=1) ∨ (¬(0=1))$.
Finally, "(there-is x (= 4 (* x 2))" is $∃x \ (4=(x∗2))$.
IMO, the example with "when" is quite confusing: the conditional connective must be used with statements (the same for "or" and "not") and not with numbers: the statement "if 0, then (either 0 or 1))" is meaningless, unless $0$ and $1$ are used also as boolean constants for False and True.
Following the previous examples, if would suggest: "(when (= 0 1) (or (= 0 1) (not (= (0 1)))))", that reads: $(0=1) → ((0=1) ∨ (¬(0=1)))$.