(unfortunately, it doesn’t look like I get any points for proving you wrong but I do not believe this to be true.

1: Property 1: If b and c are lists such that b ++ c = a, then there does not exist d such that d is an element of both b and c.

2: Claim 1: For all a, [if a is a list and a contains a finite number of elements, then the empty list is an element of a].

3: Subclaim A: If a list has a finite number of elements, one of them must be the empty list.

4: Suppose c is not the empty list. Then c = a:b where b is a list and a is an element of c. (axiom 5)

5: Subclaim B: If c is a list, then b:{} ++ c = b:c

6: b:{} ++ c = b:{{} ++ c} (axiom 10)
7: {} ++ c = c (axiom 11)
8: so b:{} ++ c = b:c

9: Subclaim C: If a is a list s.t. Property 1 holds, and a = b:c then if c has x elements, b has x + 1 elements.

10: For all d, if d = b then
11: b:{} ++ c = b:c = a (Subclaim b)
12: b is an element of b:{} (Axiom 8)
13: b is not an element of c (Property 1)

14: If d is an element of c, then d is an element of a (Axiom 8)

15: And if d != b, and d is not an element of c, then d is not an element of a. (Axiom 8)

16: So if c contains x elements, a contains every element of c plus b, or x + 1 elements.

17: Subclaim D: There does not exist a finite n > 0 (such that there exists a list a (such that a has exactly n elements and the empty list is not an element of n))

18: If there does exist such an n, there must be an m + 1 (m > 0) such that m + 1 is the smallest such n.

19: Let c be a list which contains m + 1 elements.

20: c is non empty as m > 0 (Subclaim A) so c = a:b where b is a list.
21: b contains n elements for some n
22: n + 1 = m + 1 (Subclaim C)
23: So n = m
24: m < m + 1 so the empty list is an element of b
25: Thus the empty list is an element of a (Axiom 8) And we have a contradiction

26: Claim 2: Every element of X cannot contain a finite number of elements:

27: Let c be an element of X.
28: c is a list, so b:{} ++ c = b:c (Subclaim 2)
29: {} is an element of b:{} (Axiom 8)
30: So {} cannot be an element of c (Property 1)
31: So c does not contain a finite number of elements (Claim 1)

32: But in order for the number of x such that x is an element of an element of X to be finite, then each element of X must have a finite number of elements. I have shown this to be not true, so the whole claim is false.

18: If there does exist such an n, there must be an m + 1 (m > 0) such that m + 1 is the smallest such n.

But what if smallest such n = 1?

29: {} is an element of b:{}
How so? {} can’t be an element of {} per axiom 9, so {} should be the element of b?..

ah fair point. For some reason I thought Axiom 8 allowed for equality to show that b:{}

Another comment: it took me a while to figure out how step 13 is sound. We know that a satisfies Property 1, and that a = {b} ++ c; thus, there is nothing that is an element both of {b} and of c; thus, since b is an element of {b}, b is not an element of c,

Which are what 11 and 12 state…

but yeah, given it isn’t actually true that the empty list is an element of every non-empty list like I thought it was, only question is going to be if you can make your proof rigorous enough for our liking. No way any of us are factoring that =)

Indeed: since I am the only person capable of factoring that number, it is likely that I am the only person providing a proof of this statement,

Unless it’s sufficient to say that there exist A>1 and B>1 such that AB equal that number:)

1: {} is a list
The following holds for any a:
2: a_1:{} is a list (Axiom 4)
3: a_1 is an element of a_1:{} (Axiom 8)
4: For all x, if x != a_1 then x is not an element of a_1:{} (Axiom 8)
5: a_2:a_1:{} is a list (Axiom 4)
6: a_2 is an element of a_2:a_1:{} as a_2 = a_2 (Axiom 8)
7: a_1 is an element of a_2:a_1:{} as a_1 is an element of a_1:{} (Step 3)
8: For all x, if (if x != a_1, a_2 then x is not an element of a_2:a_1:{}) (Axiom 8/Step 4)
9: a_3:a_2:a_1:{} is a list (Axiom 4)
10: a_3 is an element of a_3:a_2:a_1:{} as a_3 = a_3 (Axiom 8)
11: a_1 and a_2 are elements of a_3:a_2:a_1:{} as they are element of a_2:a_1:{} (Step 6/7)
12: For all x, if (if x != a_1, a_2 or a_3 then x is not an element of a_3:a_2:a_1:{}) (Axiom 8/Step 8)
13: It follows that a_3:a_2:a_1:{} has exactly three elements
14: The digit sum of 35 844 088 534 668 175 608 533 550 469 325 416 140 711 880 836 358 433 520 741 183 341 559 409 752 958 417 564 900 205 152 763 659 819 317 338 304 041 228 758 958 269 744 936 094 178 001 500 112 469 790 418 773 135 543 301 899 194 065 881 801 585 777 676 220 908 841 is 879
15: 897 / 3 = 293

16: If the digit sum of a number is divisible by 3, so is the number so 35 844 088 534 668 175 608 533 550 469 325 416 140 711 880 836 358 433 520 741 183 341 559 409 752 958 417 564 900 205 152 763 659 819 317 338 304 041 228 758 958 269 744 936 094 178 001 500 112 469 790 418 773 135 543 301 899 194 065 881 801 585 777 676 220 908 841 is divisible by three.

17: If X = {a_3:a_2:a_1:{}}:{} then a_3:a_2:a_1:{} is an element of X (Axiom 8)

18: There are 3 x s.t. x is an element of a_3:a_2:a_1:{}, so there are 3 x s.t. x is an element of an element of X (step 13)

19: Suppose there is an X s.t. the first seven properties hold, each element of X has 3 elements, and the number of x such that x is an element of an element of X is exactly 3 * n for some n.

20: Let a = a_3:a_2:a_1:{} where a_3, a_2, a_1 are not elements of any element of X, and none of which are equal to each other.

21: Let X’ = a:X

22: a_3, a_2, and a_1 are the only elements of a (Step 13)
23: If b is an element of an element of X’, and b is not a_3, a_2 or a_1 there some y which is an element of X such that b is an element of y
24: Such a b would have to be an element of an element of X
25: So there are 3n + 3 elements of X’
26: a is a list, and every element of X is a list, so every element of X’ is a list
27: For all elements a of X, if b and c are lists such that b ++ c = a, then there does not exist d such that d is an element of both b and c.
28: If b and c are lists such that b ++ c = a, then there does not exist d such that d is an element of both b and c.
29: For all elements a of X’, if b and c are lists such that b ++ c = a, then there does not exist d such that d is an element of both b and c.
30: For all pairs (a,b) of elements of X, there does not exist c such that c is an element of both a and b. (by assumption)
31: For all b elements of X, there does not exist c s.t. c is an element of both a and b (by assumption)
32: For all pairs (a,b) of elements of X’, there does not exist c such that c is an element of both a and b. (put the two together)
33: X has at least two elements, so X’ also does
34: Every elmenet of X’ still has three elements.
35: So there also exists a list X’ which has 3(n+1) x which are elements of elements of X’
36: By induction, for any positive integer y, there exists a list X for which all the properties hold and there are 3y values of x which are elements of elements of X
37: Specifically, because there is some y s.t. 3y = 35 844 088 534 668 175 608 533 550 469 325 416 140 711 880 836 358 433 520 741 183 341 559 409 752 958 417 564 900 205 152 763 659 819 317 338 304 041 228 758 958 269 744 936 094 178 001 500 112 469 790 418 773 135 543 301 899 194 065 881 801 585 777 676 220 908 841 there is some X for which the claim holds.

Or is a_2:a_1 an element of a_2:a_1:{}? In that case I guess you can just ignore the a_3s. But I can’t supply two proofs. Also yeah I handwaved a bit with If b and c are lists such that b ++ c = a, then there does not exist d such that d is an element of both b and c. because its obviously true but would’ve been annoying to prove.

Next time don’t pick a multiple of three Travos =)

By my count, the digit sum is actually 884, and so my number isn’t a multiple of 3 after all,

aw yeah it looks like when I copied it into my spreadsheet I trimmed off the last 41 (getting 879 not 897). Was wondering why you didn’t pick two primes…

still might be able to rules lawyer the whole a_2:a_1:{} has three elements bit =)

Wait, this statement is false.

Look at this criterion: “For all pairs (a,b) of elements of X, there does not exist c such that c is an element of both a and b.” Since X has at least two elements, there exists a pair (a,b) of elements of X with a = b. Since a has at least two elements, a is nonempty, so there is an element c of a. Since a = b, c is also an element of b. So the quoted criterion is false; no X satisfying these criteria exist.

I submit the following as my logical sequence of deductions that leads to the theorem in the Challenge Post from existing Truths:

1: All dogs are at least two miles wide.
2: There exists a wheelchair that is at least two miles wide.
3: Therefore, there exists a wheelchair that is a dog.

pairs aren’t distinct? I donno if anyone would’ve caught that.

still doesn’t clear up whether a_2:a_1 is an element of a_2:a_1:{}

No (unless a_2:a_1 is equal to a_2 or a_1). a_2:a_1:{} is a_2:(a_1:{}), so applying Axiom 8 a couple of times tells you that a_2:a_1 is an element of a_2:a_1:{} if and only if a_2:a_1 = a_2 or a_2:a_1 = a_1 or a_2:a_1 is an element of {}.

(a_1:{}) is not a list though. So how can a_2:(a_1:{}) be a list?

It would be rather silly if (a_2:a_1):{} is a list, and a_2:(a_1:{}) is a list, except you don’t write them with parenthesis so they are both written a_2:a_1:{} yet somehow aren’t equal because a_2:a_1 is only an element of (a_2:a_1):{}

{} is a list, so by Axiom 4, a_1:{} is a list. Certainly we should not write both (a_2:a_1):{} and a_2:(a_1:{}) as a_2:a_1:{}; I believe convention is that a_2:a_1:{} means a_2:(a_1:{}),

Oh, for what it’s worth, here’s the bit of the proof I’d typed up before I realized I’d made a mistake:

1. Let K_1 be the number [redacted].

2. Let K_2 be the number [redacted].

3. Let K_3 be the number 35 844 088 534 668 175 608 533 550 469 325 416 140 711 880 836 358 433 520 741 183 341 559 409 752 958 417 564 900 205 152 763 659 819 317 338 304 041 228 758 958 269 744 936 094 178 001 500 112 469 790 418 773 135 543 301 899 194 065 881 801 585 777 676 220 908 841.

4. Let N_0 be the empty list (or {}). Notice that N_0 has length 0.

5. For all n between 1 and (K_3)-1 inclusive, let N_n be {}:N_(n-1). Notice that if N_(n-1) has length n-1, then N_n has length n.

6. (from 4 and 5) By induction, we can conclude that for all n between 0 and (K_3)-1 inclusive, N_n has length n.

7. (from 6) Given two lists N_a and N_b for a not equal to b, the length of N_a is not equal to the length of N_b, so N_a is not equal to N_b.

8. K_1 * K_2 = K_3.

9. K_1 * K_2 - K_2 + K_2 - 1 = K_3 - 1.

10. (from 9) (K_1 - 1) * K_2 + K_2 - 1 = K_3 - 1.

11. 0 * K_2 + 0 = 0.

12. (from 10 and 11) For all i and j, if i is between 0 and (K_1)-1 inclusive, and j is between 0 and (K_2)-1 inclusive, then i*K_2 + j = k, for k between 0 and (K_3)-1 inclusive.

13. (from 12) For all i from 0 to (K_1)-1 inclusive, let L_i = {N_(i*K_2), N_(i*K_2 + 1), N_(i*K_2 + 2), N_(i*K_2 + 3), …, N_(i*K_2 + K_2 - 1)}.

14. (from 13) Let X = {L_0, L_1, L_2, L_3, …, L_(K_2 - 1)}.

15. (from 14) Every element of X is a list.

16. Suppose a is an element of X, and b and c are lists such that b ++ c = a.

17. (from 7, 13, and 14) Since, for all N_x in b and N_y in c, x < y, b and c have no elements in common.

18. Suppose a and b are elements of X, and a’ and b’ are elements of a and b, respectively.

But (a_2:a_1):{} (no parens) is legally a list. Given they are both written the same, I don’t get how we can argue that the lists are different.

What I’m saying is that they *aren’t* written the same; a_2:a_1:{} is not a valid way of writing (a_2:a_1):{}.

Why not? The rules don’t say “For all a, if b is a list then (a):b is a list”

Also

Well, they do say that a Formula must be unambiguous.

Per the newly enacted “They may also use the AGAINST marker if they believe any of the logical sequence of deductions (or group of deductions) used would be unreasonable for someone to figure out on their own.”

And resolving the post, with AGAINST in the lead three-to-aught, noone gets any challenge points. This Challenge Post is now in the Closed Phase.