AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug ~~Donate~~ Contacts

Quantifiers

Description

Summary

Decides forall x in S : P, exists x in S : P and exists! x in S : P where a decision is available, and says nothing where it is not.

Remarks

Three routes, in the order Sullivan and Mackey's proofs book (#1409) teaches them. Over a finite set the body
is evaluated at every member, which is the definition; a member the body cannot decide
leaves the statement as written unless the members it can decide settle it, as one
counterexample settles forall. Over an infinite set the first thing tried is a
named witness: a handful of members of the set, chosen for being where a claim
usually fails — 0, ±1, ±2, a half, an end of an interval, i in the complex numbers
— and a member where the body is false disproves forall exactly as one where it
is true proves exists. What a witness cannot do is prove forall or refute
exists, and for that the solver is asked: exists x in S : P holds
where the solution set of P meets S, and forall x in S : P where the
solution set of not P does not.
The solver route is taken only where what it answers is what was asked. Its answer to an
order comparison is a set of reals, so it is asked one only over a set of reals; its
default for a statement it has no arm for is the empty set, which as an answer to
"where does this hold" is a claim, so it is asked only about the shapes it has arms for
— comparisons of two expressions that mention the variable, joined by the connectives.
Whether the solution set meets S is read off the two sets by
Meets(AngouriMath.Entity.Set,AngouriMath.Entity.Set), and where that cannot be read — a set-builder the solver fell back to,
a member whose membership is undecided — the answer is that there is none.
Uniqueness is existence with a count: over a finite set of numbers, whose members are
distinct exactly when unequal; over anything else, from the solver's solution set when it
is a finite set of numbers. A set with a symbol in it is not counted, since two of its
members may be one.
https://github.com/asc-community/AngouriMath/issues/1409

AngouriMath

Table of contents

AngouriMath

Quantifiers

Description

Members