Adding two more documentation pages

docs/brackets.rst

@@ -0,0 +1,59 @@
+Expression Brackets
+===================
+
+One must often apply :ref:`axiom schema <axiomschema>` and :ref:`proof schema <proofschema>` to specific predicates. This is accomplished using expression brackets. Expression brackets allow the substitution of :doc:`predicates <predicates>` for unbound predicates in verified and unverified sentences.
+
+Syntax
+------
+
+.. code-block::
+
+	[parent expression][[predicate expression], [predicate expression], ...]
+
+An expression brackets term begins with a parent expression followed by a ``[`` character, a comma-separated list of predicate expressions, and a closing ``]`` character.
+
+The parent expression value must evaluate to a sentence value with at least one unbound :doc:`predicate <predicates>`. Each predicate expression must evaluate to a sentence value. The n-th predicate sentence is substituted for the n-th unbound predicate in the parent sentence, and the expression brackets term evaluates to the result. The n-th predicate sentence must have the same number of unbound objects as the number of arguments of the n-th unbound predicate of the parent sentence.
+
+The expression brackets term evaluates to a verified sentence if and only if the parent sentence is verified.
+
+Examples
+--------
+
+Suppose ``excluded_middle`` is a variable storing the following verified sentence for unbound predicate ``P()``:
+
+.. code-block::
+
+	P | ~P
+
+Then we can use expression brackets to apply this result to any predicate depending on no arguments. For example, suppose ``X`` and ``Y`` are objects, and ``<`` is a :doc:`relation <relations>`. Then the following expression:
+
+.. code-block::
+
+	excluded_middle[<: X < Y>]
+
+Evaluates to the following verified sentence:
+
+.. code-block::
+
+	X < Y | ~X < Y
+
+Suppose that ``=`` is a relation and that ``replace`` is a variable storing the following verified sentence for unbound predicate ``P(1)``:
+
+.. code-block::
+
+	*X*Y(X = Y -> (P(X) <-> P(Y)))
+
+If ``Z``, ``W``, and ``V`` are objects and ``<`` is a :doc:`relation <relations>`, then the following expression:
+
+.. code-block::
+
+	replace[<Q: Q < V>](Z, W)
+
+Evaluates to the following verified sentence:
+
+.. code-block::
+
+	Z = W -> (Z < V <-> W < V)
+
+Note that :doc:`object substitution <objectsubstitution>` is applied to the result of the expression brackets term.
+

docs/expressions.rst

@@ -12,6 +12,7 @@ Expressions allow the programmer to combine expression values to obtain new expr
 	Pipe Operator <pipe>
 	Deduction <deduction>
 	Sentence Constants <sentenceconstants>
+	Expression Brackets <brackets>
 
 .. _`expressionvalues`:
 

docs/predicates.rst

@@ -5,6 +5,8 @@ A predicate is a symbol which may reference :doc:`objects <objects>` in a :doc:`
 
 A *sentence definition* is a sentence used to define a predicate. If a predicate depends on ``n`` arguments, the sentence definition has ``n`` unbound variables. A predicate applied to ``n`` objects is a sentence logically equivalent to substituting in order those ``n`` objects for the unbound variables in the sentence definition.
 
+.. _predicateidentifier:
+
 A predicate identifier must begin with either a letter or an underscore, and may subsequently contain letters, digits, and underscores.
 
 Predicates are quantified only by :ref:`axiom schema <axiomschema>` and :ref:`proof schema <proofschema>`.

docs/sentenceconstants.rst

@@ -10,5 +10,32 @@ Syntax
 
 	<[predicate identifier]([number of arguments]), ..., [object identifier], ... : [sentence]>
 
-A sentence constant expression term begins with the character ``<``. What follows is a list of labels for unbound predicates and unbound objects. After this list is the character ``:``, and a sentence depending on the identifiers in the preceding list. The sentence constant expression is ended with the character ``>``
+A sentence constant expression term begins with the character ``<``. What follows is a list of labels for unbound predicates and unbound objects. After this list is the character ``:``, and a sentence depending on the identifiers in the preceding list. The sentence constant expression is ended with the character ``>``. The list of unbound predicate and object labels may optionally be empty, in which case the ``:`` character directly follows the ``<`` character. 
+
+An unbound predicate in the list of identifiers is denoted using a :ref:`predicate identifier <predicateidentifier>`, parentheses, and the number of arguments. If the number of arguments is zero, then the number of arguments may be omitted; however, in this case the parentheses must still be present, otherwise the identifier will be added as an unbound object instead of an unbound predicate.
+
+An unbound object in the list of identifiers is denoted using an :ref:`object identifier <objectidentifier>`.
+
+Unbound objects and predicates may be listed in any order, but the n-th unbound predicate of the output sentence value is the n-th listed unbound predicate. Likewise, the n-th unbound object of the output sentence value is the n-th listed unbound object.
+
+The output is an :ref:`unverified sentence value <unverifiedvalue>` storing the given sentence with the given unbound predicates and unbound objects.
+
+Examples
+--------
+
+If ``in`` is a :doc:`relation <relations>`, then the following expression:
+
+.. code-block::
+
+	<A, B: A in B | B in A>
+
+Evaluates to an unverified sentence with two unbound objects ``A`` and ``B`` storing the sentence ``A in B | B in A``.
+
+The following expression:
+
+.. code-block::
+
+	<P(1): ^X(P(X) & ~P(X))>
+
+Evaluates to an unverified sentence with no unbound objects and one unbound predicate ``P(1)`` storing the sentence ``^X(P(X) & ~P(X))``. It does not matter that the sentence is clearly not true since the output of the expression is an *unverified* sentence value.