godel
Class Godel2

java.lang.Object
  java.awt.Component
      java.awt.Container
          java.awt.Panel
              java.applet.Applet
                  godel.Godel2

All Implemented Interfaces:

java.awt.event.ActionListener, java.awt.event.MouseListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener, javax.accessibility.Accessible

public class Godel2
extends java.applet.Applet
implements java.awt.event.ActionListener, java.awt.event.MouseListener

This is an applet to implement a numerical encoding of arithmetical proofs. Such an encoding is required in the proof of Gödel's incompleteness theorem. It uses the axiom system describes in A proof system for arithmetic For further information see Gödel numbering applet

Author:

Stephen Lee

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class java.applet.Applet

java.applet.Applet.AccessibleApplet

Nested classes/interfaces inherited from class java.awt.Panel

java.awt.Panel.AccessibleAWTPanel

Nested classes/interfaces inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

Field Summary

(package private) javax.swing.JCheckBox	binar
(package private) javax.swing.plaf.basic.BasicArrowButton	but2 Press button to generate proof lines from proof number
(package private) java.awt.Font	cf1
(package private) int	curlin Current line number for lines of proof
(package private) boolean	endflg Set when end of proof number reached
(package private) java.math.BigInteger	FOUR
(package private) java.math.BigInteger[]	IntAx Godel numbers of integer axioms
(package private) java.math.BigInteger[]	line Store for Godel numbers of lines of proof
(package private) javax.swing.JTextArea	plines Text area for Godel numbers of lines of proof
(package private) javax.swing.JTextArea	prnum Text area for Godel number of proof
(package private) java.math.BigInteger	Proofin Holds Gödel number of proof (bitstream)
(package private) int	radx Radix for proof number input (10 or 2)
private static long	serialVersionUID
(package private) java.math.BigInteger	Source Holds bitstream number to be parsed
(package private) java.math.BigInteger	Termx replacement term for varep
(package private) java.math.BigInteger	THREE
(package private) long	varep int form of variable in Ax4 or Ind axioms Will be replaced by Termx
(package private) int[]	vlist List of bound variables relevant to current term
(package private) int	vlp Count for vlist
(package private) int	vsp Stack pointer for vstack
(package private) int[]	vstack Stack of bound variables vstack,vlist,vsp and vlp are not currently used

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

Godel2()

Method Summary

void	actionPerformed(java.awt.event.ActionEvent e) respond to down button or change of proof number radix
(package private) java.math.BigInteger	Ax1() Axiom 1: WF1⇒(WF2⇒WF1) Gets two formulae
(package private) java.math.BigInteger	Ax2() Axiom 2: (WF1⇒(WF2⇒WF3))⇒((WF1⇒WF2)⇒(WF1⇒WF3)) Gets three formulae
(package private) java.math.BigInteger	Ax3() Axiom 3 (¬WF2⇒¬WF1)⇒((¬WF2⇒WF1)⇒WF2) Gets two formulae
(package private) java.math.BigInteger	Ax4() Axiom 4:∀V WF(V)⇒WF(T) (T is a term free for V in WF) Gets a variable, a term and a formula
(package private) java.math.BigInteger	Ax5() Axiom 5: ∀V(WF1⇒WF2)⇒(WF1⇒∀V WF2) (WF1 has no free occurence of V) Gets a variable and two formulae
(package private) java.math.BigInteger	Binop(java.math.BigInteger X1, int op, java.math.BigInteger X2) Encodes the result of a binary operator
(package private) java.math.BigInteger	Gen() Generalisation: WF |- ∀V WF Gets a variable and a formula
(package private) int	get2() get 2 bits from bitstream
java.lang.String	getAppletInfo()
(package private) long	getint() Get int from bitstream
(package private) java.math.BigInteger	Glin() Gets previously established formula from line number 1st bit 1 -> next 4 bits define number of axiom 1st bit 0 -> encoded line number of proof follows
(package private) java.math.BigInteger	Ind() Induction: WF(0) ⇒((∀V (WF(V) ⇒ WF(V'))) ⇒ ∀V WF(V)) * Gets a variable and a formula
void	init() Set up applet
(package private) java.math.BigInteger	LowOrder(java.math.BigInteger x, int n) Gets low order bits of a number
void	mouseClicked(java.awt.event.MouseEvent me) Paste into upper (proof number) text area on right mouse click
void	mouseEntered(java.awt.event.MouseEvent arg0)
void	mouseExited(java.awt.event.MouseEvent arg0)
void	mousePressed(java.awt.event.MouseEvent arg0)
void	mouseReleased(java.awt.event.MouseEvent arg0)
(package private) java.math.BigInteger	MP() Modus Ponens: WF1,WF1 ⇒ WF2 |- WF2 Gets two formulae
(package private) java.math.BigInteger	proofline(int c0) Gets a line of a proof
(package private) void	proves() Produces Gödel numbers of formulae of proof from Gödel number of proof in Proofin
(package private) java.math.BigInteger	Sgetvar(boolean stk) Gets variable from input bitstream
(package private) java.math.BigInteger	Sterm() gets a term from the proof bitstream
(package private) java.math.BigInteger	Swff() Gets a formula from the proof bitstream
(package private) java.math.BigInteger	Unop(int op, java.math.BigInteger X1) Applies a unary operator to a term or formula.
(package private) java.math.BigInteger	Varb(long V) Converts int form of a variable bitstream form.

Methods inherited from class java.applet.Applet

destroy, getAccessibleContext, getAppletContext, getAudioClip, getAudioClip, getCodeBase, getDocumentBase, getImage, getImage, getLocale, getParameter, getParameterInfo, isActive, newAudioClip, play, play, resize, resize, setStub, showStatus, start, stop

Methods inherited from class java.awt.Panel

addNotify

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getInsets, getLayout, getListeners, getMaximumSize, getMinimumSize, getMousePosition, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paint, paintComponents, paramString, preferredSize, print, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, removeNotify, setComponentZOrder, setFocusCycleRoot, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, setLayout, transferFocusBackward, transferFocusDownCycle, update, validate, validateTree

Methods inherited from class java.awt.Component

action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphics, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getToolkit, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, hide, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, reshape, setBackground, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setLocation, setLocation, setMaximumSize, setMinimumSize, setName, setPreferredSize, setSize, setSize, setVisible, show, show, size, toString, transferFocus, transferFocusUpCycle

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

cf1

java.awt.Font cf1

prnum

javax.swing.JTextArea prnum

Text area for Godel number of proof

plines

javax.swing.JTextArea plines

Text area for Godel numbers of lines of proof

endflg

boolean endflg

Set when end of proof number reached

but2

javax.swing.plaf.basic.BasicArrowButton but2

Press button to generate proof lines from proof number

THREE

final java.math.BigInteger THREE

FOUR

final java.math.BigInteger FOUR

vstack

int[] vstack

Stack of bound variables vstack,vlist,vsp and vlp are not currently used

vlist

int[] vlist

List of bound variables relevant to current term

vsp

int vsp

Stack pointer for vstack

vlp

int vlp

Count for vlist

varep

long varep

int form of variable in Ax4 or Ind axioms Will be replaced by Termx

Termx

java.math.BigInteger Termx

replacement term for varep

IntAx

java.math.BigInteger[] IntAx

Godel numbers of integer axioms

line

java.math.BigInteger[] line

Store for Godel numbers of lines of proof

curlin

int curlin

Current line number for lines of proof

Proofin

java.math.BigInteger Proofin

Holds Gödel number of proof (bitstream)

Source

java.math.BigInteger Source

Holds bitstream number to be parsed

binar

javax.swing.JCheckBox binar

radx

int radx

Radix for proof number input (10 or 2)

Constructor Detail

Godel2

public Godel2()

Method Detail

actionPerformed

public void actionPerformed(java.awt.event.ActionEvent e)

respond to down button or change of proof number radix

Specified by:

actionPerformed in interface java.awt.event.ActionListener

mouseClicked

public void mouseClicked(java.awt.event.MouseEvent me)

Paste into upper (proof number) text area on right mouse click

Specified by:

mouseClicked in interface java.awt.event.MouseListener

mouseEntered

public void mouseEntered(java.awt.event.MouseEvent arg0)

Specified by:

mouseEntered in interface java.awt.event.MouseListener

mouseExited

public void mouseExited(java.awt.event.MouseEvent arg0)

Specified by:

mouseExited in interface java.awt.event.MouseListener

mousePressed

public void mousePressed(java.awt.event.MouseEvent arg0)

Specified by:

mousePressed in interface java.awt.event.MouseListener

mouseReleased

public void mouseReleased(java.awt.event.MouseEvent arg0)

Specified by:

mouseReleased in interface java.awt.event.MouseListener

init

public void init()

Set up applet

Overrides:

init in class java.applet.Applet

get2

int get2()

get 2 bits from bitstream

getint

long getint()

Get int from bitstream

Sgetvar

java.math.BigInteger Sgetvar(boolean stk)

Gets variable from input bitstream

Parameters:

stk - - set if variable is to be put on stack

Returns:

bitstream form of variable

Unop

java.math.BigInteger Unop(int op,
                          java.math.BigInteger X1)

Applies a unary operator to a term or formula. Also used for operator part of binary operators.

Parameters:

op - code for operator ' 5,¬ 1

X1 - code for input term or formula

Returns:

code for resulting term or formula

Binop

java.math.BigInteger Binop(java.math.BigInteger X1,
                           int op,
                           java.math.BigInteger X2)

Encodes the result of a binary operator

Parameters:

X1 - first term or formula

op - code for operator

X2 - second term or formula

Returns:

code for operator result

Sterm

java.math.BigInteger Sterm()

gets a term from the proof bitstream

Returns:

encoded form of term

Swff

java.math.BigInteger Swff()

Gets a formula from the proof bitstream

Returns:

encoded form of formula

LowOrder

java.math.BigInteger LowOrder(java.math.BigInteger x,
                              int n)

Gets low order bits of a number

Parameters:

x - Input number

n - Number of bits

Returns:

Low order n bits of x

Varb

java.math.BigInteger Varb(long V)

Converts int form of a variable bitstream form. The terminator is included, but the starting 3 must be added separately if needed.

Parameters:

V - Variable in int form

Returns:

Variable coded as a BigInteger

Glin

java.math.BigInteger Glin()

Gets previously established formula from line number 1st bit 1 -> next 4 bits define number of axiom 1st bit 0 -> encoded line number of proof follows

Returns:

encoded form of formula

Ax1

java.math.BigInteger Ax1()

Axiom 1: WF1⇒(WF2⇒WF1) Gets two formulae

Returns:

resulting line of proof

Ax2

java.math.BigInteger Ax2()

Axiom 2: (WF1⇒(WF2⇒WF3))⇒((WF1⇒WF2)⇒(WF1⇒WF3)) Gets three formulae

Returns:

resulting line of proof

Ax3

java.math.BigInteger Ax3()

Axiom 3 (¬WF2⇒¬WF1)⇒((¬WF2⇒WF1)⇒WF2) Gets two formulae

Returns:

resulting line of proof

Ax4

java.math.BigInteger Ax4()

Axiom 4:∀V WF(V)⇒WF(T) (T is a term free for V in WF) Gets a variable, a term and a formula

Returns:

resulting line of proof

Ax5

java.math.BigInteger Ax5()

Axiom 5: ∀V(WF1⇒WF2)⇒(WF1⇒∀V WF2) (WF1 has no free occurence of V) Gets a variable and two formulae

Returns:

resulting line of proof

MP

java.math.BigInteger MP()

Modus Ponens: WF1,WF1 ⇒ WF2 |- WF2 Gets two formulae

Returns:

resulting line of proof

Gen

java.math.BigInteger Gen()

Generalisation: WF |- ∀V WF Gets a variable and a formula

Returns:

resulting line of proof

Ind

java.math.BigInteger Ind()

Induction: WF(0) ⇒((∀V (WF(V) ⇒ WF(V'))) ⇒ ∀V WF(V)) * Gets a variable and a formula

Returns:

resulting line of proof

proofline

java.math.BigInteger proofline(int c0)

Gets a line of a proof

Parameters:

c0 - intial two bits - previously obtained

Returns:

resulting line of proof

proves

void proves()

Produces Gödel numbers of formulae of proof from Gödel number of proof in Proofin

getAppletInfo

public java.lang.String getAppletInfo()

Overrides:

getAppletInfo in class java.applet.Applet