Awoke again this morning at 8ish mentally going over what I was planning to tell Frank about this "classically true" modality, how I was disappointed that it doesn't seem to actually pin down which connectives correspond across the intuitionistic/classical boundary. Then I randomly got out a sheet of paper to see which of ~CA and C~A implied each other. To my great surprise, they turned out to be equivalent, along with the equivalences C(A & B) = CA & CB and C(A => B) = CA => CB. So I guess C being a homorphism across a connective is a good condition to require that the classical and intuitionist rules for a connective mesh right. Still it would have been nicer to have it expressed by one of the cut eliminations.
Awoke again this morning at 8ish mentally going over what I was planning to tell Frank about this "classically true" modality, how I was disappointed that it doesn't seem to actually pin down which connectives correspond across the intuitionistic/classical boundary. Then I randomly got out a sheet of paper to see which of ~CA and C~A implied each other. To my great surprise, they turned out to be equivalent, along with the equivalences C(A & B) = CA & CB and C(A => B) = CA => CB. So I guess C being a homorphism across a connective is a good condition to require that the classical and intuitionist rules for a connective mesh right. Still it would have been nicer to have it expressed by one of the cut eliminations.
- Post a new comment
- 5 comments
- Post a new comment
- 5 comments
