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/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 :
**Failing**to Know " - 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

- ``The Impact :
- But let's start with little 'ol me, and literary, not
mathematical, creativity:
- Selmer (samples) vs. Brutus
_{1}(samples again) - Brutus
_{1}and ``Weak"AI: S^{3}G as ultimate aim - Upshot: clever, perhaps, but raw origination (and point of view) left a mystery

- Selmer (samples) vs. Brutus

- Automated Theorem Proving as the computation through
which to know Gödel's mind:
- Gödel I
- OTTER
- OTTER and encoding in the propositional calculus
- Quaife's use of OTTER to prove Gödel I
- 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.
- Humans naturally develop a context-free deductive reasoning scheme at the level of elementary first-order logic.

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

- The Received View: Piaget Dead on Deductive Reasoning -- i.e.,
the following regarded false.

Need:

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:

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.
**4**

- Rules of Inference:
- If infer to then
**RN**- If infer to

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) ThmK4(x).`[`taut(x)`iff`(cnf(x) = T)`]- 2.
`ThmK4(b(x y) (b(x) b(y)))).`- 3.
`ThmK4(b(x) b(b(x))).`- 4.
`(ThmK4((x y)) ThmK4(x)) ThmK4(y))`- 5.
`ThmK4(x) ThmK4(b(x))`

``Gödel I":

`[ThmK4(x
b(x))
ThmK4(x)]
ThmK4(F)`

in OTTER:

`(ThmK4(d(x,n(b(x)))) & ThmK4(x))
ThmK4(F)).`

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

**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:

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.