predicates.some_proofs module

Some proofs in Predicate Logic.

predicates.some_proofs.syllogism_proof(print_as_proof_forms=False)

Proves from the assumptions:

  1. All men are mortal ('Ax[(Man(x)->Mortal(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof of the above inference via AXIOMS.

predicates.some_proofs.syllogism_proof_with_universal_instantiation(print_as_proof_forms=False)

Using the method add_universal_instantiation, proves from the assumptions:

  1. All men are mortal ('Ax[(Man(x)->Mortal(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof, constructed using the method add_universal_instantiation, of the above inference via AXIOMS.

predicates.some_proofs.syllogism_all_all_proof(print_as_proof_forms=False)

Proves from the assumptions:

  1. All Greeks are human ('Ax[(Greek(x)->Human(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof of the above inference via AXIOMS.

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:

  1. All Greeks are human ('Ax[(Greek(x)->Human(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof, constructed using the method add_tautological_implication, of the above inference via AXIOMS.

predicates.some_proofs.syllogism_all_exists_proof(print_as_proof_forms=False)

Proves from the assumptions:

  1. All men are mortal ('Ax[(Man(x)->Mortal(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof of the above inference via AXIOMS.

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:

  1. All men are mortal ('Ax[(Man(x)->Mortal(x))]'), and

  2. 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 constructed.

Return type

Proof

Returns

A valid proof, constructed using the method add_existential_derivation, of the above inference via AXIOMS.

predicates.some_proofs.lovers_proof(print_as_proof_forms=False)

Proves from the assumptions:

  1. Everybody loves somebody ('Ax[Ey[Loves(x,y)]]'), and

  2. 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.homework_proof(print_as_proof_forms=False)

Proves from the assumptions:

  1. No homework is fun ('~Ex[(Homework(x)&Fun(x))]'), and

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

Proof

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

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

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

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

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._not_exists_not_implies_all_proof(formula, variable, print_as_proof_forms=False)

Proves that '(~Evariable[~formula]->Avariable[formula])'.

Parameters
  • formula (Formula) – predicate for the universal quantification in the formula to be proven.

  • variable (str) – variable name for the quantifications 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 constructed.

Return type

Proof

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

Parameters
  • formula (Formula) – predicate for the universal quantification in the formula to be proven.

  • variable (str) – variable name for the quantifications 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 constructed.

Return type

Proof

Returns

A valid proof of the above formula via AXIOMS.

predicates.some_proofs.not_all_iff_exists_not_proof(formula, variable, print_as_proof_forms=False)

Proves that equivalence_of('(~Avariable[formula]', 'Evariable[~formula]').

Parameters
  • formula (Formula) – predicate for the universal quantification in the formula to be proven.

  • variable (str) – variable name for the quantifications 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 constructed.

Return type

Proof

Returns

A valid proof of the above formula via AXIOMS.