# predicates.some_proofs module¶

Some proofs in Predicate Logic.

`predicates.some_proofs.``prove_syllogism`(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 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:

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 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:

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 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:

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 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:

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 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:

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 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:

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.``prove_homework`(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.``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
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,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'`).

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 `'(~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

`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 `'(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

`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``('(~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

`Proof`

Returns

A valid proof of the above formula via `AXIOMS`.