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: Set[str]
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: Set[Formula]
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: Union[Model[str], Proof]
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: Set[Formula]
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: Set[Formula]
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).