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 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 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 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 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]) –

    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 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 whose subformulas are to be searched.

Return type

Set[Formula]

Returns

The primitive subformulas (i.e., relation invocations) of the given quantifier-free 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 prenex-normal-form sentences holds, or proves a contradiction from these sentences.

Parameters

sentences (AbstractSet[Formula]) – closed set of prenex-normal-form sentences to either find a model for 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 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, constant, instantiation, universal)

Converts the given proof of a contradiction, whose assumptions/axioms include universal and instantiation, where the latter is a universal instantiation of the former, 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.

  • instantiation (Formula) – assumption of the given proof that is obtained from the predicate of universal by replacing all free occurrences of the universal quantification variable by some constant.

Return type

Proof

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]) – 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 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
  • 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 given the 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, constant, witness, existential)

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

Parameters
  • proof (Proof) – valid proof 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.

  • witness (Formula) – assumption of the given proof that is obtained from the predicate of existential 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

Proof

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]) – 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 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).