Intuinistic Propositional Logic

A restirction of Propositional Logic to only use Intuinistic Reasoning. Kripke Semantics has:

$$w\models p⟺w\in \mathcal{V}(p)$$

In IPL, we have: let $\mathcal{B}$ be a base of logic rules. We will use Base Extensions.

$$\begin{array}{rl}{⊩}_{\mathcal{B}}p& ⟺{⊢}_{\mathcal{B}}p\\ {⊩}_{\mathcal{B}}\perp & ⟺({⊩}_{\mathcal{B}}p\forall p:\mathrm{Atom})\\ {⊩}_{\mathcal{B}}\varphi \vee \psi & ⟺\forall p:Atom;\mathcal{C}\supset \mathcal{B}.\varphi {⊩}_{\mathcal{C}}p\wedge \psi {⊩}_{\mathcal{B}}p⟹{⊩}_{\mathcal{B}}p\\ & \\ {⊩}_{\mathcal{B}}\varphi \wedge \psi & ⟺\varphi {⊩}_{\mathcal{C}}p\wedge \psi {⊩}_{\mathcal{B}}p\\ \Theta {⊩}_{\mathcal{B}}\varphi & ⟺\forall \mathcal{C}\supset \mathcal{B}.(\forall \theta \in \Theta .{⊩}_{\mathcal{C}}\theta )⟹{⊩}_{\mathcal{C}}\varphi \end{array}$$

Where w is an Atom.

Natural Deduction Derivability

Let ${⊢}_{\mathrm{NJ}}$ be natural deduction derivability.

Soundness

$\Phi {⊢}_{\mathrm{NJ}}\Psi ⟹\Phi {⊩}_{\mathcal{B}}\Psi$ Proof: Easy induction

Completeness of NJ

$\Phi {⊩}_{\mathcal{B}}\Psi ⟹\Phi {⊢}_{\mathrm{NJ}}\Psi$ Proof:

Strategy

Idea: Construct a ‘special base’ We want to set up a base of all of the possible atomic formulas Let $\Gamma$ be the set containtin al lmemebers of $\Phi \cup \Psi$ Let ${\gamma }^{♭}$ be the basic sentences corresponding to $\gamma$ such that ${\gamma }_1\ne {\gamma }_2⟹{\gamma }_1^{♭}\ne {\gamma }_2^{♭}$ so define an object ${\gamma }^{♯}$ as the ‘naturalized’ inverse of $♭$.

Assume a base $\mathcal{N}$ mimicing the rules for natural deduction by way of $♭$ s.t. (a) $\forall \gamma \in \Gamma ;\mathcal{B}\supset \mathcal{N}.{⊩}_{\mathcal{B}}{\gamma }^{♭}⟺{⊩}_{\mathcal{B}}\gamma$ (b) $\forall P,q.P{⊢}_{\mathcal{N}}q⟹P^{♯}⊢q^{♯}$

Disjunction

${⊩}_{\mathcal{B}}$ Idea behind disjunction: There’s enough ‘structure’ lying around to ‘fudge it’.