.. _K3:

********************************
L{K3} - Strong Kleene Logic
********************************

.. figure:: /res/img/Stephen_Cole_Kleene.jpg
    :alt: Photo of Stephen Kleene
    :align: right
    :scale: 50 %
    :target: https://mathshistory.st-andrews.ac.uk/Biographies/Kleene/Kleene_3.jpeg

    Stephen Kleene

L{K3} is a three-valued logic with values V{T}, V{F}, and V{N}. It can be understood
as {@FDE} without the V{B} value.

.. contents:: Contents
  :local:
  :depth: 2

------------------------

.. module:: pytableaux.logics.k3

.. _k3-semantics:
.. _k3-model:

Semantics
=========

.. _k3-truth-values:

Truth Values
------------

Common labels for the values include:

.. include:: include/k3/value-table.rst

.. rubric:: Designated Values

The set of *designated values* for L{K3} is the singleton: { V{T} }

.. _k3-truth-tables:

Truth Tables
------------

.. include:: include/truth_table_blurb.rst

.. truth-tables::
  :operators: Negation, Conjunction, Disjunction

.. rubric:: Defined Operators

.. include:: include/material_defines.rst

.. include:: include/material_tables.rst

.. rubric:: Compatibility Tables

L{K3} does not have separate `Assertion` or `Conditional` operators,
but we include tables and rules for them, for cross-compatibility.

.. truth-tables::
  :include: non_native

.. _k3-predication:

Predication
-----------

Like L{FDE}, L{K3} predication defines a predicate's *extenstion* and
*anti-extension*. The value of a predicated sentence is determined as
follows:

.. include:: include/k3/m.predication.rst

Note, unlike L{FDE}, there is an *exclusivity constraint*
on a predicate's extension/anti-extension. This means that !{ntuple}
cannot be in *both* the extension and the anti-extension of :m:`P`.

Like L{FDE}, there is no *exhaustion constraint*: there are
permissible L{K3} models where some tuple !{ntuple} is in *neither*
the extension nor the anti-extension of some predicate :m:`P`.

.. _k3-quantification:

Quantification
--------------

.. rubric:: Existential

.. include:: include/fde/m.existential.rst

.. rubric:: Universal

.. include:: include/fde/m.universal.rst

.. _k3-consequence:

Consequence
-----------

**Logical Consequence** is defined in terms of the set of *designated* values { V{T} }:

.. include:: include/fde/m.consequence.rst

.. _k3-system:

Tableaux
========

L{K3} tableaux are built similary to L{FDE}.

Nodes
-----

.. include:: include/fde/nodes_blurb.rst

Trunk
-----

.. include:: include/fde/trunk_blurb.rst

.. tableau::
  :build-trunk:
  :prolog:

Closure
-------

In addition to the L{FDE} closure rule, L{K3} includes a `glut` closure rule.
This means a branch closes when a sentence and its negation both appear as
designated nodes on the branch.

.. tableau-rules::
  :group: closure
  :titles:
  :legend:
  :doc:


.. _k3-rules:

Rules
--------

.. include:: include/fde/rules_blurb.rst

.. tableau-rules::
  :docflags:
  :group: operator
  :exclude: non_native

.. tableau-rules::
  :docflags:
  :group: quantifier

.. tableau-rules::
  :docflags:
  :title: Compatibility Rules
  :group: operator
  :include: non_native


Notes
=====

Some notable features of L{K3} include:

* L{K3} is an :term:`extension of` L{FDE}.

* Like L{FDE}, the :term:`Law of Excluded Middle`, and
  :term:`Conditional Identity` fail.

* Some classical validities are valid in L{K3}, such as :term:`Modus Ponens`,
  :term:`Modus Tollens`, :term:`Disjunctive Syllogism`, and :term:`DeMorgan laws`.

References
===========


.. cssclass:: hidden

.. autoclass:: Rules()
  :members:
  :undoc-members: