avewright/proofwiki-math huggingface dataset:
Theorem: Complex Roots of Unity are Vertices of Regular Polygon Inscribed in Circle

Let $n \in \Z$ be an integer such that $n \ge 3$.
Let $z \in \C$ be a complex number such that $z^n = 1$.
Let $U_n = \set {e^{2 i k \pi / n}: k \in \N_n}$ be the set of $n$th roots of unity.
Let $U_n$ be plotted on the complex plane.
Then the elements of $U_n$ are located at the vertices of a regular $n$-sided polygon $P$, such that:
:$(1):\quad$ $P$ is circumscribed by a unit circle whose center is at $\tuple {0, 0}$
:$(2):\quad$ one of those vertices is at $\tuple {1, 0}$.

Proof:
{{Proofread}}
600px
{{tidy}}
{{MissingLinks}}
The above diagram illustrates the $7$th roots of unity.
Let $O$ be the origin.
Consider $A_0, \cdots, A_{n - 1}$ the points $e^{0 \times 2i\pi / n}, \cdots, e^{(n - 1) \times 2 i\pi / n}$ in the complex plane.
Note $A_n = A_0$ and $A_{n+1} = A_1$.
Consider $P$ the polygon with vertices $A_0, \cdots, A_{n - 1}$
Theorem: Equation of Unit Circle in Complex Plane

Consider the unit circle $C$ whose center is at $\tuple {0, 0}$ on the complex plane.
Its equation is given by:
:$\cmod z = 1$
where $\cmod z$ denotes the complex modulus of $z$.

Proof:
From Equation of Unit Circle, the unit circle whose center is at the origin of the Cartesian $xy$ plane has the equation:
:$x^2 + y^2 = 1$
Identifying the Cartesian $xy$ plane with the complex plane:
{{ProofWanted|Can't think of the precise words I need for this at the moment}}
Theorem: Equation of Unit Circle in Complex Plane

Consider the unit circle $C$ whose center is at $\tuple {0, 0}$ on the complex plane.
Its equation is given by:
:$\cmod z = 1$
where $\cmod z$ denotes the complex modulus of $z$.

Proof:
Let $C$ be the set of points on the unit circle defined above.
Let $P$ be the set:
:$\set {z \in \C: \cmod z = 1}$
Let $z = x + i y \in C$.
$z$ can be expressed in polar form as:
:$z = \polar {r, \theta}$
where:
:$x = r \cos \theta$
:$y = r \sin \theta$
By definition of unit circle, $z$ is $1$ unit away from $\tuple {0, 0}$.
By Pythagoras's Theorem:
:$\sqrt {\paren {r \cos \theta}^2 + \paren {r \sin \theta}^2} = 1$
from which:
:$\sqrt {x^2 + y^2} = 1$
By definition of complex modulus:
:$\cmod z = 1$
and so $z \in P$.
Thus $C \subseteq P$.
Let $z \in P$.
Then by definition $\cmod z = 1$.
By Modulus of Complex Number equals its Distance from Origin, $z$ is $1$ unit away from $\tuple {0, 0}$.
By definition of $C$, it follows that $z \in C$.
Thus $P \subseteq C$.
The result follows by definition of set equality.
{{Qed}}
Theorem: Equation of Unit Circle

Let the unit circle have its center at the origin of the Cartesian plane.
Its equation is given by:
:$x^2 + y^2 = 1$
{{expand|Present it in polar coordinates as well}}

Proof:
From Equation of Circle, the equation of a circle with radius $R$ and center $\tuple {a, b}$ is:
:$\paren {x - a}^2 + \paren {y - b}^2 = R^2$
Substituting $\tuple {0, 0}$ for $\tuple {a, b}$ and $1$ for $R$ gives the result.
{{qed}}
Theorem: Equation of Unit Circle

Let the unit circle have its center at the origin of the Cartesian plane.
Its equation is given by:
:$x^2 + y^2 = 1$
{{expand|Present it in polar coordinates as well}}

Proof:
From Equation of Unit Circle, the unit circle whose center is at the origin of the Cartesian $xy$ plane has the equation:
:$x^2 + y^2 = 1$
Identifying the Cartesian $xy$ plane with the complex plane:
{{ProofWanted|Can't think of the precise words I need for this at the moment}}
Theorem: Equation of Unit Circle

Let the unit circle have its center at the origin of the Cartesian plane.
Its equation is given by:
:$x^2 + y^2 = 1$
{{expand|Present it in polar coordinates as well}}

Proof:
Let $C$ be the set of points on the unit circle defined above.
Let $P$ be the set:
:$\set {z \in \C: \cmod z = 1}$
Let $z = x + i y \in C$.
$z$ can be expressed in polar form as:
:$z = \polar {r, \theta}$
where:
:$x = r \cos \theta$
:$y = r \sin \theta$
By definition of unit circle, $z$ is $1$ unit away from $\tuple {0, 0}$.
By Pythagoras's Theorem:
:$\sqrt {\paren {r \cos \theta}^2 + \paren {r \sin \theta}^2} = 1$
from which:
:$\sqrt {x^2 + y^2} = 1$
By definition of complex modulus:
:$\cmod z = 1$
and so $z \in P$.
Thus $C \subseteq P$.
Let $z \in P$.
Then by definition $\cmod z = 1$.
By Modulus of Complex Number equals its Distance from Origin, $z$ is $1$ unit away from $\tuple {0, 0}$.
By definition of $C$, it follows that $z \in C$.
Thus $P \subseteq C$.
The result follows by definition of set equality.
{{Qed}}
Theorem: Tautological Consequent

:$p \implies \top \dashv \vdash \top$

Proof:
{{BeginTableau|p \implies \top \vdash \top}}
{{Premise|1|p \implies \top}}
{{TopIntro|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\top \vdash p \implies \top}}
{{Assumption|1|p}}
{{Premise|2|\top}}
{{Implication|3|1|p \implies \top|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Tautological Consequent

:$p \implies \top \dashv \vdash \top$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||c|ccc|} \hline
p & p & \implies & \top & \top \\
\hline
F & F & T & T & T \\
T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Tautological Antecedent

:$\top \implies p \dashv \vdash p$

Proof:
{{BeginTableau|\top \implies p \vdash p}}
{{Premise|1|\top \implies p}}
{{TopIntro|2}}
{{ModusPonens|3|1|p|1|2}}
{{EndTableau|lemma}}
{{BeginTableau|p \vdash \top \implies p}}
{{Premise|1|p}}
{{Assumption|2|\top}}
{{Implication|3|1|\top \implies p|2|1}}
{{EndTableau|qed}}
Theorem: Tautological Antecedent

:$\top \implies p \dashv \vdash p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||c|ccc|} \hline
p & \top & \implies & p \\
\hline
F & T & F & F \\
T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Contradictory Consequent

:$p \implies \bot \dashv \vdash \neg p$

Proof:
{{BeginTableau|p \implies \bot \vdash \neg p}}
{{Premise|1|p \implies \bot}}
{{Assumption|2|p}}
{{ModusPonens|3|1, 2|\bot|1|2}}
{{Contradiction|4|1|\neg p|2|3}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\neg p \vdash p \implies \bot}}
{{Premise|1|\neg p}}
{{Assumption|2|p}}
{{NonContradiction|3|1,2|1|2}}
{{Implication|4|1|p \implies \bot|2|3}}
{{EndTableau}}
{{qed}}
Theorem: Contradictory Consequent

:$p \implies \bot \dashv \vdash \neg p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||cc|} \hline
p & p & \implies & \bot & \neg & p \\
\hline
\F & \F & \T & \F & \T & \F \\
\T & \T & \F & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Contradictory Antecedent

:$\bot \implies p \dashv \vdash \top$

Proof:
{{BeginTableau|\bot \implies p \vdash \top}}
{{Premise|1|\bot \implies p}}
{{TopIntro|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\top \vdash \bot \implies p}}
{{Assumption|1|\bot}}
{{Premise|2|\top}}
{{Explosion|3|1|p|1}}
{{Implication|4||\bot \implies p|1|3}}
{{EndTableau}}
{{qed}}
Theorem: Contradictory Antecedent

:$\bot \implies p \dashv \vdash \top$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
:<nowiki>$\begin{array}{|c|ccc||c|} \hline
p & \bot & \implies & p & \top \\
\hline
\F & \F & \T & \F & \T \\
\T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Biconditional with Tautology

:$p \iff \top \dashv \vdash p$

Proof:
{{BeginTableau|p \iff \top \vdash p}}
{{Premise|1|p \iff \top}}
{{TopIntro|2}}
{{BiconditionalElimination|3|1|\top \implies p|1|2}} 
{{ModusPonens|4|1|p|2|3}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|p \vdash p \iff \top}}
{{Premise|1|\top}}
{{Assumption|2|p}}
{{TopIntro|3}}
{{Implication|4||p \implies \top|2|3}}
{{Implication|5|2|\top \implies p|1|2}}
{{BiconditionalIntro|6|2|p \iff \top|4|5}}
{{EndTableau}}
{{qed}}
Theorem: Biconditional with Tautology

:$p \iff \top \dashv \vdash p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||c|ccc|} \hline
p & p & \iff & \top & p \\
\hline
F & F & F & T & F \\
T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Exclusive Or with Tautology

:$p \oplus \top \dashv \vdash \neg p$

Proof:
{{BeginTableau|p \oplus \top \vdash \neg p}}
{{Premise|1|p \oplus \top}}
{{SequentIntro|2|1|\left({p \lor \top} \right) \land \neg \left({p \land \top}\right)|1|Definition of Exclusive Or}}
{{SequentIntro|3|1|\top \land \neg \left({p \land \top}\right)|1|Disjunction with Tautology}}
{{SequentIntro|4|1|\neg \left({p \land \top}\right)|1|Conjunction with Tautology}}
{{SequentIntro|5|1|\neg p|1|Conjunction with Tautology}} 
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\neg p \vdash p \oplus \top}}
{{Assumption|1|\neg p}}
{{TopIntro|2}}
{{SequentIntro|3||p \lor \top|2|Disjunction with Tautology}}
{{SequentIntro|4|1|\neg \left({p \land \top}\right)|1|Conjunction with Tautology}}
{{Conjunction|5|1|\left({p \lor \top}\right) \land \neg \left({p \land \top}\right)|3|4}}
{{SequentIntro|6|1|p \oplus \top|5|Definition of Exclusive Or}}
{{EndTableau}}
{{qed}}
Theorem: Exclusive Or with Tautology

:$p \oplus \top \dashv \vdash \neg p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||cc|} \hline
p & p & \oplus & \top & \neg & p \\
\hline
F & F & T & T & T & F \\
T & T & F & T & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Biconditional with Contradiction

:$p \iff \bot \dashv \vdash \neg p$

Proof:
{{BeginTableau|p \iff \bot \vdash \neg p}}
{{Premise|1|p \iff \bot}}
{{BiconditionalElimination|2|1|p \implies \bot|1|1}}
{{SequentIntro|3|1|\neg p|2|Contradictory Consequent}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\neg p \vdash p \iff \bot}}
{{Assumption|1|\neg p}}
{{SequentIntro|2|1|p \implies \bot|1|Contradictory Consequent}}
{{TopIntro|3}}
{{SequentIntro|4||\bot \implies p|3|Contradictory Antecedent}}
{{BiconditionalIntro|5|1|p \iff \bot|2|4}}
{{EndTableau}}
{{qed}}
Theorem: Biconditional with Contradiction

:$p \iff \bot \dashv \vdash \neg p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||cc|} \hline
p & p & \iff & \bot & \neg & p \\
\hline
F & F & T & F & T & F \\
T & T & F & F & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Unique Representation of Complex Number in Spherical Form

Let $\PP$ be the complex plane.
Let $\mathbb S$ be the unit sphere which is tangent to $\PP$ at $\tuple {0, 0}$ (that is, where $z = 0$).
Let the diameter of $\mathbb S$ perpendicular to $\PP$ through $\tuple {0, 0}$ be $NS$ where $S$ is the point $\tuple {0, 0}$.
Let the point $N$ be referred to as the '''north pole''' of $\mathbb S$ and $S$ be referred to as the '''south pole''' of $\mathbb S$.
:900px
Let $A$ be a point on $P$.
Let the line $NA$ be constructed.
Then $NA$ passes through exactly one point $A'$ on the surface of $\mathbb S$ apart from $N$.
Similarly, let $A'$ be a point on the surface of $\mathbb S$ apart from $N$.
Let the line $NA'$ be constructed.
Then $NA'$ passes through exactly one point $A$ on $P$.

Proof:
{{ProofWanted|Should be standard Euclidean 3-d stuff but I haven't got that far in Euclid yet.}}
Theorem: Exclusive Or with Contradiction

:$p \oplus \bot \dashv \vdash p$

Proof:
{{BeginTableau|p \oplus \bot \vdash p}}
{{Premise|1|p \oplus \bot}}
{{SequentIntro|2|1|\left({p \lor \bot} \right) \land \neg \left({p \land \bot}\right)|1| {{Defof|Exclusive Or}} }}
{{SequentIntro|3|1|p \land \neg \left({p \land \bot}\right)|2|Disjunction with Contradiction}}
{{SequentIntro|4|1|p \land \neg \bot|3|Conjunction with Contradiction}}
{{SequentIntro|5|1|p \land \top|4|Tautology is Negation of Contradiction}}
{{SequentIntro|6|1|p|5|Conjunction with Tautology}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|p \vdash p \oplus \bot}}
{{Premise|1|p}}
{{SequentIntro|2|1|p \land \top|1|Conjunction with Tautology}}
{{SequentIntro|3|1|\left({p \lor \bot}\right) \land \top|2|Disjunction with Contradiction}}
{{SequentIntro|4|1|\left({p \lor \bot}\right) \land \neg \bot|3|Tautology is Negation of Contradiction}}
{{SequentIntro|5|1|\left({p \lor \bot}\right) \land \neg \left({p \land \bot}\right)|4|Conjunction with Contradiction}}
{{SequentIntro|6|1|p \oplus \bot|5| {{Defof|Exclusive Or}} }}
{{EndTableau}}
{{qed}}
Theorem: Exclusive Or with Contradiction

:$p \oplus \bot \dashv \vdash p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
:<nowiki>$\begin{array}{|c|ccc||c|ccc|} \hline
p & p & \oplus & \bot & p \\
\hline
\F & \F & \F & \F & \F \\
\T & \T & \T & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Product of Complex Number with Conjugate by Dot and Cross Product

Let $z_1$ and $z_2$ be complex numbers.
Then:
:$\overline {z_1} z_2 = \paren {z_1 \circ z_2} + i \paren {z_1 \times z_2}$
where:
:$\overline {z_1}$ denotes the complex conjugate of $z_1$
:$z_1 \circ z_2$ denotes the complex dot product of $z_1$ with $z_2$
:$z_1 \times z_2$ denotes the complex cross product of $z_1$ with $z_2$.

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \paren {z_1 \circ z_2} + i \paren {z_1 \times z_2}
      | c = 
}}
{{eqn | r = \paren {z_1 \circ z_2} + i \frac {\overline {z_1} z_2 - z_1 \overline {z_2} } {2 i}
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 4}}
}}
{{eqn | r = \frac {\overline {z_1} z_2 + z_1 \overline {z_2} } 2 + \frac {\overline {z_1} z_2 - z_1 \overline {z_2} } 2
      | c = {{Defof|Dot Product|subdef = Complex|index = 4}}
}}
{{eqn | r = \frac {\overline {z_1} z_2 + z_1 \overline {z_2} + \overline {z_1} z_2 - z_1 \overline {z_2} } 2
      | c = 
}}
{{eqn | r = \overline {z_1} z_2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Complex Number with Conjugate in Exponential Form

Let $z_1$ and $z_2$ be complex numbers.
Then:
:$\overline {z_1} z_2 = \cmod {z_1} \, \cmod {z_2} e^{i \theta}$
where:
:$\overline {z_1}$ denotes the complex conjugate of $z_1$
:$\cmod {z_1}$ denotes the complex modulus of $z_1$
:$\theta$ denotes the angle from $z_1$ to $z_2$, measured in the positive direction.

Proof:
{{begin-eqn}}
{{eqn | l =\overline {z_1} z_2 
      | r = \paren {z_1 \circ z_2} + i \paren {z_1 \times z_2}
      | c = Product of Complex Number with Conjugate by Dot and Cross Product
}}
{{eqn | r = \cmod {z_1} \, \cmod {z_2} \cos \theta + i \paren {z_1 \times z_2}
      | c = {{Defof|Dot Product|subdef = Complex|index = 2}}
}}
{{eqn | r = \cmod {z_1} \, \cmod {z_2} \cos \theta + i \cmod {z_1} \, \cmod {z_2} \sin \theta
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 2}}
}}
{{eqn | r = \cmod {z_1} \, \cmod {z_2} \paren {\cos \theta + i \sin \theta}
      | c = 
}}
{{eqn | r = \cmod {z_1} \, \cmod {z_2} e^{i \theta}
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Numbers are Perpendicular iff Dot Product is Zero

Let $z_1$ and $z_2$ be complex numbers in vector form such that $z_1 \ne 0$ and $z_2 \ne 0$.
Then $z_1$ and $z_2$ are perpendicular {{iff}}:
:$z_1 \circ z_2 = 0$
where $z_1 \circ z_2$ denotes the complex dot product of $z_1$ with $z_2$.

Proof:
By definition of complex dot product:
:$z_1 \circ z_2 = \cmod {z_1} \, \cmod {z_2} \cos \theta$
:$\cmod {z_1}$ denotes the complex modulus of $z_1$
:$\theta$ denotes the angle from $z_1$ to $z_2$, measured in the positive direction.
Theorem: Complex Numbers are Parallel iff Cross Product is Zero

Let $z_1$ and $z_2$ be complex numbers in vector form such that $z_1 \ne 0$ and $z_2 \ne 0$.
Then $z_1$ and $z_2$ are parallel {{iff}}:
:$z_1 \times z_2 = 0$
where $z_1 \times z_2$ denotes the complex cross product of $z_1$ with $z_2$.

Proof:
By definition of complex cross product:
:$z_1 \times z_2 = \cmod {z_1} \, \cmod {z_2} \sin \theta$
:$\cmod {z_1}$ denotes the complex modulus of $z_1$
:$\theta$ denotes the angle from $z_1$ to $z_2$, measured in the positive direction.
Theorem: Tautology iff Negation is Unsatisfiable

Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is a tautology {{iff}} its negation $\neg \mathbf A$ is unsatisfiable.

Proof:
=== Necessary Condition ===
Let $\mathbf A$ be a tautology.
Let $v$ be a boolean interpretation of $\mathbf A$.
Then $\map v {\mathbf A} = \T$.
Hence, by definition of the boolean interpretation of negation:
:$\map v {\neg \mathbf A} = \F$
Since $v$ was arbitrary, it follows that $\neg \mathbf A$ is unsatisfiable.
{{qed|lemma}}
Theorem: Satisfiable iff Negation is Falsifiable

Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is satisfiable {{iff}} its negation $\neg \mathbf A$ is falsifiable.

Proof:
=== Necessary Condition ===
Let $\mathbf A$ be satisfiable.
Then there exists a boolean interpretation $v$ of $\mathbf A$ such that:
:$\map v {\mathbf A} = \T$
Hence, by definition of the boolean interpretation of negation:
:$\map v {\neg \mathbf A} = \F$
It follows that $\neg \mathbf A$ is falsifiable.
{{qed|lemma}}
Theorem: Satisfiable Set minus Formula is Satisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-satisfiable set of formulas from $\LL$.
Let $\phi \in \FF$.
Then $\FF \setminus \set \phi$ is also $\mathscr M$-satisfiable.

Proof:
This is an immediate consequence of Subset of Satisfiable Set is Satisfiable.
{{qed}}
Theorem: Subset of Satisfiable Set is Satisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-satisfiable set of formulas from $\LL$.
Let $\FF'$ be a subset of $\FF$.
Then $\FF'$ is also $\mathscr M$-satisfiable.

Proof:
Since $\FF$ is $\mathscr M$-satisfiable, there exists some model $\MM$ of $\FF$:
:$\MM \models_{\mathscr M} \FF$
Thus for every $\psi \in \FF$:
:$\MM \models_{\mathscr M} \psi$
Now, for every $\psi$ in $\FF'$:
:$\psi \in \FF$
by definition of subset.
Hence:
:$\forall \psi \in \FF': \MM \models_{\mathscr M} \psi$
that is, $\MM$ is a model of $\FF'$.
Hence $\FF'$ is $\mathscr M$-satisfiable.
{{qed}}
Category:Formal Semantics
mhft3w9ng1auehlv6bb677z62oo7zb7
Theorem: Satisfiable Set Union Tautology is Satisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-satisfiable set of formulas from $\LL$.
Let $\phi$ be a tautology for $\mathscr M$.
Then $\FF \cup \set \phi$ is also $\mathscr M$-satisfiable.

Proof:
Since $\FF$ is $\mathscr M$-satisfiable, there exists some model $\MM$ of $\FF$:
:$\MM \models_{\mathscr M} \FF$
Since $\psi$ is a tautology, also:
:$\MM \models_{\mathscr M} \psi$
Therefore, we conclude that:
:$\MM \models_{\mathscr M} \FF \cup \set \phi$
that is, $\FF \cup \set \phi$ is satisfiable.
Theorem: Unsatisfiable Set Union Formula is Unsatisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-unsatisfiable set of formulas from $\LL$.
Let $\phi$ be a logical formula.
Then $\FF \cup \set \phi$ is also $\mathscr M$-unsatisfiable.

Proof:
This is an immediate consequence of Superset of Unsatisfiable Set is Unsatisfiable.
{{qed}}
Theorem: Superset of Unsatisfiable Set is Unsatisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-unsatisfiable set of formulas from $\LL$.
Let $\FF'$ be a superset of $\FF$.
Then $\FF'$ is also $\mathscr M$-unsatisfiable.

Proof:
By assumption, $\FF$ is unsatisfiable.
Suppose now $\FF'$ were satisfiable.
Then it would follow from Subset of Satisfiable Set is Satisfiable that $\FF$ were also satisfiable.
We conclude that $\FF'$ must be unsatisfiable.
{{qed}}
Category:Formal Semantics
fca2oi6sx6lh7lv4yg1ci7rqrwdwlqq
Theorem: Unsatisfiable Set minus Tautology is Unsatisfiable

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-unsatisfiable set of formulas from $\LL$.
Let $\phi \in \FF$ be a tautology.
Then $\FF \setminus \set {\phi}$ is also $\mathscr M$-unsatisfiable.

Proof:
Suppose $\FF \setminus \set {\phi}$ were satisfiable.
Then by Satisfiable Set Union Tautology is Satisfiable, so would $\FF$ be, because:
:$\FF = \paren {\FF \setminus \set {\phi} } \cup \set {\phi}$
by Set Difference Union Intersection and Intersection with Subset is Subset.
Therefore, $\FF \setminus \set {\phi}$ must be unsatisfiable.
{{qed}}
Theorem: Semantic Consequence as Tautological Conditional

Let $\FF$ be a finite set of WFFs of propositional logic.
Let $\mathbf A$ be another WFF.
Then the following are equivalent:
{{begin-eqn}}
{{eqn | l = \FF
      | o = \models_{\mathrm {BI} }
      | r = \mathbf A
}}
{{eqn | o = \models_{\mathrm {BI} } 
      | r = \bigwedge \FF \implies \mathbf A
}}
{{end-eqn}}
that is, $\mathbf A$ is a semantic consequence of $\FF$ {{iff}} $\ds \bigwedge \FF \implies \mathbf A$ is a tautology.
Here, $\ds \bigwedge \FF$ is the conjunction of $\FF$.

Proof:
=== Necessary Condition ===
let:
:$\FF \models_{\mathrm {BI} } \mathbf A$
{{AimForCont}} $\ds \bigwedge \FF \implies \mathbf A$ were not a tautology.
Then there exists a boolean interpretation $v$ such that:
:$\map v {\ds \bigwedge \FF} = \T$
:$\map v {\mathbf A} = \F$
by definition of the boolean interpretation of $\implies$.
It now follows from the boolean interpretation of conjunction that:
:$\map v {\mathbf B} = \T$
for every $\mathbf B \in \FF$.
Hence, by definition of model:
:$v \models_{\mathrm {BI} } \FF$
It now follows from our assumption that:
:$\map v {\mathbf A} = \T$
This is a contradiction, hence $\ds \bigwedge \FF \implies \mathbf A$ is a tautology.
{{qed|lemma}}
Theorem: Semantic Consequence of Set Union Formula

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\psi$ be another logical formula.
Then:
:$\FF \cup \set \psi \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \cup \set \psi$.

Proof:
This is an immediate consequence of Semantic Consequence of Superset.
{{qed}}
Theorem: Semantic Consequence of Superset

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\FF'$ be another set of logical formulas.
Then:
:$\FF \cup \FF' \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \cup \FF'$.

Proof:
Any model of $\FF \cup \FF'$ is a fortiori also a model of $\FF$.
By definition of semantic consequence all models of $\FF$ are models of $\phi$.
Therefore all models of $\FF \cup \FF'$ are also models of $\phi$.
Hence:
:$\FF \cup \FF' \models_{\mathscr M} \phi$
as desired.
{{qed}}
Category:Formal Semantics
cowaaykdur0gx37z85obu9qhreoc7ck
Theorem: Semantic Consequence of Set minus Tautology

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\psi \in \FF$ be a tautology.
Then:
:$\FF \setminus \set \psi \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \setminus \set \psi$.

Proof:
Let $\MM$ be a model of $\FF \setminus \set \psi$.
Since $\psi$ is a tautology, it follows that:
:$\MM \models_{\mathscr M} \psi$
Hence:
:$\MM \models \FF$
which, {{hypothesis}}, entails:
:$\MM \models \phi$
Since $\MM$ was arbitrary, it follows by definition of semantic consequence that:
:$\FF \setminus \set \psi \models_{\mathscr M} \phi$
{{qed}}