Wednesday, June 12, 2013

Proposal: Propositions

Passes 6-3 / Skju

Adminned at 13 Jun 2013 19:35:08 UTC

Amend the rule “Truth” to read:

There is a wiki page called “Truths” which consists of two sections, Axioms and Theorems, each containing and ordered list of True Formulae. No Truths may contradict each other.

Any Atom can add an item to either list by submitting an entry in the “Proof” category that states the Formula to be added, which section to add it to, and, for a Theorem, a logical sequence of deductions that leads to it from existing Truths (unless the Atom already has 2 Proofs pending). Proofs are Votable Matters and as such are governed by the rule “Votable Matters”. Proofs cannot be Vetoed. The oldest pending Proof may be enacted by any Admin if either of the following is true:

  • It has been open for voting for at least 12 hours, has a number of FOR Votes that exceed or equal Quorum, and has not been Self-Killed.
  • It has been open for voting for at least 24 hours, it has more than 1 valid Vote cast on it, it has more valid Votes cast on it FOR than AGAINST, and has not been Self-Killed.

Any pending Deliberation may be failed by any Admin, if any of the following are true:

  • It could not be Enacted without either one of the Votes AGAINST it being changed, or the set of Atoms being changed.
  • It has been open for voting for at least 48 hours and cannot be Enacted.
  • It cannot be Enacted without causing a contradiction between Truths.

If a Proof somehow ends up being pending for more than 4 days, it is ignored for the purpose of calculating the oldest pending Proof, and can be failed by any Admin.

Each Theorem shall have next to it a link to the Proof that introduced it.

Enact a new rule entitled “Formulae”:

A Variable is a single lowercase letter. A Connective is a sequence of non-lowercase characters that is either unary (placed before a Formula) or binary (placed between two Formulae). A new Connective can be Defined by an Axiom that asserts the equality of a Formula that contains the Connective and a Formula that does not.

A Formula (plural Formulae) is either a single Variable or a sequence of Variables and properly-placed Connectives. Brackets (”[” and “]”) should be used around a Formula to disambiguate the order in which Connectives apply. A Formula is either True (1) or False (0).

Add the following Axioms to Truths:

  • x = x
  • [0 - 0] = 1
  • [0 - 1] = 0
  • [1 - 0] = 0
  • [1 - 1] = 0

We’ve got quite a lot going on here. Splitting Truths into Axioms and Theorems, allowing them to be added through fully democratic Proofs, defining Formulae, and introducing equality and NOR.

posted by Skju at 12 Jun 2013 02:30:06 UTC Comments (13)

Comments

RaichuKFM: she/her

12-06-2013 05:45:27 UTC

for Though could someone explain the last four axioms? Just what it is they mean.

quirck: he/him

12-06-2013 06:36:09 UTC

Last four axioms specify the Connective -, which is short for NOR.
If x=x, can we induce that y=y? If yes, then truths like x=0 lead to every variable being false, and if no, then we haven’t introduced reflexivity.
for

quirck: he/him

12-06-2013 06:54:21 UTC

Also, Proofs can be enacted, but Deliberations can be failed :)

Larrytheturtle:

12-06-2013 07:38:26 UTC

for

Skju:

12-06-2013 13:30:53 UTC

Quirck, I don’t know what we can induce because we don’t have any rules for it yet. It looks like I forgot it here, but a Variable should be “True or False within the context of the Formula that contains it” or something, so that the value of x doesn’t carry over into another Formula. We could also introduce Constants, maybe calling them nullary Connectives, for when we move past 2-valued logic.

Sphinx:

12-06-2013 13:43:44 UTC

for

nqeron:

12-06-2013 14:24:00 UTC

for

redtara: they/them

12-06-2013 17:45:21 UTC

for

Clucky: he/him

12-06-2013 18:15:48 UTC

against I like the idea on voting on Axioms, but voting on Proofs seems weird. Either they are valid or they aren’t, regardless of how we vote.

redtara: they/them

12-06-2013 20:33:27 UTC

CoV against per clucky

Skju:

13-06-2013 00:15:20 UTC

How do you have people verify a theorem proof and report back without bias? What’s the alternative? People should vote for a theorem based on the proof, not the idea. That should probably be explicit. Moreover, it currently doesn’t even matter whether or not a theorem exists so long as it follows from the axioms, and we have yet to see how that will change.

Cpt_Koen:

13-06-2013 03:13:00 UTC

against
I’m OK with voting on proofs - it doesn’t make less sense than voting on declarations of victory.

However I don’t like the idea of redefining NOR and every other “connective”. I’d prefer that we either:
* make up our own kind of weird, crazy, nomicky logic (blogic?), or
* rely on what already exists, “logic” or “common sense” or whatever, in which case we don’t really need to define anything.

The first may turn into something like ftp://ftp.nvg.ntnu.no/pub/frc/29

For the latter we may for instance define “statements” as being either an assertion in English or an Atom; statements are only accepted to be true if they are on the Truths page, but anyone may add a statement to the truths page by making a story post with a logical proof (and either we need to vote on proofs, or we can CFJ them when they are erroneous).

Skju:

13-06-2013 03:53:34 UTC

I’m not intending to redefine all of already-established conventional logic. I’m simply introducing a way to create Truths. I’ve stated that we should mess with rules of logic and manipulate the system for Nomicy purposes. I chose NOR to start from because it is one of the most versatile (functionally complete) binary connectives, so we could do the most stuff with it. I do agree that everything doesn’t have to be so symbolic, and we totally should incorporate English statements. I’ll look over the FRC archive too.