1. ## formal systems help!

I think I am really confusing myself with this problem. Here it is:

The formal system A consists of:
alphabet: 0 /
axiom: 0
inference rule: if x is a A-theorem, then so is x/

It asks for me to state a few theorems of this system. Am I right in thinking that 0/, 00/, 000/, 000//, 00// could all be examples of theorems?

It continues: Using the theorems of the A-system, we define a new B-system which consists of:
alphabet: 0,/,[,],>
axiom: Any A-theorem
inference rule: if x and y are B-theorems, then so is [x>y]

It asks again to state a few theorems of this system. Could some examples be [0/>00/], [00//>000/], [0/>0/]

Any help is really appreciated!

2. ## Re: formal systems help!

Originally Posted by samantha12
Am I right in thinking that 0/, 00/, 000/, 000//, 00// could all be examples of theorems?
No, the inference rule only allows adding /, not 0. So, theorems are 0, 0/, 0//, 0///, etc.

Originally Posted by samantha12
It continues: Using the theorems of the A-system, we define a new B-system which consists of:
alphabet: 0,/,[,],>
axiom: Any A-theorem
inference rule: if x and y are B-theorems, then so is [x>y]

It asks again to state a few theorems of this system. Could some examples be [0/>00/], [00//>000/], [0/>0/]
If you keep just one zero on each side of >, then these are theorems. A more interesting example is [[[0/>0//]>[0>0]]>0///].

3. ## Re: formal systems help!

Originally Posted by emakarov
No, the inference rule only allows adding /, not 0. So, theorems are 0, 0/, 0//, 0///, etc.

If you keep just one zero on each side of >, then these are theorems. A more interesting example is [[[0/>0//]>[0>0]]>0///].
Thank you very much! I'm confused as to how you knew that you could only add /s, because the x is not defined? And in the second example again how you knew the definition of x and y?

4. ## Re: formal systems help!

Originally Posted by samantha12
I'm confused as to how you knew that you could only add /s, because the x is not defined?
inference rule: if x is a A-theorem, then so is x/
The rule says that if one starts from x, one can only add / to it.

And in the second example again how you knew the definition of x and y?
One proves the following theorems in sequence. I'll write the corresponding values of x and y from the rule next to the theorem provided it is not an axiom of the second system (i.e., a theorem of the first system).

Code:
#1. 0/				Axiom
#2. 0//				Axiom
#3. [0/>0//]			x = 0/ (#1), y = 0// (#2)
#4. 0				Axiom
#5. [0>0]			x = 0 (#4), y = 0 (#4)
#6. [[0/>0//]>[0>0]]		x = [0/>0//] (#3), y = [0>0] (#5)
#7. 0///			Axiom
#8. [[[0/>0//]>[0>0]]>0///]	x = [[0/>0//]>[0>0]] (#6), y = 0/// (#7)

5. ## Re: formal systems help!

Everything just clicked, thank you so much!