# 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 prenex-normal-form sentences is closed.

Parameters

sentences (`AbstractSet`[`Formula`]) – set of prenex-normal-form sentences to check.

Return type

`bool`

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 prenex-normal-form sentences is primitively closed.

Parameters

sentences (`AbstractSet`[`Formula`]) – set of prenex-normal-form sentences to check.

Return type

`bool`

Returns

`True` if for every n-ary 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 prenex-normal-form sentences is universally closed.

Parameters

sentences (`AbstractSet`[`Formula`]) – set of prenex-normal-form sentences to check.

Return type

`bool`

Returns

`True` if for every universally quantified sentence from the given set of sentences, and for every constant name from these sentences, the statement quantified by this sentence, with every free occurrence of the universal quantification variable name replaced with this constant name, is also in the given set; `False` otherwise.

`predicates.completeness.``is_existentially_closed`(sentences)

Checks whether the given set of prenex-normal-form sentences is existentially closed.

Parameters

sentences (`AbstractSet`[`Formula`]) – set of prenex-normal-form sentences to check.

Return type

`bool`

Returns

`True` if for every existentially quantified sentence from the given set of sentences there exists a constant name such that the statement quantified by this sentence, with every free occurrence of the existential quantification variable name replaced with this constant name, is also in the given set; `False` otherwise.

`predicates.completeness.``find_unsatisfied_quantifier_free_sentence`(sentences, model, unsatisfied)

Given a universally and existentially closed set of prenex-normal-form 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 quantifier-free sentence from the given set that the given model does not satisfy.

Parameters
• sentences (`Container`[`Formula`]) –

universally and existentially closed set of prenex-normal-form 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 is `get_constants``(``sentences``)`.

• unsatisfied (`Formula`) – sentence (which possibly contains quantifiers) from the given sentences that is not satisfied by the given model.

Return type

`Formula`

Returns

A quantifier-free sentence from the given set of sentences that is not satisfied by the given model.

`predicates.completeness.``get_primitives`(quantifier_free)

Finds all primitive subformulas of the given quantifier-free formula.

Parameters

quantifier_free (`Formula`) – quantifier-free formula that contains no function names and no equalities, whose subformulas are to be searched.

Return type
Returns

The primitive subformulas (i.e., relation invocations) of which the given quantifier-free formula is composed using logical operators.

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 prenex-normal-form sentences holds, or proves a contradiction from these sentences.

Parameters

sentences (`AbstractSet`[`Formula`]) – closed set of prenex-normal-form sentences that contain no function names and no equalities, to either find a model of, 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 include `AXIOMS`.

• proof_from_negation (`Proof`) – valid proof of a contradiction from the same assumptions/axioms of `proof_from_affirmation`, but with one simple assumption (i.e., without any templates) `assumption` replaced with its negation `'~``assumption``'`.

Return type

`Proof`

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, universal, constant)

Converts the given proof of a contradiction, whose assumptions/axioms include `universal` and `instantiation`, where the latter is the universal instantiation of the former with the constant name `constant`, to a proof of a contradiction from the same assumptions without `instantiation`.

Parameters
• proof (`Proof`) – valid proof of a contradiction from one or more assumptions/axioms that are all sentences and that include `AXIOMS`.

• universal (`Formula`) – assumption of the given proof that is universally quantified.

• constant (`str`) – constant name such that the formula `instantiation` obtained from the statement quantified by `universal` by replacing all free occurrences of the universal quantification variable name by the given constant name, is an assumption of the given proof.

Return type

`Proof`

Returns

A valid proof of a contradiction from the assumptions/axioms of the given 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`]) – prenex-normal-form 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 from the statement quantified by any universally quantified sentence from the given sentences by replacing all occurrences of the quantification variable name with some constant name from the given sentences.

`predicates.completeness.``replace_constant`(proof, constant, variable='zz')

Replaces all occurrences of the given constant name in the given proof with the given variable name.

Parameters
• proof (`Proof`) – valid proof in which to replace.

• constant (`str`) – constant name that does not appear as a template constant name in any of the assumptions of the given proof.

• variable (`str`) – variable name that does not appear anywhere in the given proof or in its assumptions.

Return type

`Proof`

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, existential, constant)

Converts the given proof of a contradiction, whose assumptions/axioms include `existential` and `witness`, where the latter is the existential witness of the former with the witnessing constant name `constant`, to a proof of a contradiction from the same assumptions without `witness`.

Parameters
• proof (`Proof`) – valid proof, which does not contain the variable name `'zz'` in its lines or assumptions, of a contradiction from one or more assumptions/axioms that are all sentences and that include `AXIOMS`.

• existential (`Formula`) – assumption of the given proof that is existentially quantified.

• constant (`str`) – constant name such that the formula `witness` obtained from from the statement quantified by `existential` by replacing all free occurrences of the existential quantification variable name by the given constant name, is an assumption of the given proof, and such that this constant name does not appear in any assumption of the given proof except `witness`.

Return type

`Proof`

Returns

A valid proof of a contradiction from the assumptions/axioms of the given 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 sentence from these sentences for which an existential witness is missing.

Parameters

sentences (`AbstractSet`[`Formula`]) – prenex-normal-form 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 statement quantified by that sentence by replacing all occurrences of the quantification variable name with a new constant name obtained by calling `next``(``fresh_constant_name_generator``)`.