.. _P3:

***********************************
L{P3} - Post 3-valued Logic
***********************************

.. figure:: /res/img/Emil_Leon_Post.jpg
    :alt: Photo of Emil Post
    :align: right
    :scale: 50 %
    :target: https://en.wikipedia.org/wiki/File:Emil_Leon_Post.jpg

    Emil Post

Emil Post's three-valued logic, with values V{T}, V{F}, and V{N}. It features
a deviant negation that performs a *cyclic shift* in value.

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

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

.. module:: pytableaux.logics.p3

.. _p3-semantics:
.. _p3-model:

Semantics
=========

.. _p3-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{P3} is the singleton: { V{T} }

.. _p3-truth-tables:

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

.. include:: include/truth_table_blurb.rst

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

.. rubric:: Defined Operators

Conjunction :s:`&` is defined in terms of :s:`~` and :s:`V` in a standard way:

.. sentence::

  A & B := ~(~A V ~B)

Given the behavior of :s:`~`, however, this yields a non-standard table:

.. truth-tables::
  :operators: Conjunction

.. include:: include/material_defines.rst

.. include:: include/material_tables.rst

.. rubric:: Compatibility Tables

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

.. truth-tables::
  :include: non_native

.. _p3-predication:

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

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

.. _p3-consequence:

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

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

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

.. _p3-system:

Tableaux
========

L{P3} 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
-------

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

.. _p3-rules:

Rules
--------

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

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

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

Notes
=====


References
==========

- E. L. Post `Introduction to a General Theory of Elementary Propositions`_
  American Journal of Mathematics, vol. 43. 1921.

- Rescher, Nicholas. `Many-valued Logic`_. United Kingdom, McGraw-Hill, 1969.

.. _Introduction to a General Theory of Elementary Propositions:
    https://www.jstor.org/stable/2370324?origin=crossref&seq=1#metadata_info_tab_contents

.. _Many-valued Logic: https://www.google.com/books/edition/_/ZyTXAAAAMAAJ?hl=en

.. cssclass:: hidden

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