Phil 455: Homework 11

This homework is due by 4 pm on Thursday May 2.

  1. If a theory “decides” every sentence of its language (that is, either proves the sentence or proves its negation), does it follow that the theory must be “decidable” (that is, there will be an effective/mechanical algorithm for determining whether any sentence is proven by the theory)? Explain/justify your answer.

  2. Take one of the “middling arithmetics” we’ve been discussing, and let T be a theory (a deductively closed set of sentences) that “extends” it (adds 0 or more additional theorems), while remaining consistent. (T may or may not be “axiomatizable,” we don’t make assumptions about that now.)

    Here is one important definition we’ve met: We say that a set Δ of sentences is captured in T by a formula φ with free variable x iff for every m ∈ ℕ:

    (I’m following Smith’s terminology here. Some texts call this being “defined in T,” or “represented in T.”)

    Here is one important theorem that we intuitively motivated in the last few classes, and Smith discusses in his Chapter 14. For the purposes of this Problem, you can just take it as given. The theorem is called the Diagonal Lemma, and says that for any theory T that’s a consistent extension of middling arithmetic, and any formula φ of its language, there is a sentence D such that T ⊢ D ⊂⊃ φ[x ← the number ⌜D⌝ that encodes sentence D].

    Armed with that theorem, here is a proof that the set of T’s theorems is not capturable in T. in the sense defined above. Your job is to fill in the blanks.

    Suppose this set were capturable in T, by formula θ with free variable x. Let D be the sentence posited by the Diagonal Lemma for the formula ¬θ. That is, D is provably equivalent in T to the claim that ⌜D⌝ does not encode a theorem of T.

    Now D will either be a theorem of T or it won’t.

    If D is not a theorem of T, then because of what it means for θ to capture in T the set of T’s theorems, we get the result ⸏⸏⸏a⸏⸏⸏. But then, by what the Diagonal Lemma tells us about T and D, it follows that ⸏⸏⸏b⸏⸏⸏. This contradicts our assumption that D is not a theorem.

    If on the other hand, D is a theorem of T, then because of what it means for θ to capture in T the set of T’s theorems, we get the result ⸏⸏⸏c⸏⸏⸏. But then, by what the Diagonal Lemma tells us about T and D, it follows that ⸏⸏⸏d⸏⸏⸏. This contradicts the assumption that T is consistent.

    Hence our supposition that there is a formula θ that captures in T the set of T’s theorems fails.

    Since it’s true (we didn’t go through the proof, which is tedious, but you can be assured it is true) that all effectively decidable sets of sentences are capturable in consistent extensions of our middling arithmetics, it follows that the set of theorems of any theory like T won’t be effectively decidable.

    Some theories like T are axiomatizable (some of them even with only finitely many non-logical axioms). If it were effectively decidable what followed from what in first-order logic, then the set of what theorems followed from those axioms should be effectively decidable. So this tells us that it’s not effectively decidable what follows from what in first-order logic. (We discussed another route to that conclusion earlier in the class, having to do with translating the descriptions and operations of Turing Machines into first-order logic, and relying on the fact that the Halting Problem is not effectively decidable.)

  3. Let’s go back to working with strings as strings, instead of manipulating their numeric encodings. We’re trying to specify what counts as a proof of a given formula. We’ll suppose that our proofs are just lists of formulas. We worked with how to represent lists of strings as single strings earlier in the term. Let’s refresh our memory.

    We’re representing a list of strings [α, β, γ] as ":" ⁀ α ⁀ ":" ⁀ β ⁀ ":" ⁀ γ ⁀ ":". This scheme allows any of the strings α, β, or γ to be empty; but none are allowed to contain the colon ":". The empty list is represented by the string ":" (note not by the empty string, which doesn’t represent any list).

    To obtain the last string in a list of strings, we say something like this:

    dissect ... {
    λ α ⁀ β ⁀ ":" if endsWith(α, ":") and not anyWhere(β, ":")! ...;
    λ else. ...
} assuming { λ γ if startsWith(γ, ":") and endsWith(γ, ":") }

    The auxiliary function endsWith(α, ":") (which you defined in Homework 5 Problem 56) returns true if the letter ":" is a suffix of the string α. The auxiliary function anyWhere(β, ":") (which you defined in Homework 5 Problem 57) returns true if the letter ":" occurs anywhere in the string β.

    At the end of the first clause (whatever fills in the ...), the variable α will be bound to the rest of the list coming before its last element β. (It may be that α is just the empty list ":".)

    Here is a definition of listHasElem(γ, δ), that detects whether γ is a list that has the string δ as an element. (We also get the result false if δ contains a ":", or undefined if γ doesn’t represent a valid list.)

    listHasElem(γ, δ) =def dissect γ {
    λ α ⁀ β ⁀ ":" if endsWith(α, ":") and not anyWhere(β, ":")! β = δ or listHasElem(α, δ);
    λ else. false
} assuming { λ γ if startsWith(γ, ":") and endsWith(γ, ":") }

    Armed with these tools, how can we determine whether γ represents a proof of the formula ψ?

    We’ll help ourselves to a function isAxiom that returns true for any formula that counts as an axiom (either a logical axiom or whatever non-logical axioms we’re allowing ourselves). To make things easier for ourselves here (but harder for people who have to come up with the proofs), we’ll say our proof system has only the single rule of modus ponens, and we’ll say that modus ponens only applies when φ occurs in the list after (φ ⊃ ψ) is “licensed by” earlier lines in the proof. (That is, (φ ⊃ ψ) doesn’t have to explicitly occur in the list, but only be justified by earlier lines.) But in our proofs, any earlier line can always be copied/repeated again later. We also say that a list of formulas only proves the last formula in the list. Again, you can always copy/repeat earlier lines to the end if you need to.

    As before, your job is to fill in the blanks.

    isProofOf(γ, ψ) =def dissect γ {
    λ α ⁀ β ⁀ ":" if endsWith(α, ":") and not anyWhere(β, ":")! β = ψ and licenses(⸏⸏⸏a⸏⸏⸏, β);
    λ else. false
} assuming { λ γ if startsWith(γ, ":") and endsWith(γ, ":") }

licenses(γ, ψ) =def isFormula(ψ) and dissect γ {
    λ α ⁀ β ⁀ ":" if endsWith(α, ":") and not anyWhere(β, ":") and licenses(α, β)!
        licenses(⸏⸏⸏b⸏⸏⸏, "(" ⁀ β ⁀ "⊃" ⁀ ψ ⁀ ")") or licenses(α, ⸏⸏⸏c⸏⸏⸏);
    λ ":"! isAxiom(ψ);
    λ else. false
} assuming { λ γ if startsWith(γ, ":") and endsWith(γ, ":") }

  4. We introduced a class of “primitively rekursive” functions, which are always total functions from ℕj into ℕ (that is, they have a defined result for all j-tuples of arguments). Since these are built up in a systematic way, we could have a system for writing down or specifying each of the functions. Some specifications will designate the same function (counting functions as the same when the map all the same arguments to the same results). For example, Zero and Id ∘ Zero both pick out the 1-adic function that maps each argument to 0. So too does Monus ∘ (Zero, Id), which maps each x to Zero(x) monus Id(x), where y monus z is subtraction that “cuts off” at 0 (that is, 3 monus 5 = 0, and 0 monus x for any x also = 0).

    But even with different specifications designating the same function, the fact that we can specify the functions like this, in ways we could then “alphabetize,” suggests that the primitive rekursive functions will be effectively enumerable — which they are. It’s important here that it’s not just that some enumeration exists in the abstract, establishing that there are only countably many of these functions. What we have, additionally, is that there’s an effective/mechanical algorithm, that given any n ∈ ℕ, could locate the nth function, specified in a way that an effective/mechanical algorithm could then continue on to apply that function to an argument. We’ll confine our attention just to the functions that take a single ℕ as argument.

    We also talked about how to add further function-building resources (“unbounded searches,” giving us the fully/general rekursive functions, but the details aren’t important here). The additional functions this lets us build are sometimes total and sometimes not. These functions are also specifiable in ways that an effective/mechanical algorithm can perform, at least for arguments where the function has a defined value. We said that these functions (including the primitively rekursive functions too) are understood to constitute the whole set of functions on ℕ that are effective/mechanically computable.

    Here is the outline of a proof that the subset of these functions that are still total is not effectively enumerable, in the way the primitively rekursive functions are. Your job is to fill in the blanks to complete/explain the proof.

    Suppose for reductio that the set of effective/mechanically computable total functions from ℕ → ℕ is effectively enumerable, in the way envisaged. Then these functions can be indexed as f₀, f₁, ..., fk, ..., where given any n ∈ ℕ, an algorithm could locate the nth function, and then apply that function to an argument. Consider a function g from ℕ → ℕ, which maps each n ∈ ℕ to the value fn(n) + 1. This function would be effective/mechanically computable and total, because ⸏⸏⸏a⸏⸏⸏. But it would not be identical to any of the fks, because ⸏⸏⸏b⸏⸏⸏. So our assumption that the fks exhaust the effective/mechanically computable total functions from ℕ → ℕ fails.

    Last question here: what role does the restriction to total functions play in this argument? What would be different if we removed that restriction? ⸏⸏⸏c⸏⸏⸏

    (A structurally parallel proof appears in Smith’s Chapter 9; but he’s making different assumptions about the fk functions and using it to show a different result.)