2 deleted 1 character in body

In the intuitionistic natural deduction (NJ) we have a nice symmetry : each logical connective havehas an introduction rule and an elimination rule.

But when we want to switch to classical logic (NK) we have to add some rules to be able to prove classical properties like the Peirce Law, the excluded middle and such. Therefore, we break the symmetry we had.

Why is it an interesting thing to state ? Is there something wrong with that ?

Maybe it has something to do with proof normalization or another technical detail ?

In the intuitionistic natural deduction (NJ) we have a nice symmetry : each logical connective have an introduction rule and an elimination rule.

But when we want to switch to classical logic (NK) we have to add some rules to be able to prove classical properties like the Peirce Law, the excluded middle and such. Therefore, we break the symmetry we had.

Why is it an interesting thing to state ? Is there something wrong with that ?

Maybe it has something to do with proof normalization or another technical detail ?

In the intuitionistic natural deduction (NJ) we have a nice symmetry : each logical connective has an introduction rule and an elimination rule.

But when we want to switch to classical logic (NK) we have to add some rules to be able to prove classical properties like the Peirce Law, the excluded middle and such. Therefore, we break the symmetry we had.

Why is it an interesting thing to state ? Is there something wrong with that ?

Maybe it has something to do with proof normalization or another technical detail ?

1

# Is there something wrong in breaking the symmetry of Natural Deduction?

In the intuitionistic natural deduction (NJ) we have a nice symmetry : each logical connective have an introduction rule and an elimination rule.

But when we want to switch to classical logic (NK) we have to add some rules to be able to prove classical properties like the Peirce Law, the excluded middle and such. Therefore, we break the symmetry we had.

Why is it an interesting thing to state ? Is there something wrong with that ?

Maybe it has something to do with proof normalization or another technical detail ?