next up previous
Next: About this document ...

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

Theorem 1 (Gödel I)   Suppose that $\Phi$ is consistent and decidable, and that Rep $\Phi$ as well. Then there is an Sar-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

\begin{displaymath}\Phi \vdash \phi \leftrightarrow \psi(\dot{n^\phi}).\end{displaymath}




Which needs:

\fbox{G\uml {o}del numbering scheme}

% 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{displaymath}
\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}\end{displaymath}

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:

``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: S3G

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:

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

\begin{displaymath}\mbox{\fbox{E}\quad \fbox{T}\quad \fbox{4}\quad \fbox{7} }\end{displaymath}

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



 
next up previous
Next: About this document ...
Selmer Bringsjord
1998-08-12