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 predicatelogic 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[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], Schema: ((Ax[(R(x)>Q())]&Ex[R(x)])>Q()) [templates: Q, R, x]})¶ Axiomatic system for Predicate Logic, consisting of
UI
,EI
,US
,ES
,RX
, andME
.

__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 beyondAXIOMS
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.

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

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
 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
 Return type
 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
 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'A
x
[
predicate
]'
.term (
Union
[Term
,str
]) – term, specified as either a term or its string representation, that when substituted into the free occurrences ofx
inpredicate
yields the given formula.
 Return type
 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)]]'
andterm
is'h(w)'
, theninstantiation
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
 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'E
x
[
antecedent(x)
]'
, wherex
is a variable name that may have free occurrences inantecedent(x)
but has no free occurrences inconsequent
.line_number2 (
int
) – line number in the proof of the formula'(
antecedent(x)
>
consequent
)'
.
 Return type
 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
 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 withz
, 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 withz
.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 withz
, 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
 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)])'
andsubstitution_map
is{'y': 'h(w)', 'z': 'y'}
, theninstantiation
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
 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)'
andparametrized_term
is'_+7'
, thensubstituted
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
 Return type
 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 Lineline_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 lefthand side of the first equality is the lefthand side of the given equality, the righthand of each equality (except for the last) is the lefthand side of the next equality, and the righthand side of the last equality is the righthand side of the given equality.
 Return type
 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'
, thenchained
should be'a=0'
.