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 namex
that is assigned the valueTrue
in the given model, and'~
x
'
for each variable namex
that is assigned the valueFalse
.- 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
- Returns
If
formula
evaluates toTrue
in the given model, then a valid proof offormula
; otherwise a valid proof of'~
formula
'
. The returned proof is from the formulas that capture the given model, in the order returned byformulas_capturing_model
(
model
)
, viaAXIOMATIC_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 ofconclusion
from only the common assumptions.- Parameters
proof_from_affirmation (
Proof
) – valid proof ofconclusion
from one or more assumptions, the last of which is an assumptionassumption
.proof_from_negation (
Proof
) – valid proof ofconclusion
from the same assumptions and inference rules ofproof_from_affirmation
, but with the last assumption being'~
assumption
'
instead ofassumption
.
- Return type
- 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 additionMP
,I0
,I1
,D
, andR
.
Examples
If
proof_from_affirmation
is of['p', '~q', 'r'] ==> '(p&(r|~r))'
, thenproof_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
- 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
)
, viaAXIOMATIC_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
- 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
- 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
- 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 viaAXIOMATIC_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
- Returns
If
formula
evaluates toTrue
in the given model, then a valid proof offormula
; otherwise a valid proof of'~
formula
'
. The returned proof is from the formulas that capture the given model, in the order returned byformulas_capturing_model
(
model
)
, viaAXIOMATIC_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