# 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
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 `'(~E``variable``[~``formula``]->A``variable``[``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 `'(E``variable``[~``formula``]->~A``variable``[``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``('(~A``variable``[``formula``]', 'E``variable``[~``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`.