Perhaps another way to go about this is to introduce GL modal logic. Instead of creating shares in and , create shares in and . It’s not possible to exchange a pair of shares in and for cash, because is not a logical tautology.
Yeah, that is kind-of the direction my thoughts went in when I wrote the first post. I was thinking then that would be formalized by formalizing a proof system and letting correspond to the statement that has a proof in that system. This looks quite complicated to implement, and also to use.
If there is a more synthetic version where is a fundamental part of the formal system, then maybe that is a lot easier to deal with? I’m not sure how one implements such a thing in a proof checker.[1] Is just a functions from types to types? Surely it is not as simple as that?
Where do we get the original sequence of truth values ? I assume for provable or disprovable propositions, the functions need to be constant true and constant false respectively?
Perhaps another way to go about this is to introduce GL modal logic. Instead of creating shares in
Yeah, that is kind-of the direction my thoughts went in when I wrote the first post. I was thinking then that
If there is a more synthetic version where
I found this, but I don’t understand it at all right now.
Let every natural number
and as usual otherwise.
As far as I understand, the sequence always converges and you can test a proposition by checking whether every natural number assigns true to it.
Where do we get the original sequence of truth values
By “as usual otherwise”, I meant