predicates.some_proofs module¶
Some proofs in Predicate Logic.

predicates.some_proofs.
prove_syllogism
(print_as_proof_forms=False)¶ Proves from the assumptions:
All men are mortal (
'Ax[(Man(x)>Mortal(x))]'
), andAristotle is a man (
'Man(aristotle)'
)
the conclusion: Aristotle is mortal (
'Mortal(aristotle)'
).

predicates.some_proofs.
prove_syllogism_with_universal_instantiation
(print_as_proof_forms=False)¶ Using the method
add_universal_instantiation
, proves from the assumptions:All men are mortal (
'Ax[(Man(x)>Mortal(x))]'
), andAristotle is a man (
'Man(aristotle)'
)
the conclusion: Aristotle is mortal (
'Mortal(aristotle)'
). Parameters
print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created. Return type
 Returns
A valid proof, created with the help of the method
add_universal_instantiation
, of the above inference viaAXIOMS
.

predicates.some_proofs.
prove_syllogism_all_all
(print_as_proof_forms=False)¶ Proves from the assumptions:
All Greeks are human (
'Ax[(Greek(x)>Human(x))]'
), andAll humans are mortal (
'Ax[(Human(x)>Mortal(x))]'
)
the conclusion: All Greeks are mortal (
'Ax[(Greek(x)>Mortal(x))]'
).

predicates.some_proofs.
prove_syllogism_all_all_with_tautological_implication
(print_as_proof_forms=False)¶ Using the method
add_tautological_implication
, proves from the assumptions:All Greeks are human (
'Ax[(Greek(x)>Human(x))]'
), andAll humans are mortal (
'Ax[(Human(x)>Mortal(x))]'
)
the conclusion: All Greeks are mortal (
'Ax[(Greek(x)>Mortal(x))]'
). Parameters
print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created. Return type
 Returns
A valid proof, created with the help of the method
add_tautological_implication
, of the above inference viaAXIOMS
.

predicates.some_proofs.
prove_syllogism_all_exists
(print_as_proof_forms=False)¶ Proves from the assumptions:
All men are mortal (
'Ax[(Man(x)>Mortal(x))]'
), andSome men exist (
'Ex[Man(x)]'
)
the conclusion: Some mortals exist (
'Ex[Mortal(x)]'
).

predicates.some_proofs.
prove_syllogism_all_exists_with_existential_derivation
(print_as_proof_forms=False)¶ Using the method
add_existential_derivation
, proves from the assumptions:All men are mortal (
'Ax[(Man(x)>Mortal(x))]'
), andSome men exist (
'Ex[Man(x)]'
)
the conclusion: Some mortals exist (
'Ex[Mortal(x)]'
). Parameters
print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created. Return type
 Returns
A valid proof, created with the help of the method
add_existential_derivation
, of the above inference viaAXIOMS
.

predicates.some_proofs.
prove_lovers
(print_as_proof_forms=False)¶ Proves from the assumptions:
Everybody loves somebody (
'Ax[Ey[Loves(x,y)]]'
), andEverybody loves a lover (
'Ax[Az[Ay[(Loves(x,y)>Loves(z,x))]]]'
)
the conclusion: Everybody loves everybody (
'Ax[Az[Loves(z,x)]]'
).

predicates.some_proofs.
prove_homework
(print_as_proof_forms=False)¶ Proves from the assumptions:
No homework is fun (
'~Ex[(Homework(x)&Fun(x))]'
), andSome reading is homework (
'Ex[(Homework(x)&Reading(x))]'
)
the conclusion: Some reading is not fun (
'Ex[(Reading(x)&~Fun(x))]'
).

predicates.some_proofs.
GROUP_AXIOMS
= frozenset({'plus(0,x)=x', 'plus(minus(x),x)=0', 'plus(plus(x,y),z)=plus(x,plus(y,z))'})¶ The three group axioms

predicates.some_proofs.
prove_group_right_neutral
(stop_before_flipped_equality, stop_before_free_instantiation, stop_before_substituted_equality, stop_before_chained_equality, print_as_proof_forms=False)¶ Proves from the group axioms that x+0=x (
'plus(x,0)=x'
). Parameters
stop_before_flipped_equality (
bool
) – flag specifying to stop proving just before the first call toadd_flipped_equality
and to return the prefix of the proof created up to that point.stop_before_free_instantiation (
bool
) – flag specifying to stop proving just before the first call toadd_free_instantiation
and to return the prefix of the proof created up to that point.stop_before_substituted_equality (
bool
) – flag specifying stop proving just before the first call toadd_substituted_equality
and to return the prefix of the proof created up to that point.stop_before_chained_equality (
bool
) – flag specifying to stop proving just before the first call toadd_chained_equality
and to return the prefix of the proof created up to that point.print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created.
 Return type
 Returns
A valid proof of the above inference via
AXIOMS
.

predicates.some_proofs.
prove_group_unique_zero
(print_as_proof_forms=False)¶ Proves from the group axioms and from the assumption a+c=a (
'plus(a,c)=a'
) that c=0 ('c=0'
).

predicates.some_proofs.
FIELD_AXIOMS
= frozenset({'(~x=0>Ey[times(y,x)=1])', 'plus(0,x)=x', 'plus(minus(x),x)=0', 'plus(plus(x,y),z)=plus(x,plus(y,z))', 'plus(x,y)=plus(y,x)', 'times(times(x,y),z)=times(x,times(y,z))', 'times(x,1)=x', 'times(x,plus(y,z))=plus(times(x,y),times(x,z))', 'times(x,y)=times(y,x)'})¶ The six field axioms

predicates.some_proofs.
prove_field_zero_multiplication
(print_as_proof_forms=False)¶ Proves from the field axioms that 0*x=0 (
'times(0,x)=0'
).

predicates.some_proofs.
INDUCTION_AXIOM
= Schema: ((R(0)&Ax[(R(x)>R(s(x)))])>Ax[R(x)]) [templates: R]¶ Axiom schema of induction

predicates.some_proofs.
PEANO_AXIOMS
: FrozenSet[Union[str, predicates.proofs.Schema]] = frozenset({'plus(x,s(y))=s(plus(x,y))', '(s(x)=s(y)>x=y)', '~s(x)=0', 'times(x,s(y))=plus(times(x,y),x)', Schema: ((R(0)&Ax[(R(x)>R(s(x)))])>Ax[R(x)]) [templates: R], 'plus(x,0)=x', 'times(x,0)=0'})¶ The seven axioms of Peano arithmetic

predicates.some_proofs.
prove_peano_left_neutral
(print_as_proof_forms=False)¶ Proves from the axioms of Peano arithmetic that 0+x=x (
'plus(0,x)=x'
).

predicates.some_proofs.
COMPREHENSION_AXIOM
= Schema: Ey[Ax[((In(x,y)>R(x))&(R(x)>In(x,y)))]] [templates: R]¶ Axiom schema of (unrestricted) comprehension

predicates.some_proofs.
prove_russell_paradox
(print_as_proof_forms=False)¶ Proves from the axioms schema of unrestricted comprehension the contradiction
'(z=z&~z=z)'
.

predicates.some_proofs.
_prove_not_exists_not_implies_all
(variable, formula, print_as_proof_forms=False)¶ Proves that
'(~E
variable
[~
formula
]>A
variable
[
formula
])'
. Parameters
variable (
str
) – variable name for the quantifications in the formula to be proven.formula (
Formula
) – statement to be universally quantified, and whose negation is to be existentially quantified, in the formula to be proven.print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created.
 Return type
 Returns
A valid proof of the above formula via
AXIOMS
.

predicates.some_proofs.
_prove_exists_not_implies_not_all
(variable, formula, print_as_proof_forms=False)¶ Proves that
'(E
variable
[~
formula
]>~A
variable
[
formula
])'
. Parameters
variable (
str
) – variable name for the quantifications in the formula to be proven.formula (
Formula
) – statement to be universally quantified, and whose negation is to be existentially quantified, in the formula to be proven.print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created.
 Return type
 Returns
A valid proof of the above formula via
AXIOMS
.

predicates.some_proofs.
prove_not_all_iff_exists_not
(variable, formula, print_as_proof_forms=False)¶ Proves that
equivalence_of
('(~A
variable
[
formula
]', 'E
variable
[~
formula
]')
. Parameters
variable (
str
) – variable name for the quantifications in the formula to be proven.formula (
Formula
) – statement to be universally quantified, and whose negation is to be existentially quantified, in the formula to be proven.print_as_proof_forms (
bool
) – flag specifying whether the proof is to be printed in real time as it is being created.
 Return type
 Returns
A valid proof of the above formula via
AXIOMS
.