First-order Formulas

Generic

First-order Formulas#

The following class diagram summarizes the inheritance hierarchy. Next, we are going to describe the occurring classes starting at the top.

Generic Types#

logic1.firstorder.formula.α = TypeVar('α', bound='AtomicFormula')#: A type variable denoting a type of atomic formulas with upper bound logic1.firstorder.atomic.AtomicFormula.

logic1.firstorder.formula.τ = TypeVar('τ', bound='Term')#: A type variable denoting a type of terms with upper bound logic1.firstorder.atomic.Term.

logic1.firstorder.formula.χ = TypeVar('χ', bound='Variable')#: A type variable denoting a type of variables with upper bound logic1.firstorder.atomic.Variable.

logic1.firstorder.formula.σ = TypeVar('σ')#: A type variable denoting a type that is admissible in addition to terms as a dictionary entry in Formula.subs(). Instances of type σ that are passed to Formula.subs() must not contain any variables. A typical example is setting σ to int in the theory of real closed fields.

Formula Base Class#

class logic1.firstorder.formula.Formula[source]#

Bases: Generic[α, τ, χ, σ]

This abstract base class implements representations of and methods on first-order formulas recursively built using first-order operators:

Boolean operators:
1. Truth values \(\top\) and \(\bot\)
2. Negation \(\lnot\)
3. Conjunction \(\land\) and discjunction \(\lor\)
4. Implication \(\longrightarrow\)
5. Bi-implication (syntactic equivalence) \(\longleftrightarrow\)
Quantifiers \(\exists x\) and \(\forall x\), where \(x\) is a variable.

As an abstract base class, Formula cannot be instantiated. Nevertheless, it implements a number of methods on first-order formualas. The methods implemented here are typically syntactic in the sense that they do not need to know the semantics of the underlying theories.

Note

Formula depends on three type variables α, τ, χ for the types ocurring atomic formula, terms, and variables, respectively. They appear in type annotations used by static type checkers but are not relevant for the either interactive use or use as a library.

property op: type[Self]#: Operator. This property can be used with instances of subclasses of Formula. It yields the respective subclass.

property args: tuple[Any, ...]#

The arguments of a formula as a tuple.

See also

Equivalent.lhs – left hand side of a logical \(\longleftrightarrow\)
Equivalent.rhs – right hand side of a logical \(\longleftrightarrow\)
Implies.lhs – left hand side of a logical \(\longrightarrow\)
Implies.rhs – right hand side of a logical \(\longrightarrow\)
Not.arg – argument formula of a logical \(\neg\)
QuantifiedFormula.arg – argument formula of a quantifier \(\exists\) or \(\forall\)
QuantifiedFormula.var – variable of a quantifier \(\exists\) or \(\forall\)

The properties op and args are useful for decomposing and reconstructing formulas, using the invariant f = f.op(*f.args), which holds for all formulas f. This approach has been adopted from the SymPy project:

>>> from logic1.firstorder import *
>>> f = And(Implies(F, T), Or(T, Not(T)))
>>> # The class of f:
>>> f.op
<class 'logic1.firstorder.boolean.And'>
>>> # The argument tuple of f:
>>> f.args
(Implies(F, T), Or(T, Not(T)))
>>> # The invariant:
>>> f == f.op(*f.args)
True
>>> # Construction of a new formula using components of f:
>>> f.op(Equivalent(T, T), *f.args)
And(Equivalent(T, T), Implies(F, T), Or(T, Not(T)))

abstract __init__(*args: object) → None[source]#: This abstract base class is not supposed to have instances itself. Technically this is enforced via this abstract initializer.

~, &, |, >>, <<

__invert__(other: Formula) → Formula[source]#

__and__(other: Formula) → Formula[source]#

__or__(other: Formula) → Formula[source]#

__rshift__(other: Formula) → Formula[source]#

__lshift__(other: Formula) → Formula[source]#

The subclass constructors Not, And, Or, Implies are alternatively available as overloaded operators ~, &, |, >>, respectively:

>>> from logic1.firstorder import *
>>> (F >> T) &  (T |  ~ T)
And(Implies(F, T), Or(T, Not(T)))

Furthermore, f1 << f2 constructs Implies(f2, f1). Note that the Operator Precedence of Python applies and cannot be changed. In particular, the originally bitwise logical operators bind stronger than the comparison operators so that, unfortunately, equations and inequalities must be parenthesized:

>>> from logic1.theories import RCF
>>> a, b, x = RCF.VV.get('a', 'b', 'x')
>>> f = Ex(x, (x >= 0) & (a*x + b == 0))
>>> f
Ex(x, And(x >= 0, a*x + b == 0))

__le__(other: Formula[α, τ, χ, σ]) → bool[source]#

Returns True if self should be sorted before or is equal to other.

See also

AtomicFormula.__le__() – comparison of atomic formulas

__str__() → str[source]#: Representation of the Formula used in printing.

all(ignore: Iterable[χ] = {}) → Formula[α, τ, χ, σ][source]#

Universal closure. Universally quantifiy all variables occurring free in self, except the ones in ignore.

>>> from logic1.theories.RCF import *
>>> a, b, x = VV.get('a', 'b', 'x')
>>> f = Ex(x, And(x >= 0, a*x + b == 0))
>>> f.all()
All(b, All(a, Ex(x, And(x >= 0, a*x + b == 0))))

See also

All – universal quantifier
ex() – existential closure
quantify() – add quantifier prefix

as_latex() → str[source]#

LaTeX representation as a string, which can be used elsewhere.

>>> from logic1.theories.RCF import *
>>> x, y = VV.get('x', 'y')
>>> f = All(x, Or(x < 1, x - 1 == 0, x > 1))
>>> f.as_latex()
'\\forall x \\, (x - 1 < 0 \\, \\vee \\, x - 1 = 0 \\, \\vee \\, x - 1 > 0)'

See also

_repr_latex_() – LaTeX representation for Jupyter notebooks

atoms() → Iterator[α][source]#

An iterator over all instances of AtomicFormula occurring in self.

Recall that the truth values T and F are not atoms:

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = Or(And(x == 0, y == 0, T), And(x == 0, y == z, z != 0))
>>> list(f.atoms())
[x == 0, y == 0, x == 0, y - z == 0, z != 0]

The overall number of atoms:

>>> sum(1 for _ in f.atoms())
5

Count numbers of occurrences for each occurring atom using a Counter:

>>> from collections import Counter
>>> Counter(f.atoms())
Counter({x == 0: 2, y == 0: 1, y - z == 0: 1, z != 0: 1})

Recall the Python builtin next():

>>> iter = (x == 0).atoms()
>>> next(iter)
x == 0
>>> next(iter)
Traceback (most recent call last):
...
StopIteration

bvars(quantified: frozenset[χ] = frozenset({})) → Iterator[χ][source]#

An iterator over all bound occurrences of variables in self. Each variable is reported once for each term that it occurs in.

>>> from logic1.theories.RCF import *
>>> a, x, y, z = VV.get('a', 'x', 'y', 'z')
>>> f = All(y, And(Ex(x, a + x == y), Ex(z, x + y == a + x)))
>>> list(f.bvars())
[x, y, y]

Note that following the common definition in logic, occurrence refers to the occurrence in a term. Appearances of variables as a quantified variables without use in any term are not considered.

The parameter quantified specifies variable to be considered bound in addition to those that are explicitly quantified in self.

See also

fvars() – all occurring free variables
qvars() – all quantified variables
Term.vars() – all occurring variables

count_alternations() → int[source]#

Count the number of quantifier alternations.

Returns the maximal number of quantifier alternations along a path from the root to a leaf of the expression tree. Occurrence of quantified variables is not checked, so that quantifiers with unused variables are counted.

>>> from logic1.theories import RCF
>>> x, y, z = RCF.VV.get('x', 'y', 'z')
>>> f = Ex(x, (x == y) & All(x, Ex(y, Ex(z, x == x + 1))))
>>> f.count_alternations()
2

In this example the following path has two alternations, one from Ex to All and another one from All to Ex:

Ex ———— And ———— All ———— Ex ———— Ex ———— x == y + 1

depth() → int[source]#

The depth of a formula is the maximal length of a path from the root to a truth value or an AtomicFormula in the expression tree:

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = Ex(x, And(x == y, All(x, Ex(y, Ex(z, x == y + 1)))))
>>> f.depth()
5

In this example the the following path has the maximal length 5:

Ex ———— And ———— All ———— Ex ———— Ex ———— x == y + 1

Note that for this purpose truth values and AtomicFormula are considered to have depth 0.

ex(ignore: Iterable[χ] = {}) → Formula[α, τ, χ, σ][source]#

Existential closure. Existentially quantifiy all variables occurring free in self, except the ones in ignore.

>>> from logic1.theories.RCF import *
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> f = All(x, And(a < x, x + a - b < 0))
>>> f.ex(ignore={c})
Ex(b, Ex(a, All(x, And(a - x < 0, a - b + x < 0))))

See also

Ex – existential quantifier
all() – universal closure
quantify() – add quantifier prefix

fvars(quantified: frozenset[χ] = frozenset({})) → Iterator[χ][source]#

An iterator over all free occurrences of variables in self. Each variable is reported once for each term that it occurs in.

The parameter quantified specifies variable to be considered bound in addition to those that are explicitly quantified in self.

>>> from logic1.theories.RCF import *
>>> a, x, y, z = VV.get('a', 'x', 'y', 'z')
>>> f = All(y, And(Ex(x, a + x - y == 0), Ex(z, x + y == a)))
>>> list(f.fvars())
[a, a, x]

See also

bvars() – all occurring bound variables
qvars() – all quantified variables
Term.vars() – all occurring variables

static is_all(f: Formula[α, τ, χ, σ]) → TypeIs[All[α, τ, χ, σ]][source]#
static is_and(f: Formula[α, τ, χ, σ]) → TypeIs[And[α, τ, χ, σ]][source]#
static is_atomic(f: Formula[α, τ, χ, σ]) → TypeIs[α][source]#
static is_boolean_formula(f: Formula[α, τ, χ, σ]) → TypeIs[BooleanFormula[α, τ, χ, σ]][source]#
static is_equivalent(f: Formula[α, τ, χ, σ]) → TypeIs[Equivalent[α, τ, χ, σ]][source]#
static is_ex(f: Formula[α, τ, χ, σ]) → TypeIs[Ex[α, τ, χ, σ]][source]#
static is_false(f: Formula[α, τ, χ, σ]) → TypeIs[_F[α, τ, χ, σ]][source]#
static is_implies(f: Formula[α, τ, χ, σ]) → TypeIs[Implies[α, τ, χ, σ]][source]#
static is_not(f: Formula[α, τ, χ, σ]) → TypeIs[Not[α, τ, χ, σ]][source]#
static is_or(f: Formula[α, τ, χ, σ]) → TypeIs[Or[α, τ, χ, σ]][source]#
static is_quantified_formula(f: Formula[α, τ, χ, σ]) → TypeIs[QuantifiedFormula[α, τ, χ, σ]][source]#
static is_true(f: Formula[α, τ, χ, σ]) → TypeIs[_T[α, τ, χ, σ]][source]#: Type narrowing isinstance() tests for respective subclasses of Formula.

static is_term(t: τ | σ) → TypeIs[τ][source]#
static is_variable(x: object) → TypeIs[χ]#: Type narrowing isinstance() tests for firstorder.atomic.Term and firstorder.atomic.Variable, respectively,

matrix() → tuple[Formula[α, τ, χ, σ], Prefix[χ]][source]#

The matrix of a prenex formula is its quantifier free part. Its prefix is a double ended queue holding blocks of quantifiers.

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = All(x, All(y, Ex(z, x - y == z)))
>>> m, B = f.matrix()
>>> m
x - y - z == 0
>>> B
Prefix([(<class 'logic1.firstorder.quantified.All'>, [x, y]),
        (<class 'logic1.firstorder.quantified.Ex'>, [z])])

If self is not prenex, then the leading quantifiers are considered and the matrix will not be quantifier-free:

>>> h = All(x, All(y, Implies(x != 0, Ex(z, x * z == y))))
>>> m, B = h.matrix()
>>> m
Implies(x != 0, Ex(z, x*z - y == 0))
>>> B
Prefix([(<class 'logic1.firstorder.quantified.All'>, [x, y])])

See also

Prefix – a quantifier prefix
quantify() – add quantifier prefix
to_pnf() – prenex normal form

quantify(prefix: Prefix[χ]) → Formula[α, τ, χ, σ][source]#

Add quantifier prefix.

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = x - y == z
>>> p = Prefix((All, [x, y]), (Ex, [z]))
>>> f.quantify(p)
All(x, All(y, Ex(z, x - y - z == 0)))

See also

Prefix – a quantifier prefix
all() – universal closure
ex() – existential closure
matrix() – prenex formula without quantifier prefix

qvars() → Iterator[χ][source]#

An iterator over all quantified variables in self.

In the following example, z is a quantified variable but not a bound variable:

>>> from logic1.theories.RCF import *
>>> a, b, c, x, y, z = VV.get('a', 'b', 'c', 'x', 'y', 'z')
>>> f = All(y, And(Ex(x, a == y), Ex(z, a == y)))
>>> list(f.qvars())
[y, x, z]

See also

bvars() – all occurring bound variables
fvars() – all occurring free variables
Term.vars() – all occurring variables

_repr_latex_() → str[source]#

A LaTeX representation for Jupyter notebooks. In general, the underlying method as_latex() should be used instead.

Due to a current limitation of Jupyter, the LaTeX representration is cut off after at most 5000 characters.

See also

as_latex() – LaTeX representation

simplify() → Formula[α, τ, χ, σ][source]#

Fast basic simplification. The result is equivalent to self. The following first-order simplifications are applied:

Truth values:
1. Evaluate Not(F) to T, and evaluate Not(T) to F.
2. Evaluate And(..., F, ...) to F and Or(..., T, ...) to T.
3. Evaluate Implies(F, arg) and Implies(arg, T) to T.
4. Remove T from And(..., T, ...) and F from Or(..., F, ...).
5. Transform Implies(T, arg) into arg, and transform Implies(arg, F) into Not(arg).
6. Transform Equivalent(T, arg) and Equivalent(arg, T) into arg, and transform Equivalent(F, arg), Equivalent(arg, F) into Not(arg).
Nested operators:
1. Transform Not(Not(arg)) into arg.
2. Transform And(..., And(*args), ...) into And(..., *args, ...). The same for Or instead of And.
Equal arguments:
1. Transform And(..., arg, ..., arg, ...) into And(..., arg, ...). The same for Or instead of And.
2. Evaluate Implies(arg, arg) to T. The same for Equivalent instead of Implies.
Sort arg_1, ..., arg_n within And(arg_1, ..., arg_n) using a canonical order. The same for Or instead of And.

Overloading of AtomicFormula provides a hook for theories to extend simplify() to atomic formulas.

See also

simplify methods of classes derived from AtomicFormula within various theories:

RCF.atomic.AtomicFormula.simplify – real closed fields
Sets.atomic.AtomicFormula.simplify – theory of Sets

More powerful simplifiers provided by various theories:

RCF.simplify.simplify()
– real closed fields, standard simplifier based on implicit theories
Sets.simplify.simplify()
– sets, standard simplifier based on implicit theories

subs(substitution: dict[χ, τ | σ]) → Self[source]#

Substitution of terms for variables.

>>> from logic1.theories.RCF import *
>>> a, b, x = VV.get('a', 'b', 'x')
>>> f = Ex(x, x == a)
>>> f.subs({x: a})
Ex(x, a - x == 0)
>>> f.subs({a: x})
Ex(G0001_x, -G0001_x + x == 0)
>>> g = Ex(x, _ & (b == 0))
>>> g.subs({b: x})
Ex(G0002_x, And(Ex(G0001_x, -G0001_x + G0002_x == 0), x == 0))

to_nnf(to_positive: bool = True, _not: bool = False) → Formula[α, τ, χ, σ][source]#

Convert to Negation Normal Form.

A Negation Normal Form (NNF) is an equivalent formula within which the application of Not is restricted to atomic formulas, i.e., instances of AtomicFormula, and truth values T and F. The only other operators admitted are And, Or, Ex, and All.

If the input is quanitfier-free, to_nnf() will not introduce any quanitfiers.

If to_positive is True, Not is eliminated via replacing relation symbols with their complements. The result is then even a Positive Normal Form.

>>> from logic1.theories.RCF import *
>>> a, y = VV.get('a', 'y')
>>> f = Equivalent(And(a == 0, T), Ex(y, Not(y == a)))
>>> f.to_nnf()
And(Or(a != 0, F, Ex(y, a - y != 0)),
    Or(All(y, a - y == 0), And(a == 0, T)))

to_pnf(prefer_universal: bool = False, is_nnf: bool = False) → Formula[α, τ, χ, σ][source]#

Convert to Prenex Normal Form.

A Prenex Normal Form (PNF) is a Negation Normal Form (NNF) in which all quantifiers Ex and All stand at the beginning of the formula. The method used here minimizes the number of quantifier alternations in the prenex block [Burhenne-1990].

If the minimal number of alternations in the result can be achieved with both Ex and All as the first quantifier in the result, then the former is preferred. This preference can be changed with a keyword argument prefer_universal=True.

An keyword argument is_nnf=True indicates that self is already in NNF. to_pnf() then skips the initial NNF computation, which can be useful in time-critical situations.

>>> from logic1.theories.RCF import *
>>> a, b, y = VV.get('a', 'b', 'y')
>>> f = Equivalent(And(a == 0, b == 0, y == 0),
...                Ex(y, Or(y == a, a == 0)))
>>> f.to_pnf()
Ex(G0001_y, All(G0002_y,
    And(Or(a != 0, b != 0, y != 0, -G0001_y + a == 0, a == 0),
        Or(And(-G0002_y + a != 0, a != 0), And(a == 0, b == 0, y == 0)))))

transform_atoms(tr: Callable[[...], Formula[α, τ, χ, σ]]) → Formula[α, τ, χ, σ][source]#

Apply tr to all atomic formulas.

Replaces each atomic subformula of self with the Formula tr(self).

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = And(x == y, y < z)
>>> f.transform_atoms(lambda atom: atom.op(atom.lhs - atom.rhs, 0))
And(x - y == 0, y - z < 0)

Boolean Formulas#

We introduce formulas with Boolean toplevel operators as subclasses of Formula.

class logic1.firstorder.boolean.BooleanFormula[source]#

Bases: Formula[α, τ, χ, σ]

A class whose instances are Boolean formulas in the sense that their toplevel operator is one of the Boolean operators \(\top\), \(\bot\), \(\lnot\), \(\wedge\), \(\vee\), \(\longrightarrow\), \(\longleftrightarrow\).

final class logic1.firstorder.boolean.Equivalent[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A class whose instances are equivalences in the sense that their toplevel operator represents the Boolean operator \(\longleftrightarrow\).

>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Equivalent(x >= 0, Or(x > 0, x == 0))
Equivalent(x >= 0, Or(x > 0, x == 0))

property lhs: Formula[α, τ, χ, σ]#

The left-hand side of the equivalence.

See also

args – all arguments as a tuple
op – operator

property rhs: Formula[α, τ, χ, σ]#

The right-hand side of the equivalence.

See also

args – all arguments as a tuple
op – operator

final class logic1.firstorder.boolean.Implies[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A class whose instances are equivalences in the sense that their toplevel operator represents the Boolean operator \(\longrightarrow\).

>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Implies(x == 0, x >= 0)
Implies(x == 0, x >= 0)

See also

>>, __rshift__() – infix notation of Implies
<<, __lshift__() – infix notation of converse Implies

property lhs: Formula[α, τ, χ, σ]#

The left-hand side of the implication.

See also

args – all arguments as a tuple
op – operator

property rhs: Formula[α, τ, χ, σ]#

The right-hand side of the implication.

See also

args – all arguments as a tuple
op – operator

final class logic1.firstorder.boolean.And[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A class whose instances are conjunctions in the sense that their toplevel operator represents the Boolean operator \(\wedge\).

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> And()
T
>>> And(x == 0)
x == 0
>>> And(x == 1, x == y, y == z)
And(x - 1 == 0, x - y == 0, y - z == 0)

See also

&, __and__() – infix notation of And
args – all arguments as a tuple
op – operator

classmethod dual() → type[Or[α, τ, χ, σ]][source]#: A class method yielding the class Or, which implements the dual operator \(\vee\) of \(\wedge\).

classmethod definite() → type[_F[α, τ, χ, σ]][source]#: A class method yielding the class _F, which is the operator of the constant Formula F. The definite is the dual of the neutral.

classmethod definite_element() → _F[α, τ, χ, σ][source]#: A class method yielding the unique instance F of the _F.

classmethod neutral() → type[_T[α, τ, χ, σ]][source]#: A class method yielding the class _T, which is the operator of the constant Formula T. The neutral is the dual of the definite.

classmethod neutral_element() → _T[α, τ, χ, σ][source]#: A class method yielding the unique instance T of the _T.

final class logic1.firstorder.boolean.Or[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A class whose instances are disjunctions in the sense that their toplevel operator represents the Boolean operator \(\vee\).

>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> Or()
F
>>> Or(x == 0)
x == 0
>>> Or(x == 1, x == 2, x == 3)
Or(x - 1 == 0, x - 2 == 0, x - 3 == 0)

See also

|, __or__() – infix notation of Or
args – all arguments as a tuple
op – operator

classmethod dual() → type[And[α, τ, χ, σ]][source]#: A class method yielding the class And, which implements the dual operator \(\wedge\) of \(\vee\).

classmethod definite() → type[_T[α, τ, χ, σ]][source]#: A class method yielding the class _T, which is the operator of the constant Formula T. The definite is the dual of the neutral.

classmethod definite_element() → _T[α, τ, χ, σ][source]#: A class method yielding the unique instance T of the _T.

classmethod neutral() → type[_F[α, τ, χ, σ]][source]#: A class method yielding the class _F, which is the operator of the constant Formula F. The neutral is the dual of the definite.

classmethod neutral_element() → _F[α, τ, χ, σ][source]#: A class method yielding the unique instance F of the _F.

final class logic1.firstorder.boolean.Not[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A class whose instances are negated formulas in the sense that their toplevel operator is the Boolean operator \(\neg\).

>>> from logic1.theories.RCF import *
>>> a, = VV.get('a')
>>> Not(a == 0)
Not(a == 0)

See also

~, __invert__() – short notation of Not

property arg: Formula[α, τ, χ, σ]#

The one argument of the operator \(\neg\).

See also

args – all arguments as a tuple
op – operator

logic1.firstorder.boolean.involutive_not(arg: Formula[α, τ, χ, σ]) → Formula[α, τ, χ, σ][source]#

Construct a formula equivalent Not(arg) using the involutive law if applicable.

>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> involutive_not(x == 0)
Not(x == 0)
>>> involutive_not(Not(x == 0))
x == 0
>>> involutive_not(T)
Not(T)

final class logic1.firstorder.boolean._T[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A singleton class whose sole instance represents the constant Formula that is always true.

>>> _T()
T
>>> _T() is _T()
True

classmethod dual() → type[_F[α, τ, χ, σ]][source]#: A class method yielding the class _F, which implements the dual operator \(\bot\) of \(\top\).

logic1.firstorder.boolean.T = _T()#

Support use as a constant without parentheses.

We instantiate type variables with their respective upper bounds, which is the best we can do at the module level. T cannot be generic. Therefore, _T() should be used within statically typed code instead.

>>> T is _T()
True

final class logic1.firstorder.boolean._F[source]#

Bases: BooleanFormula[α, τ, χ, σ]

A singleton class whose sole instance represents the constant Formula that is always false.

>>> _F()
F
>>> _F() is _F()
True

classmethod dual() → type[_T[α, τ, χ, σ]][source]#: A class method yielding the class _T, which implements the dual operator \(\top\) of \(\bot\).

logic1.firstorder.boolean.F = _F()#

Support use as a constant without parentheses.

We instantiate type variables with their respective upper bounds, which is the best we can do at the module level. F cannot be generic. Therefore, _F() should be used within statically typed code instead.

>>> F is _F()
True

Quantified Formulas#

We provide subclasses of Formula that implement quanitfied formulas in the sense that their toplevel operator is a one of the quantifiers \(\exists\) or \(\forall\).

class logic1.firstorder.quantified.QuantifiedFormula[source]#

Bases: Formula[α, τ, χ, σ]

A class whose instances are quanitfied formulas in the sense that their toplevel operator is a one of the quantifiers \(\exists\) or \(\forall\). Note that members of QuantifiedFormula may have subformulas with other logical operators deeper in the expression tree.

property var: χ#

The variable of the quantifier.

>>> from logic1.theories.RCF import *
>>> x, y = VV.get('x', 'y')
>>> f = All(x, Ex(y, x == y))
>>> f.var
x

See also

args – all arguments as a tuple
op – operator

property arg: Formula[α, τ, χ, σ]#

The subformula in the scope of the QuantifiedFormula.

>>> from logic1.theories.RCF import *
>>> x, y = VV.get('x', 'y')
>>> f = All(x, Ex(y, x == y))
>>> f.arg
Ex(y, x - y == 0)

See also

args – all arguments as a tuple
op – operator

final class logic1.firstorder.quantified.Ex[source]#

Bases: QuantifiedFormula[α, τ, χ, σ]

A class whose instances are existentially quanitfied formulas in the sense that their toplevel operator represents the quantifier symbol \(\exists\). Besides variables, the quantifier accepts sequences of variables as a shorthand.

>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> Ex(x, x**2 == y)
Ex(x, x^2 - y == 0)
>>> Ex([x, y], And(x > 0, y > 0, z == x - y))
Ex(x, Ex(y, And(x > 0, y > 0, x - y - z == 0)))

classmethod dual() → type[All[α, τ, χ, σ]][source]#: A class method yielding the class All, which implements the dual operator \(\forall\) of \(\exists\).

final class logic1.firstorder.quantified.All[source]#

Bases: QuantifiedFormula[α, τ, χ, σ]

A class whose instances are universally quanitfied formulas in the sense that their toplevel operator represents the quantifier symbol \(\forall\). Besides variables, the quantifier accepts sequences of variables as a shorthand.

>>> from logic1.theories.RCF import *
>>> x, y = VV.get('x', 'y')
>>> All(x, x**2 >= 0)
All(x, x^2 >= 0)
>>> All([x, y], (x + y)**2 >= 0)
All(x, All(y, x^2 + 2*x*y + y^2 >= 0))

classmethod dual() → type[Ex[α, τ, χ, σ]][source]#: A class method yielding the dual class Ex of class:All.

class logic1.firstorder.quantified.Prefix[source]#

Bases: deque[tuple[type[All | Ex], list[χ]]]

Holds a quantifier prefix of a formula.

>>> from logic1.theories.RCF import *
>>> x, x0, epsilon, delta = VV.get('x', 'x0', 'epsilon', 'delta')
>>> Prefix((All, [x0, epsilon]), (Ex, [delta]), (All, [x]))
Prefix([(<class 'logic1.firstorder.quantified.All'>, [x0, epsilon]),
        (<class 'logic1.firstorder.quantified.Ex'>, [delta]),
        (<class 'logic1.firstorder.quantified.All'>, [x])])
>>> print(_)
All [x0, epsilon]  Ex [delta]  All [x]

See also

collections.deque – for mehods inherited from double-ended queues
matrix – the matrix of a prenex formula
quantify – add quantifier prefix

First-order Formulas

Contents

First-order Formulas#

Generic Types#

Formula Base Class#

Boolean Formulas#

Quantified Formulas#