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

_assumptions (FrozenSet[Schema]) – the assumptions/axioms of the proof being created, which include AXIOMS.
_lines (List[Line]) – the lines so far of the proof being created.
_print_as_proof_forms (bool) – flag specifying whether the proof being created is being printed in real time as it forms.

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: ((Ax[(R(x)->Q())]&Ex[R(x)])->Q()) [templates: Q, R, x], Schema: (Ax[R(x)]->R(c)) [templates: R, c, x], Schema: (R(c)->Ex[R(x)]) [templates: R, c, x], Schema: c=c [templates: c], Schema: (c=d->(R(c)->R(d))) [templates: R, c, d], Schema: (Ax[(Q()->R(x))]->(Q()->Ax[R(x)])) [templates: Q, R, x]})¶: 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

assumptions (Collection[Union[Schema, Formula, str]]) – the assumptions/axioms beyond AXIOMS for the proof to be created, each specified as either a schema, a formula that constitutes the unique instance of the assumption, or the string representation of the unique instance of the assumption.
print_as_proof_forms (bool) – flag specifying whether the proof to be created is to be printed in real time as it forms.

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

instance (Union[Formula, str]) – instance to be appended, specified as either a formula or its string representation.
assumption (Schema) – assumption/axiom of the current prover that instantiates the given instance.
instantiation_map (Mapping[str, Union[Term, str, Formula]]) – mapping instantiating the given instance from the given assumption/axiom. Each value of this map may also be given as a string representation (instead of a term or a formula).

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

quantified (Union[Formula, str]) – universally quantified formula to be appended, specified as either a formula or its string representation.
nonquantified_line_number (int) – line number in the proof of the statement quantified by 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_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

conclusion (Union[Formula, str]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation.
proof (Proof) – valid proof of the given formula from a subset of the assumptions/axioms of the current prover.

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 'Ax[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

implication (Union[Formula, str]) – conclusion of the sequence of lines to be appended, specified as either a formula or its string representation.
line_numbers (AbstractSet[int]) – line numbers in the proof of formulas of which implication is a tautological implication.

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 'Ex[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

flipped (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 that is the same as the given equality, except that the two sides of the equality are exchanged.

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, 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 that are z followed by a number.
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 that are z followed by a number, 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'.