Note

This document is an initial stub as part of a work in progress.

Tables

Lexical Tables

Parser Symbols

	polish (default)	standard (default)
Assertion	T	*
Negation	N	~
Conjunction	K	&
Disjunction	A	V
Material Conditional	C	>
Material Biconditional	E	<
Conditional	U	$
Biconditional	B	%
Possibility	M	P
Necessity	L	N
Existential	S	X
Universal	V	L
Existence	J	!
Identity	I	=
Predicates	F, G, H, O	F, G, H, O
Constants	m, n, o, s	a, b, c, d
Variables	x, y, z, v	x, y, z, v
Atomics	a, b, c, d, e	A, B, C, D, E

Python attributes

Comparison across types is aided by some shared creation methods like .first(), as well a the LexType class, which contains bookkeeping information such as a list of all lexical classes.

For example, we can examine the spec attribute for an item of each lexical type with this code:

rows = [
    (item, item.spec)
    for item in (
        member.cls.first()
        for member in LexType
    )
]

spec

A spec is a tuple built from integers, strings. These can nest to become complex, but only with tuples built from integers and strings, and so on. The spec should contain all the information to recreate the object, so long as you know its original type.

Type	Item	spec
Predicate	F	(0, 0, 1)
Constant	a	(0, 0)
Variable	x	(0, 0)
Quantifier	∃	('Existential',)
Operator	⚬	('Assertion',)
Atomic	A	(0, 0)
Predicated	Fa	((0, 0, 1), (('Constant', (0, 0)),))
Quantified	∃xFx	('Existential', (0, 0), ('Predicated', ((0, 0, 1), (('Variable', (0, 0)),))))
Operated	⚬A	('Assertion', (('Atomic', (0, 0)),))

We can use the spec as arguments to create the item. For example:

>>> from pytableaux.lang import Predicated
>>> Predicated((0, 0, 1), (('Constant', (0, 0)),))
<Sentence: Fa>

ident

The ident attribute is similar to spec, but also contains the type information. Thus an ident attribute is just a 2tuple, or ordered pair of the type name, and the spec.

Type	Item	ident
Predicate	F	('Predicate', (0, 0, 1))
Constant	a	('Constant', (0, 0))
Variable	x	('Variable', (0, 0))
Quantifier	∃	('Quantifier', ('Existential',))
Operator	⚬	('Operator', ('Assertion',))
Atomic	A	('Atomic', (0, 0))
Predicated	Fa	('Predicated', ((0, 0, 1), (('Constant', (0, 0)),)))
Quantified	∃xFx	('Quantified', ('Existential', (0, 0), ('Predicated', ((0, 0, 1), (('Variable', (0, 0)),)))))
Operated	⚬A	('Operated', ('Assertion', (('Atomic', (0, 0)),)))

We can pass the ident tuple as a single argument to LexicalAbc to create the item. For example:

>>> from pytableaux.lang import LexicalAbc, Predicate, Quantifier
>>> LexicalAbc(('Predicate', (0, 0, 1))) == Predicate(0, 0, 1)
True
>>> LexicalAbc(('Quantifier', ('Existential',))) is Quantifier.Existential
True
>>> LexicalAbc(('Quantified', ('Existential', (0, 0), ('Predicated', ((0, 0, 1), (('Variable', (0, 0)),))))))
<Sentence: ∃xFx>

sort tuple

A sort_tuple is a flat tuple of integers that encodes less information overall, but should still be unique for distinct items. It might not contain enough information to recreate an object, but it provides a convenient method for comparing, sorting, and hashing items. This works across different types, for example between a predicate and a quantifier, without the risk of confusing one for the other.

Type	Item	sort_tuple
Predicate	F	(10, 0, 0, 1)
Constant	a	(20, 0, 0)
Variable	x	(30, 0, 0)
Quantifier	∃	(40, 0)
Operator	⚬	(50, 10)
Atomic	A	(60, 0, 0)
Predicated	Fa	(70, 10, 0, 0, 1, 20, 0, 0)
Quantified	∃xFx	(80, 40, 0, 30, 0, 0, 70, 10, 0, 0, 1, 30, 0, 0)
Operated	⚬A	(90, 50, 10, 60, 0, 0)

For example:

>>> from pytableaux.lang import Constant, Variable
>>> c = Constant(0,0)
>>> v = Variable(0,0)
>>> c.spec == v.spec
True
>>> v > c
True