//
// README.txt
//
//
// Source: [R0-v1.0.0 (doi: 10.4444/100.10.3)]
//
// Copyright (c) 2017 Owl of Minerva Press GmbH. All rights reserved.
// Written by Ken Kubota ().
//
// This file is part of the publication of the mathematical logic R0.
// For more information, visit:
//
This file is subject to change and shall be extended continuously.
Please check for a newer version at: http://doi.org/10.4444/100.10.3
A tutorial on the R0 proof language can be found in the file 'tutorial.r0i.txt'.
A full treatment of R0 shall be announced at: http://doi.org/10.4444/100.10.1
For the references, please see: http://doi.org/10.4444/100.111
For questions and suggestions, send an email to mail@kenkubota.de after
reading the material provided online via the link above.
0. DESCRIPTION
This work contains the software implementation of the mathematical logic R0, a
further development of Peter B. Andrews' logic Q0. The syntactic features
provided by R0 are type variables (polymorphic type theory), the binding of
type variables with the abstraction operator and single variable binder λ (type
abstraction), and (some of) the means necessary for dependent types (dependent
type theory).
A short introduction can be found on pp. 11 f. of "Mathematical Formulae",
available online at: http://doi.org/10.4444/100.10.2
For more information, please visit: http://doi.org/10.4444/100.10
1. INSTALLATION
This software was created on an Apple MacBook Air with OS X Version 10.11.6, a
Unix-based operating system, and should run on any Unix system with no or minor
modifications. If you want to use the program to create PDF files, installation
of LaTeX and pandoc is required.
In the following, the installation of R0 on a Mac is described.
1.1. Installation of R0
Download the archive R0-v1.0.0.tar.gz from http://doi.org/10.4444/100.10.3
(license restrictions apply) and extract the files either by double-clicking
the archive or entering the following commands within the terminal:
cd ~/Downloads/
tar xzvf R0-v1.0.0.tar.gz
Then create the R0 program after switching into the newly created directory:
cd R0-v1.0.0
make
Now you can run the program.
1.2. Installation of software for creating PDF files (optional)
First, download and install the LaTeX package from: http://www.tug.org/mactex/
Second, install the program pandoc (for interpreting markdown syntax created by
R0 for PDF output).
One way is installing MacPorts from https://www.macports.org and compiling and
installing pandoc with the command
port -N install pandoc
The other way is to download and install pandoc directly from: http://pandoc.org
2. RUNNING
R0 can be invoked simply by typing
./R0
After invocation, enter
:h
or
:help
for help, and
:q
or
:quit
to quit the program.
Specifying an argument will make R0 processing this file as input, e.g., the
standard definitions in file basics.r0 with
./R0 basics.r0.txt
In order to continue interactively after having processed the file, add a
hyphen (for standard input) as last argument, since the arguments are processed
in the given order:
./R0 basics.r0.txt -
With ':d' you can display the definitions, and with ':q' quit the program.
Usually, no further axioms are allowed except the four axioms for R0 in file
'axioms.r0.txt'. In order to allow further axioms (e.g., for demonstration
purposes), add the option '--allow-additional-axioms':
./R0 --allow-additional-axioms basics.r0.txt -
The invocations most often used are implemented in the Makefile. For example,
the last command above can be abbreviated by entering
make run
To create a text file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.txt
To create and automatically display the text file, enter
make A5211.r0.out.txt && less $_
Enter 'q' to quit.
To create a HTML file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.html
To create and automatically open the HTML file (OS X only), enter
make A5211.r0.out.html && open -a Finder $_
Opening HTML files generated by R0 will cause a request to the server
cdn.mathjax.org.
To create a PDF file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.pdf
To create and automatically open the PDF file (OS X only), enter
make A5211.r0.out.pdf && open -a Finder $_
To create a PDF file containing all proofs, run
make math
From the very beginning, the R0 program was designed to be able to re-read not
only its printed terms, but also whole proofs. (For terms, this concept was
defined independently as the notion of 'Pollack-consistency' by Freek Wiedijk
[Wiedijk, 2012, p. 85].) In order to process all proofs two times, with the
output of the first run as the input of the second, enter
make check
The process would stop immediately if the outputs of two runs differ.
Generally, definitions once introduced cannot be removed or redefined
(implementing the notion of 'faithfulness' as defined by Mark Adams in [Adams,
2016, p. 21].) After starting the program with
./R0 basics.r0.txt -
the attempt to undefine the definition of truth by entering
:= T
or to redefine the definition of truth by entering
:= T F
will result in an error message, unless the option '--allow-definition-removal'
was set explicitly on program invocation:
./R0 --allow-definition-removal basics.r0.txt -
The exit code of the R0 program is
0 if no error occured
1 if one error occured
2 if two errors occured
...
253 if 253 or more errors occured
254 if there are temporary definitions left
255 if an internal error occured
To run the tutorial, enter
make tutorial
The file 'tutorial.r0i.out.txt' will contain the generated tutorial including
the results and give further explanation on how to create proofs with R0.