But can get infinitely more complicated
The addition in the ring is $\oplus$
The multiplication is $\wedge$
SO, I made a post just now
about that see my profile
Why doesn't this ever come up etc. It's like purposely hidden knowledge
The point being, why don't we work with proofs like we do expressions in a ring
And all the things you can do with ideals, etc.
Then variable substitution is what? A ring endomorphism
$a \implies b \equiv a(1 + b) = 0$ in this ring
Where we say that $P = 0$ whenever we know or have assumed that $P$ is a false proposition
So we got rid of logical union, but you can reconstructe it with $+ = \oplus =$ xor: $a \vee b = a + b - ab$.
$a b = a \wedge b$ by definition
Okay, we use it a lot. Anyway, when we speak of multiple things in a theorem, the logic is usually and between the things
Let $a \in B$, (AND) let $b \in A$.
So it's natural that juxtaposition of letters (prop variables) be logical and
@geocalc33 see above notes when you're back. Let me know if you want to code on it with me. I think we should use either C++/D or rust. Yes, there are some interesting things. I'm currently liking the way Metamath works, not their old-style HTML UI, but its verification code is rather simple. < 1000 lines in Python 3.
The verification code is called a verifier, and all it does is run through a file of proofs, import missing proofs, and check each one against the axioms.
Supposedly the only thing a human needs to know about when reading metamath is "variable subst", but I don't believe that
What's impressive about metamath is that it's able to verify 28,000 proofs in < 1 second, at least this rust code on github is capable
Proof search is not verification though. It's a whole other arena of algorithm
It's what factorization is to checking factorization of an integer. Checking $XY = N$ is easy once you know $XY$, but computing $X,Y$ is believed to generally be exponentially difficult in the # digits of $N$
So, two hopelessly diffferent yet mathematically related algorithms
