Just to give you some (very late) clarification: The theory I describe above (a first order theory) can handle statements perfectly well, it just represents them as strings, rather than giving them their own separate type. The problem isn’t inherently with giving them their own separate type though, it’s with expecting to be able to just stick a member of that type in our expression where we’re supposed to expect a truth value.
You can skip past my proof and its messy programming notation, and just look here.
Just to give you some (very late) clarification: The theory I describe above (a first order theory) can handle statements perfectly well, it just represents them as strings, rather than giving them their own separate type. The problem isn’t inherently with giving them their own separate type though, it’s with expecting to be able to just stick a member of that type in our expression where we’re supposed to expect a truth value.
You can skip past my proof and its messy programming notation, and just look here.