From e54ac9f3f0405206331e1901e3ca1e62f084381a Mon Sep 17 00:00:00 2001 From: been-jamming Date: Mon, 11 Jul 2022 15:29:54 -0700 Subject: [PATCH] Adding two more documentation pages --- docs/brackets.rst | 59 ++++++++++++++++++++++++++++++++++++++ docs/expressions.rst | 1 + docs/predicates.rst | 2 ++ docs/sentenceconstants.rst | 29 ++++++++++++++++++- 4 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 docs/brackets.rst diff --git a/docs/brackets.rst b/docs/brackets.rst new file mode 100644 index 0000000..c9628ee --- /dev/null +++ b/docs/brackets.rst @@ -0,0 +1,59 @@ +Expression Brackets +=================== + +One must often apply :ref:`axiom schema ` and :ref:`proof schema ` to specific predicates. This is accomplished using expression brackets. Expression brackets allow the substitution of :doc:`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 `. 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 `. 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 `, then the following expression: + +.. code-block:: + + replace[](Z, W) + +Evaluates to the following verified sentence: + +.. code-block:: + + Z = W -> (Z < V <-> W < V) + +Note that :doc:`object substitution ` is applied to the result of the expression brackets term. + diff --git a/docs/expressions.rst b/docs/expressions.rst index b24b3ee..fd53050 100644 --- a/docs/expressions.rst +++ b/docs/expressions.rst @@ -12,6 +12,7 @@ Expressions allow the programmer to combine expression values to obtain new expr Pipe Operator Deduction Sentence Constants + Expression Brackets .. _`expressionvalues`: diff --git a/docs/predicates.rst b/docs/predicates.rst index a11caa2..d54523b 100644 --- a/docs/predicates.rst +++ b/docs/predicates.rst @@ -5,6 +5,8 @@ A predicate is a symbol which may reference :doc:`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 ` and :ref:`proof schema `. diff --git a/docs/sentenceconstants.rst b/docs/sentenceconstants.rst index 225f988..3941302 100644 --- a/docs/sentenceconstants.rst +++ b/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 `, 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 `. + +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 ` storing the given sentence with the given unbound predicates and unbound objects. + +Examples +-------- + +If ``in`` is a :doc:`relation `, then the following expression: + +.. code-block:: + + + +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:: + + + +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.