propositions.tautology module

The Tautology Theorem and its implications.

propositions.tautology.formulas_capturing_model(model)

Computes the formulas that capture the given model: 'x' for each variable name x that is assigned the value True in the given model, and '~x' for each variable name x that is assigned the value False.

Parameters

model (Mapping[str, bool]) – model to construct the formulas for.

Return type

List[Formula]

Returns

A list of the constructed formulas, ordered alphabetically by variable name.

Examples

>>> formulas_capturing_model({'p2': False, 'p1': True, 'q': True})
[p1, ~p2, q]
propositions.tautology.prove_in_model(formula, model)

Either proves the given formula or proves its negation, from the formulas that capture the given model.

Parameters
  • formula (Formula) – formula that contains no constants or operators beyond '->' and '~', whose affirmation or negation is to prove.

  • model (Mapping[str, bool]) – model from whose formulas to prove.

Return type

Proof

Returns

If formula evaluates to True in the given model, then a valid proof of formula; otherwise a valid proof of '~formula'. The returned proof is from the formulas that capture the given model, in the order returned by formulas_capturing_model(model), via AXIOMATIC_SYSTEM.

Examples

>>> proof = prove_in_model(Formula.parse('(p->q7)'),
...                        {'q7': False, 'p': False})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
(p->q7)
>>> proof.statement.assumptions
(~p, ~q7)
>>> proof.rules == AXIOMATIC_SYSTEM
True
>>> proof = prove_in_model(Formula.parse('(p->q7)'),
...                        {'q7': False, 'p': True})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
~(p->q7)
>>> proof.statement.assumptions
(p, ~q7)
>>> proof.rules == AXIOMATIC_SYSTEM
True
propositions.tautology.reduce_assumption(proof_from_affirmation, proof_from_negation)

Combines the two given proofs, both of the same formula conclusion and from the same assumptions except that the last assumption of the latter is the negation of that of the former, into a single proof of conclusion from only the common assumptions.

Parameters
  • proof_from_affirmation (Proof) – valid proof of conclusion from one or more assumptions, the last of which is an assumption assumption.

  • proof_from_negation (Proof) – valid proof of conclusion from the same assumptions and inference rules of proof_from_affirmation, but with the last assumption being '~assumption' instead of assumption.

Return type

Proof

Returns

A valid proof of conclusion from only the assumptions common to the given proofs (i.e., without the last assumption of each), via the same inference rules of the given proofs and in addition MP, I0, I1, D, and R.

Examples

If proof_from_affirmation is of ['p', '~q', 'r'] ==> '(p&(r|~r))', then proof_from_negation must be of ['p', '~q', '~r'] ==> '(p&(r|~r))' and the returned proof is of ['p', '~q'] ==> '(p&(r|~r))'.

propositions.tautology.prove_tautology(tautology, model={})

Proves the given tautology from the formulas that capture the given model.

Parameters
  • tautology (Formula) – tautology that contains no constants or operators beyond '->' and '~', to prove.

  • model (Mapping[str, bool]) – model over a (possibly empty) prefix (with respect to the alphabetical order) of the variable names of tautology, from whose formulas to prove.

Return type

Proof

Returns

A valid proof of the given tautology from the formulas that capture the given model, in the order returned by formulas_capturing_model(model), via AXIOMATIC_SYSTEM.

Examples

>>> proof = prove_tautology(Formula.parse('(~(p->p)->q)'),
...                         {'p': True, 'q': False})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
(~(p->p)->q)
>>> proof.statement.assumptions
(p, ~q)
>>> proof.rules == AXIOMATIC_SYSTEM
True
>>> proof = prove_tautology(Formula.parse('(~(p->p)->q)'))
>>> proof.is_valid()
True
>>> proof.statement.conclusion
(~(p->p)->q)
>>> proof.statement.assumptions
()
>>> proof.rules == AXIOMATIC_SYSTEM
True
propositions.tautology.proof_or_counterexample(formula)

Either proves the given formula or finds a model in which it does not hold.

Parameters

formula (Formula) – formula that contains no constants or operators beyond '->' and '~', to either prove or find a counterexample for.

Return type

Union[Proof, Mapping[str, bool]]

Returns

If the given formula is a tautology, then an assumptionless proof of the formula via AXIOMATIC_SYSTEM, otherwise a model in which the given formula does not hold.

propositions.tautology.encode_as_formula(rule)

Encodes the given inference rule as a formula consisting of a chain of implications.

Parameters

rule (InferenceRule) – inference rule to encode.

Return type

Formula

Returns

The formula encoding the given rule.

Examples

>>> encode_as_formula(InferenceRule([Formula('p1'), Formula('p2'),
...                                  Formula('p3'), Formula('p4')],
...                                 Formula('q')))
(p1->(p2->(p3->(p4->q))))
>>> encode_as_formula(InferenceRule([], Formula('q')))
q
propositions.tautology.prove_sound_inference(rule)

Proves the given sound inference rule.

Parameters

rule (InferenceRule) – sound inference rule whose assumptions and conclusion contain no constants or operators beyond '->' and '~', to prove.

Return type

Proof

Returns

A valid proof of the given sound inference rule via AXIOMATIC_SYSTEM.

propositions.tautology.model_or_inconsistency(formulas)

Either finds a model in which all the given formulas hold, or proves '~(p->p)' from these formulas.

Parameters

formulas (Sequence[Formula]) – formulas that use only the operators '->' and '~', to either find a model of, or prove '~(p->p)' from.

Return type

Union[Mapping[str, bool], Proof]

Returns

A model in which all of the given formulas hold if such exists, otherwise a valid proof of '~(p->p)' from the given formulas via AXIOMATIC_SYSTEM.

propositions.tautology.prove_in_model_full(formula, model)

Either proves the given formula or proves its negation, from the formulas that capture the given model.

Parameters
  • formula (Formula) – formula that contains no operators beyond '->', '~', '&', and '|' (and may contain constants), whose affirmation or negation is to prove.

  • model (Mapping[str, bool]) – model from whose formulas to prove.

Return type

Proof

Returns

If formula evaluates to True in the given model, then a valid proof of formula; otherwise a valid proof of '~formula'. The returned proof is from the formulas that capture the given model, in the order returned by formulas_capturing_model(model), via AXIOMATIC_SYSTEM_FULL.

Examples

>>> proof = prove_in_model_full(Formula.parse('(p&q7)'),
...                             {'q7': True, 'p': True})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
(p&q7)
>>> proof.statement.assumptions
(p, q7)
>>> proof.rules == AXIOMATIC_SYSTEM_FULL
True
>>> proof = prove_in_model_full(Formula.parse('(p&q7)'),
...                             {'q7': False, 'p': True})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
~(p&q7)
>>> proof.statement.assumptions
(p, ~q7)
>>> proof.rules == AXIOMATIC_SYSTEM_FULL
True