API Reference

Subclasses

There are seven proposition classes in total, with Proposition being the base class of all proposition types. Each subclass is a dataclass type, which means instances can be created and be treated like a regular dataclass type:

import classical_logic as cl

u = cl.And(cl.Predicate('P'), cl.Predicate('Q'))
assert u == cl.prop('P & Q')
assert u.left == cl.prop('P')
assert u.right == cl.prop('Q')

v = cl.Or(left=cl.Predicate(name='P'), right=cl.Predicate(name='Q'))
assert v == cl.prop('P | Q')
assert v.left == cl.prop('P')
assert v.right == cl.prop('Q')

w = cl.Not(cl.Predicate('P'))
assert w == cl.prop('~P')
assert w.inner == cl.prop('P')
assert w.inner.name == 'P'

The following table gives the subclass constructors and the proposition it corresponds to:

Class Constructor	Proposition
And(left, right)	P & Q
Iff(left, right)	P <-> Q
Implies(left, right)	P -> Q
Not(inner)	~P
Predicate(name)	P
Or(left, right)	P | Q

---

And dataclass

Represents a logical conjunction, which is interpreted to be true just in the case that both of its operands are true.

Truth table of P & Q:

P	Q	P & Q
T	T	T
T	F	F
F	T	F
F	F	F

Attributes:

Name	Type	Description
left	Proposition	Left conjunct.
right	Proposition	Right conjunct.

---

Iff dataclass

Represents a logical biconditional, which is interpreted to be true just in the case that both of its operands share the same truth value.

Truth table of P & Q:

P	Q	P <-> Q
T	T	T
T	F	F
F	T	F
F	F	T

Attributes:

Name	Type	Description
left	Proposition	Left operand.
right	Proposition	Right operand.

---

Implies dataclass

Represents a logical material conditional, which is interpreted to be true just in the case its first operand is false or both of its operands are true.

Truth table of P -> Q:

P	Q	P -> Q
T	T	T
T	F	F
F	T	T
F	F	T

Attributes:

Name	Type	Description
left	Proposition	Antecedent.
right	Proposition	Consequent.

---

Not dataclass

Represents a logical negation, which is interpreted to be true just in the case that its operand is false.

Truth table of ~P:

P	~P
T	F
F	T

Attributes:

Name	Type	Description
inner	Proposition	Inner operand.

---

Predicate dataclass

Represents an predicate in formal logic. Currently, classical-logic only supports nullary (0-argument) predicates, which are used to serve as propositional variables.

When creating a new instance, if the given name is not valid, a ValueError is raised.

Attributes:

Name	Type	Description
name	str	The name of the predicate.

---

Proposition

Represents a logical proposition. This type serves as the base class for all proposition types in the classical-logic package.

Operation Summary

The following table summarizes the special operations on this class:

Operation	Description
p[i]	Gets the component at index i of p. Raises IndexError if index is out of range.
iter(p)	Returns an iterator over the (immediate) components of p.
~p	Returns Not(p).
p & q	Returns And(p, q).
p | q	Returns Or(p, q).
p(mapping) p(**kwargs)	Interprets p. See Interpreting for more information.
p == q	Checks if p and q are structurally equal.
p != q	Checks if p and q are not structurally equal.
hash(p)	Returns the hash value of p.
str(p)	Returns a parsable string representation of p. See Formatting for more information.
repr(p)	Returns the canonical string representation of p. See Formatting for more information.
format(p, spec)	Returns a formatted string representation of p. See Formatting for more information.

Note: bool(p) is not supported as the truth value of a proposition is ambiguous.

degree() -> int abstractmethod

Returns the number of immediate component propositions this proposition contains.

For example, a negation (~P) has a degree of 1 because it's a unary (two-place) operation, which takes one operand.

A conjunction (P & Q) and a disjunction (P | Q) both have degrees of 2, because they are both binary (two-place) operations.

A predicate (P) has a degree of 0, since it doesn't contain any components.

Example

import classical_logic as cl


# Degree of a predicate is 0
assert cl.prop('P').degree() == 0

# Degree of a negation is 1
assert cl.prop('~P').degree() == 1

# The outermost connective determines the degree
assert cl.prop('~~~P').degree() == 1
assert cl.prop('~(~~P)').degree() == 1

# Degree of a binary (two-place) operation is 2
assert cl.prop('P & Q').degree() == 2

# The outermost connective determines the degree
assert cl.prop('~P & Q').degree() == 2
assert cl.prop('~(P & Q)').degree() == 1

# Remember: (P & Q) & R == P & Q & R
assert cl.prop('(P & Q) & R').degree() == 2
assert cl.prop('P & Q & R').degree() == 2

iff(other: Proposition) -> Iff

Returns Iff(self, other).

implies(other: Proposition) -> Implies

Returns Implies(self, other).

---

Or dataclass

Represents a logical disjunction, which is interpreted to be true just in the case that at least one of its operands is true.

Truth table of P | Q:

P	Q	P | Q
T	T	T
T	F	T
F	T	T
F	F	F

Attributes:

Name	Type	Description
left	Proposition	Left disjunct.
right	Proposition	Right disjunct.

---

prop(text: str) -> Proposition

Parses a proposition.

Raises a ValueError if text contains invalid syntax.

Please see the prop() and props() section in the User Guide for more details.

Example: Example Usage

```python
import classical_logic as cl

u = cl.prop('P')
v = cl.prop('P & Q | R')
w = cl.prop('(P -> Q) <-> R')
```

---

props(text: str) -> tuple[Proposition, ...]

Parses zero or more propositions, separated by commas. (Trailing commas are not allowed.)

Raises a ValueError if text contains invalid syntax.

Please see the prop() and props() section in the User Guide for more details.

Example: Example Usage:

```python
import classical_logic as cl

# Some use cases:
ps = cl.props('P, P -> Q, Q')  # Returns tuple of 3 propositions
p, q = cl.props('P, Q')  # Unpacks tuple into p and q
p, q, r, s = cl.props('P, Q, R, S')

# Trailing commas are not allowed, raises ValueError
#   p, q = cl.props('P, Q,')

# Empty/whitespace strings not allowed, raises ValueError
#   ps = cl.props('  ')
```