5
$\begingroup$

One of the exercises in Hofstadter's Gödel, Escher, Bach (on page 227 of this pdf) asks us to produce the theorem $$\neg \forall b : \exists a : Sa = b$$ using only the first axiom of Typographical Number Theory and four rules relating to quantifiers:

Axiom 1: $\forall a : \neg Sa = 0$

Rule of Specification: Suppose $u$ is a variable which occurs inside the string $x$. If the string $\forall u: x$ is a theorem, then so is $x$, and so are any strings made from $x$ by replacing $u$, wherever it occurs, by one and the same term. (Restriction: The term which replaces $u$ must not contain any variable that is quantified in $x$.)

Rule of Generalization: Suppose $x$ is a theorem in which $u$, a variable, occurs free. Then $\forall u: x$ is a theorem. (Restriction: No generalization is allowed in a fantasy on any variable which appeared free in the fantasy's premise.)

Rule of Interchange: Suppose $u$ is a variable. Then the strings $\forall u: \neg$ and $\neg \exists u: $ are interchangeable anywhere inside any theorem.

Rule of Existence: Suppose a term (which may contain variables as long as they are free) appears one, or multiply, in a theorem. Then any (or several, or all) of the appearances o the term may be replaced by a variable which otherwise does not occur in the theorem, and the corresponding existential quantifier must be placed in front.

In my attempts, I can't seem to get around the introduction and removal of a double negative, which is not a specified rule. I also can't seem to derive the double negative rules from the given ones. So I'm having quite a hard time producing the required theorem. Here is what I have:

$$\begin{align*} \forall a : \neg Sa = 0 \tag{axiom 1} \\ \exists b : \forall a : \neg Sa = 0 \tag{existence} \\ \neg\neg \exists b : \forall a : \neg Sa = b \tag{introduce double neg} \\ \neg \forall b : \neg \forall a : \neg Sa = b \tag{interchange} \\ \neg \forall b : \neg\neg \exists a : Sa = b \tag{interchange} \\ \neg \forall b : \exists a : Sa = b \tag{remove double neg} \end{align*}$$

I'd like to prove the validity of introducing and removing double negatives using only the rules specified for this problem, but I don't even know how to start. I don't quite understand what can be taken as a premise. For example, can I start with a general $\forall x : P$ and somehow get to $\forall x : \neg\neg P$ and vice versa? Or is that not a valid term... sentence... predicate...? I'm very confused.

Regardless, if we can prove $\forall x : P$ implies $\forall x : \neg\neg P$, then I should be able to use the same logic to replace steps 3 and 6 in my proof above. I suppose that's what I'm asking for help with.

Thank you!

$\endgroup$
3
  • 1
    $\begingroup$ You don't need $\neg\neg$-elimination. The implication from $\exists x. P(x)$ to $\neg \forall x. \neg P(x)$ is valid intuitionistically ($\lambda (x, p). \lambda k. k\,x\,p$). See also math.stackexchange.com/a/5130518. $\endgroup$ Commented Apr 3 at 18:19
  • $\begingroup$ I'm glad I don't need $\neg\neg$-elimination, but if I'm going to use $\exists x. P(x) \implies \neg \forall x. \neg P(x)$, I'd want to derive it from what I have. The only rule I see relating $\forall$ and $\exists$ is interchange, but I don't know how to use it to get from $\exists x. P(x)$ to $\neg \forall x \neg P(x)$. Is this implication provable from the four rules above? $\endgroup$ Commented Apr 3 at 20:13
  • 1
    $\begingroup$ @msb15 : as the answer from pastebee says, because those four rules preserve the number of negation symbols in a formula, there is no way to get from two negation symbols to zero with those rules. $\endgroup$ Commented Apr 3 at 20:15

2 Answers 2

Reset to default
3
$\begingroup$

Using only the specific axiom and rules you quoted, this exercise is impossible. More specifically, it is not possible to prove any theorem which contains two instances of $\neg$, or a $\forall$ after a $\neg$, with only these rules.

We can see this by checking that none of the rules can be used to prove such a theorem unless we have proved one already:

  • Axiom 1 does not contain two $\neg$s or a $\forall$ after a $\neg$.
  • The rules of Specification and Generalization do not affect the number of occurrences of $\neg$, and cannot add a $\forall$ after a $\neg$ because they only add or remove $\forall$s at the beginning of the statement.
  • The rule of Interchange does not affect the number of occurrences of $\neg$. If there is only one $\neg$, then it cannot introduce a $\forall$ after a $\neg$, because it can only convert $\neg \exists$ into $\forall \neg$, which is the wrong way around.
  • The rule of Existence just adds an $\exists$, which clearly does not affect our conditions at all.

But the statement you are trying to prove begins with $\neg \forall$, so, taking your question at face value, it is not provable.

(I agree with Carl Mummert that the author's actual intention is almost certainly that the allowed rules for this exercise also include the rules of propositional logic given earlier in the book, which includes the double negation rule that the proof you gave uses. This answer is just showing that something like that is necessary.)

$\endgroup$
2
$\begingroup$

You have $\forall a . \lnot S(a) = 0$. Why not use "interchange" to get $\lnot \exists a . S(a) = 0$?

Then you can generalize on $0$ to get $\exists b . \lnot \exists a . S(a) = b$ and apply interchange again.

Note that double-negation elimination is given as an acceptable inference rule on page 191, and this is probable the easiest way to derive the "other" interchange rule from the one explicitly stated.

On page 223 the author states, "Firstly, as was promised, all of the rules of the Propositional Calculus are taken over into TNT." so TNT does seem to include the double negation rule already.

One thing about Hofstadter's system is that it is idiosyncratic. There are many ways to formalize logic, but phrasing double negation elimination as "The string '~~' can be deleted from any theorem." is not how most people would say it.

$\endgroup$
2
  • $\begingroup$ Doesn't applying interchange to $\exists b. \neg \exists a. S(a)=b$ give us $\exists b. \forall a. \neg S(a)=b$? I don't see how that gets us closer to $\neg \forall b. \exists a. S(a)=b$. $\endgroup$ Commented Apr 3 at 20:09
  • 1
    $\begingroup$ Interchanging the $\exists b \lnot$ gives $\lnot \forall b$ at the front. Presumably the reason why the author only states one and not the other form of interchange is that the logic already has double negation elimination and so the second one is derivable. $\endgroup$ Commented Apr 3 at 20:10

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.