This homework is due by Thursday May 5 at 8 am.
For our discussion in the last few classes, two crucial effective procedures were (i) building the self-application of an open formula, and (ii) determining whether something counts as a proof of a given formula.
The first three of our final homework problems will work out what those procedures look like in more detail. Instead of trying to work with the cumbersome (and only recently introduced) system of (primitively) recursive functions, or with the even more cumbersome languages of formal arithmetic we talked about, we’ll help ourselves to the resources of algorithms that manipulate and detect properties of strings, that we worked with at the start of term. This makes some things a lot easier (though as you saw in Homework 6, it would make defining notions like multiplication a bit complicated). The general principles used in the string-focused system are the same as in the other, number-focused systems.
First, we’ll figure out how to transform a formula φ into the result of replacing unbound occurrences of a variable ξ with a “closed term” τ. This is what I’ve been writing in the last part of the class as φ[ξ ← τ]. (“Closed terms” are term constants like a and 1, and complex terms built up out of other closed terms. So no variables or complex terms that include variables. We confine our attention to closed terms here so that we don’t have to worry about renaming bound variables as we’d have to when replacing unbound occurences of x with y in ∃y(Qy ⊃ Rxy).)
To make things easier for ourselves here, we’ll assume that our language is sparse and regimented. The only logical connectives we’ll allow are ~ and ⊃, and the quantifier ∀. We’ll be strict about requiring parentheses around any formula of the shape (ψ ⊃ φ). We’ll assume that complex terms always have the shape of a unary functor η followed by a term, or the shape (β η α), where β and α are terms and η is a binary functor. We’ll assume that atomic formulas always have the shape of a unary predicate ρ followed by a single term, or the shape β ρ α, where β and α are terms and ρ is a binary predicate (including =). We don’t need to require parentheses here.
We’ll assume that no predicate, functor, term constant, or variable is a proper prefix or suffix of any other of these expressions. Thus if x and 1 are a variable and a term constant, we can’t also have variables like x1 or xx, or predicates or functors like rx or f1.
We’ll help ourselves to functions isBinaryPredicate, isUnaryPredicate, isBinaryFunctor, isUnaryFunctor, isTermConstant, and isVariable that detect the corresponding expressions. These won’t be defined here.
To make some of our patterns shorter, I use the $-shorthand from earlier in the term. Remember that the pattern λ "blah $x bleg" is the same as λ "blah" ⁀ x ⁀ "bleg".
The else at the end of the definitions below is just a pattern variable that matches any string that wasn’t matched by the earlier clauses.
Your job is to fill in the blanks.
isTerm(s) =def dissect s {
λ "( $β $η $α )" if isTerm(β) and isBinaryFunctor(η)! isTerm(α);
λ "$η $α" if isUnaryFunctor(η)! isTerm(α);
λ else. isTermConstant(s) or isVariable(s)
}
isFormula(g) =def dissect g {
λ "~ $φ"! isFormula(φ);
λ "( $ψ ⊃ $φ )" if isFormula(ψ)! ⸏⸏⸏a⸏⸏⸏;
λ "∀ $u $φ" if isVariable(u)! isFormula(φ);
λ "$β $ρ $α" is isTerm(β) and isBinaryPredicate(ρ)! isTerm(α);
λ "$ρ $α" if isUnaryPredicate(ρ)! ⸏⸏⸏b⸏⸏⸏;
λ else. false
}
replaceUnbound(g, ξ, τ) =def dissect g {
λ "~ $φ"! "~" ⁀ replaceUnbound(⸏⸏⸏c⸏⸏⸏, ξ, τ);
λ "( $ψ ⊃ $φ )" if isFormula(ψ)! ⸏⸏⸏d⸏⸏⸏;
λ "∀ $u $φ" if isVariable(u) and u ≠ ξ! "∀" ⁀ u ⁀ replaceUnbound(⸏⸏⸏e⸏⸏⸏, ξ, τ);
λ "$β $ρ $α" if isTerm(β) and isBinaryPredicate(ρ)! replaceInTerm(β, ξ, τ) ⁀ ρ ⁀ replaceInTerm(α, ξ, τ);
λ "$ρ $α" if isUnaryPredicate(ρ)! ρ ⁀ replaceInTerm(α, ξ, τ);
λ else. g
}
replaceInTerm(s, ξ, τ) =def dissect s {
λ "( $β $η $α )" if isTerm(β) and isBinaryFunctor(η)! "(" ⁀ replaceInTerm(β, ξ, τ) ⁀ η ⁀ replaceInTerm(α, ξ, τ) ⁀ ")";
λ "$η $α" if isUnaryFunctor(η)! η ⁀ replaceInTerm(α, ξ, τ);
λ α if isVariable(α) and α = ξ! ⸏⸏⸏f⸏⸏⸏;
λ else. ⸏⸏⸏g⸏⸏⸏
}Suppose name is a function that takes a string φ as argument and returns a string that names or designates φ. If the domain that the terms in φ take as values are numbers, name(φ) would have to be some term designating a number that “encodes” string φ. If instead the terms in φ take strings as their values, name(φ) could be a quoted version of φ. (In that case, if φ might itself contain quotes, we’d have to have some arrangement for “escaping” those quotes, so that name(quote ⁀ "cat" ⁀ quote ⁀ "is a noun") would result in the string quote ⁀ escapedQuote ⁀ "cat" ⁀ escapedQuote ⁀ "is a noun" ⁀ quote.)
You can ignore the details of how name works.
Using name and your answers to Problem 1, how would you formulate the “self-application” of a formula φ which has a free variable x?
Next, we’ll figure out how to determine whether something 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 [x, y, z] as ":" ⁀ x ⁀ ":" ⁀ y ⁀ ":" ⁀ z ⁀ ":". This scheme allows any of the strings x, y, or z 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 ... {
λ "$hs $h :" if endsWith(hs, ":") and not anyWhere(h, ":")! ...;
λ else. ...
}The auxiliary function endsWith(hs, ":") (which you defined in Homework 1 Problem 1) returns true if the letter ":" is a suffix of the string hs. The auxiliary function anyWhere(h, ":") (which you defined in Homework 1 Problem 2) returns true if the letter ":" occurs anywhere in the string h.
At the end of the first clause (whatever fills in the ...), the variable hs will be bound to the rest of the list coming before its last element h. (It may be that hs is just the empty list ":".)
Here is a definition of listHasElem(fs, g), that detects whether fs is a list that has the string g as an element. (We also get the result false if fs doesn’t represent a valid list, or if g contains a ":".)
listHasElem(fs, g) =def dissect fs {
λ "$hs $h :" if endsWith(hs, ":") and not anyWhere(h, ":")! h = g or listHasElem(hs, g);
λ else. false
}Armed with these tools, how can we determine whether fs represents a proof of the formula g?
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 after (φ ⊃ ψ) is licensed by earlier lines in the proof. 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 at the end if you need to.
As before, your job is to fill in the blanks.
isProofOf(fs, g) =def dissect fs {
λ "$hs $h :" if endsWith(hs, ":") and not anyWhere(h, ":")! h = g and licenses(⸏⸏⸏a⸏⸏⸏, h);
λ else. false
}
licenses(fs, g) =def isFormula(g) and dissect fs {
λ "$hs $h :" if endsWith(hs, ":") and not anyWhere(h, ":") and licenses(hs, h)!
licenses(⸏⸏⸏b⸏⸏⸏, "(" ⁀ h ⁀ "⊃" ⁀ g ⁀ ")") or licenses(hs, ⸏⸏⸏c⸏⸏⸏);
λ ":"! isAxiom(g);
λ else. false
}We introduced a class of “primitively recursive” 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) ∸ Id(x), where y ∸ z (y “monus” z) is subtraction that “cuts off” at 0 (that is, 3 ∸ 5 = 0, and 0 ∸ 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 recursive 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 minimization,” giving us the fully/general recursive 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 recursive 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 recursive 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⸏⸏⸏
If a theory “decides” every sentence of its language (that is, either proves the sentence or proves its negation), will the theory be “decidable” (that is, will there be an effective/mechanical algorithm for determining whether any sentence is proven by the theory)? Explain/justify your answer.
Let T be a theory that is a “consistent extension” of one of the “middling arithmetics” we met. (T may or may not be “axiomatizable,” we don’t make assumptions about that now.)
We say that a set Δ is defined in T by an open formula φ iff for every m ∈ ℕ:
m encodes an element of Δ, then T ⊢ φ[x ← SmZ]m does not encode an element of Δ, then T ⊢ ~φ[x ← SmZ]Here is a proof that the set of T’s theorems is not definable in T. As before, your job is to fill in the blanks.
Suppose this set were definable in T, by formula θ with free variable x. The Diagonal Lemma says that for any extension of middling arithmetic and any formula φ of its language, there is a sentence D such that T ⊢ D ⊂⊃ φ[x ← the number that encodes sentence D]. Let φ be ~θ, that is, the formula that (we’re supposing) would define “x does not encode a theorem of T.” Let D be the sentence posited by the Diagonal Lemma for this formula ~θ. 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 define 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 define 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 defines in T the set of T’s theorems fails.
Since it’s true (we didn’t talk through the proof, which is tedious, but you can be assured it is true) that all effectively decidable sets are definable in consistent extensions of our middling arithmetics, it follows that the set of theorems of any theory like T won’t be effectively decidable.