Propositional Calculus

Here we describe an example (c4.3) of proof calculus which are also examples of hilbert systems. In the end, we show some variations (c4.3.5, and q4.9) of this proof calculus

Characterization

Language

• The dialect $L_{\to }$ of the proposional language
  • convectives: $\{\neg ,\to \}$
  • the propositions are either elementary propositions, negation propositions in the form $\neg \phi$, or propositions in the form $(\phi \to \psi )$

Logical Axioms

(Each one is general form of one of infinite propositions. Also, these axioms are tautologies (q4.6))

	Logical Axioms
Ax1	$(\phi \to (\psi \to \phi ))$
Ax2	$([\phi \to (\psi \to \theta )]\to [(\phi \to \psi )\to (\psi \to \theta )])$
Ax3	$[(\neg \phi \to \neg \psi )\to (\psi \to \phi )]$

Rules of inference

(Modus ponens) $\frac{\phi ,(\phi \to \psi )}{\psi }$

Definitions

Here are some definitions related to this proof calculus:

Proof Sequence

• Let $K$ be a set of propositions, a proof sequence from a set $K$ (in our calculus) is a sequence of propositions ${\phi }_1,\dots ,{\phi }_n$ such that each proposition in the sequence is either:
  • A logical axiom
  • A proposition in the set $K$
  • Derived from two previous propositions in the sequence using rules of inference (here is only modus ponens)
• A proof sequence in the calculus is proof sequence from the empty set. (i.e. each proposition is either a logical axiom or derived from two previous propositions)
• A proof sequence from $K$ to $\phi$ is a proof sequence from $K$, such that $\phi$ is the last proposition

Provable Proposition

• $\phi$ is theorem (משפט) of $K$ (or is provable (יכיח) from $K$) and denoted by $K⊢\phi$, if and only if it has (at least one) proof sequence from $K$
• (4.1)
  • If ${\phi }_1,\dots ,{\phi }_n$ is a proof sequence from $K$, then for each $i\le n$ the proof sequence ${\phi }_1,\dots ,{\phi }_i$ is is a proof sequence from $K$. (todo )
  • If ${\phi }_1,\dots ,{\phi }_n$ is a proof sequence from $K$, and ${\psi }_1,\dots ,{\psi }_n$ is also a proof sequence from $K$, then ${\phi }_1,\dots ,{\phi }_n,{\psi }_1,\dots ,{\psi }_n$
  • If $K⊢\phi$ and $K\subseteq K^{\prime }$ then $K^{\prime }⊢\phi$
  • If $\phi$ is a theorem of $K$, and $K\cup \{\phi \}⊢\psi$ then $K⊢\psi$.
    • Similarly, ${\phi }_1,\dots ,{\phi }_n$ are theorems of $K$ and $K\cup \{{\phi }_1,\dots ,{\phi }_n\}⊢\psi$ then $K⊢\psi$.
  • If $K⊢\phi$ then there exists a finite subset of $K^{\prime }$ such that $K^{\prime }⊢\phi$

Note: all these properties (4.1) are not unique to the specific calculus we chose with three axioms and the MP rule.

We can show that a proposition is a theorem (provable), using either showing its proof sequence or using t4.3

Theory

• Given a set of propositions $K$
  • $K$ is inconsistent if there exists a proposition $\phi$ s.t. $K⊢\phi$ and $K⊢\neg \phi$
  • $K$ is consistent if it is not inconsistent
  • $K$ is maximally consistent if every superset of $K$ is inconsistent
• A consistent set of propositions is called a theory
• (Syntactical completeness) A theory is complete (תורה שלמה) if for every proposition $\phi$, either $K⊢\phi$ (provable) or $K⊢\neg \phi$ (disproved)

In some books, the definitions requires a theory to be closed under logical implication

Properties

Here are some properties of this proof calculus

• lemma:
  • if $\phi$ is a logical axiom or $\phi \in K$ then $K⊢\phi$
  • if $K⊢\psi$ and $K⊢(\psi \to \phi )$ then $K⊢\phi$
  • if $K⊢\phi$ then for each proposition $\psi$: $K⊢(\psi \to \phi )$
  • for each proposition $\phi$: $K⊢(\phi \to \phi )$
• (4.2) Deduction theorem: if $K\cup \{\psi \}⊢\phi$ then $K⊢(\psi \to \phi )$ (in Cunningham’s he shows the reverse direction)
  • example: arrow transitivty
• (Lemma) Let $K$ be an infinite set of proposition. If $K$ is inconsistent, then there exists a finite inconsistent subset of $K$.
• q4.7todo
• (4.3) Proof-by-Contradiction Theorem
  • For each proposition $\phi$, $\{\psi ,\neg \psi \}⊢\phi$
  • If $K$ is inconsistent, then $K⊢\phi$ for each proposition $\phi$ (todo is it iff?)
  • If $K\cup \{\neg \phi \}$ is inconsistent, then $K⊢\phi$
• examplestodo
• (4.4) Soundness Theorem (נאותות)
  • This proof calculus is sound, i.e.
  • Let $K$ be a set of propositions and $\psi$ be a proposition. If $K⊢\phi$ (provable), then $K⟹\phi$ (logically implied. common notation $K\models \phi$)
    • In particular, if $\varnothing ⊢\phi$ then, $\phi$ is a tautology ($\models \phi$)
    • Corollary: If a set of propositions has a model, then it is consistent
• (4.5) Every complete theory has unique model
• todo If a set of propositions $K$ has unique model, then $K$ is a complete theory
• (4.6) For each theory $K$ there exist a complete theory $\overline{K}$ such that $K\subseteq \overline{K}$
• (4.7) Completeness Theorem
  • This proof calculus is strongly complete
  • For every theory $K$, there exists a model $M$ such that $M\models K$
  • If a theory $K$ logically implies a proposition $\psi$, then $\psi$ is provable from $K$
  • If $K⟹\psi$ then $K⊢\psi$
• Corollary: A set of propositions is consistent iff it is satisfiable

Summary

Syntax	Semantics
$\stackrel{\text{Soundness}}{\to }$	$\stackrel{\text{Completeness}}{\leftarrow }$
$K⊢\phi$ ($\phi$ is provable from $K$)	$K\models \phi$ (or $K⟹\psi$) ($K$ logically implies $\psi$)
$⊢\phi$ (or $\varnothing ⊢\phi$) ($\phi$ is provable from the logical axioms)	$\models \phi$ ($\phi$ is a tautology)
$K$ is consistent (theory)	$M\models K$ ($K$ has a model $M$ (or, $K$ is satisfiable))
$K$ is a complete theory	$K$ has unique model

---

Other Variations

here we show some variations (c4.3.5, and q4.9) of proof calculus we saw above.

Example (c4.3.5)

This is an expansion of the proof calculus we saw above

Language

Convectives: $\{\neg ,\wedge ,\vee ,\to ,\leftrightarrow \}$

Logical Axioms

Transclude of #logical-axioms

plus the following

	Logical Axioms
Ax4.1	$(\alpha \wedge \beta )\to \alpha$
Ax4.2	$(\alpha \wedge \beta )\to \beta$
Ax5	$(\alpha \to (\beta \to (\alpha \wedge \beta )))$
Ax6.1	$\alpha \to (\alpha \vee \beta )$
Ax6.2	$\beta \to (\alpha \vee \beta )$
Ax7	$[\neg \alpha \to ((\alpha \vee \beta )\to \beta )]$
Ax8.1	$[(\alpha \leftrightarrow \beta )\to ((\alpha \to \beta ))]$
Ax8.2	$[(\alpha \leftrightarrow \beta )\to ((\beta \to \alpha ))]$
Ax9	$((\alpha \to \beta )\to ((\beta \to \alpha )\to (\alpha \leftrightarrow \beta )))$

Example (q4.9)

• q4.9 - $L=\{\neg ,\to ,\wedge \}$ and other axioms todo