## 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:xSave your file, then go to the command line, and from the folder where you created your file, run:ornotx

oak proof.oakYou 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:

xWe get:ory

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**

The commandaxiomforallx, p(x)

**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:
You get:axiomeverymanismortalaxiomSocratesisamansoSocratesismortal

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:
givesaxiomxandysoxsonotnotxsoy

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**

**by**

.
Note that labelled statements do not enter the context. They can only be accessed by their labels.axiomA1: xandy xbyA1 ybyA1

axiomA1: xandysox

proof.oak: processing line 1 2 error at line 2: nothing for "so" to useLabels can be written either after commands (as above) or before them (as below).

A1:axiomx A2:axiomy xandybyA1, A2

proof.oak: processing line 1 2 3 all lines accepted 2 axioms in proof.oak proof successful!

**now**

blocks

A **now**

**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.
Here, theaxiomA:forallx, p(x)axiomB:forallx, p(x)impliesq(x) p(i)byAsoq(i)byBnowp(j)byAsoq(j)byBendsoq(i)andq(j)

**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**

**suppose**

TheaxiomA1: xorysupposenotxsoybyA1endsonotximpliesy

**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.
axiomA1:forallx, p(x)impliesq(x)axiomA2:fornox, q(x)supposeforsomex, p(x)soq(x)byA1socontradictionbyA2endsofornox, p(x)

## Comments

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

## Conditions

Conditions can be placed on quantified variables by using the operator**where**

(or its alias **such**** ****that**

).
In addition toaxiomforallxwherep(x), q(x)axiomforallxsuchthatq(x), r(x)soforallx, p(x)impliesr(x)

**where**

and **such**** ****that**

, there are "shortcut" operators for common conditions. These include **in**

and **not** **in**

, inequalities (like `<`

), and set relations (like ⊆).
You can also use arbitrary predicates as conditions. For example, instead offorsomeA ⊆ B, p(A)foralli,j > 0, q(i,j)forsomexinSandyinT, r(x,y)foratmostonec ≠ d, s(c)

you can writeforallx, whale(x)impliesmammal(x)

forallwhale x, mammal(x)

**take**

With a **take**

**take**

block, you can prove something about an arbitrary variable meeting some condition, and then generalize the result to all variables meeting that condition.
axiomA1:forallxinS, xisinTaxiomA2:forallxinT, xisinUtakeanyxinSsoxisinTbyA1soxisinUbyA2endsoforallxinS, xisinU

**assume**

While working on your proof, you might want to temporarily leave a "gap" to be filled in later. If you use **assume**

**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.
supposexassumey # will prove this later!endsoximpliesy

proof.oak: processing line 1 2 3 4 all lines accepted proof.oak: assumption on line 2 proof incomplete due to 1 assumptionA series of statements can be assumed with

**begin**** ****assume**

and **end** **assume**

.
# just assume these for nowbeginassume1: x 2: yendassumexandyby1,2

**proof**

blocks

Instead of using **proof**

**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:axiomforallx, p(x)impliesq(x) A2:axiomforallx, q(x)impliesp(x) theorem 1:forallx, p(x)iffq(x)prooftakeanyx p(x)impliesq(x)byA1 q(x)impliesp(x)byA2sop(x)iffq(x)endsothesisendp(a)iffq(a)bytheorem 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, **define**

`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.
To guarantee that a variable keeps its original binding, useassumeforsomex, p(x)sop(x)assumeforsomex, q(x)soq(x)

**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.
Notice that theassumedefinexsuchthatp(x)sop(x)assumeforsomex, q(x) # error

**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.
Here, the variableaxiomA1:thereisannwithp(n)axiomA2:forallx, p(x)impliesq(x) q(n)byA2 # no need to cite A1

`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.
For performance reasons, tie-ins cannot include quantifiers.takeanyinteger ninSsuchthatp(n) integer(n) # succeeds nisinS # succeeds p(n) # fails, needs a citationend

## Command-line options

Oak has some handy command-line options.-c check for unneeded citationsThis 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.

axiomA1:forallx, p(x)axiomA2:forallx, q(x) p(c)byA1,A2

line 3: citation can be reduced from: A1, A2 to: A1The -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**

**include**

to access one file from another. Create a new file "axioms.oak" with the following content:
Now put the following in your original file proof.oak.axiomA1:forallx, p(x)axiomA2:forallx, q(x)

include"axioms.oak" p(a)byA1 q(a)byA2

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**

**exit**

command skips the rest of the proof. It outputs a notice that the remaining lines were skipped and marks the proof as incomplete.
axiomforallx, p(x)sop(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.
Here, a tie-in is created with the patternaxiomA1:forallx, p(x)impliesq(x)tie-in`p(x)`with`p(x)impliesq(x)`forallxbyA1supposep(c)soq(c) # no need to cite A1 hereend

`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
you must provetie-in`x+y`with`x+y = y+x`forallx,y

For performance reasons, parameterized tie-ins cannot instantiate quantified variables.forallx,y, x+y = y+x

## 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:Here, the meta variableaxiomschemaforallmetaφ, `ifφ{x:0}andforallx, φimpliesφ{x:x+1},thenforallx, φ`assumep(0)orq(0)assumeforallx, p(x)orq(x)impliesp(x+1)orq(x+1)soforallx, p(x)orq(x)byinduction

`φ`

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:axiomschemaforallmetap,φsuchthatnotfree(p,φ), `forsomep,forallninN, p(n)iffφ` # succeedsforsomep,forallninN, p(n)iffnotq(n)bycomprehension # failsforsomep,forallninN, p(n)iffnotp(n)bycomprehension

proof.oak: processing line 1 6 9 error at line 9: could not instantiate schemaThe first instantiation succeeds, but in the second one,

`φ`

is **not** p(n)

, so `p`

occurs free in `φ`

, and the instantiation fails.