User:IssaRice/Computability and logic/Some important distinctions and equivalences in introductory mathematical logic
This page lists some important distinctions in introductory mathematical logic and computability theory. Bizarrely, most books won't even mention these distinctions, so you will probably be very confused at the start as you inevitably conflate these ideas.
This page is kind of a "list of things I wish someone told me" as I was learning basic logic. It's not intended as a standalone introduction to mathematical logic, but rather a supplement to more standard resources.
For the LessWrong audience: (1) there have been a number of posts on mathematical logic before; (2) some folks are studying this material in preparation for doing AI alignment research; (3) making distinctions between concepts that seem similar at first seems like a useful rationality skill [1] [2].
Completeness
The term "complete" can apply to a logic, in which case it is also called "semantically complete". If a logic is semantically complete, it means that if a set of sentences semantically implies a sentence (i.e. every interpretation that makes every sentence in true also makes true), then it is possible to prove using as the set of assumptions. This meaning of completeness is the topic of Gödel's completeness theorem. In addition, this form of completeness can be stated in another way by saying that any consistent set of sentences is satisfiable (has a model); some proofs of Gödel's completeness theorem use this formulation.
The term "complete" can also apply to a theory, in which case it is also called "negation-complete". If a theory is negation-complete, it means that for every sentence , the theory proves either or (if it proves both, it is still negation-complete, but it is also inconsistent, so is not an interesting theory). This meaning of completeness is the topic of Gödel's first incompleteness theorem (which states that certain theories of interest are not negation-complete).
These two ideas are actually related. See Peter Smith's footnote on this.
The lesson with completeness is to always be sure what kind of object it is being applied to.
Soundness
soundness: sound logic (soundness theorem) vs sound theory. soundness of logic is about truth in all interpretations, while soundness of theory is about truth in a specific interpretation. unless the axioms of a theory are just valid sentences (in which case, the axioms are not really adding anything beyond what the logic already has, assuming the logic is complete), the axioms of a theory will in general be false in some interpretations -- this is what makes theories interesting, because they have non-logical content.
Truth in intended interpretation vs truth in all interpretations
Let be a predicate, and let be a constant. Is the sentence true? You would rightly say that the truth depends on what meanings we gave to the predicate and the constant. What about the sentence ? Now we might be tempted to say that this sentence is true. Someone might say "But you don't even know what and mean! How can you know if it's true or not?" One might respond that no matter what meanings we gave to and , the sentence would come out true. In other words, there is no way to assign meanings to and that would make the sentence false.
truth in all interpretations (validity) vs truth in the intended interpretation (natural reading, standard interpretation): see User:IssaRice/Computability and logic/Intended interpretation versus all interpretations
The models symbol
The models symbol, , comes up a lot in logic. But its meaning can be quite different depending on how it is used.
The two basic variations are:
- When a set of sentences comes before the symbol, like in . In this case, we are talking about the truth in all interpretations.
- When a structure comes before the symbol, like in . In this case, we are talking about the truth in just that one structure.
Syntax vs semantics
I have a rough draft quiz about this that I should post. Also see [1]
- "proves" vs "semantically implies" (absence of counterexample)
In computability theory, "syntax" corresponds to algorithms and "semantics" corresponds to functions computable via algorithms. See Rice's theorem, where this distinction becomes especially important.
Sentence vs wff vs formula vs closed formula
Enumerating vs computably enumerating vs primitive-recursively enumerating
First of all, there's a lot of terms that mean the same thing, so to clarify: "computably enumerable" means "recursively enumerable" means "effectively enumerable" (although the last one might be used as the informal counterpart).
Let be a set of natural numbers. We might say that enumerates iff is surjective. Why? because we can list out the elements of as follows: . Since is surjective, every element of will show up in this list at some point, i.e. we have "enumerated" the elements of . Call a set enumerable if there is a function that enumerates it. For those who have studied countability/uncountability, the definition of "enumerable" given here is the same as "at most countable".
The idea in computability theory is that we don't want just any enumeration. Since we are studying computable functions, we want to restrict our attention to computable enumerations. This leads to the idea of computably enumerable sets.
Given that primitive recursive functions are a strictly smaller class compared to partial recursive functions, one might suspect that sets which can be enumerated by primitive recursive functions are also a smaller class compared to sets which can be enumerated by partial recursive functions. To put it another way, suppose that a set is primitive-recursively enumerable. Then we have some primitive recursive function that enumerates it. But primitive recursive functions are recursive, so is recursive. Thus the set is recursively enumerable. That's one way, but it's not obvious whether the converse holds. It turns out that the converse does hold.
NOTE: in Solomonoff induction and related areas there is a concept of "enumerable" which is different from the enumeration used here.
notes
- decides: decidable set/relation vs deciding a sentence vs a theory being decidable vs deciding every sentence vs a logic being decidable (decidability of logic has several equivalent formulations; this is the topic of the Entscheidungsproblem)
- structure vs interpretation vs model: synecdoche problem
- interpretation: there's interpretation in the "structure" sense and also interpretation in the sense of embedding one theory inside another theory (e.g. doing arithmetic with sets)
- theory vs axioms: synecdoche problem
- language vs logic vs formal system vs system
- proves logically vs proves in a particular theory: each theory adds some non-logical axioms that allows it to prove things that aren't logically valid
- : when a set of sentences comes before the symbol vs when a structure comes before the symbol: see User:IssaRice/Computability and logic/Models symbol
- deciding (corresponding to computable total functions) vs recognizing (semi-deciding, computably enumerating; corresponding to computable partial functions)
- algorithm vs program vs index vs Godel number
- algorithm vs function computed by algorithm: see User:IssaRice/Computability and logic/Function versus algorithm
- expresses vs captures (strong capture, weak capture): see User:IssaRice/Computability and logic/Expresses versus captures
- primitive recursive vs (general, μ) recursive
- vs
- formulas vs relations vs sets
- enumerating vs computably enumerating vs primitively recursively enumerating
- different kinds of deduction systems: axiomatic, natural deduction, sequents, trees
- model as representation vs that which is represented (in mathematical logic, it is that which is represented, but in other disciplines a different meaning of "model" is used)
More speculative:
- different kinds of diagonalization?
There are also some important equivalences to keep in mind:
- Turing computable = computable = recursive = unbounded loops
- Primitive recursive = bounded loops
- computably enumerating = semi-deciding
- computably enumerating in order = deciding
- diagonalization lemma = rogers fixed point theorem
- Kleene's T predicate, godel beta function, Prf(m,n) https://machinelearning.subwiki.org/wiki/User:IssaRice/Computability_and_logic/Bounded_computation_trick