The Impact of Computing on Epistemology:
Knowing Gödel's Mind Through Computation

Selmer Bringsjord
Director, The Minds & Machines Laboratory
Dept. of Philosophy, Psychology & Cognitive Science
Department of Computer Science
Rensselaer Polytechnic Institute (RPI)
Troy NY 12180 USA
selmer@rpi.edu
http://www.rpi.edu/$\sim$brings

• I know that those of you who know my mind know that I think I know that we can't know Gödel's mind through computation:
  • ``The Impact $\ldots$: Failing to Know $\ldots$"
  • If computationalism is false, observant philosophers willing to get their hands dirty should be able to find tell-tale signs
    • today: automated theorem proving
    • tomorrow (Eastern APA): robots as zombanimals
• But let's start with little 'ol me, and literary, not mathematical, creativity:
  • Selmer (samples) vs. Brutus<sub>1</sub> (samples again)
  • Brutus<sub>1</sub> and ``Weak"AI: S³G as ultimate aim
  • Upshot: clever, perhaps, but raw origination (and point of view) left a mystery

• Automated Theorem Proving as the computation through which to know Gödel's mind:
  • Gödel I$\dots$
  • OTTER$\dots$
  • OTTER and encoding in the propositional calculus$\ldots$
  • Quaife's use of OTTER to prove Gödel I$\dots$
  • Quickie litmus test: teach Gödel I via Quaife-OTTER? No!
  • Searle a welcome ghost: Gödel's mind not to be found in symbol manipulation
  • Penrose a welcome ghost: what mathematicians (and logicians) do, not to be found in computation
• On the positive side: morals for teaching logic (very briefly):
  • The Received View: Piaget Dead on Deductive Reasoning -- i.e., the following regarded false.

    $\cal F$

    Humans naturally develop a context-free deductive reasoning scheme at the level of elementary first-order logic.

  • Challenges from the Psychology of Reasoning$\ldots$
  • Teaching logic as if teaching machines will fail to produce those able to meet these challenges

Theorem 1 (Gödel I)   Suppose that $\Phi$ is consistent and decidable, and that Rep $\Phi$ as well. Then there is an S_ar-sentence $\phi_g$ such that neither $\Phi \vdash \phi_g$ nor $\Phi \vdash \neg\phi_g$.

Need:

Theorem 2 (Fixed Point Theorem)   If Rep $\Phi$, then for every arithmetic formula $\psi$ with one free variable (i.e., formally, for every $\psi \in L_1^{S_{ar}}$) there is an arithmetic sentence $\phi$ such that

$$\Phi \vdash \phi \leftrightarrow \psi(\dot{n^\phi}).$$

Which needs:

% This propositional logic problem that was the
% "most difficult" (!) theorem proved by the 
% original Logic Theorist of 1957.
% 
% Selmer Bringsjord (born 1958)
% Intro to Logic Programming and AI, Spring 98

set(auto).
set(propositional).

formula_list(usable).

-((p -> q) <-> (-q -> -p)).

end_of_list.

---------------- PROOF ----------------

1 [] -p|q.
2 [] -q.
3 [] p.
4 [hyper,3,1] q.
5 [binary,4.1,2.1] $F.

------------ end of proof -------------

set(auto).
% Proof 9.26 from Barwise and Etchemendy's
% *Hyperproof*

formula_list(usable).
-(exists x (R(x) -> (all y R(y)))).
end_of_list.

formula_list(usable).
-(exists x (R(x)-> (all y R(y)))).
end_of_list.

-------> usable clausifies to:
list(usable).
0 [] R(x).
0 [] -R($f1(x)).
end_of_list.

---------------- PROOF ----------------
1 [] -R($f1(x)).
2 [] R(x).
3 [binary,2.1,1.1] $F.
------------ end of proof -------------

The schema for hyperresolution looks like this:

$$\begin{array}{ll} \Phi_1 \cup \{\neg\psi_1, \neg\psi_2, \ldo... ...Phi_1 \cup \Phi_ 2 \cup \cdots \cup \Phi_{n+1} &\\ \end{array}$$

Now here is an example in OTTER, first an input file and then an output file showing the proof. Note here that both ur-resolution and hyper-resolution are used.

% An input file for evoking hyperresolution.

set(hyper_res).
set(ur_res).

list(usable).
p | q | -r | s.
end_of_list.

list(sos).
p | q | r.
-s.
-q.
-p.
end_of_list.

---------------- PROOF ----------------

1 [] p|q| -r|s.
2 [] p|q|r.
3 [] -s.
4 [] -q.
5 [] -p.
6 [ur,5,1,4,3] -r.
7 [hyper,2,6] p|q.
8 [hyper,7,4] p.
9 [binary,8.1,5.1] $F.

------------ end of proof -------------

set(auto).

formula_list(usable).
%MP
all x all y ((T(i(x,y)) & T(x)) -> T(y)).
%PL
all x all y (T(i(x,i(y,x)))).
all x all y all z (T(i(i(x,i(y,z)),i(i(x,y),i(x,z))))).
all x all y (T(i(i(n(x),n(y)),i(y,x)))).

%-(all x (T(i(n(n(x)),x)))).
%-(all x (T(i(x,x)))).
-(all x all y T((i(i(x,y),i(n(y),n(x)))))).

end_of_list.

---------------- PROOF ----------------

1 [] -T(i(x,y))| -T(x)|T(y).
2 [] -T(i(i($c2,$c1),i(n($c1),n($c2)))).
3 [] T(i(x,i(y,x))).
4 [] T(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
5 [] T(i(i(n(x),n(y)),i(y,x))).
6 [hyper,3,1,3] T(i(x,i(y,i(z,y)))).
7 [hyper,6,1,3] T(i(x,i(y,i(z,i(u,z))))).
8 [hyper,5,1,3] T(i(x,i(i(n(y),n(z)),i(z,y)))).
11 [hyper,4,1,4] T(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).
12 [hyper,4,1,3] T(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).
13 [hyper,4,1,8] T(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).
14 [hyper,4,1,6] T(i(i(x,y),i(x,i(z,y)))).
16 [hyper,4,1,3] T(i(i(x,y),i(x,x))).
19 [hyper,16,1,8] T(i(x,x)).
20 [hyper,19,1,4] T(i(i(i(x,y),x),i(i(x,y),y))).
21 [hyper,19,1,3] T(i(x,i(y,y))).
22 [hyper,21,1,3] T(i(x,i(y,i(z,z)))).
28 [hyper,14,1,5] T(i(i(n(x),n(y)),i(z,i(y,x)))).
60 [hyper,20,1,22] T(i(i(i(x,i(y,y)),z),z)).
66 [hyper,20,1,6] T(i(i(i(x,i(y,x)),z),z)).
77 [hyper,11,1,60] T(i(i(x,i(x,y)),i(x,y))).
89 [hyper,11,1,7] T(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).
90 [hyper,11,1,6] T(i(i(x,i(i(y,x),z)),i(x,z))).
110 [hyper,12,1,11] T(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))).
137 [hyper,13,1,66] T(i(n(x),i(x,y))).
154 [hyper,137,1,13] T(i(n(n(x)),i(y,x))).
157 [hyper,154,1,77] T(i(n(n(x)),x)).
167 [hyper,157,1,28] T(i(x,i(y,n(n(y))))).
171 [hyper,157,1,3] T(i(x,i(n(n(y)),y))).
247 [hyper,167,1,4] T(i(i(x,y),i(x,n(n(y))))).
252 [hyper,171,1,11] T(i(i(n(n(x)),i(x,y)),i(n(n(x)),y))).
8373 [hyper,90,1,12] T(i(i(x,y),i(i(z,x),i(z,y)))).
8648 [hyper,8373,1,89] T(i(i(i(x,y),z),i(y,z))).
8654 [hyper,8648,1,3] T(i(x,i(i(i(y,z),u),i(z,u)))).
8656 [hyper,8648,1,252] T(i(i(x,y),i(n(n(x)),y))).
8906 [hyper,8654,1,110] T(i(i(x,i(y,z)),i(y,i(x,z)))).
9024 [hyper,8906,1,247] T(i(x,i(i(x,y),n(n(y))))).
9051 [hyper,9024,1,8656] T(i(n(n(x)),i(i(x,y),n(n(y))))).
9127 [hyper,9051,1,8906] T(i(i(x,y),i(n(n(x)),n(n(y))))).
9154 [hyper,9127,1,13] T(i(i(x,y),i(n(y),n(x)))).
9155 [binary,9154.1,2.1] $F.

------------ end of proof -------------

K4:

Axioms:

Propositional tautologies.

$\Box (\phi \Rightarrow \psi) \Rightarrow (\Box \phi \Rightarrow \Box \psi)$

4

$\Box \phi \Rightarrow \Box \Box \phi$

Rules of Inference:

If $\vdash \phi \Rightarrow \psi$ infer to $\vdash \phi$ then $\vdash \psi$

RN

If $\vdash \phi$ infer to $\vdash \Box \phi$

Because RN is a bit of a problem, Quaife represents a first-order metatheory of K4 within OTTER:

• Interpret ``b(x)" to mean ``x is provable in PA"
• Formulas of K4 become terms in OTTER.
• Specifically, the predicate ThmK4(x) means that the formula x is a theorem of K4, and taut stands for `tautology.' We have

  1.

  taut(x) $\Rightarrow$ ThmK4(x). [taut(x) iff (cnf(x) = T)]

  2.

  ThmK4(b(x $\Rightarrow$ y) $\Rightarrow$ (b(x) $\Rightarrow$ b(y)))).

  3.

  ThmK4(b(x) $\Rightarrow$ b(b(x))).

  4.

  (ThmK4((x $\Rightarrow$ y)) $\wedge$ ThmK4(x)) $\Rightarrow$ ThmK4(y))

  5.

  ThmK4(x) $\Rightarrow$ ThmK4(b(x))

``Gödel I":

[ThmK4(x $\Leftrightarrow$ $\neg$b(x)) $\wedge$ ThmK4(x)] $\Rightarrow$ ThmK4(F)

in OTTER:

(ThmK4(d(x,n(b(x)))) & ThmK4(x)) $\Rightarrow$ ThmK4(F)).

A four line proof using hyperresolution and binary resolution; it can be done in about 1 second on a decent computer.

  

Figure 1: S³G

P1: Wason's Selection Task

Suppose that I have a pack of cards each of which has a letter written on one side and a number written on the other side. Suppose in addition that I claim the following rule is true:

• If a card has a vowel on one side, then it has an even number on the other side.

Imagine that I now show you four cards from the pack:

$$\mbox{\fbox{E}\quad \fbox{T}\quad \fbox{4}\quad \fbox{7} }$$

Which card or cards should you turn over in order to decide whether the rule is true or false?

Johnson-Laird's Challenges (``Cognitive Illusions"), e.g.,

If one of the following assertions is true then so is the other:

1.

There is a king in the hand if and only if there is an ace in the hand.

2.

There is a king in the hand.

Which is more likely to be in the hand, if either: the king or the ace?

  

Figure 2: The ``Frenchmen" Syllogism Disproved in Hyperproof