Does this symbolic logic proof work?

Question

So, I have this proof:

Let a be an open sentential variable. Let K and C be prepositional variables asserted of sentences.

Given

1. K(a) <=> C(a) & a
2. C(a) <=> C( C(a))
3. C(a & b) <=> C(a) & C(b)

If

4. K(a)

Then

5. C(a) & a //by 1,4
6. C( C(a)) //by 2,5
7. C( C(a)) & C(a) //by 5,6
8. C( C(a) & a) //by 3,7
9. C( K(a)) //by 1,8
10. C( K(a)) & K(a) //by 4,9
11. K( K(a)) //by 1,10

Thus

12. K(a) -> K( K(a))
13. K( K(a)) -> K(a) //by 1

And so

14. K(a) <=> K( K(a)) //by 12,13

QED

Can anyone see any issues with this? The thing that I'm least sure about is the use of recursive.

Thanks

Answer 1

It is correct, but you've skipped over some steps, which obsured your reasoning.

For instance step 13. You just say K(K(a)) → K(a) by 1. Why?

Well, indeed, applying 1 gives you K(K(a)) ↔ C(K(a)) & K(a) and you can obtain the desired result from that, but you should spell this out. Show your working more.