search

bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 1: consistency and completeness #15

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

This is a pretty minor issue and fully hashing it out may not be worth the time, but I think there's a subtle detail that is glossed over in the definitions of "consistent" and "complete" for formal systems, having to do with the interpretation of the word "true".

In a formal system it doesn't really make sense to say that a given statement is "true", at least not in the way people usually think of that word. The best a formal system can do by itself is say that a statement is "provable" -- follows from the inference rules. We can think of this as syntactic truth. Then we can take a particular model of the formal system -- a thing where the formal system has a concrete interpretation -- and ask whether some statements are true about the model. If it's a bona fide model, then every provable statement should be true. But there may be true statements in that model that aren't provable in the formal system.

This gets sticky in the definition of incomplete:

"the system is incomplete if there are statements that are true but which cannot be proved to be true inside that system."

The problem is: what does it mean to say that a statement in a formal system is true? There are two concepts at play here: a statement can be (1) derivable from the inference rules (syntactically true), or it can be (2) true in every possible interpretation of the formal system (semantically true). Consistency means that we can't prove a statement that turns out to be false in some model. Completeness means that if a statement is true in every model, then we can find a proof for it.

Fully fleshing out the distinction between the two would probably require talking about models, and that's it's own can of worms.

But here's the thing - and this is a pedagogical opinion that you're free to disregard - I'm not sure that it's necessary to understand consistency and completeness in order to use formal logic to do useful work. In practice we use well studied formal systems where these issues have been fleshed out already and the dragons tamed; we choose consistency, and incompleteness doesn't really present any problems.

I haven't gotten into the later chapters, but if consistency/completeness is not used again, I would think about leaving it out.

bor0 commented 6 years ago

I see your point. It may turn out that this is a distraction and that it can just go to the footnotes. I'll double-check, thanks!

bor0 commented 6 years ago

We mention completeness/consistency in 2.1.3. I think it's worth just briefly mentioning it in chapter 1, so that readers are at least aware of it. Let's leave it at that, or feel free to file a PR for a future release.