I really like the conversion to a representation that's more familiar but I suspect it's also confusing me. Here are the questions that I have to start:
Does 'there-is' evaluate to a boolean (is boolean a thing? is evaluation a thing?)
I was surprised that the axioms don't use there-is but I sense I shouldn't be?
what does '(when 0 (or 0 1))' mean, it's described as 'when 0, then there is either 0 or 1' but I'm not sure what that means? is '(when 0 0)' true and '(when 1 0)' false? Why not use '(when A B)' as equals?
Not a question but in the axioms I assume pairs should be pears and applies should be apples.
How goes 'implies' get introduced by '(when (when q r) (when (or p q) (or p r))'? Also, this introduces a category in the example i.e. fruits but not sure how that happened.
Why do we need to have second '(not (factor? x 3^22 ...))', isn't it sufficient to say that (factor? x 3^21 ...) to establish that the 2nd term is 'there-is'?
For existential quantification, we use the `there-is` function.
Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification.
Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.
I took these to mean the existential operator and the implication operator, but I agree they were insufficiently defined for me, esp. as we're building from first principles. The post could have made the early proofs more obvious in how they were constructed (e.g. how the language is really used to prove statements).
Does 'there-is' evaluate to a boolean (is boolean a thing? is evaluation a thing?)
I was surprised that the axioms don't use there-is but I sense I shouldn't be?
what does '(when 0 (or 0 1))' mean, it's described as 'when 0, then there is either 0 or 1' but I'm not sure what that means? is '(when 0 0)' true and '(when 1 0)' false? Why not use '(when A B)' as equals?
Not a question but in the axioms I assume pairs should be pears and applies should be apples.
How goes 'implies' get introduced by '(when (when q r) (when (or p q) (or p r))'? Also, this introduces a category in the example i.e. fruits but not sure how that happened.
Why do we need to have second '(not (factor? x 3^22 ...))', isn't it sufficient to say that (factor? x 3^21 ...) to establish that the 2nd term is 'there-is'?