# 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 `x` that is assigned the value `True` in the given model, and `'~``x``'` for each variable `x` that is assigned the value `False`.

Parameters

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

Return type
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
Return type

`Proof`

Returns

If the given formula evaluates to `True` in the given model, then a valid proof of the 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': True})
>>> 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': False})
>>> 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 given two 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
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
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 for or prove `'~(p->p)'` from.

Return type
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
Return type

`Proof`

Returns

If the given formula evaluates to `True` in the given model, then a valid proof of the 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': False, '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': True, 'p': True})
>>> proof.is_valid()
True
>>> proof.statement.conclusion
(p&q7)
>>> proof.statement.assumptions
(p, q7)
>>> proof.rules == AXIOMATIC_SYSTEM_FULL
True
```