- #1

- 1,266

- 11

## Main Question or Discussion Point

I want to write a Post production system if we have the set of symbols {A,B} where all strings are wffs, and the set of theorems is [itex]\{A^nB^{3n} : n\geq 1\}[/itex]. Would it the following system be correct:

For example, A

1. AB

2. AB

So, is my system correct? Are there better ways to make the rules as simple as possible?

- Alphabet is {A,B}

- The only Axiom is AB
^{3}.

- Rules of inference:

- From x infer xAB
^{3}

For example, A

^{2}B^{6}is a theorem. To see this, we can provide the following derivation:1. AB

^{3}(Axiom)2. AB

^{3}AB^{3}= A^{2}B^{6}(From 1 by rule 2)So, is my system correct? Are there better ways to make the rules as simple as possible?