predicates.prenex module¶
Conversion of predicatelogic 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.

predicates.prenex.
is_in_prenex_normal_form
(formula)¶ Checks if the given formula is in prenex normal form.

predicates.prenex.
equivalence_of
(formula1, formula2)¶ States the equivalence of the two given formulas as a formula.

predicates.prenex.
has_uniquely_named_variables
(formula)¶ Checks if the given formula has uniquely named variables.
 Parameters
formula (
Formula
) – formula to check. Return type
 Returns
False
if in the given formula some variable name has both quantified 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 withz
. 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 ofequivalence_of
(
formula
,
returned_formula
)
) viaAXIOMS
andADDITIONAL_QUANTIFICATION_AXIOMS
.
Examples
>>> formula = Formula.parse('~(w=xAw[(Ex[(x=w&Aw[w=x])]>Ax[x=y])])') >>> returned_formula, proof = _uniquely_rename_quantified_variables(formula) >>> returned_formula ~(w=xAz58[(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
'~
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
]
…]]'
wheren
>=0, eachQi
is a quantifier, eachxi
is a variable name, andinner_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 eachQ'i
is a quantifier, and where thexi
variable names andinner_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 ofequivalence_of
(
formula
,
returned_formula
)
) viaAXIOMS
andADDITIONAL_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
'(
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, eachQi
is a quantifier, eachxi
is a variable name, andinner_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 eachQ'i
is a quantifier, and where the operator*
, thexi
variable names,inner_first
, andsecond
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 ofequivalence_of
(
formula
,
returned_formula
)
) viaAXIOMS
andADDITIONAL_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
*
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, eachQi
is a quantifier, eachxi
is a variable name, andinner_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 eachQ'i
is a quantifier, and where the operator*
, thexi
variable names,first
, andinner_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 ofequivalence_of
(
formula
,
returned_formula
)
) viaAXIOMS
andADDITIONAL_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
'(
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, eachQi
andPi
is a quantifier, eachxi
andyi
is a variable name, and neitherinner_first
norinner_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 eachQ'i
andP'i
is a quantifier, and where the operator*
, thexi
andyi
variable names,inner_first
, andinner_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 ofequivalence_of
(
formula
,
returned_formula
)
) viaAXIOMS
andADDITIONAL_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
 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
)
) viaAXIOMS
andADDITIONAL_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 starting withz
. 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
)
) viaAXIOMS
andADDITIONAL_QUANTIFICATION_AXIOMS
.
Examples
>>> formula = Formula.parse('~(w=xAw[(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