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 template relation name) predicate-logic formula that does not refer to any variable name in the schema (except possibly through its instantiated argument 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:

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.
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.
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 name occurrences originating in the given formula are substituted (i.e., name occurrences 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]) – variable names 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 specified to be treated as bound:

>>> 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 relation names 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:

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

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 invocation of the template relation name.
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

assumptions (AbstractSet[Schema]) – the assumption/axioms for the proof.
conclusion (Formula) – the conclusion for the proof.
lines (Sequence[Union[AssumptionLine, MPLine, UGLine, TautologyLine]]) – the lines for the proof.

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/axiom, and its instantiation map from the justifying assumption/axiom.

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

assumptions (AbstractSet[Schema]) – assumptions/axioms of the proof.
lines (Sequence[Union[AssumptionLine, MPLine, UGLine, TautologyLine]]) – lines of the proof.
line_number (int) – line number of the current line in the given lines.

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 to justify the line.
conditional_line_number (int) – the line number of the conditional of the MP inference to justify 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

assumptions (AbstractSet[Schema]) – assumptions/axioms of the proof.
lines (Sequence[Union[AssumptionLine, MPLine, UGLine, TautologyLine]]) – lines of the proof.
line_number (int) – line number of the current line in the given lines.

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, nonquantified_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.
nonquantified_line_number (int) – the line number of the statement quantified by the formula.

__init__(formula, nonquantified_line_number)¶

Initializes a UGLine from its formula and line number of the statement quantified by the formula.

Parameters

formula (Formula) – the formula to be justified by the line.
nonquantified_line_number (int) – the line number of the statement quantified by the formula.

__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

assumptions (AbstractSet[Schema]) – assumptions/axioms of the proof.
lines (Sequence[Union[AssumptionLine, MPLine, UGLine, TautologyLine]]) – lines of the proof.
line_number (int) – line number of the current line in the given lines.

Return type

bool

Returns

True if the formula of the current line is of the form 'Ax[nonquantified]', where nonquantified is the formula of the line from the given lines whose number is the nonquantified 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

assumptions (AbstractSet[Schema]) – assumptions/axioms of the proof.
lines (Sequence[Union[AssumptionLine, MPLine, UGLine, TautologyLine]]) – lines of the proof.
line_number (int) – line number of the current line in the given lines.

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)¶

Composes the given propositional-logic specialization map, specifying the transformation from a propositional-logic axiom to a specialization of it, and the given substitution map, specifying the transformation from that specialization (as a propositional skeleton) to a predicate-logic formula, into an instantiation map specifying how to instantiate the schema equivalent of that axiom into the same predicate-logic formula.

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 propositional variable name 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)¶

Translates the given proof of a propositional skeleton of the given predicate-logic formula into 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 propositional variable name of the propositional 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, whose propositional skeleton contains no constants or operators beyond '->' and '~', 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.