Oak Tutorial

Learn Oak!

Installation

Oak is available for download as a .tar.gz file (see the main page). Extract the file somewhere. If you like, add the extracted folder to your system's PATH variable so that you can run Oak from anywhere just by typing oak.

Oak requires the Ruby programming language, so if you get an error about Ruby not being installed, go here to find out how to install it.

Usage

Oak is a command-line application which takes a proof file as input, and tells you whether or not the proof is correct.
  oak [-v] [filename]
      -v  print the version number of Oak

Getting started

Let's get started with Oak. To begin, we'll create a one-line proof. Make a new file called "proof.oak" and open it with a text editor. In the file, put the following line:
x or not x
Save your file, then go to the command line, and from the folder where you created your file, run:
  oak proof.oak
You should see the following output:
proof.oak: processing line 1 
all lines accepted
proof successful!
This tells you that your one-line "proof" was correct. Since x or not x is a simple tautology, Oak was able to accept it outright, without needing any further justification from you.

Now let's see the output for an incorrect proof. Change proof.oak to the following:
x or y
We get:
proof.oak: processing line 1 
line 1: invalid derivation "x or y"
This tells you that your proof is not correct. That's because the statement x or y is not valid (universally true): if x and y are both false, then the statement is false.

axiom

Any statement can be accepted by making it an axiom. Change your file to:
axiom for all x, p(x)
The command axiom simply accepts the accompanying statement without proof. Oak reports that the proof is correct, and notes that the proof file contained an axiom.
proof.oak: processing line 1 
all lines accepted
1 axiom in proof.oak
proof successful!

so

Once a statement is accepted, it goes into something called the context. The command so uses the current context to prove its accompanying statement. Try the following:
axiom every man is mortal
axiom Socrates is a man
so Socrates is mortal
You get:
proof.oak: processing line 1 2 3 
all lines accepted
2 axioms in proof.oak
proof successful!
Above, the first two statements go into the context. Then so uses them to prove the third statement. After so proves its accompanying statement, it clears the context, and then puts the accompanying statement in it. The context after a so therefore contains only the accompanying statement. For example:
axiom x and y
so x
so not not x
so y
gives
proof.oak: processing line 1 2 3 4 
line 4: invalid derivation "y"
After the second line, the context contains only x. That's enough to prove the third line, after which the context contains only not not x. The fourth line then fails.

Labels and by

It is possible to give a statement a label, and refer to it using by.
axiom A1: x and y
x by A1
y by A1
Note that labelled statements do not enter the context. They can only be accessed by their labels.
axiom A1: x and y
so x
proof.oak: processing line 1 2 
error at line 2: nothing for "so" to use
Labels can be written either after commands (as above) or before them (as below).
A1: axiom x
A2: axiom y
x and y by A1, A2
proof.oak: processing line 1 2 3 
all lines accepted
2 axioms in proof.oak
proof successful!

now blocks

A now block creates a new context. Statements inside the block use the new context. At the end of the block, its context is added to the outer context.
axiom A: for all x, p(x)
axiom B: for all x, p(x) implies q(x)

p(i) by A
so q(i) by B
now
  p(j) by A
  so q(j) by B
end
so q(i) and q(j)
Here, the so in the now block uses only the inner context p(j), and not the outer context q(i). However, it can still access labelled statements with by. At the end of the now block, its final context q(j) is added to the outer context, which then contains both q(i) and q(j).

suppose

axiom A1: x or y
suppose not x
  so y by A1
end
so (not x) implies y
The suppose command creates a new context containing the accompanying statement, in this case not x. When a suppose ends, it takes its final context, makes it conditional on the supposition that started the suppose, and adds the result to the outer context. Here, the inner context y is added to the outer context as (not x) implies y. The so in the last line then uses the outer context to prove its accompanying statement.

The suppose command can be used for proof by contradiction.
axiom A1: for all x, p(x) implies q(x)
axiom A2: for no x, q(x)

suppose for some x, p(x)
  so q(x) by A1
  so contradiction by A2
end
so there is no x with p(x)

Comments

Oak supports both line comments and block comments.
/#
  Here is a block comment at the beginning of the proof.
  ...
#/

x or not x  # this is a tautology

Conditions

Conditions can be placed on quantified variables, using the operators in, with, and such that, in the manner below. The operators with and such that are synonymous.
axiom for all x in S, p(x)
axiom for all x with p(x), q(x)
axiom for all x such that q(x), r(x)
so for all x in S, r(x)

take

With a take block, you can prove something about an arbitrary variable meeting some condition, and then generalize the result to all variables meeting that condition.
axiom A1: for all x in S, x is in T
axiom A2: for all x in T, x is in U

take any x in S
  so x is in T by A1
  so x is in U by A2
end
so for all x in S, x is in U

assume

While working on your proof, you might want to temporarily leave a "gap" to be filled in later. If you use axiom for these gaps as well as for actual premises of your proof, it could become hard to keep track of which are which. For this reason, Oak has the command assume. It's like axiom, but generates a warning that your proof is incomplete. Thus, you can use it for "gaps", and as long as it is present, Oak will remind you that your proof is not finished.

assume can also be used in places that axiom cannot, e.g. in a suppose block.
suppose x
  assume y  # will prove this later!
end
so x implies y
proof.oak: processing line 1 2 3 4 
all lines accepted
proof.oak: assumption on line 2
proof incomplete due to assumptions

proof blocks

Instead of using so or by to justify a statement, you can provide a proof block. In the block, you can use thesis as a shortcut for the statement to be proved.
A1: axiom for all x, p(x) implies q(x)
A2: axiom for all x, q(x) implies p(x)

theorem 1: for all x, p(x) iff q(x)
proof
  take any x
    p(x) implies q(x) by A1
    q(x) implies p(x) by A2
    so p(x) iff q(x)
  end
  so thesis
end

p(a) iff q(a) by theorem 1
proof.oak: processing line 1 2 4 6 7 8 9 10 11 12 14 
all lines accepted
2 axioms in proof.oak
proof successful!
Actually, the "theorem" above is simple enough that Oak can prove it directly from the axioms (try it!); the proof block here is just for the sake of the example.

include

As your proof gets bigger, you may wish to split it into multiple files. You can use include to access one file from another. Create a new file "axioms.oak" with the following content:
axiom A1: for all x, p(x)
axiom A2: for all x, q(x)
Now put the following in your original file proof.oak.
include "axioms.oak"

p(a) by A1
q(a) by A2
proof.oak: processing line 1 
axioms.oak: processing line 1 2 
proof.oak: processing line 3 4 
all lines accepted
2 axioms in axioms.oak
proof successful!

Axiom schemas

In addition to axiom statements, Oak supports axiom schemas. An axiom schema is a "meta statement" which can be instantiated as multiple statements. An axiom schema must begin with for all meta, a quantifier which ranges over expressions. The body of for all meta must be enclosed in backticks, denoting a statement pattern to be instantiated.
induction: axiom schema for all meta φ,
    `if φ{x:0} and 
        for all x, φ implies φ{x:x+1},
     then
        for all x, φ`

assume p(0) or q(0)
assume for all x, (p(x) or q(x)) implies (p(x+1) or q(x+1))
so for all x, p(x) or q(x) by induction
Here, the meta variable φ is instantiated as the expression p(x) or q(x). In the schema, φ{x:0} means "φ with all occurrences of x replaced by 0", and φ{x:x+1} means "φ with all occurrences of x replaced by x+1".

Free variable checks are also possible. Below, free(p,φ) is true iff p occurs free in φ (unbound by a quantifier).
comprehension: axiom schema
  for all meta p,φ such that not free(p,φ),
    `for some p, for all n in N, p(n) iff φ`

# succeeds
for some p, for all n in N, p(n) iff not q(n) by comprehension

# fails
for some p, for all n in N, p(n) iff not p(n) by comprehension
proof.oak: processing line 1 6 9 
error at line 9: could not instantiate schema
The first instantiation succeeds, but in the second one, φ is not p(n), so p occurs free in φ, and the instantiation fails.

Any questions?

Feel free to contact Tim Smith with any questions or comments.

You can also post to the issue tracker on Oak's page at GitHub.