roam
Aug2-11, 08:03 AM
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 AB3.
Rules of inference:
From x infer xAB3
For example, A2B6 is a theorem. To see this, we can provide the following derivation:
1. AB3 (Axiom)
2. AB3AB3 = A2B6 (From 1 by rule 2)
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 AB3.
Rules of inference:
From x infer xAB3
For example, A2B6 is a theorem. To see this, we can provide the following derivation:
1. AB3 (Axiom)
2. AB3AB3 = A2B6 (From 1 by rule 2)
So, is my system correct? Are there better ways to make the rules as simple as possible?