predicates.completeness module¶
Building blocks for proving the Completeness Theorem for Predicate Logic.

predicates.completeness.
get_constants
(formulas)¶ Finds all constant names in the given formulas.
 Parameters
formulas (
AbstractSet
[Formula
]) – formulas to find all constant names in. Return type
 Returns
A set of all constant names used in one or more of the given formulas.

predicates.completeness.
is_closed
(sentences)¶ Checks whether the given set of prenexnormalform sentences is closed.
 Parameters
sentences (
AbstractSet
[Formula
]) – set of prenexnormalform sentences to check. Return type
 Returns
True
if the given set of sentences is primitively, universally, and existentially closed;False
otherwise.

predicates.completeness.
is_primitively_closed
(sentences)¶ Checks whether the given set of prenexnormalform sentences is primitively closed.
 Parameters
sentences (
AbstractSet
[Formula
]) – set of prenexnormalform sentences to check. Return type
 Returns
True
if for every nary relation name from the given sentences, and for every n (not necessarily distinct) constant names from the given sentences, either the invocation of this relation name over these constant names (in order), or the negation of this invocation (or both), is one of the given sentences;False
otherwise.

predicates.completeness.
is_universally_closed
(sentences)¶ Checks whether the given set of prenexnormalform sentences is universally closed.
 Parameters
sentences (
AbstractSet
[Formula
]) – set of prenexnormalform sentences to check. Return type
 Returns
True
if for every universally quantified sentence of the given sentences, and for every constant name from the given sentences, the predicate of this quantified sentence, with every free occurrence of the universal quantification variable replaced with this constant name, is one of the given sentences;False
otherwise.

predicates.completeness.
is_existentially_closed
(sentences)¶ Checks whether the given set of prenexnormalform sentences is existentially closed.
 Parameters
sentences (
AbstractSet
[Formula
]) – set of prenexnormalform sentences to check. Return type
 Returns
True
if for every existentially quantified sentence of the given sentences there exists a constant name such that the predicate of this quantified sentence, with every free occurrence of the existential quantification variable replaced with this constant name, is one of the given sentences;False
otherwise.

predicates.completeness.
find_unsatisfied_quantifier_free_sentence
(sentences, model, unsatisfied)¶ Given a closed set of prenexnormalform sentences, given a model whose universe is the set of all constant names from the given sentences, and given a sentence from the given set that the given model does not satisfy, finds a quantifierfree sentence from the given set that the given model does not satisfy.
 Parameters
sentences (
Container
[Formula
]) –closed set of prenexnormalform sentences, which is only to be accessed using containment queries, i.e., using the
in
operator as in:>>> if sentence in sentences: ... print('contained!')
model (
Model
[str
]) – model for all element names from the given sentences, whose universe isget_constants
(
sentences
)
.unsatisfied (
Formula
) – sentence (which possibly contains quantifiers) from the given sentences that is not satisfied by the given model.
 Return type
 Returns
A quantifierfree sentence from the given sentences that is not satisfied by the given model.

predicates.completeness.
get_primitives
(quantifier_free)¶ Finds all primitive subformulas of the given quantifierfree formula.
 Parameters
quantifier_free (
Formula
) – quantifierfree formula whose subformulas are to be searched. Return type
 Returns
The primitive subformulas (i.e., relation invocations) of the given quantifierfree formula.
Examples
The primitive subformulas of
'(R(c1,d)~(Q(c1)>~R(c2,a)))'
are'R(c1,d)'
,'Q(c1)'
, and'R(c2,a)'
.

predicates.completeness.
model_or_inconsistency
(sentences)¶ Either finds a model in which the given closed set of prenexnormalform sentences holds, or proves a contradiction from these sentences.
 Parameters
sentences (
AbstractSet
[Formula
]) – closed set of prenexnormalform sentences to either find a model for or prove a contradiction from. Return type
 Returns
A model in which all of the given sentences hold if such exists, otherwise a valid proof of a contradiction from the given formulas via
AXIOMS
.

predicates.completeness.
combine_contradictions
(proof_from_affirmation, proof_from_negation)¶ Combines the given two proofs of contradictions, both from the same assumptions/axioms except that the latter has an extra assumption that is the negation of an extra assumption that the former has, into a single proof of a contradiction from only the common assumptions/axioms.
 Parameters
proof_from_affirmation (
Proof
) – valid proof of a contradiction from one or more assumptions/axioms that are all sentences and that includeAXIOMS
.proof_from_negation (
Proof
) – valid proof of a contradiction from the same assumptions/axioms ofproof_from_affirmation
, but with one simple assumptionassumption
replaced with its negation'~
assumption
'
.
 Return type
 Returns
A valid proof of a contradiction from only the assumptions/axioms common to the given proofs (i.e., without
assumption
or its negation).

predicates.completeness.
eliminate_universal_instantiation_assumption
(proof, constant, instantiation, universal)¶ Converts the given proof of a contradiction, whose assumptions/axioms include
universal
andinstantiation
, where the latter is a universal instantiation of the former, to a proof of a contradiction from the same assumptions withoutinstantiation
. Parameters
proof (
Proof
) – valid proof of a contradiction from one or more assumptions/axioms that are all sentences and that includeAXIOMS
.universal (
Formula
) – assumption of the given proof that is universally quantified.instantiation (
Formula
) – assumption of the given proof that is obtained from the predicate ofuniversal
by replacing all free occurrences of the universal quantification variable by some constant.
 Return type
 Returns
A valid proof of a contradiction from the assumptions/axioms of the proof except
instantiation
.

predicates.completeness.
universal_closure_step
(sentences)¶ Augments the given sentences with all universal instantiations of each universally quantified sentence from these sentences, with respect to all constant names from these sentences.
 Parameters
sentences (
AbstractSet
[Formula
]) – prenexnormalform sentences to augment with their universal instantiations. Return type
 Returns
A set of all of the given sentences, and in addition any formula that can be obtained replacing in the predicate of any universally quantified sentence from the given sentences, all occurrences of the quantification variable with some constant from the given sentences.

predicates.completeness.
replace_constant
(proof, constant, variable='zz')¶ Replaces all occurrences of the given constant in the given proof with the given variable.
 Parameters
 Return type
 Returns
A valid proof where every occurrence of the given constant name in the given proof and in its assumptions is replaced with the given variable name.

predicates.completeness.
eliminate_existential_witness_assumption
(proof, constant, witness, existential)¶ Converts the given proof of a contradiction, whose assumptions/axioms include
existential
andwitness
, where the latter is an existential witness of the former, to a proof of a contradiction from the same assumptions withoutwitness
. Parameters
proof (
Proof
) – valid proof of a contradiction from one or more assumptions/axioms that are all sentences and that includeAXIOMS
.existential (
Formula
) – assumption of the given proof that is existentially quantified.witness (
Formula
) – assumption of the given proof that is obtained from the predicate ofexistential
by replacing all free occurrences of the existential quantification variable by some constant that does not appear in any assumption of the given proof except for this assumption.
 Return type
 Returns
A valid proof of a contradiction from the assumptions/axioms of the proof except
witness
.

predicates.completeness.
existential_closure_step
(sentences)¶ Augments the given sentences with an existential witness that uses a new constant name, for each existentially quantified sentences from these sentences for which an existential witness is missing.
 Parameters
sentences (
AbstractSet
[Formula
]) – prenexnormalform sentences to augment with any missing existential witnesses. Return type
 Returns
A set of all of the given sentences, and in addition for every existentially quantified sentence from the given sentences, a formula obtained from the predicate of that quantified sentence by replacing all occurrences of the quantification variable with a new constant name obtained by calling
next
(
fresh_constant_name_generator
)
.