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 current lines 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: (R(c)->Ex[R(x)]) [templates: R, c, x], Schema: c=c [templates: c], Schema: ((Ax[(R(x)->Q())]&Ex[R(x)])->Q()) [templates: Q, R, x], Schema: (Ax[R(x)]->R(c)) [templates: R, c, x], Schema: (Ax[(Q()->R(x))]->(Q()->Ax[R(x)])) [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
  • 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 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, unquantified_line_number)

Appends to the proof being created by the current prover a line that validly justifies the given universally quantified formula, whose predicate 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.

  • unquantified_line_number (int) – line number in the proof of the predicate of the given quantified 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 of the formula of 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[predicate]'.

  • term (Union[Term, str]) – term, specified as either a term or its string representation, that when substituted into the free occurrences of x in predicate 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 the conclusion of a tautological inference whose assumptions are 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 from which conclusion can be a tautologically inferred.

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 second specified already existing line of the proof, whose antecedent is existentially quantified 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 an equality from 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 the free variable names of the formula of 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 variables, 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 names 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 an equality from 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 two equalities from 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 equalities from 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'.