"What is it exactly that you don't know, again?  Try to tell me out loud what it is that you want to do and can't see any way to do."

"I want to say 'here's what it is to add one to something', using just and, and not, and implies, and for all. And you can go 'for all numbers, this number plus one equals....something, but I don't know how to say what the something is."

"Hint desired or undesired?"

What kind of fucking question is that.

Maybe he's just very sadistic and this is all an elaborate game he is playing with them. 

"I think I might need one," she says very lightly.

"If you take the hint now, you'll never know whether or not you needed a hint or just more time... but we're trying to industrialize a planet and that's probably more important than you ever knowing whether you could have punched above your measured intelligence level and discovered the deeper orders of Validity from scratch, so, yeah, hint.  You cannot build 'add one' out of only and, not, implies, for all.  I previously showed you a system that had predicates like 'blue' and 'red', which took in the kind of object that 'forall' quantifies over, and spat out truth or falsehood depending on whether the object was red or not.  There's no way to build 'add one' out of only those materials, because 'add one' takes in an object, a number, and spits out another object."

"This doesn't mean your system has to start out knowing what add-one means.  It does mean that you're going to have to conjure up an add-one symbol that maps objects to objects, and then start describing what it means.  But that description needs to talk about add-one as a hypothetical function whose properties will be described, not build it purely out of the predicate symbols and logical connectors.  You are also going to need a symbol '=' for equality between two objects; that one is usually assumed primitive - that even if the system starts out knowing nothing else about the objects it describes, it knows how to tell when two objects are equal.  '=' takes in two objects, and spits out truth or falsehood."

"There's a more sophisticated trick you can pull to not need to introduce a special symbol for add-one - roughly, you say, for all functions from objects to objects, if that function has these properties, this stuff follows - but that would involve quantifying over functions, which we can skip for now.  So, to reiterate:  You get to conjure the symbol for add-one from nowhere; you get to declare by fiat and premise that it takes in an object and spits out an object; you don't, however, get to assume that it has any behaviors beyond that, or means anything in particular, except for whatever statements you make using the add-one symbol.  Same for two-object functions like add, or multiply.  You can declare that there's a plus symbol, and that it takes in two objects and spits out a third object, but anything about which objects has to be described by you, and that's what makes the symbols meaningful."

"Okay," she says shakily. "....I think I need time to think -"

"Anyone else want to try what she tried doing, at all?  Trying something and failing is more impressive than not trying at all."

Carissa is too busy worrying about whether things can be both true and heretical to pay this the amount of concentrated attention it clearly deserves, but "I think you want to start by saying what zero is, and what one is? I'm not sure what that is, mind - I was thinking maybe zero is 'for all things, not that thing", but that doesn't seem quite right."

"Well, indeed.  If it was the case that no object was zero, there wouldn't be a number called that.  What does make zero special, among the numbers?  If you have any ideas here, say them informally first; saying it formally is usually harder, and it's usually wiser to solve the easy problems before you tackle the hard ones."

"Well, it's what you get if you take a away from a, for any a."

"Can you say that formally?"

"I don't see how to until we have defined addition or subtraction, which is the thing we were trying to do. The thing I'd say is \k, k+ 0 = k, but I don't think that's meaningful if I haven't said what plus is yet."

"Remember how we managed to build 'or' out of 'implies' and 'not'?  And that wasn't even set up on purpose by anyone or anything, it's just the human mind being thrown together by a design process that included more structure than the strict minimum?  Each time you say something like '\k. k + 0 = k', you constrain the meaning that + and 0 can have.  Imagine looking at these blue circles, each a possible world; imagine that instead of colored shapes inside them, there are objects that might be numbers, a function that might be plus.  Every time you make another statement like '\k. k + 0 = k', you kick out some of the worlds and mappings where the function you mapped onto '+' and the object you mapped onto '0' didn't always eat an object and 0 and spit that same object back out again.  Make enough statements like that, and maybe you can narrow down the possible worlds to ones that only contain objects that look like the numbers you know?  That, from a certain perspective, is what it means to define numbers and arithmetic - to find statements such that anything they are true about must be numbers and arithmetic.  Got any more statements like it?  Somebody wipe this wall, please, we'll want to start writing down the statements like forall k, k plus 0 equals k."

" - oh." She thinks of it before he's halfway done. "Zero is the only number where zero plus zero equals zero. - I said that poorly, but -"

"By all means say it better then."

"0 + 0 = 0.  \k, k = ~0 -> k + k ~= k."

"Progress.  But '~0' isn't a thing in this language, 'not' takes in propositions, which have the values of truth or falsehood, and spits out falsehood or truth.  'Not four' isn't a number - or if you wanted it to talk about the collection of all numbers except four, we'd have to start introducing collections and that's a big ol' subject.  ~= isn't already a symbol in our language either, and in fact you don't particularly need to define a new symbol for it.  Next rewrite?" 

\k, (k = 0 /\ k + k =k) \/ ~(k + k = k) 

She writes this rather than saying it, because it seems like it'd be quite unpleasant to say and harder to tweak while speaking. She writes it with Prestidigitation because she has better control and precision than a student and they ought to remember it.

"Good try, but your statement doesn't quite narrow down the possible worlds to where you wanted - it includes worlds where ~(k + k = k) is true of every number, including the one you called zero.  Can anyone see how to fix it?"

"Can't you just add ~(k=0) to the second part?"

"Works unless I've missed something myself, but do you want to write out exactly what you mean there, to make sure it's not just my own imagination supplying the answer I think is correct?"

\k, (k = 0 /\ k + k =k) \/ ~(k=0) /\ ~(k + k = k) 

He supposes it's good that people are finding so many detailed ways to be wrong, exhibiting them early and getting them out of the way.

"We haven't said anything about adding - outside the system, up at our level - rules for adding in parentheses that weren't in the written formula.  So that could mean either of -"

\k. ((k=0 /\ k + k = k) \/ ~(k=0)) /\ ~(k + k = k)
\k. (k=0 /\ k + k = k) \/ (~(k=0) /\ ~(k + k = k))

"Second one," the girl says.

"Then it looks good to me.  Keeping in mind that these don't exactly match standard forms I learned, since we're making them up as we go, and my own intelligence is not at the level where I will reliably spot errors on the first pass.  I'm not sure quite why I feel the need to say this - it seems like the sort of thing that should be obvious? - but if I'm the one who makes an error, or it just looks like that, speak up.  If you're right, you get to be impressive, and if you're wrong, you need to know which mistake you made."

Keltham keeps prodding the group for a while, dropping hints as needed, until he's pretty sure they've written enough random rules to yield in their combination all the constraints of first-order arithmetic except for the induction axiom schema.  If anybody from Cheliax brilliantly pulls the induction axiom schema out of their ass, he's going to be sure they're getting it from somewhere; maybe dath ilani geniuses can pull that kind of shit at their age (he doubts it), but the geniuses of this world are only as smart as him unless they're wearing intelligence headbands.