Tuesday, June 18, 2013

Proposal: Let’s skip this part

Passes 8-0 / Skju

Adminned at 19 Jun 2013 17:44:07 UTC

Amend Rule 2.3 “Formulae” to read:

A Formula is an unambiguous statement in first-order logic. Formulae may contain free variables. Formulae may be written using prose, symbols, or a mixture of the two. The use of undefined terminology does not constitute ambiguity unless it results in the structure of the Formula being ambiguous. A Formula is either True or False within its context.

In a Formula, “=” denotes equality; Formulae are considered equal if and only if they have the same truth value. “&&”, “||”, and “~” denote the logical AND, OR, and NOT operators, respectively. “->” denotes the material implication operator. “FA” and “TE” are abbreviations of “for all” and “there exists”, respectively. Square brackets function only as a grouping symbol; they do not have any additional semantics. “0” and “1” represent the trivially False Formula and the trivially True Formula, respectively.

Delete the axioms that were numbered 1 through 15 as of the beginning of June 17 (because they are tautologies in first-order logic, so it would be valid to use them in Proofs even if they were not present in the Truths page).

It looks to me like if we don’t do this, we’re just going to end up implementing first-order logic in a more tedious manner and end up with something that’s harder to use, so I suggest that we just skip over all that,

posted by Tavros at 18 Jun 2013 00:15:05 UTC Comments (10)

Comments

kikar:

18-06-2013 00:45:17 UTC

for

redtara: they/them

18-06-2013 02:09:43 UTC

for

RaichuKFM: she/her

18-06-2013 02:39:11 UTC

for

Skju:

18-06-2013 03:16:49 UTC

for

Skju:

18-06-2013 03:18:25 UTC

(I especially like “The use of undefined terminology does not constitute ambiguity unless it results in the structure of the Formula being ambiguous”, which I suppose functions as a window for importing externally-established truths.)

Larrytheturtle:

18-06-2013 04:04:14 UTC

for

Tavros:

18-06-2013 05:02:40 UTC

Well, my purpose in including that clause was to allow us to define things axiomatically without having to state what we’re doing. Like, if we wanted to try to define the real numbers, we could go ahead and start stating properties that real numbers have, without having to say “the real numbers are anything that satisfies these properties”, or “the real numbers are defined by these axioms”, or anything like that,

I think defining the real numbers would be really tricky, by the way, because I think the usual axiomatic definition of the real numbers uses second-order logic, and the usual way of imitating second-order logic using first-order logic uses infinitely many axioms,

Perhaps we ought to replace “first-order logic” with “second-order logic”, but on the other hand, are we really going to need the real numbers?

Clucky: he/him

18-06-2013 07:13:48 UTC

I still think it would be more fun if we didn’t do first order logic because we’ll just be working out of a textbook, but this is better than what we currently have.  for

Sphinx:

18-06-2013 13:39:46 UTC

for

Tavros:

19-06-2013 03:48:39 UTC

for , lest the Admins miscount