predicates.prenex module¶

Conversion of predicate-logic formulas into prenex normal form.

predicates.prenex.ADDITIONAL_QUANTIFICATION_AXIOMS = (Schema: ((~Ax[R(x)]->Ex[~R(x)])&(Ex[~R(x)]->~Ax[R(x)])) [templates: R, x], Schema: ((~Ex[R(x)]->Ax[~R(x)])&(Ax[~R(x)]->~Ex[R(x)])) [templates: R, x], Schema: (((Ax[R(x)]&Q())->Ax[(R(x)&Q())])&(Ax[(R(x)&Q())]->(Ax[R(x)]&Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]&Q())->Ex[(R(x)&Q())])&(Ex[(R(x)&Q())]->(Ex[R(x)]&Q()))) [templates: Q, R, x], Schema: (((Q()&Ax[R(x)])->Ax[(Q()&R(x))])&(Ax[(Q()&R(x))]->(Q()&Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()&Ex[R(x)])->Ex[(Q()&R(x))])&(Ex[(Q()&R(x))]->(Q()&Ex[R(x)]))) [templates: Q, R, x], Schema: (((Ax[R(x)]|Q())->Ax[(R(x)|Q())])&(Ax[(R(x)|Q())]->(Ax[R(x)]|Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]|Q())->Ex[(R(x)|Q())])&(Ex[(R(x)|Q())]->(Ex[R(x)]|Q()))) [templates: Q, R, x], Schema: (((Q()|Ax[R(x)])->Ax[(Q()|R(x))])&(Ax[(Q()|R(x))]->(Q()|Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()|Ex[R(x)])->Ex[(Q()|R(x))])&(Ex[(Q()|R(x))]->(Q()|Ex[R(x)]))) [templates: Q, R, x], Schema: (((Ax[R(x)]->Q())->Ex[(R(x)->Q())])&(Ex[(R(x)->Q())]->(Ax[R(x)]->Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]->Q())->Ax[(R(x)->Q())])&(Ax[(R(x)->Q())]->(Ex[R(x)]->Q()))) [templates: Q, R, x], Schema: (((Q()->Ax[R(x)])->Ax[(Q()->R(x))])&(Ax[(Q()->R(x))]->(Q()->Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()->Ex[R(x)])->Ex[(Q()->R(x))])&(Ex[(Q()->R(x))]->(Q()->Ex[R(x)]))) [templates: Q, R, x], Schema: (((R(x)->Q(x))&(Q(x)->R(x)))->((Ax[R(x)]->Ay[Q(y)])&(Ay[Q(y)]->Ax[R(x)]))) [templates: Q, R, x, y], Schema: (((R(x)->Q(x))&(Q(x)->R(x)))->((Ex[R(x)]->Ey[Q(y)])&(Ey[Q(y)]->Ex[R(x)]))) [templates: Q, R, x, y])¶: Additional axioms of quantification for Predicate Logic.

predicates.prenex.is_quantifier_free(formula)¶

Checks if the given formula contains any quantifiers.

Parameters: formula (Formula) – formula to check.
Return type: bool
Returns: False if the given formula contains any quantifiers, True otherwise.

predicates.prenex.is_in_prenex_normal_form(formula)¶

Checks if the given formula is in prenex normal form.

Parameters: formula (Formula) – formula to check.
Return type: bool
Returns: True if the given formula in prenex normal form, False otherwise.

predicates.prenex.equivalence_of(formula1, formula2)¶

States the equivalence of the two given formulas as a formula.

Parameters

formula1 (Formula) – first of the formulas the equivalence of which is to be stated.
formula2 (Formula) – second of the formulas the equivalence of which is to be stated.

Return type

Formula

Returns

The formula '((formula1->formula2)&(formula2->formula1))'.

predicates.prenex.has_uniquely_named_variables(formula)¶

Checks if the given formula has uniquely named variables.

Parameters: formula (Formula) – formula to check.
Return type: bool
Returns: False if in the given formula some variable name has both bound and free occurrences or is quantified by more than one quantifier, True otherwise.

Examples

>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ax[R(x)]|Ex[R(x)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ax[R(x)]|Ey[R(y)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(y=0&(Ax[R(x)]|Ex[R(x)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ay[R(y)]|Ez[R(z)]))'))
True

predicates.prenex._uniquely_rename_quantified_variables(formula)¶

Converts the given formula to an equivalent formula with uniquely named variables, and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula to convert, which contains no variable names that are z followed by a number.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, with the exact same structure but with the additional property of having uniquely named variables, obtained by consistently replacing each variable name that is bound in the given formula with a new variable name obtained by calling next(fresh_variable_name_generator). The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~(w=x|Aw[(Ex[(x=w&Aw[w=x])]->Ax[x=y])])')
>>> returned_formula, proof = _uniquely_rename_quantified_variables(
...     formula)
>>> returned_formula
~(w=x|Az58[(Ez17[(z17=z58&Az4[z4=z17])]->Az32[z32=y])])
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex._pull_out_quantifications_across_negation(formula)¶

Converts the given formula with uniquely named variables of the form '~Q1x1[Q2x2[…Qnxn[inner_formula]…]]' to an equivalent formula of the form 'Q'1x1[Q'2x2[…Q'nxn[~inner_formula]…]]', and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula to convert, whose root is a negation, i.e., which is of the form '~Q1x1[Q2x2[…Qnxn[inner_formula]…]]' where n>=0, each Qi is a quantifier, each xi is a variable name, and inner_formula does not start with a quantifier.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[…Q'nxn[~inner_formula]…]]' where each Q'i is a quantifier, and where the xi variable names and inner_formula are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~Ax[Ey[R(x,y)]]')
>>> returned_formula, proof = _pull_out_quantifications_across_negation(
...     formula)
>>> returned_formula
Ex[Ay[~R(x,y)]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex._pull_out_quantifications_from_left_across_binary_operator(formula)¶

Converts the given formula with uniquely named variables of the form '(Q1x1[Q2x2[…Qnxn[inner_first]…]]*second)' to an equivalent formula of the form 'Q'1x1[Q'2x2[…Q'nxn[(inner_first*second)]…]]' and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(Q1x1[Q2x2[…Qnxn[inner_first]…]]*second)' where * is a binary operator, n>=0, each Qi is a quantifier, each xi is a variable name, and inner_first does not start with a quantifier.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[…Q'nxn[(inner_first*second)]…]]' where each Q'i is a quantifier, and where the operator *, the xi variable names, inner_first, and second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]&Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_from_left_across_binary_operator(
...     formula)
>>> returned_formula
Ax[Ey[(R(x,y)&Ez[P(1,z)])]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex._pull_out_quantifications_from_right_across_binary_operator(formula)¶

Converts the given formula with uniquely named variables of the form '(first*Q1x1[Q2x2[…Qnxn[inner_second]…]])' to an equivalent formula of the form 'Q'1x1[Q'2x2[…Q'nxn[(first*inner_second)]…]]' and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(first*Q1x1[Q2x2[…Qnxn[inner_second]…]])' where * is a binary operator, n>=0, each Qi is a quantifier, each xi is a variable name, and inner_second does not start with a quantifier.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[…Q'nxn[(first*inner_second)]…]]' where each Q'i is a quantifier, and where the operator *, the xi variable names, first, and inner_second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]|Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_from_right_across_binary_operator(
...     formula)
>>> returned_formula
Ez[(Ax[Ey[R(x,y)]]|P(1,z))]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex._pull_out_quantifications_across_binary_operator(formula)¶

Converts the given formula with uniquely named variables of the form '(Q1x1[Q2x2[…Qnxn[inner_first]…]]*P1y1[P2y2[…Pmym[inner_second]…]])' to an equivalent formula of the form 'Q'1x1[Q'2x2[…Q'nxn[P'1y1[P'2y2[…P'mym[(inner_first*inner_second)]…]]]…]]' and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(Q1x1[Q2x2[…Qnxn[inner_first]…]]*P1y1[P2y2[…Pmym[inner_second]…]])' where * is a binary operator, n>=0, m>=0, each Qi and Pi is a quantifier, each xi and yi is a variable name, and neither inner_first nor inner_second starts with a quantifier.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[…Q'nxn[P'1y1[P'2y2[…P'mym[(inner_first*inner_second)]…]]]…]]' where each Q'i and P'i is a quantifier, and where the operator *, the xi and yi variable names, inner_first, and inner_second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]->Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_across_binary_operator(
...     formula)
>>> returned_formula
Ex[Ay[Ez[(R(x,y)->P(1,z))]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex._to_prenex_normal_form_from_uniquely_named_variables(formula)¶

Converts the given formula with uniquely named variables to an equivalent formula in prenex normal form, and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula with uniquely named variables to convert.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but in prenex normal form. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(~(Ax[Ey[R(x,y)]]->Ez[P(1,z)])|S(w))')
>>> returned_formula, proof = _to_prenex_normal_form_from_uniquely_named_variables(
...     formula)
>>> returned_formula
Ax[Ey[Az[(~(R(x,y)->P(1,z))|S(w))]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True

predicates.prenex.to_prenex_normal_form(formula)¶

Converts the given formula to an equivalent formula in prenex normal form, and proves the equivalence of these two formulas.

Parameters: formula (Formula) – formula to convert, which contains no variable names that are z followed by a number.
Return type: Tuple[Formula, Proof]
Returns: A pair. The first element of the pair is a formula equivalent to the given formula, but in prenex normal form. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~(w=x|Aw[(Ex[(x=w&Aw[w=x])]->Ax[x=y])])')
>>> returned_formula, proof = to_prenex_normal_form(formula)
>>> returned_formula
Ez58[Ez17[Az4[Ez32[~(w=x|((z17=z58&z4=z17)->z32=y))]]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True