# Models for Propositional Logic

It has been suggested that this page be renamed.To discuss this page in more detail, feel free to use the talk page. |

This page has been identified as a candidate for refactoring of advanced complexity.In particular: These should all be proper proof pages in themselvesUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.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 `{{Refactor}}` from the code. |

## Theorem

This page gathers together some useful results that can be used in the derivation of proofs by propositional tableau.

Let $\MM$ be a model for propositional logic, and let $\mathbf A$ and $\mathbf B$ be WFFs of propositional logic.

Then the following results hold.

The symbol $\models$ is used throughout to denote semantic consequence.

### Double Negation

- $\MM \models \neg \neg \mathbf A$ if and only if $\MM \models \mathbf A$

This is the rule of Double Negation.

### And

- $\MM \models \paren {\mathbf A \land \mathbf B}$ if and only if both $\MM \models \mathbf A$ and $\MM \models \mathbf B$

This follows by definition of Conjunction.

### Not And

- $\MM \models \neg \paren {\mathbf A \land \mathbf B}$ if and only if either $\MM \models \neg \mathbf A$ or $\MM \models \neg \mathbf B$

This follows from De Morgan's Laws: Disjunction of Negations.

### Or

- $\MM \models \paren {\mathbf A \lor \mathbf B}$ if and only if either $\MM \models \mathbf A$ or $\MM \models \mathbf B$

This follows by definition of Disjunction.

### Not Or

- $\MM \models \neg \paren {\mathbf A \lor \mathbf B}$ if and only if $\MM \models \neg \mathbf A$ and $\MM \models \neg \mathbf B$

This follows from De Morgan's Laws: Conjunction of Negations.

### Implies

- $\MM \models \paren {\mathbf A \implies \mathbf B}$ if and only if either $\MM \models \neg \mathbf A$ or $\MM \models \mathbf B$

This follows from Disjunction and Implication.

### Not Implies

- $\MM \models \neg \paren {\mathbf A \implies \mathbf B}$ if and only if $\MM \models \mathbf A$ and $\MM \models \neg \mathbf B$

This follows from Conjunction and Implication.

### Iff

- $\MM \models \paren {\mathbf A \iff \mathbf B}$ if and only if either:
- both $\MM \models \mathbf A$ and $\MM \models \mathbf B$

or:

- both $\MM \models \neg \mathbf A$ and $\MM \models \neg \mathbf B$

This follows by definition of biconditional.

### Exclusive Or

- $\MM \models \mathbf A \oplus \mathbf B$ if and only if either:
- both $\MM \models \mathbf A$ and $\MM \models \neg \mathbf B$

or:

- both $\MM \models \neg \mathbf A$ and $\MM \models \mathbf B$

This follows by definition of exclusive or.

## Sources

- 1996: H. Jerome Keisler and Joel Robbin:
*Mathematical Logic and Computability*... (previous) ... (next): $\S 1.5$: Semantics of Propositional Logic: Proposition $1.5.2$