# 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
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 starting with `z`.

Return type
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(
True
```
`predicates.prenex.``_pull_out_quantifications_across_negation`(formula)

Converts the given formula with uniquely named variables of the form `'~``Q1``x1``[``Q2``x2``[``Qn``xn``[``inner_formula``]``]]'` to an equivalent formula of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[~``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 `'~``Q1``x1``[``Q2``x2``[``Qn``xn``[``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
Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[~``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(
True
```
`predicates.prenex.``_pull_out_quantifications_from_left_across_binary_operator`(formula)

Converts the given formula with uniquely named variables of the form `'(``Q1``x1``[``Q2``x2``[``Qn``xn``[``inner_first``]``]]``*``second``)'` to an equivalent formula of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[(``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 `'(``Q1``x1``[``Q2``x2``[``Qn``xn``[``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
Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[(``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(
True
```
`predicates.prenex.``_pull_out_quantifications_from_right_across_binary_operator`(formula)

Converts the given formula with uniquely named variables of the form `'(``first``*``Q1``x1``[``Q2``x2``[``Qn``xn``[``inner_second``]``]])'` to an equivalent formula of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[(``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``*``Q1``x1``[``Q2``x2``[``Qn``xn``[``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
Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[(``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(
True
```
`predicates.prenex.``_pull_out_quantifications_across_binary_operator`(formula)

Converts the given formula with uniquely named variables of the form `'(``Q1``x1``[``Q2``x2``[``Qn``xn``[``inner_first``]``]]``*``P1``y1``[``P2``y2``[``Pm``ym``[``inner_second``]``]])'` to an equivalent formula of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[``P'1``y1``[``P'2``y2``[``P'm``ym``[(``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 `'(``Q1``x1``[``Q2``x2``[``Qn``xn``[``inner_first``]``]]``*``P1``y1``[``P2``y2``[``Pm``ym``[``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
Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form `'``Q'1``x1``[``Q'2``x2``[``Q'n``xn``[``P'1``y1``[``P'2``y2``[``P'm``ym``[(``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(
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
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(
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 starting with `z`.

Return type
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(