On Tue, Aug 6, 2013 at 1:02 AM, Tanner Swett <swe...@mail.gvsu.edu> wrote:
> Arguments:
I'm not sure whether I agree with you or not. I agree that
00:53 < tswett> If a rule were to say "if it is POSSIBLE to do X, then
it is POSSIBLE to do Y", I think we would treat
this as meaning something very different from "if it
is IMPOSSIBLE to do Y, then it is POSSIBLE to do
X".
and that therefore, we should not treat Agora's ruleset as a set of
axioms. However, I don't think this is actually divorced from logic
somehow - e.g. I think that a CFJ on whether Fool CAN deregister
everyone would have still been FALSE, and don't think that adding an
indirection in the form of a definition, which would seem to require
some form of logic (e.g. Fool uses Curry's paradox to establish that e
is a Yak Master, then creates some Yaks) would change anything.
Actually, a simple way to model this in formal logic, which I did not
think of (doh), is to make the statements in the rules primitive
inference rules rather than axioms.
Registrar(p) ⊢ YakMaster(p) # definition
Player(p) ⊢ CanDeregister(p) # mechanism
This gets more complicated in the presence of self-contradictory
statements and the "default deny" rule:
~CanDoX(p) ⊢ CanDoX(p) # bad rule
[can't prove CanDoX(p)] ⊢ ~CanDoX(p) # ??? this shouldn't exist
⊥
CanDoY(p)
so it may be required to use more power than inference rules in some
unusual situations, but it's a reasonable general framework.
