avewright/proofwiki-math huggingface dataset:
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
Let the cardinality $\size I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$.
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
which has been proved.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcup_{i \mathop = 1}^k T_i = \bigcap_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcup_{i \mathop = 1}^k T_i \cup T_{k + 1} }
      | c = Union is Associative
}}
{{eqn | r = \paren {S \setminus \bigcup_{i \mathop = 1}^k T_i} \cap \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcap_{i \mathop = 1}^k \paren {S \setminus T_i} } \cap \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Intersection is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
Let $x \in S$ througout.
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1 \cup T_2}
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1 \cup T_2} \subseteq \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1} \cap \relcomp S {T_2} \subseteq \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
By definition of set equality:
:$\relcomp S {T_1 \cup T_2} = \relcomp S {T_1} \cap \relcomp S {T_2}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{begin-eqn}}
{{eqn | l = \overline {T_1 \cap T_2}
      | r = \mathbb U \setminus \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \paren {\mathbb U \setminus T_1} \cup \paren {\mathbb U \setminus T_2}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \overline {T_1} \cup \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cap T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \land x \in T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \lor \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Disjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \lor x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cup \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cap T_2} = \overline {T_1} \cup \overline {T_2}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement {\map \complement A \cup \map \complement B}
      | r = \map \complement {\map \complement A} \cap \map \complement {\map \complement B}
      | c = De Morgan's Laws: Complement of Union
}}
{{eqn | r = A \cap B
      | c = Complement of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement {\map \complement {\map \complement A \cup \map \complement B} }
      | r = \map \complement {A \cap B}
      | c = taking complements of both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement A \cup \map \complement B
      | r = \map \complement {A \cap B}
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cup T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \land \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Conjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \land x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cap \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cup T_2} = \overline {T_1} \cap \overline {T_2}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap \mathbb T$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcap \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall T' \in \mathbb T}
      | l = x
      | o = \in
      | r = \rightparen {T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: Four Color Theorem

Let $G$ be a planar graph.
Then:
:$\map \chi G \le 4$
where the $\map \chi G$ denotes the chromatic number of $G$.
That is, $G$ can be assigned a proper vertex $k$-coloring such that $k \le 4$.

Proof:
It can be shown that it is necessary to consider only planar graphs which are simple.
Hence any discussion below about a graph will carry the assumption that it is both simple and planar.
{{finish|The thesis follows.}}
{{ProofWanted}}
Theorem: Cycle does not Contain Subcycles

Let $G$ be a cycle graph.
Then the only cycle graph that is a subgraph of $G$ is $G$ itself.

Proof:
{{AimForCont}} $G$ contains a subgraph $C$ such that:
:$C$ is a cycle graph
:$C \ne G$ is non-empty.
Then there exists some vertex $v$ that is not in $C$.
Let $u$ be any vertex of $C$.
Since $G$ is a cycle graph, it is connected.
Therefore there is a walk from $u$ to $v$ in $G$.
There must be some vertex $x$ that is the last vertex in $C$ along that walk.
Therefore, $x$ is adjacent to a vertex not in $C$.
Thus it has a degree of at least $3$.
But $G$ is a cycle graph and every vertex in a cycle graph has degree $2$.
The result follows by Proof by Contradiction.
{{Qed}}
Category:Cycles (Graph Theory)
53fys6owdew0gpmmgzmqaa5obkcnq36
Theorem: Dirac's Theorem

Let $G$ be a connected simple graph with $n$ vertices such that $n > 3$.
Let the degree of each vertex be at least $\dfrac n 2$.
Then $G$ is Hamiltonian.

Proof:
Let $P = p_1 p_2 \ldots p_k$ be the longest path in $G$.
If $p_1$ is adjacent to some vertex $v$ not in $P$, then the path  $v p_1 p_2 \ldots p_k$ would be longer than $P$, contradicting the choice of $P$.
The same argument can be made for $p_k$.
So both $p_1$ and $p_k$ are adjacent only to vertices in $P$.
Since $\map \deg {p_1} \ge \dfrac n 2$ and $p_1$ cannot be adjacent to itself, $k \ge \dfrac n 2 + 1$.
;Claim
There is some value of $j \in \set {1, 2, \ldots, k}$ such that:
:$p_j$ is adjacent to $p_k$
and:
:$p_{j + 1}$ is adjacent to $p_1$.
{{AimForCont}} that the claim is not true.
Then since all vertices adjacent to $p_1$ or $p_k$ lie on $P$, there must be at least $\map \deg {p_1}$ vertices on $P$ not adjacent to $p_k$.
Since all the vertices adjacent to $p_k$ and $p_k$ itself also lie on $P$, the path must have at least $\map \deg {p_1} + \map \deg {p_k} + 1 \ge n + 1$ vertices.
But $G$ has only $n$ vertices: a contradiction.
This gives a cycle $C = p_{j + 1} p_{j + 2} \ldots p_k p_j p_{j - 1} \ldots p_2 p_1 p_{j + 1}$.
{{AimForCont}} $G \setminus C$ is non-empty.
Then since $G$ is connected, there must be a vertex $v \in G \setminus C$ adjacent to some $p_i$.
So the path from $v$ to $p_i$ and then around $C$ to the vertex adjacent to $p_i$ is longer than $P$, contradicting the definition of $P$.
Therefore all vertices in $G$ are contained in $C$, making $C$ a Hamilton cycle.
{{Qed}}
Theorem: Dirac's Theorem

Let $G$ be a connected simple graph with $n$ vertices such that $n > 3$.
Let the degree of each vertex be at least $\dfrac n 2$.
Then $G$ is Hamiltonian.

Proof:
Take any two non-adjacent vertices $u, v \in G$.
Then:
:$\deg u + \deg v \ge \dfrac n 2 + \dfrac n 2 = n$
The result follows by a direct application of Ore's Theorem.
{{qed}}
Theorem: Three-Way Exclusive Or and Equivalence

Let $p \iff q$ be the biconditional operator, and $p \oplus q$ be the exclusive or operator.
Then:
: $p \iff q \iff r \dashv \vdash p \oplus q \oplus r$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccc|} \hline
(p & \iff & q) & \iff & r & (p & \oplus & q) & \oplus & r \\
\hline
F & T & F & F & F & F & F & F & F & F \\
F & T & F & T & T & F & F & F & T & T \\
F & F & T & T & F & F & T & T & T & F \\
F & F & T & F & T & F & T & T & F & T \\
T & F & F & T & F & T & T & F & T & F \\
T & F & F & F & T & T & T & F & F & T \\
T & T & T & F & F & T & F & T & F & F \\
T & T & T & T & T & T & F & T & T & T \\
\hline
\end{array}$
{{qed}}
From Biconditional is Associative and Exclusive Or is Associative, we have that both $\iff$ and $\oplus$ are associative, which justifies the rendition of this result without parentheses.
Theorem: NAND and NOR are Functionally Complete

The NAND and NOR operators are each functionally complete.
That is, NAND and NOR are Sheffer operators.

Proof:
In NAND is Functionally Complete it is demonstrated that NAND is functionally complete.
In NOR is Functionally Complete it is demonstrated that NOR is functionally complete.
Theorem: Proof of Theorem by Truth Table

Let $\phi$ be a propositional formula whose atoms are $p_1, p_2, \ldots, p_n$.
Let $l$ be the line number of any row in the truth table of $\phi$.
Let $\hat {p_i}$ be defined as:
:<nowiki>$\hat {p_i} = \begin{cases}
p_i & : \text {the entry in line } l \text { of } p_i \text { is } \T \\
\neg p_i & : \text {the entry in line } l \text { of } p_i \text { is } \F
\end{cases}$</nowiki>
for all $i$ such that $1 \le i \ne n$.
Then:
:$(1): \quad \hat {p_1}, \hat {p_2}, \ldots, \hat {p_n} \vdash \phi$ is provable if the entry for $\phi$ in line $l$ is $\T$
:$(2): \quad \hat {p_1}, \hat {p_2}, \ldots, \hat {p_n} \vdash \neg \phi$ is provable if the entry for $\phi$ in line $l$ is $\F$

Proof:
:$(1): \quad$ Suppose $\phi$ is an atom $p$.
Then we need to show that $p \vdash p$ and $\neg p \vdash \neg p$.
These are proved in one line in the proof of the Law of Identity.
:$(2): \quad$ Suppose $\phi$ is of the form $\neg \phi_1$.
There are two cases to consider:
Suppose $\phi$ evaluates to $\T$.
{{finish|More hard work. I'll come back to this once I've got some more basics done.}}
Category:Propositional Logic
45atq9lcjh9aoqzumjow3ead1nywq6y
Theorem: WFFs of PropLog of Length 1

The only WFFs of propositional logic of length $1$ are:
* The letters of the formal grammar of propositional logic $\LL_0$
* The tautology symbol $\top$
* The contradiction symbol $\bot$.

Proof:
We refer to the rules of formation.
From $\mathbf W: \T \F$, $\top$ and $\bot$ (both of length 1) are WFFs.
From $\mathbf W: \PP_0$, all elements of $\PP_0$ (all of length 1) are WFFs.
Every other rule of formation of the formal grammar of propositional logic consists of an existing WFF in addition to at least one other primitive symbol.
Hence the result.
{{qed}}
Theorem: WFF of PropLog is Balanced

Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is a balanced string.

Proof:
We will prove by strong induction on $n$ that:
:All WFFs of length $n$ are balanced.
Let $\map l {\mathbf A}$ denote the number of left brackets in a string $\mathbf A$.
Let $\map r {\mathbf A}$ denote the number of right brackets in a string $\mathbf A$.
Theorem: Prefix of WFF of PropLog is not WFF

Let $\mathbf A$ be a WFF of propositional logic.
Let $\mathbf S$ be a prefix of $\mathbf A$.
Then $\mathbf S$ is not a WFF of propositional logic.

Proof:
The proof proceeds by strong induction on the length of a WFF of propositional logic.
Let $\map l {\mathbf Q}$ denote the length of a string $\mathbf Q$.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:A prefix of $\mathbf A$ such that $\map l {\mathbf A} = n$ is not a WFF of propositional logic.
By definition, $\mathbf S$ is a prefix of $\mathbf A$ {{iff}} $\mathbf A = \mathbf {S T}$ for some non-null string $\mathbf T$.
Thus we note that $\map l {\mathbf S} < \map l {\mathbf A}$.
Theorem: Construction of Parallel Line

Given a straight line, and a given point not on that straight line, it is possible to draw a parallel to the given straight line.
{{:Euclid:Proposition/I/31}}

Proof:
The transversal $AD$ cuts the lines $BC$ and $AE$ and makes $\angle DAE = \angle ADC$.
From Equal Alternate Angles implies Parallel Lines it follows that $EA \parallel BC$.
{{qed}}
{{Euclid Note|31|I}}
Theorem: Sum of Angles of Triangle equals Two Right Angles

In a triangle, the sum of the three interior angles equals two right angles.
{{:Euclid:Proposition/I/32}}

Proof:
:300px
Let $\triangle ABC$ be a triangle.
Let $BC$ be extended to a point $D$.
From External Angle of Triangle equals Sum of other Internal Angles:
: $\angle ACD = \angle ABC + \angle BAC$
Bby by Euclid's Second Common Notion:
: $\angle ACB + \angle ACD = \angle ABC + \angle BAC + \angle ACB$
But from Two Angles on Straight Line make Two Right Angles, $\angle ACB + \angle ACD$ equals two right angles.
So by Euclid's First Common Notion, $\angle ABC + \angle BAC + \angle ACB$ equals two right angles.
{{qed}}
Theorem: Sum of Angles of Triangle equals Two Right Angles

In a triangle, the sum of the three interior angles equals two right angles.
{{:Euclid:Proposition/I/32}}

Proof:
:480px
Let $\Delta ABC$ be a triangle.
Let $DAE$ be a line such that $DE \parallel BC$.
By Parallelism implies Equal Alternate Angles:
:$\angle DAB = \angle ABC$
and:
:$\angle EAC = \angle ACB$
Therefore, the sum of the three angles is:
:$\angle ABC + \angle BCA + \angle CAB = \angle DAB + \angle BAC + \angle CAE = 180 \degrees$
{{qed}}
Theorem: Equivalence of Logical Implication and Conditional

:$\paren {p \implies q} \dashv \vdash \paren {p \vdash q}$
That is, the conditional is logically equivalent to logical implication.

Proof:
This directly follows from:
* The Modus Ponendo Ponens: $p \implies q, p \vdash q$
* The Rule of Implication: $\left({p \vdash q}\right) \vdash p \implies q$.
{{qed}}
Theorem: Soundness Theorem for Propositional Tableaux and Boolean Interpretations

Tableau proofs (in terms of propositional tableaux) are a sound proof system for boolean interpretations.
That is, for every WFF $\mathbf A$:
:$\vdash_{\mathrm{PT} } \mathbf A$ implies $\models_{\mathrm{BI} } \mathbf A$

Proof:
This is a corollary of the Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations:
Let $\mathbf H$ be a countable set of propositional formulas.
Let $\mathbf A$ be a propositional formula.
If $\mathbf H \vdash \mathbf A$, then $\mathbf H \models \mathbf A$.
In this case, we have $\mathbf H = \O$.
Hence the result.
{{qed}}
Theorem: No Boolean Interpretation Models a WFF and its Negation

Let $v$ be a boolean interpretation.
Let $\mathbf A$ be a WFF of propositional logic.
Then $v$ can not model both $\mathbf A$ and $\neg \mathbf A$.

Proof:
Suppose that $v$ models $\mathbf A$:
:$v \models \mathbf A$
Then $v \left({\mathbf A}\right) = T$ by definition of models.
By definition of boolean interpretation, $v \left({\neg \mathbf A}\right) = F$.
In particular, $v (\neg \mathbf A) \ne T$, so that:
:$v \not\models \neg \mathbf A$
Hence the result.
{{qed}}
Category:Propositional Logic
r1x63wssaxbv1ldoku4z649dfz2wow9
Theorem: Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations

Tableau proofs (in terms of propositional tableaux) are a strongly sound proof system for boolean interpretations.
That is, for every collection $\mathbf H$ of WFFs of propositional logic and every WFF $\mathbf A$:
:$\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ implies $\mathbf H \models_{\mathrm{BI}} \mathbf A$

Proof:
By definition of tableau proof, $\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ means:
:There exists a tableau confutation of $\mathbf H \cup \set {\neg\mathbf A}$.
By Tableau Confutation implies Unsatisfiable, it follows that $\mathbf H \cup \set {\neg\mathbf A}$ is unsatisfiable for boolean interpretations.
Therefore, if some boolean interpretation $v$ models $\mathbf H$:
:$v \models_{\mathrm{BI}} \mathbf H$
then since $\mathbf H \cup \set {\neg\mathbf A}$ is unsatisfiable:
:$v \not\models_{\mathrm{BI}} \neg\mathbf H$
Now by definition of the relation $\models_{\mathrm{BI}}$, it must be that:
:$\map v {\neg \mathbf A} = F$
By the truth table for $\neg$, this implies:
:$\map v {\mathbf A} = T$
which is to say $v \models_{\mathrm{BI}} \mathbf A$.
Hence:
:$v \models_{\mathrm{BI}} \mathbf H$ implies $v \models_{\mathrm{BI}} \mathbf A$
that is, $\mathbf A$ is a $\mathrm{BI}$-semantic consequence of $\mathbf H$:
:$\mathbf H \models_{\mathrm{BI}} \mathbf A$
which was to be shown.
{{qed}}