diff --git a/docs/connectives.rst b/docs/connectives.rst index 9ec1ba9..e4f1dc2 100644 --- a/docs/connectives.rst +++ b/docs/connectives.rst @@ -5,18 +5,22 @@ Logical connectives create new :doc:`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 ` command. A sentence of the form ``~A`` is logically equivalent to the sentence ``A -> false``. Given ``A`` and ``~A``, one can :ref:`deduce ` ``false``. +Sentences composed with the ``~`` connective can be proven using the :doc:`not ` command. A sentence of the form ``~A`` is logically equivalent to the sentence ``A -> false``. Given ``A`` and ``~A``, one can :doc:`deduce ` ``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 `. .. _`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 ` the verified sentence ``{B}``. +Verified sentences ``{A} -> {B}`` and ``{A}`` can be used to :doc:`deduce ` 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 `. Verified sentences ``{A} <-> {B}`` and ``{A}`` can be used to :ref:`deduce ` the verified sentence ``{B}``. In addition, verified sentences ``{A} <-> {B}`` and ``{B}`` can be used to :ref:`deduce ` ``{A}``. +Sentences composed with the ``<->`` logical connective can be constructed from implications using the built-in function :doc:`iff `. Verified sentences ``{A} <-> {B}`` and ``{A}`` can be used to :doc:`deduce ` the verified sentence ``{B}``. In addition, verified sentences ``{A} <-> {B}`` and ``{B}`` can be used to :doc:`deduce ` ``{A}``. .. _`connective precedence`: diff --git a/docs/deduction.rst b/docs/deduction.rst index 1601c11..69f88d1 100644 --- a/docs/deduction.rst +++ b/docs/deduction.rst @@ -1,4 +1,52 @@ Deduction ========= -Deduction is applied to sentence values containing a top level :ref:`implication ` to prove a conclusion given a premise. +Deduction is applied to :ref:`sentence values ` containing a top level :ref:`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 `. 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 `, :ref:`biconditional `, or :ref:`not ` connective. + +Each of the argument sentence values are linked together using the :ref:`and ` connective. The resulting sentence will be referred to as the *premise sentence* + +If the parent expression sentence value is :ref:`verified ` 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`. + +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 ` 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 ` ``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 ` ``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``. + diff --git a/docs/expressions.rst b/docs/expressions.rst index 5f3f789..b24b3ee 100644 --- a/docs/expressions.rst +++ b/docs/expressions.rst @@ -11,6 +11,7 @@ Expressions allow the programmer to combine expression values to obtain new expr Object Substitution Pipe Operator Deduction + Sentence Constants .. _`expressionvalues`: diff --git a/docs/logic.rst b/docs/logic.rst index 2ea7ebf..1d51ae8 100644 --- a/docs/logic.rst +++ b/docs/logic.rst @@ -12,3 +12,4 @@ The principal data type in CORE is a first-order sentence. Relations Connectives Quantifiers + Trivial Truth diff --git a/docs/sentenceconstants.rst b/docs/sentenceconstants.rst new file mode 100644 index 0000000..225f988 --- /dev/null +++ b/docs/sentenceconstants.rst @@ -0,0 +1,14 @@ +Sentence Constants +================== + +Sentence constants provide a way for the programmer to produce any :ref:`unverified sentence value ` without proof. Sentence constants are most often used for :doc:`predicate substitution ` of :ref:`axiom schema ` or :ref:`proof schema `. + +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 ``>`` + diff --git a/docs/trivialtruth.rst b/docs/trivialtruth.rst new file mode 100644 index 0000000..d05279c --- /dev/null +++ b/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 ` 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 ` :ref:`sentence terms `, then ``P`` trivially implies ``Q``. +#. If ``P`` and ``Q`` are identical :doc:`predicate ` :ref:`sentence terms `, 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``. +