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))]'), and
Aristotle 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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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))]'), and
Aristotle 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: Proof
Returns: A valid proof, created with the help of the method add_universal_instantiation, of the above inference via AXIOMS.

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))]'), and
All 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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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))]'), and
All 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: Proof
Returns: A valid proof, created with the help of the method add_tautological_implication, of the above inference via AXIOMS.

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))]'), and
Some 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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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))]'), and
Some 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: Proof
Returns: A valid proof, created with the help of the method add_existential_derivation, of the above inference via AXIOMS.

predicates.some_proofs.prove_lovers(print_as_proof_forms=False)¶

Proves from the assumptions:

Everybody loves somebody ('Ax[Ey[Loves(x,y)]]'), and
Everybody loves a lover ('Ax[Az[Ay[(Loves(x,y)->Loves(z,x))]]]')

the conclusion: Everybody loves everybody ('Ax[Az[Loves(z,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: Proof
Returns: A valid proof of the above inference via AXIOMS.

predicates.some_proofs.prove_homework(print_as_proof_forms=False)¶

Proves from the assumptions:

No homework is fun ('~Ex[(Homework(x)&Fun(x))]'), and
Some reading is homework ('Ex[(Homework(x)&Reading(x))]')

the conclusion: Some reading is not fun ('Ex[(Reading(x)&~Fun(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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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 to add_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 to add_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 to add_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 to add_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

Proof

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').

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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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').

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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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,0)=x', 'times(x,s(y))=plus(times(x,y),x)', '~s(x)=0', Schema: ((R(0)&Ax[(R(x)->R(s(x)))])->Ax[R(x)]) [templates: R], '(s(x)=s(y)->x=y)', 'plus(x,s(y))=s(plus(x,y))', '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').

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: Proof
Returns: A valid proof of the above inference via AXIOMS.

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)'.

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: Proof
Returns: A valid proof of the above inference via AXIOMS.

predicates.some_proofs._prove_not_exists_not_implies_all(variable, formula, print_as_proof_forms=False)¶

Proves that '(~Evariable[~formula]->Avariable[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

Proof

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 '(Evariable[~formula]->~Avariable[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

Proof

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('(~Avariable[formula]', 'Evariable[~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

Proof

Returns

A valid proof of the above formula via AXIOMS.