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.term.Term.

logic1.firstorder.formula.χ = TypeVar('χ', bound='Variable')#

A type variable denoting a type of variables with upper bound logic1.firstorder.term.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: ABC, Generic[α, τ, χ, σ]

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

  1. Boolean operators:

    1. Truth values \(\top\) and \(\bot\)

    2. Negation \(\lnot\)

    3. Conjunction \(\land\) and disjunction \(\lor\)

    4. Implication \(\longrightarrow\)

    5. Bi-implication (syntactic equivalence) \(\longleftrightarrow\)

  2. 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 formulas. 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 of atomic formulas, terms, and variables, respectively. They appear in type annotations used by static type checkers but are not relevant for 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

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)))
abstractmethod __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

__str__() → str[source]#

Representation of the Formula used in printing.

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

Universal closure. Universally quantify 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

as_redlog() → str[source]#

Returns the Redlog representation of this formula.

>>> from logic1.theories.RCF import *
>>> x, y = VV.get('x', 'y')
>>> f = All(x, Or(x < 1, x - 1 == 0, x > 1))
>>> f.as_redlog()
'all(x, ((x - 1 < 0) or (x - 1 = 0) or (x - 1 > 0)))'

See also

The Redlog interface for Real Closed Fields

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

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

A quantifier-free formula has zero alternations.

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 quantify 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

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.term.Term and firstorder.term.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

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

_repr_latex_() → str[source]#

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

To remain below MathJax’s default 5 KiB TeX input buffer, the representation is truncated to approximately 5000 characters.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')

>>> f = All(x, Ex(y, x - y == 0))
>>> f._repr_latex_()
'$\\displaystyle \\forall x \\, \\exists y \\, (x - y = 0)$'

>>> g = And(*(x == 0 for _ in range(1000)))
>>> latex = g._repr_latex_()
>>> latex == '$\\displaystyle ' + 'x = 0 \\, \\wedge \\, ' * 263 + 'x ={}\\dots$'
True

See also

as_latex() – LaTeX representation

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

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

  1. 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).

  2. Nested operators:

    1. Transform Not(Not(arg)) into arg.

    2. Transform And(..., And(*args), ...) into And(..., *args, ...). The same for Or instead of And.

  3. 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.

  4. 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:

More powerful simplifiers provided by various theories:

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

Simultaneous 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, And(_, 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 quantifier-free, to_nnf() will not introduce any quantifiers.

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)))))
traverse(*, map_atoms: ~typing.Callable[[...], ~logic1.firstorder.formula.Formula[~logic1.firstorder.formula.α, ~logic1.firstorder.formula.τ, ~logic1.firstorder.formula.χ, ~logic1.firstorder.formula.σ]] = <function Formula.<lambda>>, sort_levels: bool = False) → Formula[α, τ, χ, σ][source]#

Apply map_atoms to all atomic formulas.

Replaces each atomic subformula of self with the Formula map_atoms(self). If sort_levels is True, all subformulas built from commutative Boolean operators (And, Or, Equivalent) are sorted after the application of map_atoms.

>>> from logic1.theories.RCF import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = And(x == y, y < z)
>>> f.traverse(map_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 implications 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

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

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

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

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 quantified formulas in the sense that their toplevel operator is one of the quantifiers \(\exists\) or \(\forall\).

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

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

A class whose instances are quantified formulas in the sense that their toplevel operator is 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 quantified 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)))
__init__(vars_: χ | Sequence[χ], arg: Formula[α, τ, χ, σ]) → None[source]#

Construct an existentially quantified formula.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> Ex(x, x**2 == y)
Ex(x, x**2 - y == 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 quantified 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))
__init__(vars_: χ | Sequence[χ], arg: Formula[α, τ, χ, σ]) → None[source]#

Construct a universally quantified formula.

>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> All(x, x**2 >= 0)
All(x, x**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