Using PL to Describe Properties of Systems

Let ${\mathcal {L}}_{2}={\mathcal {L}}(\mathrm {A} ,\Omega ,\mathrm {Z} ,\mathrm {I} )$, where $\mathrm {A}$, $\Omega$, $\mathrm {Z}$, $\mathrm {I}$ are defined as follows:

• The alpha set $\mathrm {A}$, is a countably infinite set of symbols, for example:

$\mathrm {A} =\{p,q,r,s,t,u,p_{2},\ldots \}$.

• The omega set $\Omega =\Omega _{1}\cup \Omega _{2}$ partitions as follows:

$\Omega _{1}=\{\lnot \}$,

$\Omega _{2}=\{\land ,\lor ,\to ,\leftrightarrow \}$.

In the following example of a propositional calculus, the transformation rules are intended to be interpreted as the inference rules of a so-called natural deduction system. The particular system presented here has no initial points, which means that its interpretation for logical applications derives its theorems from an empty axiom set.

• The set of initial points is empty, that is, $\mathrm {I} =\varnothing$.
• The set of transformation rules, $\mathrm {Z}$, is described as follows:

Our propositional calculus has eleven inference rules. These rules allow us to derive other true formulas given a set of formulas that are assumed to be true. The first ten simply state that we can infer certain well-formed formulas from other well-formed formulas. The last rule however uses hypothetical reasoning in the sense that in the premise of the rule we temporarily assume an (unproven) hypothesis to be part of the set of inferred formulas to see if we can infer a certain other formula. Since the first ten rules do not do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule.

In describing the transformation rules, we may introduce a metalanguage symbol $\vdash$. It is basically a convenient shorthand for saying "infer that". The format is $\Gamma \vdash \psi$, in which Γ is a (possibly empty) set of formulas called premises, and ψ is a formula called conclusion. The transformation rule $\Gamma \vdash \psi$ means that if every proposition in Γ is a theorem (or has the same truth value as the axioms), then ψ is also a theorem. Considering the following rule Conjunction introduction, we will know whenever Γ has more than one formula, we can always safely reduce it into one formula using conjunction. So for short, from that time on we may represent Γ as one formula instead of a set. Another omission for convenience is when Γ is an empty set, in which case Γ may not appear.

Negation introduction

$(p\to q)$ and $(p\to \neg q)$, infer $\neg p$.

That is, $\{(p\to q),(p\to \neg q)\}\vdash \neg p$.

Negation elimination

From $\neg p$, infer $(p\to r)$.

That is, $\{\neg p\}\vdash (p\to r)$.

Double negation elimination

From $\neg \neg p$, infer p.

That is, $\neg \neg p\vdash p$.

Conjunction introduction

From p and q, infer $(p\land q)$.

That is, $\{p,q\}\vdash (p\land q)$.

Conjunction elimination

From $(p\land q)$, infer p.

From $(p\land q)$, infer q.

That is, $(p\land q)\vdash p$ and $(p\land q)\vdash q$.

Disjunction introduction

From p, infer $(p\lor q)$.

From q, infer $(p\lor q)$.

That is, $p\vdash (p\lor q)$ and $q\vdash (p\lor q)$.

Disjunction elimination

From $(p\lor q)$ and $(p\to r)$ and $(q\to r)$, infer r.

That is, $\{p\lor q,p\to r,q\to r\}\vdash r$.

Biconditional introduction

From $(p\to q)$ and $(q\to p)$, infer $(p\leftrightarrow q)$.

That is,$\{p\to q,q\to p\}\vdash (p\leftrightarrow q)$.

Biconditional elimination

From $(p\leftrightarrow q)$, infer $(p\to q)$.

From $(p\leftrightarrow q)$, infer $(q\to p)$.

That is, $(p\leftrightarrow q)\vdash (p\to q)$ and $(p\leftrightarrow q)\vdash (q\to p)$.

Modus ponens (conditional elimination)

From p and $(p\to q)$, infer q.

That is, $\{p,p\to q\}\vdash q$.

Conditional proof (conditional introduction)

From [accepting p allows a proof of q], infer $(p\to q)$.

That is, $(p\vdash q)\vdash (p\to q)$.