Updating docs

docs/connectives.rst

@@ -5,18 +5,22 @@ Logical connectives create new :doc:`sentences <sentences>` from two or more con
 
 .. _negation:
 
+.. _not:
+
 Negation
 --------
 
 The logical connective ``~`` represents negation. Unlike the other four connectives, this is a unary connective. If ``A`` represents a well formed sentence, then ``~A`` is a well formed sentence. The sentence ``~A`` should be interpreted to mean that ``A`` is not true.
 
-Sentences composed with the ``~`` connective can be proven using the :doc:`not <not>` command. A sentence of the form ``~A`` is logically equivalent to the sentence ``A -> false``. Given ``A`` and ``~A``, one can :ref:`deduce <deduction>` ``false``.
+Sentences composed with the ``~`` connective can be proven using the :doc:`not <not>` command. A sentence of the form ``~A`` is logically equivalent to the sentence ``A -> false``. Given ``A`` and ``~A``, one can :doc:`deduce <deduction>` ``false``.
 
 .. note::
 	Since CORE uses a kind of `intuitionistic logic`_, it is not true in general that ``A | ~A`` for any sentence of the form ``A``. Additionally, ``~~A`` is generally weaker than the sentence ``A``. One can model classical logic by adding the law of excluded middle as an :doc:`axiom <axiom>`.
 
 .. _`intuitionistic logic`: https://en.wikipedia.org/wiki/Intuitionistic_logic
 
+.. _and:
+
 And
 ---
 
@@ -38,14 +42,16 @@ Implies
 
 The logical connective ``->`` represents implication. If ``{A}`` and ``{B}`` represent well formed sentences, then ``{A} -> {B}`` is a well formed sentence. ``{A} -> {B}`` is interpreted to be true if and only if whenever one can prove ``{A}``, one can prove ``{B}``.
 
-Verified sentences ``{A} -> {B}`` and ``{A}`` can be used to :ref:`deduce <deduction>` the verified sentence ``{B}``.
+Verified sentences ``{A} -> {B}`` and ``{A}`` can be used to :doc:`deduce <deduction>` the verified sentence ``{B}``.
+
+.. _biconditional:
 
 Biconditional
 -------------
 
 The logical connective ``<->`` represents the biconditonal connective. If ``{A}`` and ``{B}`` represent well formed sentences, then ``{A} <-> {B}`` is a well formed sentences. ``{A} <-> {B}`` is logically equivalent to ``({A} -> {B}) & ({B} -> {A})``.
 
-Sentences composed with the ``<->`` logical connective can be constructed from implications using the built-in function :doc:`iff <ifffunc>`. Verified sentences ``{A} <-> {B}`` and ``{A}`` can be used to :ref:`deduce <deduction>` the verified sentence ``{B}``. In addition, verified sentences ``{A} <-> {B}`` and ``{B}`` can be used to :ref:`deduce <deduction>` ``{A}``.
+Sentences composed with the ``<->`` logical connective can be constructed from implications using the built-in function :doc:`iff <ifffunc>`. Verified sentences ``{A} <-> {B}`` and ``{A}`` can be used to :doc:`deduce <deduction>` the verified sentence ``{B}``. In addition, verified sentences ``{A} <-> {B}`` and ``{B}`` can be used to :doc:`deduce <deduction>` ``{A}``.
 
 .. _`connective precedence`:
 

docs/deduction.rst

@@ -1,4 +1,52 @@
 Deduction
 =========
 
-Deduction is applied to sentence values containing a top level :ref:`implication <implication>` to prove a conclusion given a premise.
+Deduction is applied to :ref:`sentence values <sentencevalue>` containing a top level :ref:`implication <implication>` to prove a conclusion given a premise.
+
+Syntax
+------
+
+.. code-block::
+
+	[expression value]([expression value], [expression value], ...)
+
+A deduction sentence term begins with a *parent expression* evaluating to a :ref:`sentence value <sentencevalue>`. Following the parent expression is the character ``(``, one or more argument expressions evaluating to sentence values, and the character ``)``. The parent expression sentence value must begin with a top level :ref:`implies <implication>`, :ref:`biconditional <biconditional>`, or :ref:`not <not>` connective.
+
+Each of the argument sentence values are linked together using the :ref:`and <and>` connective. The resulting sentence will be referred to as the *premise sentence*
+
+If the parent expression sentence value is :ref:`verified <sentencevalue>` and every argument sentence value is verified, then the deduction sentence term evaluates to a verified sentence value. Otherwise, it evaluates to an :ref:`unverified sentence value<unverifiedvalue>`.
+
+Implication Deduction
+---------------------
+
+If the parent expression sentence is of the form ``A -> B`` for sentences ``A`` and ``B``, then it is checked that the premise sentence :ref:`trivially implies <trivialimplication>` the sentence ``A``. If not, an error is raised. The deduction sentence term evaluates to the sentence value ``B``.
+
+Biconditional Deduction
+-----------------------
+
+If the parent expression sentence is of the form ``A <-> B`` for sentences ``A`` and ``B``, then it is checked that the premise sentence either :ref:`trivially implies <trivialimplication>` ``A`` or ``B``. If not, an error is raised. If the premise sentence implies ``A``, then the deduction sentence term evaluates to the sentence ``B``, otherwise it evaluates to the sentence value ``A``.
+
+Negation Deduction
+------------------
+
+If the parent expression sentence is of the form ``~A`` for the sentence ``A``, then it is checked that the premise sentence :ref:`trivially implies <trivialimplication>` ``A``. If not, an error is raised. The deduction sentence term evaluates to the sentence ``false``.
+
+Examples
+--------
+
+Suppose ``in`` is a relation; ``A``, ``B``, ``C``, and ``D`` are objects; and ``union_D`` is a sentence variable storing the following sentence value:
+
+.. code-block::
+
+	A in B & B in C -> A in D
+
+If ``A_in_B`` is a sentence variable storing ``A in B`` and ``B_in_C`` is a sentence variable storing ``B in C``, then the expression ``union_D(A_in_B, B_in_C)`` evaluates to the sentence value ``A in D``. 
+
+Suppose ``equal`` is a sentence variable storing the following sentence value:
+
+.. code-block::
+
+	A in C | B in C -> A = B
+
+If ``B_in_C`` is a sentence variable storing ``B in C``, then the expression ``equal(B_in_C)`` evaluates to the sentence value ``A = B``.
+

docs/expressions.rst

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

docs/logic.rst

@@ -12,3 +12,4 @@ The principal data type in CORE is a first-order sentence.
 	Relations <relations>
 	Connectives <connectives>
 	Quantifiers <quantifiers>
+	Trivial Truth <trivialtruth>

docs/sentenceconstants.rst

@@ -0,0 +1,14 @@
+Sentence Constants
+==================
+
+Sentence constants provide a way for the programmer to produce any :ref:`unverified sentence value <unverifiedvalue>` without proof. Sentence constants are most often used for :doc:`predicate substitution <predicatesubstitution>` of :ref:`axiom schema <axiomschema>` or :ref:`proof schema <proofschema>`.
+
+Syntax
+------
+
+.. code-block::
+
+	<[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 ``>``
+

docs/trivialtruth.rst

@@ -0,0 +1,64 @@
+Trivial Truth
+=============
+
+In order to balance convenience for the programmer with precision, CORE has a notion of when a sentence is *trivially true*
+
+Trivially True
+--------------
+
+Suppose ``P`` is a sentence. To determine whether ``P`` is trivially true, search for the first applicable rule from the beginning in the following list:
+
+#. If ``P`` is of the form ``A -> B`` for sentences ``A`` and ``B``, ``P`` is trivially true if ``A`` *trivially implies* ``B``.
+#. If ``P`` is of the form ``A <-> B``, ``P`` is trivially true if ``A`` trivially implies ``B`` and ``B`` trivially implies ``A``
+#. If ``P`` is of the form ``A & B``, ``P`` is trivially true if ``A`` is trivially true and ``B`` is trivially true.
+#. If ``P`` is of the form ``A | B``, ``P`` is trivially true if ``A`` is trivially true or ``B`` is trivially true.
+#. If ``P`` is of the form ``*X(A(X))``, ``P`` is trivially true if ``A`` is trivially true.
+#. If ``P`` is of the form ``~A``, ``P`` is trivially true if ``A`` is trivially false.
+#. If ``P`` is the sentence ``true``, ``P`` is trivially true.
+
+One should interpret the trivial truth of a sentence with or without unbound variables to mean that no matter which objects are substituted for the unbound variables, the sentence can easily be prove true. A case for the trivial truth of a sentence beginning with an :ref:`existential quantifier <existential>` does not exist because not all models may have objects.
+
+Trivially False
+---------------
+
+Suppose ``P`` is a sentence. To determine whether ``P`` is trivially false, search for the first applicable rule from the beginning in the following list:
+
+#. If ``P`` is of the form ``A -> B`` for sentences ``A`` and ``B``, ``P`` is trivially false if ``A`` is trivially true and ``B`` is trivially false.
+#. If ``P`` is of the form ``A <-> B``, ``P`` is trivially false if either ``A -> B`` or ``B -> A`` is trivially false.
+#. If ``P`` is of the form ``A & B``, ``P`` is trivially false if either ``A`` is trivially false or ``B`` is trivially false.
+#. If ``P`` is of the form ``A | B``, ``P`` is trivially false if ``A`` is trivially false and ``B`` is trivially false.
+#. If ``P`` is of the form ``^X(A(X))`` or the form ``*X(A(X))``, ``P`` is trivially false if ``A`` is trivially false.
+#. If ``P`` is of the form ``~A``, ``P`` is trivially false if ``A`` is trivially true.
+#. If ``P`` is the sentence ``false``, ``P`` is trivially false.
+
+One should interpret the trivial falsity of a sentence with or without unbound variables to mean that no matter which objects are substituted for the unbound variables, the sentence can easily be proven false.
+
+.. _trivialimplication:
+
+Trivial Implication
+-------------------
+
+Suppose ``P`` and ``Q`` are sentences. To determine whether ``P`` *trivially implies* ``Q``, search for the first applicable rule from the beginning of the following list. At most one rule is applied, so if a rule is applied and the rule does not give trivial implication, then ``P`` does not trivially imply ``Q``.
+
+#. If ``P`` and ``Q`` have mismatching numbers of unbound variables or predicates, then ``P`` does not trivially imply ``Q``.
+#. If ``P`` is of the form ``A | B``, ``P`` trivially implies ``Q`` if ``A`` trivially implies ``Q`` and ``B`` trivially implies ``Q``.
+#. If ``Q`` is of the form ``A & B``, ``P`` trivially implies ``Q`` if ``P`` trivially implies ``A`` and ``P`` trivially implies ``B``.
+#. If ``P`` is of the form ``~A`` and ``Q`` is of the form ``~B``, ``P`` trivially implies ``Q`` if ``B`` trivially implies ``A``.
+#. If ``P`` is of the form ``A -> B`` and ``Q`` is of the form ``C -> D``, then ``P`` trivially implies ``Q`` if ``C`` trivially implies ``A`` and ``B`` trivially implies ``D``.
+#. If ``P`` is of the form ``*X(A(X))`` and ``Q`` is of the form ``*X(B(X)``, then ``P`` trivially implies ``Q`` if ``A`` trivially implies ``B``.
+#. If ``P`` is of the form ``^X(A(X))`` and ``Q`` is of the form ``^X(B(X))``, then ``P`` trivially implies ``Q`` if ``A`` trivially implies ``B``.
+#. If ``P`` is of the form ``A <-> B`` and ``Q`` is of the form ``C <-> D``, then apply any of the following rules:
+	- If ``A`` trivially implies ``C``, ``C`` trivially implies ``A``, ``B`` trivially implies ``D``, and ``D`` trivially implies ``B``, then ``P`` trivially implies ``Q``.
+	- If ``A`` trivially implies ``D``, ``D`` trivially implies ``A``, ``B`` trivially implies ``C``, and ``C`` trivially implies ``B``, then ``P`` trivially implies ``Q``.
+	- If ``C`` trivially implies ``D`` and ``D`` trivially implies ``C``, then ``P`` trivially implies ``Q``.
+#. If ``Q`` is of the form ``A <-> B``, ``P`` trivially implies ``Q`` if ``A`` trivially implies ``B`` and ``B`` trivially implies ``A``.
+#. If ``P`` and ``Q`` are identical :doc:`relation <relations>` :ref:`sentence terms <sentenceterm>`, then ``P`` trivially implies ``Q``.
+#. If ``P`` and ``Q`` are identical :doc:`predicate <predicates>` :ref:`sentence terms <sentenceterm>`, then ``P`` trivially implies ``Q``.
+#. If ``P`` is trivially false, then ``P`` trivially implies ``Q``.
+#. If ``Q`` is trivially true, then ``P`` trivially implies ``Q``.
+#. Otherwise, apply any of the following rules:
+	- If ``P`` is of the form ``A & B`` and either ``A`` trivially implies ``Q`` or ``B`` trivially implies ``Q``, then ``P`` trivially implies ``Q``.
+	- If ``Q`` is of the form ``A | B`` and either ``P`` trivially implies ``A`` or ``P`` trivially implies ``B``, then ``P`` trivially implies ``Q``.
+
+Regardless of the number of unbound variables of ``A`` and ``B``, one should interpret "``A`` trivially implies ``B``" to mean that no matter which objects are substituted for the unbound variables, one can easily prove that ``A`` implies ``B``.
+