Nate Cull (.social)Hmm, Rulelog.
I *really* hope this is not the best synthesis of logic to date. It looks kinda... hairy.
How did we get from
0 = false
1 = true
to
Skolemize the monotonadic varptor function of the pre-literal dynastic modifier base importation exclusion-by-failure nonterminator defeasement
Surely there must be some *simpler things* that all this weird stuff is built out of?
And then the weird stuff can be a program?
Like, how do logicians argue about points of logic? They use some kind of logic to do it, right?
Shouldn't we just take whatever system logicians use, and code *that* up first?
Or are they actual wizards, and they settle arguments in the Journal of Constructivist Philosophical Logic by channelling their astral ether and turning other wizards into pies?
That might be difficult to code as a kernel proof algorithm, sure.