Is This Post Production System Correct for Generating Theorems?

[roam]

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 $\{A^nB^{3n} : n\geq 1\}$. Would it the following system be correct:

• Alphabet is {A,B}

• The only Axiom is AB³.

• Rules of inference:

1. From x infer xAB³

For example, A²B⁶ is a theorem. To see this, we can provide the following derivation:

1. AB³ (Axiom)
2. AB³AB³ = A²B⁶ (From 1 by rule 2)

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

 

[Valkarie]

Yes, your system is correct. The rules you have provided are sufficient for the set of theorems given. However, if you want to make the rules simpler, you could use an induction proof instead. For example, if we can show that A^(n+1)B^(3n+3) is true for some n, then it must be true for all n >= 1. Therefore, we can prove that A^nB^(3n) is true for all n >= 1 by proving that A^2B^6 is true, and then showing that if A^nB^(3n) is true, then A^(n+1)B^(3n+3) must also be true.