Oak Tutorial

Learn Oak!

Installation

Oak is available for download as an archive file (see the main page). Extract the file somewhere. If you like, add the extracted folder to your system's PATH variable so 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] [-c] [-w] [filename]
  -v  print the version number of Oak
  -c  check for unneeded citations
  -w  wait for validity (does not change proof outcome)

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 for no x, 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 by using the operator where (or its alias such that).
axiom for all x where p(x), q(x)
axiom for all x such that q(x), r(x)
so for all x, p(x) implies r(x)
In addition to where and such that, there are "shortcut" operators for common conditions. These include in and not in, inequalities (like <), and set relations (like ⊆).
for some A ⊆ B, p(A)
for all i,j > 0, q(i,j)
for some x in S and y in T, r(x,y)
for at most one c ≠ d, s(c)
You can also use arbitrary predicates as conditions. For example, instead of
for all x, whale(x) implies mammal(x)
you can write
for all whale x, mammal(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 1 assumption
A series of statements can be assumed with begin assume and end assume.
# just assume these for now
begin assume
1: x
2: y
end assume

x and y by 1,2

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.

define

For your convenience, statements beginning with an existential quantifier bind variables so that they can be used in subsequent lines. Variables bound in this way can later be rebound. Below, x is bound on line 1, then rebound on line 3. Thus, the x on line 2 is a different x than the one on line 4.
assume for some x, p(x)
so p(x)
assume for some x, q(x)
so q(x)
To guarantee that a variable keeps its original binding, use define. Variables bound with define cannot be rebound in the same scope. This ensures that a variable you bind at the beginning of your proof will have the same binding at the end.
assume define x such that p(x)
so p(x)
assume for some x, q(x)  # error
Notice that the define above is preceded by an assume. To define a variable with a condition, you must show that such a variable exists, just as if you had used for some instead of define.

Tie-ins

When you bind a variable, you can give it a tie-in. Tie-ins are statements about variables that "follow them around", meaning you do not have to cite them when you use the variable. The operator with creates a tie-in.
axiom A1: there is an n with p(n)
axiom A2: for all x, p(x) implies q(x)
q(n) by A2  # no need to cite A1
Here, the variable n is given the tie-in p(n). Henceforth, whenever n is used, p(n) is automatically included. Thus, line 3 does not need to cite line 1.

In addition to with, the "shortcut" condition operators (e.g. in) also create tie-ins, when binding a variable. The use of a predicate as a condition (e.g. for all integer n) also creates a tie-in. The condition operator where (and its alias such that) does not create a tie-in.
take any integer n in S such that p(n)
  integer(n)  # succeeds
  n is in S  # succeeds
  p(n)  # fails, needs a citation
end
For performance reasons, tie-ins cannot include quantifiers.

Command-line options

Oak has some handy command-line options.
-c  check for unneeded citations
This option notifies you of any citations in your proof that can be reduced. For example, in the last line of the proof below, you only need to cite A1, not A2. Calling Oak with -c gives the subsequent output.
axiom A1: for all x, p(x)
axiom A2: for all x, q(x)
p(c) by A1,A2
line 3: citation can be reduced from:
  A1, A2
to:
  A1
The -c option slows down the proof checker, so don't use it all the time, just when you want to clean up your citations.
-w  wait for validity (does not change proof outcome)
Sometimes, when checking a proof, Oak will stop at some line and say "could not determine validity of derivation". This means the prover exceeded the "amount of work" allowed for that line, so your proof failed. If you pass -w, Oak will "keep working" to try to determine if the line in question is valid. However, this is only for your edification, and does not change the proof outcome. Even if -w finds that the line is valid, Oak will not accept that line until you fix it (e.g. by breaking it into smaller steps).

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!

exit

The exit command skips the rest of the proof. It outputs a notice that the remaining lines were skipped and marks the proof as incomplete.
axiom for all x, p(x)
so p(c)
exit
# under construction, not ready to be checked yet
q(c)
proof.oak: processing line 1 2 3
exit at line 3: skipping remaining lines
all lines accepted prior to exit
1 axiom in proof.oak
proof incomplete due to exit

Parameterized tie-ins

In addition to tie-ins created when binding a variable, there are parameterized tie-ins, created with the tie-in command. These "free-floating" tie-ins apply not just to one variable, but to any term matching a pattern.
axiom A1: for all x, p(x) implies q(x)
tie-in `p(x)` with `p(x) implies q(x)` for all x by A1

suppose p(c)
  so q(c) # no need to cite A1 here
end
Here, a tie-in is created with the pattern p(x) and body p(x) implies q(x), parameterized by x. Afterwards, any occurrence of the pattern will trigger the tie-in, causing the body to be included.

When using tie-in to create a parameterized tie-in, you must prove that the body holds for all values of its parameters. For example, to create the tie-in
tie-in `x+y` with `x+y = y+x` for all x,y
you must prove
for all x,y, x+y = y+x
For performance reasons, parameterized tie-ins cannot instantiate quantified variables.

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 create an issue on Oak's page at GitHub.