Math 2.0

statement theorem

Negation of an existential statement

Statement

Let XX be a set and let P(x)P(x) be a predicate on XX. The negation of ∃x∈X, P(x)\exists x \in X, \, P(x) is logically equivalent to ∀x∈X, ¬P(x)\forall x \in X, \, \neg P(x). ¬(∃x∈X, P(x))≡∀x∈X, ¬P(x)\neg \bigl( \exists x \in X, \, P(x) \bigr) \equiv \forall x \in X, \, \neg P(x)

Remarks

This equivalence is valid in intuitionistic logic as well as in classical logic. Together with the negation of a universal statement, it gives a rule. To negate a quantified statement, swap each ∀\forall and ∃\exists and negate the predicate.

Explanations

L1 human

"No student failed" means "every student did not fail". To deny that some element has a property, you must show that each element lacks it.

What this node needs for W1
  • an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What this needs

To read this node, read these 6 nodes in this order. The foundations come first, and the list ends with this node.

Proposition, concept, no evidence levelPropositionconceptNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionExistential quantifier, definition, no evidence levelExistential quantifierdefinitionUniversal quantifier, definition, no evidence levelUniversal quantifierdefinitionNegation of an existential statement, statement, no evidence levelNegation of an existe…statement
Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.
  • no evidence level
  1. Proposition concept
  2. Negation definition
  3. Predicate definition
  4. Existential quantifier definition
  5. Universal quantifier definition
  6. Negation of an existential statement statement

Sources

  1. Web https://en.wikipedia.org/wiki/Quantifier_(logic), lead section

What links here

No node links to this node yet.