The well-formed formulas of a propositional or predicate calculus can get recursively generated.  All well-formed formulas of a propositional calculus have a length which we can use a natural number to measure.  All natural numbers that we know of belong to a finite set.  There exists a countable infinity of natural numbers all of which are greater than any natural numbers we know.  Similarly, there exists a countable infinity of tautologies longer than the complete set of known tautologies (all known and knowable tautologies are short). 

No claim or conjecture is a theorem until proven.  Every proof is finite, and thus no claim or conjecture becomes a theorem without adequate physical objects, or communication, to prove the conjecture.  The number of possible physical objects in existence is finite.  Thus, there do not exist enough materials, nor will there ever exist enough materials to prove all tautologies.

But there exist tautologies which require more materials to prove than is possible.  Thus, not every tautology can become a theorem.

Therefore, all claims of completeness are incorrect.

But, if a claim that some well-formed formula is a tautology needs to get validated in order for that well-formed formula to qualify as a tautology, then the number of tautologies is also finite.  Since generating theorems by various techniques, including by theorem provers, seems to overwhelmingly produce more well-formed formulas which are theorems than validating processes seem to produce tautologies, that implies that either there exists some small set of tautologies which have not gotten validated, or completeness claims are likely correct.

Larry Wos's Recent Newsletter

In the most recent newsletter of the Association for Automated Reasoning, Dr. Larry Wos presents us with a collection of axioms, with labels for them.
" f(e,x) = x. % left identity

 f(x,e) = x. % right identity
 f(g(x),x) = e. % left inverse
 f(x,g(x)) = e. % right inverse
 f(f(x,y),z) = f(x,f(y,z)). % associativity
 h(x,y) = f(x,f(y,f(g(x),g(y)))). % definition of commutator"

I'll call the relevant set of axioms G.

Then he presents three properties:

"h(h(x,y),z = h(x,h(y,z)), commutator is associative, property 1
f(h(x,y),z) = f(z,h(x,y)), commutator has the property of nilpotent class 2, 

property 3
f(h(x,z),h(y,z)) = h(f(x,y),z), commutator distributes over product, property 2"

He then asks us prove that property 1 follows from property 2, property 1 from 3,
2 from 1, 2 from 3, 3 from 1, and 3 from 2.

And then a careful reader is either confused or laughing, 
since if your only axiom has only one function like 'h', 
it's impossible to correctly get to a property with a function like 'f' 
(or I don't understand the term 'property' correctly). 

What I suspect Dr. Wos means to ask is about relationships between theories.

The theories are G supplemented with property 1 (G1), 
G supplemented with property 2 (G2), and G supplemented with property 3 (G3).

Thus, more precisely, Dr. Wos's first challenge is to prove that G2 follows from G3,
G2 from G1, G1 from G3, G1 from G2, G3 from G2, and G3 from G1.

Edit: That's not the intended challenge either.

Property 1 should be h(h(x,y),z) = h(x,h(y,z)). or h(h(x,y),z) = h(x,h(y,z)), .  
Also, the termination symbol for the supplementary axioms need to match those in G 
(the commas need to get replaced by periods 
or the periods have to get replaced by commas).

If anything is incorrect in the above, hopefully it gets corrected.
    

The Decline of Eve Camps on BigServer2 And More

The same four families have apparently lived on bigserver2 since the latest change on Friday (see edit below).  There's an essay on the One Hour One Life forums called "On The Decline of Eve Camps" (or something similar).  Basically, I suspect that families move more and more in the direction of civilization maintenance as time passes.  Will things change at some point and families migrate?

My understanding that One Hour One Life comes as intended as a game where every life feels unique.  Or at least many of those lives that one plays.  But does this happen with the same four families alive?

Is it a good sign when civilization building declines so much that civilization maintenance becomes far more prominent?

Informed players can use the custom server box in the settings tab to select a server like 'server4.onehouronelife.com' (2-15 are the other numbers for those servers) to have a greater probability of playing in an Eve camp or as an Eve out in the wild.  But, often times players on those servers get no children, or no grandchildren, and lineages usually are rather short.

A similar pattern of falling into a cycle of civilization maintenance happened during many periods of The Rift as I understand it.

Why is there so little between the bigserver2 context and the context of servers 2 through 15?  Why does this game tend to extremes like that?

Does there exist enough variety in all of this?

Edit: There did exist a new family, the Meagles on bs2 who came into existence on Monday morning. I've also changed the title to the decline of Eve camps from 'No More Eve Camps'.

Re-Direction Process Dooming Lineages And Making Children Unavailable

The server system splits players not checking a custom server from bs2 to "bs2 and s1" or {bs2, s1} when the population gets high enough for load balancing purposes.  Usually, it has happened that when the player population declines enough, players just get directed back to bs2.  Then there exist no children for the remaining players on s1, which implies the doom of lineages.

Families apparently doomed by this process:

1: The Gemzas

(this lineage might not be on s1)

2:  The Corals

3: The Gardners


4: The Berrys

The servers split a second time again and s1 had these families:

5: Eve Judisch and her descendants

6: The Zaagmans

7: The Aas

8: The Fos

9: The Emms

Incoming players not checking a custom server got split again on Sunday:

10: The Fars

11: The Daes

12: The Edas

13: The Pococks

Does Jason Want In-Game Issues Reported Or Was His Stickied Post About Something Else?

I used a random number generator to select the server I would play on, with 0 for bigserver2 and 1-15 for the rest of the servers.  I didn't look at the reflector either.

The game is intended of one parenting.  I didn't get any children for the server I ended up on.  Nor did I meet anyone who was parenting.

Doesn't that mean we have a serious issue and one that has to happen every week to players when 'children of men' mode is active on bigserver2 and then server1 during the update period, and also when load balancing shifts people not checking a custom server around?

Here's my report:

Jason rejected it as an issue.  So, does Jason want in-game issues reported or not?

More doomed lineages.  This continues on a post of mine from the OHOL forums (given that such a post still exists).

1: The Groots: http://lineage.onehouronelife.com/server.php?action=character_page&id=5807110&rel_id=5807978

2: The Samanthas: http://lineage.onehouronelife.com/server.php?action=character_page&id=5807975

3: The Kilars: http://lineage.onehouronelife.com/server.php?action=character_page&id=5806763&rel_id=5806763

4: The Naitos: http://lineage.onehouronelife.com/server.php?action=character_page&id=5807848&rel_id=5807970

5: The Cooks: http://lineage.onehouronelife.com/server.php?action=character_page&id=5807301&rel_id=5807966

The longest lineage which happened all week was the Cocks, which I think happened after the latest update: http://lineage.onehouronelife.com/server.php?action=character_page&id=5774696&rel_id=5774696

6: The Dragons: http://lineage.onehouronelife.com/server.php?action=character_page&id=5808517

7: A nameless lineage: http://lineage.onehouronelife.com/server.php?action=character_page&id=5808531

8: The Dobbies: http://lineage.onehouronelife.com/server.php?action=character_page&id=5808820&rel_id=5808934

9: The Adams: http://lineage.onehouronelife.com/server.php?action=character_page&id=5808947

10: The Blacks: http://lineage.onehouronelife.com/server.php?action=character_page&id=5808946

11: The Loves: http://lineage.onehouronelife.com/server.php?action=character_page&id=5810387

12: The Kims: http://lineage.onehouronelife.com/server.php?action=character_page&id=5810377

13: The Dragons: http://lineage.onehouronelife.com/server.php?action=character_page&id=5810393

14: The Brownies: http://lineage.onehouronelife.com/server.php?action=character_page&id=5811765

15: The Kings: http://lineage.onehouronelife.com/server.php?action=character_page&id=5811754

16: The Zacariases: http://lineage.onehouronelife.com/server.php?action=character_page&id=5811198&rel_id=5811198

17: The Aplfelbaums: http://lineage.onehouronelife.com/server.php?action=character_page&id=5812232

18: The Matiles: http://lineage.onehouronelife.com/server.php?action=character_page&id=5812282

19: The Winters: http://lineage.onehouronelife.com/server.php?action=character_page&id=5812288

20: The Stellas: http://lineage.onehouronelife.com/server.php?action=character_page&id=5812380

21: The Overlocks: http://lineage.onehouronelife.com/server.php?action=character_page&id=5812581

One of the axiom sets for two-valued propositional calculus got discovered by Wajsberg, which with some letter substitution would become as follows:

A1: CxCyx

A2: CCxCyzCCxyCxz

A3W: CCCx00x

It turns out that A3W consists of a special case in that a more general tautology A3 can get formulated in the sense that we can obtain A3W by uniform substitution from A3, but we cannot obtain A3 by uniform substitution from A3W.  A3 is as follows:

A3: CCCxy0x

The notation of a letter or constant on the left side of a '/' with a letter or constant on the blank indicates that we will substitute whatever lies on the left with whatever lies on the right.

To check the soundness of A3 we can set up the following equations:

C00 = 1, C10 = 0, C01 = 1, C11 = 1.

A3 x/0 y/0 yields CCC0000.  So, CCC0000 = CC100 = C00 = 1.

A3 x/0 y/1 yields CCC0100.  So, CCC0100 = CC100 = C00 = 1.

A3 x/1 y/0 yields CCC1001.  So, CCC1001 = CC001 = C11 = 1.

A4 x/1 y/1 yields CCC1101.  So, CCC1101 = CC101 = C01 = 1.

Consequently, CCCxy0x is a tautology.

Now we substitute y with 0 in A3 obtaining CCCx00x.

Therefore, since the above axiom set of Wajsberg consists of an axiom set for C-0 propositional calculus, it follows that {CxCyx, CCxCyzCCxyCxz, CCCxy0x} makes for an axiom set for C-0 propositional calculus under the rules of uniform substitution and detachment.

The author wants to note that N1: {CxCyx, CCxCyzCCxyCxz, CNCxyx} is not a basis for C-N propositional calculus.  To see this we only need to check that if we define N as follows N0 = 0, and N1 = 0, and define C as how it usually gets defined propositional calculi, then CNCxyx = 1.  But, the law of Clavius CCNxxx, with x/0 becomes CCN000, and

CCN000 = CC000= C10 = 0.  Thus, the law of Clavius is not derivable in system N1 under uniform substitution and detachment.