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.