1. Post production system

Here's my question:

Attempt:

So the set of theorems is $\{ B^j A^i \ : \ i \equiv 0 \mod 3\}$.

• The only axiom is $B$.

• The alphabet is $\{ A, B \}$

• Rules of inference (here $x$ and $y$ represent any string, possibly empty, of symbols from the alphabet):
1. From $x$ infer $xAAA$
2. From xyx infer xBx
For example $B^2A^6$ is a theorem of this system. To see this, we provide the following derivation:

1. $B$ (Axiom)
2. $BAAA$ (From 1 by rule 1)
3. $BAAAAAA$ (From 2 by rule 1)
4. $BBAAAAAA = B^2A^6$ (From 3 by rule 2)

Is this correct?

2. Re: Post production system

1. Could you give a link to a definition of the Post production system? Does Post canonical system sound similar?

2. Is the empty string a wff and theorem? If so, then it should probably be the axiom.

3. I don't see where the problem statement says that all A's must follow B's.

3. Re: Post production system

Originally Posted by emakarov
1. Could you give a link to a definition of the Post production system? Does Post canonical system sound similar?
Here is a link to the definition:

http://img535.imageshack.us/img535/2...production.jpg

3. I don't see where the problem statement says that all A's must follow B's.
No, it doesn't say. That's why I'm a bit confused about what notation to use. It could be

$\{ B^j A^i \equiv 0 \mod 3 \}$ or $\{ A^i \ B^j \equiv 0 \mod 3 \}$.

Which one should I use?

2. Is the empty string a wff and theorem? If so, then it should probably be the axiom.
Yes, for i=j=0, we have 1. So the empty string is a theorem.

4. Re: Post production system

Originally Posted by emakarov
2. Is the empty string a wff and theorem? If so, then it should probably be the axiom.
It is a theorem but I don't think the empty string is a well-formed formula (with strings from the given alphabet, in this case {A,B}). Isn't it?

But for this problem can't we take the axiom to be $A^3B$. And use only one rule of inference:

1. From $A^3xyB$ infer $A^3A^3xyBB$.

And since all of the theorems are of the form $A^{3n}B^n$, the can be derived using that rule. Right?

5. Re: Post production system

Here is a link to the definition:

http://img535.imageshack.us/img535/2...production.jpg
Thanks. One still needs to know the possible shape of inference rules. If rules can be arbitrary, then we could have an empty string (or B) as an axiom and just one inference rule: from the empty string derive any string that has the number of A's that is divisible by 3. Alternatively, consider the same axiom and two rules: given a string, insert a B in an arbitrary place, and given a string, insert 3 A's in arbitrary places. The problem does ask for simple rules, but "simple" is a little ambiguous.

Originally Posted by demode
It is a theorem but I don't think the empty string is a well-formed formula (with strings from the given alphabet, in this case {A,B}). Isn't it?
All theorems are wffs by definition, so the empty string can't be a theorem and not a wff. It's a question of definition, not mathematics: either you are considering all strings or only nonempty ones.

But for this problem can't we take the axiom to be $A^3B$. And use only one rule of inference:

1. From $A^3xyB$ infer $A^3A^3xyBB$.

And since all of the theorems are of the form $A^{3n}B^n$, the can be derived using that rule. Right?
I don't think you can derive $A^6B$. I am wondering if the original problem requires all, or only some, strings where the number of A's is divisible by 3 to be theorems (presumable, all). More importantly, ABABA should also be a theorem.