.TH OPERETTA 1 "23 Feb 21" "Operetta version 0.1"
.SH NAME
operetta \- simple formal logic evaluator

.SH SYNOPSIS
\fBoperetta\fP <file> [--version] [--help] 

.SH DESCRIPTION
Operetta is a simple way to evaluate logical claims.
Is it true that P implies P or Q? Operetta will tell you.

.SH OPTIONS
\fB--help\fP
\-\- Displays usage info.

\fB--version\fP
\-\- Displays version info, and license information.

.SH SYNTAX
Operetta's syntax is fairly flexible. It is line based, so every proposition must be on its own line.
It is whitespace dependent, so indents must be used only where applicable.
Every line in operetta is split into two components--a proposition, and a justification.
The proposition is essentially a statement. The base unit of a proposition is a variable,
which is a letter or word that has a truth value. A variable is written as any letter or word in
ALL CAPS. Suppose P stands for "it is raining".
Writing [ P ] then means "it is raining." [ ~P ] means "it is not raining." The other component,
the justification, is introduced by [ : ] or [ | ], following the proposition. A complete line looks
like this: [ P | pr ], and is read "P is a premise." Most logical claims start with premises--things
that are accepted to be true. From these premises, you may derive other truths. Suppose that you have
[ P->Q | pr ], read as "P implies Q is a premise." If P implies Q, then whenever P is true, Q is too.
Since P necessitates Q, you can derive Q from P. So, if the following two premises hold:
[ P->Q | pr ], [ P | pr ], then [ Q | ->e x, x ] is true. Here, the justification is not a premise,
it is the deductive rule called implication elimination. Implication elimination is a rule that
justifies the right hand side of an proposition, if the proposition as a whole is true and the left hand side is true.
Most rules follow a simple form: [ xe / xi ], where x is some connection in a proposition, i stands for introduction, and e stands for elimination.
In this way, you can intuit the correct rule for a given application. Following the rule are two numbers,
the lines that the justification references.

.SH SYMBOLS
\fB^\fP
\-\- Conjunction, or AND.

\fBv\fP
\-\- Disjunction, or OR.

\fB->\fP
\-\- Implication.

\fBu<->\fP
\-\- Bi-implication.

\fBu~ or !\fP
\-\- Negation, or NOT.

\fBu? or x\fP
\-\- Contradiction.

.SH RULES
\fBpr\fP
\-\- Premise. Always true, can only be defined in the top-most scope.

\fBas\fP
\-\- Assumption. Always true, but only in the new scope it creates.

\fB^e\fP
\-\- Conjunction elimination. Cite a proposition A^B. May justify either A or B.

\fB^i\fP
\-\- Conjunction introduction. Cite a proposition A and a proposition B. May justify A^B.

\fBvi\fP
\-\- Disjunction introduction. Cite a proposition A. May justify AvB, or BvA.

\fB->e\fP
\-\- Implication elimination. Cite a proposition A->B and a proposition A. May justify B.

\fB->i\fP
\-\- Implication introduction. Cite an assumption A, and a result of that assumption B. May justify A->B.

\fBu?i or xi\fP
\-\- Contradiction introduction. Cite a proposition A and a proposition ~A. May justify ? or x.

\fBu~i or !i\fP
\-\- Negation introduction. Cite an assumption A and a contradiction resulting from that assumption, B. May justify ~A.

.SH AUTHOR
Developed and maintained by Kai Stevenson.
See git.aberrantflux.xyz/operetta.git for the latest version
of the software.

.SH "SEE ALSO"
vi(1)