// // README.txt // // // Source: [R0-v1.0.3 (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.3.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.3.tar.gz Then create the R0 program after switching into the newly created directory: cd R0-v1.0.3 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.