User:Prime.mover/Proof Structures
Ordinary proofs
{{begin-eqn}} {{eqn | q = | l = | o = = | r = | c = }} {{eqn | ll= \leadsto | l = | o = = | r = | c = }} {{end-eqn}}
and so on.
Axiom schemata
{{begin-axiom}} {{axiom | n = \text A 0 | lc= | q = | t = | rc= }} {{axiom | n = \text A 1 | lc= | q = | m = | rc= }} {{axiom | n = \text A 2 | lc= | q = | ml= | mo= | mr= | mm= | rc= }} {{axiom | n = \text A 3 | lc= | q = | tl= | to= | tr= | rc= }} {{end-axiom}}
and so on.
See {{Axiom}}
Definition
== Definition == <onlyinclude> Definition </onlyinclude> === [[Definition:Definiend/Symbol|Symbol]] === {{:Definition:Definiend/Symbol}} == [[Definiend/Examples|Examples]] == {{:Definiend/Examples}} == [[Definition:Definiend/Also known as|Also known as]] == {{:Definition:Definiend/Also known as}} == Also see == {{Link-to-category|Definiend|definiend}} {{NamedforDef|eponym|cat = surname}} == [[Definition:Definiend/Historical Note|Historical Note]] == {{:Definition:Definiend/Historical Note}} == [[Definition:Definiend/Linguistic Note|Linguistic Note]] == {{:Definition:Definiend/Linguistic Note}} == Sources == {{NoSources}} [[Category:Definitions/Definiend]]
== Examples of [[Definition:Definiend|Definiends]] == <onlyinclude> === [[Definiend/Examples/Arbitrary Example 1|Arbitrary Example]] === {{:Definiend/Examples/Arbitrary Example 1}}</onlyinclude> [[Category:Examples of Definiends]]
{{ExampleCategory|def = Definiend}} [[Category:Definiends]]
#Redirect [[Definition:Definiend]] [[Category:Definitions/Definiends]]
== [[Definition:Definiend|Definiend]]: Also known as == <onlyinclude> A '''[[Definition:Definiend|definiend]]''' is also known as a '''[[Definition:Alternative Definiend|alternative definiend]]'''. </onlyinclude> == Sources == {{SourceReview}} [[Category:Definitions/Definiends]]
== Historical Note on [[Definition:Definiend|Definiend]] == <onlyinclude> </onlyinclude> == Sources == {{NoSources}} [[Category:Historical Notes]]
== Linguistic Note on [[Definition:Definiend|Definiend]] == <onlyinclude> </onlyinclude> == Sources == {{SourceReview}} [[Category:Linguistic Notes]]
== [[Definition:Definiend|Definiend]]: [[Symbols:x/Definiend|Symbol]] == <onlyinclude> The [[Symbols:x/Definiend|symbol]] for the '''[[Definition:Definiend|definiend]]''' is $...$. </onlyinclude> == Sources == {{SourceReview}} [[Category:Definitions/Definiends]]
Theorems
== Theorem == <onlyinclude> Let $...$ be a [[Definition:definiend|definiend]]. </onlyinclude> == Proof == {{ProofWanted}} == Also see == {{Namedfor|eponym|cat = surname}} == [[Theorem/Historical Note|Historical Note]] == {{:Theorem/Historical Note}} == Sources == {{SourceReview}} [[Category:definiends]]
Disambiguation
{{Disambiguation}} === [[Definition:definiend (context)|definiend (context)]] === {{:Definition:definiend (context)}} === [[Definition:definiend (context)|definiend (context)]] === {{:Definition:definiend (context)}} [[Category:Definitions/definiends]]
Definition Equivalences
== Theorem == {{TFAE|def = [definiend] }} === [[Definition:[definiend]/Definition 1|Definition $1$]] === {{:Definition:[definiend]/Definition 1}} === [[Definition:[definiend]/Definition 2|Definition $2$]] === {{:Definition:[definiend]/Definition 2}} == Proof == === Definition $(1)$ implies Definition $(2)$ === Let $...$ be a [[Definition:[definiend]/Definition 1|[definiend] by definition $1$]]. Then by definition: : [Definition 1 of definiend] : : Thus $...$ is a [[Definition:[definiend]/Definition 2|[definiend] by definition $2$]]. {{qed|lemma}} === Definition $(2)$ implies Definition $(1)$ === Let $...$ be a [[Definition:[definiend]/Definition 2|[definiend] by definition $2$]]. Then by definition: : [Definition 2 of definiend] : : : Thus $...$ is a [[Definition:[definiend]/Definition 1|[definiend] by definition $1$]]. {{qed|lemma}} [[Category:[definiend]]]
Technical Notes
== Technical Note for [[Definition:definiend|definiend]] == <onlyinclude> {{LatexFor|for = <latex-code> }} When either of the arguments is a single character, it is usual to omit the [[Symbols:Braces|braces]]: :<code><latex-code></code> </onlyinclude> This command is specific to {{ProofWiki}}. [[Category:Technical Notes]] [[Category:Definitions/definiends]]
Search Convenience
#Redirect [[target]] [[Category:Search Convenience]]
Integration by Parts
With a view to expressing the [[Definition:Primitive (Calculus)|primitive]] in the form: :$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$ let: {{begin-eqn}} {{eqn | l = u | r = ... | c = }} {{eqn | ll= \leadsto | l = \frac {\d u} {\d x} | r = ... | c = link to rule }} {{end-eqn}} and let: {{begin-eqn}} {{eqn | l = \frac {\d v} {\d x} | r = ... | c = }} {{eqn | ll= \leadsto | l = v | r = ... | c = link to rule }} {{end-eqn}} Then: {{begin-eqn}} {{eqn | l = \int ... | r = \int u \rd v | c = }} {{eqn | r = \paren {u} \paren {v} - \int \paren {v} \paren {\frac {\d u} {\d x} } \rd x | c = [[Integration by Parts]] }} {{eqn | r = ... | c = etc }} {{end-eqn}} {{qed}}
Iff Proofs
=== Necessary Condition === === Sufficient Condition ===
Partition Proofs
Testing each of the criteria for a [[Definition:Set Partition|partition]] as follows: === Each element in no more than one component === Thus each [[Definition:Element|element]] of ... is in no more than one [[Definition:Component of Partition|component]] of ... . {{qed|lemma}} === Each element in at least one component === Thus each [[Definition:Element|element]] of ... is in at least one [[Definition:Component of Partition|component]] of ... . {{qed|lemma}} === No component is empty === Thus no [[Definition:Component of Partition|component]] of ... is [[Definition:Empty Set|empty]]. {{qed|lemma}} Thus ... is a [[Definition:Set Partition|partition]] by definition. {{qed|lemma}}
Metric Space proofs
It is to be demonstrated that $d$ satisfies all the [[Axiom:Metric Space Axioms|metric space axioms]]. === Proof of {{Metric-space-axiom|1|nolink}} === {{begin-eqn}} {{eqn | l = \map d {x, x} | r = | c = Definition of $d$ }} {{eqn | r = 0 | c = as ... fulfils {{Metric-space-axiom|1}} }} {{end-eqn}} So {{Metric-space-axiom|1}} holds for $d$. {{qed|lemma}} === Proof of {{Metric-space-axiom|2|nolink}} === {{begin-eqn}} {{eqn | l = \map d {x, y} + \map d {y, z} | r = | c = Definition of $d$ }} {{eqn | r = | c = }} {{eqn | o = \ge | r = | c = as ... fulfils {{Metric-space-axiom|2}} }} {{eqn | r = \map d {x, z} | c = Definition of $d$ }} {{end-eqn}} So {{Metric-space-axiom|2}} holds for $d$. {{qed|lemma}} === Proof of {{Metric-space-axiom|3|nolink}} === {{begin-eqn}} {{eqn | l = \map d {x, y} | r = | c = Definition of $d$ }} {{eqn | r = k \cdot \map d {y, x} | c = as ... fulfils {{Metric-space-axiom|3}} }} {{eqn | r = \map d {y, x} | c = Definition of $d$ }} {{end-eqn}} So {{Metric-space-axiom|3}} holds for $d$. {{qed|lemma}} === Proof of {{Metric-space-axiom|4|nolink}} === {{begin-eqn}} {{eqn | l = x | o = \ne | r = y | c = }} {{eqn | ll= \leadsto | l = ... \map d {x, y} | o = > | r = 0 | c = as ... fulfils {{Metric-space-axiom|4}} }} {{eqn | ll= \leadsto | l = | o = > | r = 0 | c = }} {{eqn | ll= \leadsto | l = \map d {x, y} | o = > | r = 0 | c = Definition of $d$ }} {{end-eqn}} So {{Metric-space-axiom|4}} holds for $d$. {{qed|lemma}} Thus $d$ satisfies all the [[Axiom:Metric Space Axioms|metric space axioms]] and so is a [[Definition:Metric|metric]]. {{qed}}
Topology Proofs
Each of the [[Axiom:Open Set Axioms|open set axioms]] is examined in turn: === {{Open-set-axiom|1|nolink}} === Let $\family {U_i}_{i \mathop \in I}$ be an [[Definition:Indexed Family|indexed family]] of [[Definition:Open Set (Topology)|open sets]] of $T$. Let $\ds V = \bigcup_{i \mathop \in I} U_i$ be the [[Definition:Union of Family|union]] of $\family {U_i}_{i \mathop \in I}$. : : Hence $V$ is [[Definition:Open Set (Topology)|open]] by definition. {{qed|lemma}} === {{Open-set-axiom|2|nolink}} === Let $U$ and $V$ be [[Definition:Open Set (Topology)|open sets]] of $T$. : : Hence $U \cap V$ is [[Definition:Open Set (Topology)|open]] by definition. {{qed|lemma}} === {{Open-set-axiom|3|nolink}} === : : {{qed|lemma}} All the [[Axiom:Open Set Axioms|open set axioms]] are fulfilled, and the result follows. {{qed}}
Equivalence Proofs
Checking in turn each of the criteria for [[Definition:Equivalence Relation|equivalence]]: === Reflexivity === Thus ... is seen to be [[Definition:Reflexive Relation|reflexive]]. {{qed|lemma}} === Symmetry === Thus ... is seen to be [[Definition:Symmetric Relation|symmetric]]. {{qed|lemma}} === Transitivity === Thus ... is seen to be [[Definition:Transitive Relation|transitive]]. {{qed|lemma}} ... has been shown to be [[Definition:Reflexive Relation|reflexive]], [[Definition:Symmetric Relation|symmetric]] and [[Definition:Transitive Relation|transitive]]. Hence by definition it is an [[Definition:Equivalence Relation|equivalence relation]]. {{qed}}
Ordering Proofs
Checking in turn each of the criteria for an [[Definition:Ordering|ordering]]: === Reflexivity === So ... has been shown to be [[Definition:Reflexive Relation|reflexive]]. {{qed|lemma}} === Transitivity === So ... has been shown to be [[Definition:Transitive Relation|transitive]]. {{qed|lemma}} === Antisymmetry === So ... has been shown to be [[Definition:Antisymmetric Relation|antisymmetric]]. {{qed|lemma}} ... has been shown to be [[Definition:Reflexive Relation|reflexive]], [[Definition:Transitive Relation|transitive]] and [[Definition:Antisymmetric Relation|antisymmetric]]. Hence by definition it is an [[Definition:Ordering|ordering]]. {{qed}}
Strict Ordering Proofs
Checking in turn each of the criteria for a [[Definition:Strict Ordering|strict ordering]]: === Antireflexivity === So ... has been shown to be [[Definition:Antireflexive Relation|antireflexive]]. {{qed|lemma}} === Transitivity === So ... has been shown to be [[Definition:Transitive Relation|transitive]]. {{qed|lemma}} === Asymmetry === So ... has been shown to be [[Definition:Asymmetric Relation|asymmetric]]. {{qed|lemma}} ... has been shown to be [[Definition:Antireflexive Relation|antireflexive]], [[Definition:Transitive Relation|transitive]] and [[Definition:Asymmetric Relation|asymmetric]]. Hence by definition it is a [[Definition:Strict Ordering|strict ordering]]. {{qed}}
Semigroup Proofs
Taking the [[Axiom:Semigroup Axioms|semigroup axioms]] in turn: === {{SemigroupAxiom|0|nolink}} === Thus $...$ and so $...$ is [[Definition:Closed Algebraic Structure|closed]]. {{qed|lemma}} === {{SemigroupAxiom|1|nolink}} === Thus $...$ is [[Definition:Associative Operation|associative]]. {{qed|lemma}} The [[Axiom:Semigroup Axioms|semigroup axioms]] are thus seen to be fulfilled, and so $...$ is a [[Definition:Semigroup|semigroup]]. {{qed}}
Group Proofs
Taking the [[Axiom:Group Axioms|group axioms]] in turn: === {{GroupAxiom|0|nolink}} === Thus $...$ and so $...$ is [[Definition:Closed Algebraic Structure|closed]]. {{qed|lemma}} === {{GroupAxiom|1|nolink}} === Thus $...$ is [[Definition:Associative Operation|associative]]. {{qed|lemma}} === {{GroupAxiom|2|nolink}} === Thus $...$ is the [[Definition:Identity Element|identity element]] of $...$. {{qed|lemma}} === {{GroupAxiom|3|nolink}} === We have that $...$ is the [[Definition:Identity Element|identity element]] of $...$. Thus every [[Definition:Element|element]] $...$ of $...$ has an [[Definition:Inverse Element|inverse]] $...$. {{qed|lemma}} All the [[Axiom:Group Axioms|group axioms]] are thus seen to be fulfilled, and so $...$ is a [[Definition:Group|group]]. {{qed}}
Semilattice Proofs
Taking the [[Axiom:Semilattice Axioms|semilattice axioms]] in turn: === {{Semilattice-axiom|0|nolink}} === Thus $...$ is [[Definition:Closed Algebraic Structure|closed]]. {{qed|lemma}} === {{Semilattice-axiom|1|nolink}} === Thus $...$ is [[Definition:Associative Operation|associative]]. {{qed|lemma}} === {{Semilattice-axiom|2|nolink}} === Thus $...$ is [[Definition:Commutative Operation|commutative]]. {{qed|lemma}} === {{Semilattice-axiom|3|nolink}} === Thus $...$ is [[Definition:Idempotent Operation|idempotent]]. {{qed|lemma}} All the [[Axiom:Semilattice Axioms|semilattice axioms]] are thus seen to be fulfilled, and so $...$ is a [[Definition:Semilattice|semilattice]]. {{qed}}
Group Action Proofs
The [[Axiom:Group Action Axioms|group action axioms]] are investigated in turn. Let $g, h \in G$ and $s \in S$. Thus: {{begin-eqn}} {{eqn | l = g * \paren {h * s} | r = ... | c = by definition of $*$ }} : : {{eqn | r = \paren {g \circ h} * s | c = by definition of $*$ }} {{end-eqn}} demonstrating that {{GroupActionAxiom|1}} holds. Then: {{begin-eqn}} {{eqn | l = e * s | r = ... | c = }} {{eqn | r = s | c = ... }} {{end-eqn}} demonstrating that {{GroupActionAxiom|2}} holds. The [[Axiom:Group Action Axioms|group action axioms]] are thus seen to be fulfilled, and so $*$ is a [[Definition:Group Action|group action]]. {{qed}}
Ring Proofs
Taking the [[Axiom:Ring Axioms|ring axioms]] in turn: === {{Ring-axiom|A|nolink}} === === {{Ring-axiom|M0|nolink}} === === {{Ring-axiom|M1|nolink}} === === {{Ring-axiom|D|nolink}} ===
Proof by Mathematical Induction
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
- $proposition_n$
$\map P 0$ is the case:
- $proposition_0$
Thus $\map P 0$ is seen to hold.
Basis for the Induction
$\map P 1$ is the case:
- $proposition_1$
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
Induction Hypothesis
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
- $proposition_k$
from which it is to be shown that:
- $proposition_{k + 1}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
- $\forall n \in \Z_{\ge 0}: proposition_n$
Proof by Complete Induction
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
- $proposition_n$
$\map P 0$ is the case:
- $proposition_0$
Thus $\map P 0$ is seen to hold.
Basis for the Induction
$\map P 1$ is the case:
- $proposition_1$
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
Induction Hypothesis
Now it needs to be shown that if $\map P j$ is true, for all $j$ such that $0 \le j \le k$, then it logically follows that $\map P {k + 1}$ is true.
This is the induction hypothesis:
- $proposition_k$
from which it is to be shown that:
- $proposition_{k + 1}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $\map P k \implies \map P {k + 1}$ and the result follows by the Second Principle of Mathematical Induction.
Therefore:
- $proposition_n$
Proof by Finite Induction
The proof will proceed by the Principle of Finite Induction on $\Z_{>0}$.
Let $S$ be the set defined as:
- $S := \set {n \in \Z_{>0}: ...}$
That is, $S$ is to be the set of all $n$ such that:
- $...$
Basis for the Induction
We have that:
(proof that $1 \in S$)
So $1 \in S$.
This is the basis for the induction.
Induction Hypothesis
It is to be shown that if $k \in S$ where $k \ge 1$, then it follows that $k + 1 \in S$.
This is the induction hypothesis:
- $\text {expression for $k$}$
It is to be demonstrated that it follows that:
- $\text {expression for $k + 1$}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $k \in S \implies k + 1 \in S$ and the result follows by the Principle of Finite Induction:
- $\forall n \in \Z_{>0}: ...$
Proof by Complete Finite Induction
The proof will proceed by the Principle of Complete Finite Induction on $\Z_{>0}$.
Let $S$ be the set defined as:
- $S := \set {n \in \Z_{>0}: ...}$
That is, $S$ is to be the set of all $n$ such that:
- $...$
Basis for the Induction
We have that:
(proof that $1 \in S$)
So $1 \in S$.
This is the basis for the induction.
Induction Hypothesis
It is to be shown that if $j \in S$ for all $j$ such that $0 \le j \le k$, then it follows that $k + 1 \in S$.
This is the induction hypothesis:
- $\forall j \in \Z_{>0}: 1 \le j \le k: \text {expression for $j$}$
It is to be demonstrated that it follows that:
- $\text {expression for $k + 1$}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $\forall j \in S: 0 \le j \le k: j \in S \implies k + 1 \in S$ and the result follows by the Principle of Complete Finite Induction:
- $\forall n \in \Z_{>0}: ...$
Proof by General Induction
The proof proceeds by general induction.
For all $x \in M$, let $\map P x$ be the proposition:
- $\text {proposition}_x$
Basis for the Induction
$\map P \O$ is the case:
- $\text {proposition}_\O$
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
Induction Hypothesis
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
- $\text {proposition}_x$
from which it is to be shown that:
- $\text {proposition}_{\map g x}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
- $\forall x \in M: \text {proposition}_x$
Proof by Superinduction
The proof proceeds by superinduction.
For all $x \in M$, let $\map P x$ be the proposition:
- $\text {proposition}_x$
Basis for the Induction
$\map P \O$ is the case:
- $\text {proposition}_\O$
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
$\Box$
Induction Hypothesis
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
- $\text {proposition}_x$
from which it is to be shown that:
- $\text {proposition}_{\map g x}$
Induction Step
This is the induction step:
\(\ds \) | \(=\) | \(\ds \) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \) | \(=\) | \(\ds \) |
So $\map P x \implies \map P {\map g x}$.
$\Box$
Closure under Chain Unions
It remains to demonstrate closure under chain unions.
Let $\map P x$ be true for all $x \in C$, where $C$ is an arbitrary chain of elements of $M$.
That is:
- $\forall x \in C: \text {proposition}_x$
This needs considerable tedious hard slog to complete it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Finish}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
and so:
- $\text {proposition}_{\ds \bigcup C}$
That is:
- $\forall C: \forall x \in C: \map P x \implies \map P {\ds \bigcup C}$
The result follows by the Principle of Superinduction.
$\Box$
Therefore:
- $\forall x \in M: \text {proposition}_x$
Tableau proofs
{| border="1" |- ! Line !! ! Pool ! Formula ! Rule ! Depends upon ! Notes |- | align="right" | <line number> || | align="right" | <line numbers> | $\ldots{}$ | [[link to ProofWiki entry]] | <line numbers> |- | align="right" | <line number> || | align="right" | <line numbers> | $\ldots{}$ | [[link to ProofWiki entry]] | <line numbers> |} ...etc.
Puzzle (Dudeney Modern Puzzles)
== {{BookLink|Modern Puzzles|Henry Ernest Dudeney}} by {{AuthorRef|Henry Ernest Dudeney}}: $...$ == <onlyinclude> ;<title> :''<rubric>'' </onlyinclude> == Solution == == Proof == == Sources == * {{BookReference|Modern Puzzles|1926|Henry Ernest Dudeney|prev = Dudeney's Modern Puzzles/Arithmetical and Algebraical Problems/Money Puzzles/5 - Doubling the Value|next = Dudeney's Modern Puzzles/Arithmetical and Algebraical Problems/Money Puzzles/7 - Generous Gifts}}: Arithmetical and Algebraical Problems: Money Puzzles: $6$. -- Generous Gifts [[Category:Dudeney's Modern Puzzles]]