predicates.some_proofs module¶
Some proofs in Predicate Logic.

predicates.some_proofs.
syllogism_proof
(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.
syllogism_proof_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 constructed. Return type
 Returns
A valid proof, constructed using the method
add_universal_instantiation
, of the above inference viaAXIOMS
.

predicates.some_proofs.
syllogism_all_all_proof
(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.
syllogism_all_all_proof_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 constructed. Return type
 Returns
A valid proof, constructed using the method
add_tautological_implication
, of the above inference viaAXIOMS
.

predicates.some_proofs.
syllogism_all_exists_proof
(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.
syllogism_all_exists_proof_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 constructed. Return type
 Returns
A valid proof, constructed using the method
add_existential_derivation
, of the above inference viaAXIOMS
.

predicates.some_proofs.
lovers_proof
(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.
homework_proof
(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.
right_neutral_proof
(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 constructed 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 constructed 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 constructed 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 constructed 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 constructed.
 Return type
 Returns
A valid proof of the above inference via
AXIOMS
.

predicates.some_proofs.
unique_zero_proof
(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.
multiply_zero_proof
(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({'times(x,s(y))=plus(times(x,y),x)', 'plus(x,0)=x', Schema: ((R(0)&Ax[(R(x)>R(s(x)))])>Ax[R(x)]) [templates: R], 'plus(x,s(y))=s(plus(x,y))', 'times(x,0)=0', '~s(x)=0', '(s(x)=s(y)>x=y)'})¶ The seven axioms of Peano arithmetic

predicates.some_proofs.
peano_zero_proof
(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.
russell_paradox_proof
(print_as_proof_forms=False)¶ Proves from the axioms schema of unrestricted comprehension the contradiction
'(z=z&~z=z)'
.

predicates.some_proofs.
_not_exists_not_implies_all_proof
(formula, variable, print_as_proof_forms=False)¶ Proves that
'(~E
variable
[~
formula
]>A
variable
[
formula
])'
. Parameters
 Return type
 Returns
A valid proof of the above formula via
AXIOMS
.

predicates.some_proofs.
_exists_not_implies_not_all_proof
(formula, variable, print_as_proof_forms=False)¶ Proves that
'(E
variable
[~
formula
]>~A
variable
[
formula
])'
. Parameters
 Return type
 Returns
A valid proof of the above formula via
AXIOMS
.