# predicates.prover module¶

Axiomatic schemas of Predicate Logic, and useful proof creation maneuvers using them.

class `predicates.prover.``Prover`(assumptions, print_as_proof_forms=False)

Bases: `object`

A class for gradually creating a predicate-logic proof from given assumptions as well as from the six axioms (`AXIOMS`) Universal Instantiation (`UI`), Existential Introduction (`EI`), Universal Simplification (`US`), Existential Simplification (`ES`), Reflexivity (`RX`), and Meaning of Equality (`ME`).

Variables
`UI` = Schema: (Ax[R(x)]->R(c)) [templates: R, c, x]

Axiom schema of universal instantiation

`EI` = Schema: (R(c)->Ex[R(x)]) [templates: R, c, x]

Axiom schema of existential introduction

`US` = Schema: (Ax[(Q()->R(x))]->(Q()->Ax[R(x)])) [templates: Q, R, x]

Axiom schema of universal simplification

`ES` = Schema: ((Ax[(R(x)->Q())]&Ex[R(x)])->Q()) [templates: Q, R, x]

Axiom schema of existential simplification

`RX` = Schema: c=c [templates: c]

Axiom schema of reflexivity

`ME` = Schema: (c=d->(R(c)->R(d))) [templates: R, c, d]

Axiom schema of meaning of equality

`AXIOMS` = frozenset({Schema: c=c [templates: c], Schema: (R(c)->Ex[R(x)]) [templates: R, c, x], Schema: (Ax[(Q()->R(x))]->(Q()->Ax[R(x)])) [templates: Q, R, x], Schema: (Ax[R(x)]->R(c)) [templates: R, c, x], Schema: ((Ax[(R(x)->Q())]&Ex[R(x)])->Q()) [templates: Q, R, x], Schema: (c=d->(R(c)->R(d))) [templates: R, c, d]})

Axiomatic system for Predicate Logic, consisting of `UI`, `EI`, `US`, `ES`, `RX`, and `ME`.

`__init__`(assumptions, print_as_proof_forms=False)

Initializes a `Prover` from its assumptions/additional axioms. The proof created by the prover initially has no lines.

Parameters
`qed`()

Concludes the proof created by the current prover.

Return type

`Proof`

Returns

A valid proof, from the assumptions of the current prover as well as `AXIOMS`’, of the formula justified by the last line appended to the current prover.

`_add_line`(line)

Appends to the proof being created by the current prover the given validly justified line.

Parameters

line (`Union`[`AssumptionLine`, `MPLine`, `UGLine`, `TautologyLine`]) – proof line that is validly justified when appended to the lines of the proof being created by the current prover.

Return type

`int`

Returns

The line number of the appended line in the proof being created by the current prover.

`add_instantiated_assumption`(instance, assumption, instantiation_map)

Appends to the proof being created by the current prover a line that validly justifies the given instance of the given assumptions/axioms of the current prover.

Parameters
Return type

`int`

Returns

The line number of the newly appended line that justifies the given instance in the proof being created by the current prover.

`add_assumption`(unique_instance)

Appends to the proof being created by the current prover a line that validly justifies the unique instance of one of the assumptions/axioms of the current prover.

Parameters

unique_instance (`Union`[`Formula`, `str`]) – unique instance of one of the assumptions/axioms of the current prover, to be appended, specified as either a formula or its string representation.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given instance in the proof being created by the current prover.

`add_tautology`(tautology)

Appends to the proof being created by the current prover a line that validly justifies the given tautology.

Parameters

tautology (`Union`[`Formula`, `str`]) – tautology to be appended, specified as either a formula or its string representation.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given tautology in the proof being created by the current prover.

`add_mp`(consequent, antecedent_line_number, conditional_line_number)

Appends to the proof being created by the current prover a line that validly justifies the given consequent of an MP inference from the specified already existing lines of the proof.

Parameters
• consequent (`Union`[`Formula`, `str`]) – consequent of MP inference to be appended, specified as either a formula or its string representation.

• antecedent_line_number (`int`) – line number in the proof of the antecedent of the MP inference that derives the given formula.

• conditional_line_number (`int`) – line number in the proof of the conditional of the MP inference that derives the given formula.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

`add_ug`(quantified, nonquantified_line_number)

Appends to the proof being created by the current prover a line that validly justifies the given universally quantified formula, the statement quantified by which is the specified already existing line of the proof.

Parameters
Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

`add_proof`(conclusion, proof)

Appends to the proof being created by the current prover a validly justified inlined version of the given proof of the given conclusion, the last line of which validly justifies the given formula.

Parameters
Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

`add_universal_instantiation`(instantiation, line_number, term)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given formula, which is the result of substituting a term for the outermost universally quantified variable name in the formula in the specified already existing line of the proof.

Parameters
• instantiation (`Union`[`Formula`, `str`]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation.

• line_number (`int`) – line number in the proof of a universally quantified formula of the form `'A``x``[``statement``]'`.

• term (`Union`[`Term`, `str`]) – term, specified as either a term or its string representation, that when substituted into the free occurrences of `x` in `statement` yields the given formula.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

Examples

If Line `line_number` contains the formula `'Ay[Az[f(x,y)=g(z,y)]]'` and `term` is `'h(w)'`, then `instantiation` should be `'Az[f(x,h(w))=g(z,h(w))]'`.

`add_tautological_implication`(implication, line_numbers)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given formula, which is a tautological implication of the formulas in the specified already existing lines of the proof.

Parameters
Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

`add_existential_derivation`(consequent, line_number1, line_number2)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given formula, which is the consequent of the formula in the second specified already existing line of the proof, whose antecedent is existentially quantified by the formula in the first specified already existing line of the proof.

Parameters
• consequent (`Union`[`Formula`, `str`]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation.

• line_number1 (`int`) – line number in the proof of an existentially quantified formula of the form `'E``x``[``antecedent(x)``]'`, where `x` is a variable name that may have free occurrences in `antecedent(x)` but has no free occurrences in `consequent`.

• line_number2 (`int`) – line number in the proof of the formula `'(``antecedent(x)``->``consequent``)'`.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

`add_flipped_equality`(flipped, line_number)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given equality, which is the result of exchanging the two sides of the equality in the specified already existing line of the proof.

Parameters
Return type

`int`

Returns

The line number of the newly appended line that justifies the given equality in the proof being created by the current prover.

`add_free_instantiation`(instantiation, line_number, substitution_map)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given formula, which is the result of substituting terms for free variable names in the formula in the specified already existing line of the proof.

Parameters
• instantiation (`Union`[`Formula`, `str`]) – conclusion of the sequence of lines to be appended, which contains no variable names starting with `z`, specified as either a formula or its string representation.

• line_number (`int`) – line number in the proof of a formula with free variable names, which contains no variable names starting with `z`.

• substitution_map (`Mapping`[`str`, `Union`[`Term`, `str`]]) – mapping from free variable names of the formula with the given line number to terms that contain no variable names starting with `z`, to be substituted for them to obtain the given formula. Each value of this map may also be given as a string representation (instead of a term). Only variable name occurrences originating in the formula with the given line number are substituted (i.e., variable names originating in one of the specified substitutions are not subjected to additional substitutions).

Return type

`int`

Returns

The line number of the newly appended line that justifies the given formula in the proof being created by the current prover.

Examples

If Line `line_number` contains the formula `'(z=5&Az[f(x,y)=g(z,y)])'` and `substitution_map` is `{'y': 'h(w)', 'z': 'y'}`, then `instantiation` should be `'(y=5&Az[f(x,h(w))=g(z,h(w))])'`.

`add_substituted_equality`(substituted, line_number, parametrized_term)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given equality, whose two sides are the results of substituting the two respective sides of the equality in the specified already existing line of the proof into the given parametrized term.

Parameters
• substituted (`Union`[`Formula`, `str`]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation.

• line_number (`int`) – line number in the proof of an equality.

• parametrized_term (`Union`[`Term`, `str`]) – term parametrized by the constant name `'_'`, specified as either a term or its string representation, such that substituting each of the two sides of the equality with the given line number into this parametrized term respectively yields each of the two sides of the given equality.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given equality in the proof being created by the current prover.

Examples

If Line `line_number` contains the formula `'g(x)=h(y)'` and `parametrized_term` is `'_+7'`, then `substituted` should be `'g(x)+7=h(y)+7'`.

`_add_chaining_of_two_equalities`(line_number1, line_number2)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies an equality that is the result of chaining together the two equalities in the specified already existing lines of the proof.

Parameters
• line_number1 (`int`) – line number in the proof of an equality of the form `'``first``=``second``'`.

• line_number2 (`int`) – line number in the proof of an equality of the form `'``second``=``third``'`.

Return type

`int`

Returns

The line number of the newly appended line that justifies the equality `'``first``=``third``'` in the proof being created by the current prover.

Examples

If Line `line_number1` contains the formula `'a=b'` and Line `line_number2` contains the formula `'b=f(b)'`, then the last appended line will contain the formula `'a=f(b)'`.

`add_chained_equality`(chained, line_numbers)

Appends to the proof being created by the current prover a sequence of validly justified lines, the last of which validly justifies the given equality, which is the result of chaining together the equalities in the specified already existing lines of the proof.

Parameters
• chained (`Union`[`Formula`, `str`]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation, of the form `'``first``=``last``'`.

• line_numbers (`Sequence`[`int`]) – line numbers in the proof of equalities of the form `'``first``=``second``'`, `'``second``=``third``'`, …, `'``before_last``=``last``'`, i.e., the left-hand side of the first equality is the left-hand side of the given equality, the right-hand of each equality (except for the last) is the left-hand side of the next equality, and the right-hand side of the last equality is the right-hand side of the given equality.

Return type

`int`

Returns

The line number of the newly appended line that justifies the given equality in the proof being created by the current prover.

Examples: If `line_numbers` is `[7,3,9]`, Line 7 contains the formula `'a=b'`, Line 3 contains the formula `'b=f(b)'`, and Line 9 contains the formula `'f(b)=0'`, then `chained` should be `'a=0'`.