predicates.proofs module

Schemas and proofs in Predicate Logic.

predicates.proofs.InstantiationMap

A mapping from constant names, variable names, and relation names to terms, variable names, and formulas respectively.

alias of Mapping[str, Union[predicates.syntax.Term, str, predicates.syntax.Formula]]

class predicates.proofs.Schema(formula, templates=frozenset({}))

Bases: object

An immutable schema of predicate-logic formulas, comprised of a formula along with the constant names, variable names, and nullary or unary relation names in that formula that serve as templates. A template constant name is a placeholder for any term. A template variable name is a placeholder for any variable name. A template nullary or unary relation name is a placeholder for any (parametrized for a unary relation name) predicate-logic formula that does not refer to any variable name in the schema (except possibly through its instantiated parameter for a unary relation name).

Variables
  • formula (Formula) – the formula of the schema.

  • templates (FrozenSet[str]) – the constant, variable, and relation names from the formula that serve as templates.

__init__(formula, templates=frozenset({}))

Initializes a Schema from its formula and template names.

Parameters
  • formula (Formula) – the formula for the schema.

  • templates (AbstractSet[str]) – the constant, variable, and relation names from the formula to serve as templates.

__repr__()

Computes a string representation of the current schema.

Return type

str

Returns

A string representation of the current schema.

__eq__(other)

Compares the current schema with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is a Schema object that equals the current schema, False otherwise.

__ne__(other)

Compares the current schema with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is not a Schema object or does not equal the current schema, False otherwise.

exception BoundVariableError(variable_name, relation_name)

Bases: Exception

Raised by _instantiate_helper when a variable name becomes bound during a schema instantiation in a way that is disallowed in that context.

Variables
  • variable_name (str) – the variable name that became bound in a way that was disallowed during a schema instantiation.

  • relation_name (str) – the relation name during whose substitution the relevant occurrence of the variable name became bound.

__init__(variable_name, relation_name)

Initializes a BoundVariableError from the offending variable name and the relation name during whose substitution the error occurred.

Parameters
  • variable_name (str) – variable name that is to become bound in a way that is disallowed during a schema instantiation.

  • relation_name (str) – the relation name during whose substitution the relevant occurrence of the variable name is to become bound.

static _instantiate_helper(formula, constants_and_variables_instantiation_map, relations_instantiation_map, bound_variables=frozenset({}))

Performs the following substitutions in the given formula:

  1. Substitute each occurrence of each constant name or variable name that is a key of the given constants and variables instantiation map with the term mapped to this name by this map.

  2. Substitute each nullary invocation of each relation name that is a key of the given relations instantiation map with the formula mapped to it by this map.

  3. For each unary invocation of each relation name that is a key of the given relations instantiation map, first perform all substitutions to the argument of this invocation (according to the given constants and variables instantiation map), then substitute the result for each occurrence of the constant name '_' in the formula mapped to the relation name by this map, and then substitute the result for this unary invocation of the relation name.

Only names originating in the given formula are substituted (i.e., names originating in one of the above substitutions are not subjected to additional substitutions).

Parameters
  • formula (Formula) – formula in which to perform the substitutions.

  • constants_and_variables_instantiation_map (Mapping[str, Term]) – mapping from constant names and variable names in the given formula to terms to be substituted for them, where the roots of terms mapped to variable names are variable names.

  • relations_instantiation_map (Mapping[str, Formula]) – mapping from nullary and unary relation names in the given formula to formulas to be substituted for them, where formulas to be substituted for unary relation names are parametrized by the constant name '_'.

  • bound_variables (AbstractSet[str]) – variables to be treated as bound (see below).

Return type

Formula

Returns

The result of all substitutions.

Raises

BoundVariableError – if one of the following occurs when substituting an invocation of a relation name: 1. A free occurrence of a variable name in the formula mapped to the relation name by the given relations instantiation map is in bound_variables or becomes bound by a quantification in the given formula after all variable names in the given formula have been substituted. 2. For a unary invocation: a variable name that is in the argument to that invocation after all substitutions have been applied to this argument, becomes bound by a quantification in the formula mapped to the relation name by the given relations instantiation map.

Examples

The following succeeds:

>>> Schema._instantiate_helper(
...     Formula.parse('Ax[(Q(c)->R(x))]'), {'x': Term('w')},
...     {'Q': Formula.parse('y=_')}, {'x', 'z'})
Aw[(y=c->R(w))]

however the following fails since 'Q(c)' is to be substituted with 'y=c' while 'y' is in the given bound variables:

>>> Schema._instantiate_helper(
...     Formula.parse('Ax[(Q(c)->R(x))]'), {},
...     {'Q': Formula.parse('y=_')}, {'x', 'y', 'z'})
Traceback (most recent call last):
  ...
predicates.proofs.Schema.BoundVariableError: ('y', 'Q')

and the following fails since as 'Q(c)' is to be substituted with 'y=c', 'y' is to become bound by the quantification 'Ay':

>>> Schema._instantiate_helper(
...     Formula.parse('Ax[(Q(c)->R(x))]'), {'x': Term('y')},
...     {'Q': Formula.parse('y=_')})
Traceback (most recent call last):
  ...
predicates.proofs.Schema.BoundVariableError: ('y', 'Q')

The following succeeds:

>>> Schema._instantiate_helper(
...     Formula.parse('Ax[(Q(c)->R(x))]'),
...     {'c': Term.parse('plus(d,x)')},
...     {'Q': Formula.parse('Ey[y=_]')})
Ax[(Ey[y=plus(d,x)]->R(x))]

however the following fails since as '_' is to be substituted with 'plus(d,y)' in 'Ey[y=_]', the 'y' in 'plus(d,y)' is to become bound by the quantification 'Ey':

>>> Schema._instantiate_helper(
...     Formula.parse('Ax[(Q(c)->R(x))]'),
...     {'c': Term.parse('plus(d,y)')},
...     {'Q': Formula.parse('Ey[y=_]')})
Traceback (most recent call last):
  ...
predicates.proofs.Schema.BoundVariableError: ('y', 'Q')
instantiate(instantiation_map)

Instantiates the current schema according to the given map from templates of the current schema to expressions.

Parameters

instantiation_map (Mapping[str, Union[Term, str, Formula]]) – mapping from templates of the current schema to expressions of the type for which they serve as placeholders. That is, constant names are mapped to terms, variable names are mapped to variable names (strings), and relation names are mapped to formulas where unary relations are mapped to formulas parametrized by the constant name '_'.

Return type

Optional[Formula]

Returns

The predicate-logic formula obtained by applying the substitutions specified by the given map to the formula of the current schema:

  1. Each occurrence in the formula of the current schema of each template constant name specified in the given map is substituted with the term to which that template constant name is mapped.

  2. Each occurrence in the formula of the current schema of each template variable name specified in the given map is substituted with the variable name to which that template variable name is mapped.

  3. Each nullary invocation in the formula of the current schema of each template relation name specified in the given map is substituted with the formula to which that template relation name is mapped.

  4. Each unary invocation in the formula of the current schema of each template relation name specified in the given map is substituted with the formula to which that template relation name is mapped, in which each occurrence of the constant name '_' is substituted with the instantiated argument of that invocation of the template relation name (that is, the term that results from instantiating the argument of that invocation by performing all the specified substitutions on it).

None is returned if one of the keys of the given map is not a template of the current schema or if one of the following occurs when substituting an invocation of a template relation name:

  1. A free occurrence of a variable name in the formula substituted for the template relation name becomes bound by a quantification in the instantiated schema formula, except if the template relation name is unary and this free occurrence originates in the instantiated argument of the relation invocation.

  2. For a unary invocation: a variable name in the instantiated argument of that invocation becomes bound by a quantification in the formula that is substituted for the invocation of the template relation name.

Examples

>>> s = Schema(Formula.parse('(Q(c1,c2)->(R(c1)->R(c2)))'),
...            {'c1', 'c2', 'R'})
>>> s.instantiate({'c1': Term.parse('plus(x,1)'),
...                'R': Formula.parse('Q(_,y)')})
(Q(plus(x,1),c2)->(Q(plus(x,1),y)->Q(c2,y)))
>>> s.instantiate({'c1': Term.parse('plus(x,1)'),
...                'c2': Term.parse('c1'),
...                'R': Formula.parse('Q(_,y)')})
(Q(plus(x,1),c1)->(Q(plus(x,1),y)->Q(c1,y)))
>>> s = Schema(Formula.parse('(P()->P())'), {'P'})
>>> s.instantiate({'P': Formula.parse('plus(a,b)=c')})
(plus(a,b)=c->plus(a,b)=c)

For the following schema:

>>> s = Schema(Formula.parse('(Q(d)->Ax[(R(x)->Q(f(c)))])'),
...            {'R', 'Q', 'x', 'c'})

the following succeeds:

>>> s.instantiate({'R': Formula.parse('_=0'),
...                'Q': Formula.parse('x=_'),
...                'x': 'w'})
(x=d->Aw[(w=0->x=f(c))])

however, the following returns None because 'd' is not a template of the schema:

>>> s.instantiate({'R': Formula.parse('_=0'),
...                'Q': Formula.parse('x=_'),
...                'x': 'w',
...                'd': Term('z')})

and the following returns None because 'z' that is free in the assignment to 'Q' is to become bound by a quantification in the instantiated schema formula:

>>> s.instantiate({'R': Formula.parse('_=0'),
...                'Q': Formula.parse('s(z)=_'),
...                'x': 'z'})

and the following returns None because 'y' in the instantiated argument 'f(plus(a,y))' of the second invocation of 'Q' is to become bound by the quantification in the formula substituted for 'Q':

>>> s.instantiate({'R': Formula.parse('_=0'),
...                'Q': Formula.parse('Ay[s(y)=_]'),
...                'c': Term.parse('plus(a,y)')})
class predicates.proofs.Proof(assumptions, conclusion, lines)

Bases: object

An immutable deductive proof in Predicate Logic, comprised of a list of assumptions/axioms, a conclusion, and a list of lines that prove the conclusion from (instances of) these assumptions/axioms and from tautologies, via the Modus Ponens (MP) and Universal Generalization (UG) inference rules.

Variables
  • assumptions (FrozenSet[Schema]) – the assumption/axioms of the proof.

  • conclusion (Formula) – the conclusion of the proof.

  • lines (Tuple[Line]) – the lines of the proof.

__init__(assumptions, conclusion, lines)

Initializes a Proof from its assumptions/axioms, conclusion, and lines.

Parameters
class AssumptionLine(formula, assumption, instantiation_map)

Bases: object

An immutable proof line justified as an instance of an assumption/axiom.

Variables
  • formula (Formula) – the formula justified by the line.

  • assumption (Schema) – the assumption/axiom that instantiates the formula.

  • instantiation_map (Mapping[str, Union[Term, str, Formula]]) – the mapping instantiating the formula from the assumption/axiom.

__init__(formula, assumption, instantiation_map)

Initializes an AssumptionLine from its formula, its justifying assumption, and its instantiation map from the justifying assumption.

Parameters
  • formula (Formula) – the formula to be justified by the line.

  • assumption (Schema) – the assumption/axiom that instantiates the formula.

  • instantiation_map (Mapping[str, Union[Term, str, Formula]]) – the mapping instantiating the formula from the assumption/axiom.

__repr__()

Computes a string representation of the current line.

Return type

str

Returns

A string representation of the current line.

is_valid(assumptions, lines, line_number)

Checks if the current line is validly justified in the context of the specified proof.

Parameters
Return type

bool

Returns

True if the assumption/axiom of the current line is an assumption/axiom of the specified proof and if the formula justified by the current line is a valid instance of this assumption/axiom via the instantiation map of the current line, False otherwise.

class MPLine(formula, antecedent_line_number, conditional_line_number)

Bases: object

An immutable proof line justified by the Modus Ponens (MP) inference rule.

Variables
  • formula (Formula) – the formula justified by the line.

  • antecedent_line_number (int) – the line number of the antecedent of the MP inference justifying the line.

  • conditional_line_number (int) – the line number of the conditional of the MP inference justifying the line.

__init__(formula, antecedent_line_number, conditional_line_number)

Initializes a MPLine from its formula and line numbers of the antecedent and conditional of the MP inference justifying it.

Parameters
  • formula (Formula) – the formula to be justified by the line.

  • antecedent_line_number (int) – the line number of the antecedent of the MP inference justifying the line.

  • conditional_line_number (int) – the line number of the conditional of the MP inference justifying the line.

__repr__()

Computes a string representation of the current line.

Return type

str

Returns

A string representation of the current line.

is_valid(assumptions, lines, line_number)

Checks if the current line is validly justified in the context of the specified proof.

Parameters
Return type

bool

Returns

True if the formula of the line from the given lines whose number is the conditional line number justifying the current line is '(antecedent->consequent)', where antecedent is the formula of the line from the given lines whose number is the antecedent line number justifying the current line and consequent is the formula justified by the current line; False otherwise.

class UGLine(formula, predicate_line_number)

Bases: object

An immutable proof line justified by the Universal Generalization (UG) inference rule.

Variables
  • formula (Formula) – the formula justified by the line.

  • predicate_line_number (int) – the line number of the predicate of the UG inference justifying the line.

__init__(formula, predicate_line_number)

Initializes a UGLine from its formula and line number of the predicate of the UG inference justifying it.

Parameters
  • formula (Formula) – the formula to be justified by the line.

  • predicate_line_number (int) – the line number of the predicate of the UG inference justifying the line.

__repr__()

Computes a string representation of the current line.

Return type

str

Returns

A string representation of the current line.

is_valid(assumptions, lines, line_number)

Checks if the current line is validly justified in the context of the specified proof.

Parameters
Return type

bool

Returns

True if the formula of the current line is of the form 'Ax[predicate]', where predicate is the formula of the line from the given lines whose number is the predicate line number justifying the current line and x is any variable name; False otherwise.

class TautologyLine(formula)

Bases: object

An immutable proof line justified as a tautology.

Variables

formula (Formula) – the formula justified by the line.

__init__(formula)

Initializes a TautologyLine from its formula.

Parameters

formula (Formula) – the formula to be justified by the line.

__repr__()

Computes a string representation of the current line.

Return type

str

Returns

A string representation of the current line.

is_valid(assumptions, lines, line_number)

Checks if the current line is validly justified in the context of the specified proof.

Parameters
Return type

bool

Returns

True if the formula justified by the current line is a (predicate-logic) tautology, False otherwise.

Line

An immutable proof line.

__repr__()

Computes a string representation of the current proof.

Return type

str

Returns

A string representation of the current proof.

is_valid()

Checks if the current proof is a valid proof of its claimed conclusion from (instances of) its assumptions/axioms.

Return type

bool

Returns

True if the current proof is a valid proof of its claimed conclusion from (instances of) its assumptions/axioms, False otherwise.

predicates.proofs.I0_SCHEMA

Schema equivalent of the propositional-logic self implication axiom I0.

predicates.proofs.I1_SCHEMA

Schema equivalent of the propositional-logic implication introduction (right) axiom I1.

predicates.proofs.D_SCHEMA

Schema equivalent of the propositional-logic self-distribution of implication axiom D.

predicates.proofs.I2_SCHEMA

Schema equivalent of the propositional-logic implication introduction (left) axiom I2.

predicates.proofs.N_SCHEMA

Schema equivalent of the propositional-logic converse contraposition axiom N.

predicates.proofs.NI_SCHEMA

Schema equivalent of the propositional-logic negative-implication introduction axiom NI.

predicates.proofs.NN_SCHEMA

Schema equivalent of the propositional-logic double-negation introduction axiom NN.

predicates.proofs.R_SCHEMA

Schema equivalent of the propositional-logic resolution axiom R.

predicates.proofs.PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS

Schema system equivalent of the axioms of the propositional-logic large axiomatic system for implication and negation AXIOMATIC_SYSTEM.

predicates.proofs.PROPOSITIONAL_AXIOM_TO_SCHEMA

Mapping from propositional-logic axioms for implication and negation to their schema equivalents.

predicates.proofs._axiom_specialization_map_to_schema_instantiation_map(propositional_specialization_map, substitution_map)

Converts the given propositional-logic specialization map from a propositional-logic axiom to its specialization, to an instantiation map from the schema equivalent of that axiom to a predicate-logic formula whose skeleton is that specialization.

Parameters
  • propositional_specialization_map (Mapping[str, Formula]) – mapping specifying how some propositional-logic axiom axiom (which is not specified) from AXIOMATIC_SYSTEM specializes into some specialization specialization (which is also not specified), and containing no constants or operators beyond '~', '->', '|', and '&'.

  • substitution_map (Mapping[str, Formula]) – mapping from each atomic propositional subformula of specialization to a predicate-logic formula.

Return type

Mapping[str, Formula]

Returns

An instantiation map for instantiating the schema equivalent of axiom into the predicate-logic formula obtained from its propositional skeleton specialization by the given substitution map.

Examples

>>> _axiom_specialization_map_to_schema_instantiation_map(
...     {'p': PropositionalFormula.parse('(z1->z2)'),
...      'q': PropositionalFormula.parse('~z1')},
...     {'z1': Formula.parse('Ax[(x=5&M())]'),
...      'z2': Formula.parse('R(f(8,9))')})
{'P': (Ax[(x=5&M())]->R(f(8,9))), 'Q': ~Ax[(x=5&M())]}
predicates.proofs._prove_from_skeleton_proof(formula, skeleton_proof, substitution_map)

Converts the given proof of a propositional skeleton of the given predicate-logic formula to a proof of that predicate-logic formula.

Parameters
  • formula (Formula) – predicate-logic formula to prove.

  • skeleton_proof (Proof) – valid propositional-logic proof of a propositional skeleton of the given formula, from no assumptions and via AXIOMATIC_SYSTEM, and containing no constants or operators beyond '~', '->', '|', and '&'.

  • substitution_map (Mapping[str, Formula]) – mapping from each atomic propositional subformula of the skeleton of the given formula that is proven in the given proof to the respective predicate-logic subformula of the given formula.

Return type

Proof

Returns

A valid predicate-logic proof of the given formula from the axioms PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS via only assumption lines and MP lines.

predicates.proofs.prove_tautology(tautology)

Proves the given predicate-logic tautology.

Parameters

tautology (Formula) – predicate-logic tautology to prove.

Return type

Proof

Returns

A valid proof of the given predicate-logic tautology from the axioms PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS via only assumption lines and MP lines.