Godel is an attempt to fix the problems I have been facing while learning mathematics. It’s an attempt to define math books which are interactive and allows readers to solve problems which aren’t just choose one of the options. More importantly it should check if my proofs are right. So as a first step, Godel has a proof assistant which allows users to build proofs for the exercises in it.
Godel proof assistant is built on the foundations of Calculus of construction. It is a programming language with very strict and powerful type system. Godel proof language contains two mini languages, one is the Expression Language which is sort of the kernel of Godel proof assistant and there is a Defintion Language which is useful to clearly state the mathematical structures and theorems.
In Godel, every expression has Type associated with it and Types are first class entities, ie., You can define function which takes and gives out Types as result. One of the basic constructs in Godel is a function. Arguments to the function has to be annotated with a type, while the body of the function’s type is infered. Godel is purely functional language, there is no notion of statements/actions, so the body of a function is a single expression. One of the simplest function defintion looks like this
λA: *, λx: A, x
The above defintion is a family of identity functions. You could get a identity function of a particular type, by passing the type as the first argument to it. So the function defined above take a type A and takes a value x of type A and gives back x itself. But what is the type of the function. Its defined like this.
∀A: *, ∀x: A, A
Its read like for all type A forall x of type A it returns A. Godel is dependent typed, ie., the value of the argument could in essence define what the body’s type is. The above function could never be expressed in a language which treats type as first class but doesn’t have the dependent types built in. Since the type of the identity function it returns is dependent on the value of the argument to the function.
We could ask what is the type of the above type. We take for the simplicity as a kind *. Which denotes the type of the types, which is exactly what we did before in the definition of family of identity functions.
In order to make the functions useful, we should be able to apply the functions to specific arguments. Normal juxta-positioning the argument and functions means a function application. Like this,
λA: *, λx: A, (λy: A, y) x
Paranthesis above is used to disambiguate, everything associates to right in Godel. Thus the following will not type check
λA: *, λx: A, λy: A, y x
as that is equivalent to
λA: *, λx: A, λy: A, (y x)
Since, y is not a function which takes A. Though you could ask we don’t know what type A stand for yet. But we definitely can be sure that A cannot be a function which takes a value of type A itself as a parameter, other wise A would be infintely long. So in short, Godel disallows application of arguments to anything which it clearly dont know as function.
The entire syntax of Godel’s expression language could be summarized as
\<variable> : <type>, <body> or alternatively λ<variable> : <type>, body\/<variable> : <type>, <body> or alternatively ∀<variable> : <type>, bodyThe definition language allows us to build definitions/theorems/lemmas and prove them or take some of them as axioms. Constructively a proof is a program satisfying a type. So the types tell us what we are proving and the program is really a proof.
We could define definitions like this,
definition <name> : <type> = <expression>.
or
definition <name> = <expression>.
Godel definitions don’t distinguish between definition / theorem / lemma, they are just syntactic sugar over the expression language, where as the axiom is a definition of an object of a type for which we don’t have proof. Axioms are defined like this
axiom <name> : <type>.
Note that axioms don’t have a body/expression satisfying the type.
We can define some of the basic propositional connectives as follows.
definition imply = λA: *, λB: *, ∀x: A, B.
definition false = ∀A: *, A.
definition not = λA: *,
(imply A false).
definition or = λA: *, λB: *, ∀C: *,
(imply (imply (imply A C) (imply B C)) C).
definition and = λA: *, λB: *, ∀C: *,
(imply (imply (imply A B) C) C).
And can prove some constructive tautologies like this.
theorem not-not-a-imply-a : ∀A: *, (imply A (not (not A))) =
λA: *, λa: A,
λnot-a: (not A),
(not-a a).
Godel repl can be run as (expressions)
nodejs js/Main.js
And to run a program (defintions)
nodejs js/Main.js <files>