Constructing Natural Deduction Sequences?

77 Views Asked by At

My question is at the very end of this preamble, which I think will aid in the understanding of the question and I therefore included.

Start with a 'set' $P$, of atomic proposition 'characters', connectives $C = \{\rightarrow,\leftrightarrow,\wedge,\vee\}$ which are also taken to be character 'strings' and auxillary symbols (brackets , the negation operator and the falsity atom) $A = \{(,),\neg,\bot\}$. Consider the set of all finite length sequences, $\Omega$, that is this is the set of all $s : \{1,...,k\} \rightarrow P \cup C \cup A$. Each $s$ is to be interpreted as the string $S$ with length $k$, and whose $i$th character is $S(i) = s(i)$.

Clearly $\Omega$, viewed as a set of strings, satisfies the following properties:

(0) $P \subset \Omega$

(1)For all $c \in C$: $a,b \in \Omega$ $\implies$ $(acb) \in \Omega$

(2) If $a \in \Omega$, then $(\neg a) \in \Omega$

(3) $\bot \in \Omega$

as $\Omega$ is defined to be the set of all finite length strings with characters in $P \cup C \cup A$. Now we may take the smallest subset of $\Omega$ satisfying $(0) - (3)$, calling it $W(P)$. This is the set of all 'sentences' that we will deal with in our propositional logic.

Formation Sequences:

A finite length sequence $s : \{1,...,k\} \rightarrow P \cup C \cup A$ is called a formation sequence, if $s$ satisfies the following properties:

For all $i \in \{1,...,k\}$, $s(i) \in P$, or $$s(i) = ( s(j)\ c\ s(k) )$$, where $j,k < i$ and $c \in C$, or $s(i) = \bot$, or $s(i) = ( \neg s(j) )$ for some $j < i$.

It is easy to show that the set of all sequences that are formation sequences is $W(P)$ by an inductive argument.


Natural Deduction:

We start with the connectives $\{\rightarrow,\wedge,\bot\}$, which we will write rules for.

Start with a premise set: $\Sigma$ (may be empty) which contains sentences constructible from connectives in
$\{\rightarrow,\wedge \}$ and may include $\bot$.

Let $N$ be the set of all sentences that follow from $\Sigma$ via the rules of natural deduction ( we will define it later ).

Define the set $W(P)\{\rightarrow,\wedge,\bot\}$ to be the set of all propositonal sentences at most involving atomic propositions, connectives in $\{\rightarrow,\wedge\}$ and $\bot$.

Consider the set $2^{W(P)\{\rightarrow,\wedge,\bot\}} \times W(P)\{\rightarrow,\wedge,\bot\}$. Notice it is an example of a set $X \subset 2^{W(P)\{\rightarrow,\wedge,\bot\}} \times W(P)\{\rightarrow,\wedge,\bot\}$ satisfying all of the following rules:

$(0) : \phi \in \Sigma \implies (\Sigma,\phi) \in X$

$\rightarrow I : (\Sigma \cup \{\phi\},\psi) \in X \implies (\Sigma, \phi \rightarrow \psi) \in X$

$\rightarrow E : (\Sigma,\phi \rightarrow \psi),(\Sigma,\phi) \in X \implies (\Sigma,\psi) \in X$

$\wedge I : ((\Sigma,\phi),(\Sigma,\psi)) \in X^2 \implies (\Sigma,(\phi \wedge \psi)) \in X$

$\wedge E : (\Sigma,(\phi \wedge \psi)) \in X \implies (\Sigma,\phi), (\Sigma,\psi) \in X$

$\bot 1 : (\Sigma,((\phi \rightarrow \bot)) \rightarrow \bot)) \in X \implies (\Sigma,\phi) \in X$

$\bot 2: (\Sigma,\bot) \in X \implies (\Sigma,\phi) \in X$ for all $\phi$ a propositional sentence only involving the connective $\{\wedge,\rightarrow\}$ and possibly $\bot$

Define $N$ to be the smallest subset satisfying all the above properties, noting that the intersection of all such subsets is nonempty, since it contains $\Sigma$ at the very least, and that the intersection must satisfy all the above properties.

Now in a somewhat analogous way to when I defined 'formation sequences' for propositional sentences, I wonder if from here on I may define a 'deduction sequence', and show that $N$ is really the set of all sentences that are the resultants of these deduction sequences?

One of my issues with this is that the deduction sequence should in some sense represent the entire proof, but this is quite messy as each item should either be in $\Sigma$ , or should be a consequent of a deduction rule involving previous consequents also in the sequence. However if the deduction rule was for instance $\rightarrow I$, then I do not know how to deal with any additional (cancelled) assumptions made.