​​民主主義の形式化2
​​

​​問題設定

​​
​​「任意の熟議がsoundな政体(DeFi DAOも含む)及び任意の操作を入力として、その操作がその政体の熟議をunsoundにするかどうかを検査できる関数を作る」というのがやりたいこと
​​
​​土台として「ある政体の熟議がsound(健全)である」ということを定義しないといけないので、下記の議論に繋がる
​​
​​

​​民主主義の健全性の定義

​​
​​liveness: あるunsoundな熟議を持つ政体が、その状態機械の少なくとも一つの要素をunsafe=>safeにする作用f()を少なくとも1つ持つとき、その作用f()の後に熟議がsoundになるような作用のパターンが少なくとも1つあるなら、その政体の状態機械はlivenessがある
​​
​​safety: あるsoundあるいはunsoundな熟議を持つ政体が、その状態機械の現状態を初期状態として任意回数同一の内容の提案をランダムに選ばれる審議員で繰り返すとき、有意に大きいn,kについてn+k回目とn+k+1回目の熟議の結果が異なる組み合わせが存在しないならば、その政体の状態機械はsafetyがある
​​
​​

​​平たく言うと

​​
​​liveness: 罷免でき、それで熟議が健全になるならlive
​​
​​safety: 熟議が外圧に影響されないならsafe
​​
​​

​​ふたつあわせて

​​
​​「罷免でき、それで熟議が健全になり、かつ熟議が外圧に影響されないなら、その政体は健全である」
​​
​​＊
​​

​​たぶんより緻密にやるなら必要であろう言及

​​ 
​​用語定義
​​ 
  • ​​内部状態
  • ​​= (ブロックチェーンだと) オンチェーン状態
  • ​​= (ガバナンス全般に一般化すると) オペランド
  • ​​
  • ​​外部状態
  • ​​= (ブロックチェーンだと) オフチェーン状態
  • ​​= (ガバナンス全般に一般化すると) ビザンチンアクター
​​ 
  • ​​状態遷移関数/入力 f が作用可能なのは「内部状態/オペランド」のみ
​​
  • ​​Adversaryが物理的に介入可能なのは「外部状態/ビザンチンアクター」のみ
​​
​​
​​ビザンチンアクターが存在する際のsafetyとlivenessの相互依存性について
​​ 
  • ​​1. safetyが満たされている限りlivenessは満たされる
  • ​​