A Propositional Calculus in Natural Deduction Style draft for the lecture on logic, Dec. 2004

Tudor Jebelean RISC-Linz

Johannes Kepler University, A-4040 Linz, Austria

                                         www.risc.uni-linz.ac.at

Abstract

We construct a simple propositional calculus based on rewrite rules which correspond to the natural rules used by human provers. This is in fact a formalization of the propositional prover implemented in the Theorema system by Buchberger, and later improved by Jebelean. The purpose of the formalization is to show that the propositional prover of Theorema is correct and complete, and also to investigate possible improvements concerning efficiency and naturalness. The main differences from the traditional propositional theory consist in applying the logical connectives “and” and “or” to sets, and in the treatment of sequents as syntactical alternatives to logical formulae.

1 Syntax and Semantics

Let V be an enumerable set, whose elements will be called propositional variables (e.g. P, Q, R, …). Definition (F). The set F of propositional formulae is the smallest set having the properties:

(FV) V ⊆ F (expressions consisting of one variable);

(F¬) ¬A ∈ F for any A ∈ F;

(F∧) ∧A ∈ F for any finite A ⊂ F

(F∨) ∨A ∈ F for any finite A ⊂ F

Formulae of type P ∈ V are called atoms, formulae of type P and ¬P (also denoted \overline{P}) are called literals. Note that in (S∧) and (S∨) A may be empty: we will sometimes denote the constants ∧∅ and ∨∅ by T (true) and F (false), respectively. Definition (I). An interpretation I is a subset of V: I ⊂ V. Given an interpretation I, the truth value of a formula A under the interpretation I ⟨A⟩_{I} is defined by:

(IV) for any P ∈ V : ⟨P ⟩_{I} = T if P ∈ I, and F otherwise;

(I¬) for any A ∈ F : ⟨¬A⟩_{I} = T if ⟨A⟩_{I} = F, and F otherwise;

(I∧) for any A ⊂ F : ⟨∧A⟩_{I} = T if ⟨A⟩_{I} = T for any A ∈ A, and F otherwise; (I∨) for any A ⊂ F : ⟨∨A⟩_{I} = T if ⟨A⟩_{I} = T for some A ∈ A, and F otherwise;

The notions: true under I, satisfied by I, I-true, I is a model of A, false under I, I-false, are defined in the usual way, as are the notions of validity, inconsistency, satisfiability, and [semantic] equivalence for formulae. Note that ∧∅ (T) is valid and ∨∅ (F) is inconsistent. We denote formulae of the type ∨{G, ¬∧A} by ⟨G, A⟩, and call them proof-situations. We call assumptions the formulae in A and goal the formula G. Such a proof situation is usually called sequent in the traditional theory, but note that we only consider sequents which have one single formula as the goal, because this is more similar to the natural human proving style.

2 Proving by Rewriting

Our purpose is to design a rewriting system which constructs proofs for formulae of type ⟨G, A⟩, i.e. for proof-situations. Simpler rewrite rules could be defined in a similar manner (e.g. for computing the con[dis]junctive normal form, for resolution proving, etc.), however we choose a particular system which is appropriate for developing proofs in “natural deduction style”, i.e. imitating human provers. In the sequel A, G denote (arbitrary) formulae, A, A′, G denote sets of formulae (including the empty set), and \overline{A} = \{¬A|A ∈ A\} (note that \overline{∅} = ∅). In the context of rewrite rules we will use expressions like {A}ˇ∪A in order to denote a set which contains A. Here the symbol ˇ∪ denotes exclusive union (union between disjoint sets) and should be understood as an abbreviation for stating that the respective rule applies if A ∉ A. Definition (⟶). The rewriting relation “⟶” is defined by: (A) Assumption-rules

(A.¬.¬) ⟨G, {¬¬A}ˇ∪A⟩ ⟶ ⟨G, {A}∪A⟩  (delete double negation)
(A.¬.∧) ⟨G, \{¬ ∧ A\}ˇ∪A′⟩ ⟶ ⟨G, \{∨\overline{A}\}∪A′⟩  (de Morgan)
(A.¬.∨) ⟨G, \{¬ ∨ A\}ˇ∪A′⟩ ⟶ ⟨G, \{∧\overline{A}\}∪A′⟩  (de Morgan)
(A.∧) ⟨G, {∧A}ˇ∪A′⟩ ⟶ ⟨G, A∪A′⟩ (split conjunction)
(A.∨)  ⟨G, {∨A}ˇ∪A′⟩ ⟶ ∧{⟨G, {A}∪A′⟩ | A ∈ A} (proof by cases)

(G) Goal-rules

(G.¬) ⟨¬G, A⟩ ⟶ ⟨F, {G}∪A⟩ (proof by contradiction)
(G.∧)  ⟨∧G, A⟩ ⟶ ∧{⟨G, A⟩ | G ∈ G⟩} (prove each part of a conjunction)
(G.∨) ⟨∨\{G\}ˇ∪G, A⟩ ⟶ ⟨G, \overline{G}∪A⟩  (prove one alternative by negating the others)

Note the particular behaviour of some rules when A or G is empty:

(A.¬.∧)_{∅} ⟨G, {¬T}ˇ∪A⟩ ⟶ ⟨G, {F}∪A⟩ (“not true” rewrites to “false”)
(A.¬.∨)_{∅} ⟨G, {¬F}ˇ∪A⟩ ⟶ ⟨G, {T}∪A⟩ (“not false” rewrites to “true”)
(A.∧)_{∅}  ⟨G, {T}ˇ∪A⟩ ⟶ ⟨G, A′⟩  (eliminate “true” assumption)
(A.∨)_{∅}  ⟨G, {F}ˇ∪A⟩ ⟶ T  (anything follows from “false” assumption)
(G.∧)_{∅}  ⟨T, A⟩ ⟶ T  (“true” follows from anything)

3 Correctness

It is straightforward to prove that each rule transforms a formula into an equivalent one. As illustration, we prove below one implication corresponding to (A.∧). (Note that some of the rules listed above are practically applied in the proof.)

Lemma. For any G, A, A′,

⟨G, {∨A}∪A′⟩ is equivalent to ∧{⟨G, {A}∪A′⟩ | A ∈ A}.

Proof. Let I be an arbitrary but fixed interpretation. We prove:

⟨G, {∨A}∪A′⟩ is I-true iff ∧{⟨G, {A}∪A′⟩ | A ∈ A} is I-true.

(⇒) Assume ∨{G, ¬ ∧ {∨A}∪A′} is I-true.

Case 1 : G is I-true. Then ∨{G, ¬ ∧ {A}∪A′} is I-true for each A in A.

Case 2 : ¬ ∧ {∨A}∪A′ is I-true. Then ∧{∨A}∪A′ is I-false, hence either ∨A or some A′ in A′ is I-false. Case 2.1 : ∨A is I-false. Then each A in A is I-false, hence ∧{A}∪A′ is I-false. Case 2.2 : Some A′ in A′ is I-false. Then again the former holds. Therefore, ∨{G, ¬ ∧ {A}∪A′}} is I-true for all A in A.

Consequently, ∧{∨{G, ¬ ∧ {A}∪A′}} | A ∈ A} is I-true.

(⇐) … (similarly).

The rewrite rules (A), (G) transform each proof-situation into another proof-situation or a (conjunctive) set of proof-situations. It is natural to represent this process as a proof-tree, in which the root is the initial proof-situation, while each node has as son[s] the proof-situation[s] in which it is rewritten. A node has no sons only if no rewrite rule can apply to it (that is, we consider only complete proof trees). Since, on one hand, the rewrite rules preserve the truth-value and, on the other hand, each set of “brothers” represents a conjunction, it is clear that a node is valid iff all his descendents are valid. Moreover, if the tree is finite, then validating the root is equivalent to validating all leaves.

4 Termination

We show now that each proof tree is finite. For this, by König’s Lemma, it is enough to show that each path in the tree is finite, therefore we show that the rule which defines the son-father relationship is terminating. This relationship, which will be denoted by “⟼”, is defined by the same rules as “⟶”, except for (A.∨) and (G.∧), which have to be replaced by:

\begin{matrix}(A.∨)’ & ⟨G, \{∨A\}ˇ∪A′⟩ & ⟼ & ⟨G, \{A\}∪A′⟩ & iff A ∈ A \\ (G.∧)’ & ⟨∧G, A⟩ & ⟼ & ⟨G, A⟩ & iff G ∈ G \end{matrix}

The special cases (A.∨)_{∅} and (G.∧)_{∅} do not hold for ⟼, but this does not affect termination. Let us consider separately the relation ⟼_{A} defined on the set of assumptions by the A-rules and the relation ⟼_{G} defined on the goals by the G-rules. Then ⟼ is a subset of their lexicografic composition:

⟨G, A⟩ ⟼_{G}, A⟨G′, A′⟩ iff \{ \begin{matrix}G ⟼_{G} G′ \\ or \\ G = G′ and A ⟼_{A} A′ \end{matrix}

hence it is enough to prove termination for ⟼_{A} and ⟼_{G}: ⟼_{A} is normalization combined with ∨ elimination, (G.¬) is terminal, and (G.∧), (G.∨)’ shorten G.

5 Completeness

Each proof-tree has a finite number of leaves, which will be called terminal proof-situations (TPS). Examining the right-hand-side of ⟶ we see that a TPS can have only one of the forms ⟨G, A⟩ or T.

Lemma. A formula X is a TPS iff:

(1) X = T or

(2) X = ⟨F, L⟩ for some set of literals L or

(3) X = ⟨P, L⟩ for some atom P and some set of literals L

(⇐). By examining the rewrite rules, one sees that formulae of the above types cannot be rewritten. (⇒). Let X be a TPS which is not T. Then X = ⟨G, A⟩ for some formula G and some set of formulae A. If G is neither an atom, nor F, then one of the (G)-rules will apply to it. Also, if A is not empty, then any member of it must be of the form P or ¬P, otherwise one of the (A)-rules will apply.

Lemma. ⟨∨∅, L⟩ is valid iff {P, ¬P } ⊂ L for some atom P. Proof. ⟨F, L⟩ denotes the formula ∨{F, ¬ ∧ L}, which is equivalent (by ∨-flattening) to ¬ ∧ L. If {P, ¬P } ⊂ L then ∧L is obviously inconsistent. Conversely, if ∧L is inconsistent, then L¬ = ∅. Consider L_{+} the set of positive atoms in L. If no P from L_{+} has its opposite in L, then L_{+} is an interpretation which satisfies ∧L.

Lemma. ⟨Q, L⟩ is valid iff Q ∈ L or {P, ¬P } ⊂ L for some atom P. Proof. ⟨Q, L⟩ denotes the formula ∨{Q, ¬ ∧ L} The right-to-left implication is obvious. For the converse, let us assume ∨{Q, ¬ ∧ L} is valid, and Q is not in L. Then L¬ = ∅ and one can construct, as in the previous proof, an interpretation which satisfies L but does not contain Q.

Since, on one hand, the rewrite rules preserve the truth-value and, on the other hand, each set of “brothers” in the proof-tree represents a conjunction, it is clear that a node is valid iff all his descendents are valid. Moreover, if the tree is finite, then validating the root is equivalent to validating all TPSs, which is simple to perform by the criteria given by the last lemmatas. Therefore, the rewrite system can be already considered a proof procedure, which is terminating, complete and correct, no matter in which order the rules are applied.

Example. A proof tree is presented in Fig. 1.

⟨∨{¬ ∨ {P, Q}, R}, {∨{¬P, R}, ∨{¬Q, R}}⟩

(G.∨)

⟨R, {∨{¬¬ ∨ {P, Q}}, ∨{¬P, R}, ∨{¬Q, R}}⟩

(A.∨)

⟨R, {¬¬ ∨ {P, Q}, ∨{¬P, R}, ∨{¬Q, R}}⟩

(A.∧)

⟨R, {¬¬ ∨ {P, Q}, ∨{¬P, R}, ∨{¬Q, R}}⟩

(A.¬.¬)

⟨R, {∨{P, Q}, ∨{¬P, R}, ∨{¬Q, R}}⟩

(A.∨)

\begin{matrix}⟨R, \{P, ∨\{¬P, R\}, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \{P, R, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \\ \{P, R, ¬Q\}⟩ \end{matrix} & \begin{matrix}⟨R, \\ \{P, R\}⟩ \end{matrix} \end{matrix} & \begin{matrix}⟨R, \{P, R, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \\ \{P, R, ¬Q\}⟩ \end{matrix} & \begin{matrix}⟨R, \\ \{P, R\}⟩ \end{matrix} \end{matrix} \end{matrix}  \begin{matrix}⟨R, \{Q, ∨\{¬P, R\}, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \{Q, R, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \\ \{Q, R, ¬Q\}⟩ \end{matrix} & \begin{matrix}⟨R, \\ \{Q, R\}⟩ \end{matrix} \end{matrix} & \begin{matrix}⟨R, \{Q, R, ∨\{¬Q, R\}\}⟩ \\ (A. ∨) \\ \begin{matrix}⟨R, \\ \{Q, R, ¬Q\}⟩ \end{matrix} & \begin{matrix}⟨R, \\ \{Q, R\}⟩ \end{matrix} \end{matrix} \end{matrix}

Figure 1: A proof-tree.

6 Possible Extensions

It is possible to add more formulae and rules to the system, in order to obtain simpler and more natural proofs. The new formulae and rules will be “short-hands” for the initial formulae and for the rules (A), (G) and for the TPS validity checks, therefore they do not change the termination, completeness and correctness of the system.

First one can add some terminal rules which perform the TPS validity check: Definition (T). Terminal-rules are defined by:

(T.pos) ⟨G, {G}ˇ∪A⟩ ⟶ T,

(T.neg) ⟨G, {A, ¬A}ˇ∪A⟩ ⟶ T

for any formulae A, G and any set of formulae A. These rules will rewrite each terminal proof situation into T, hence we have the following:

Theorem. If a proof-situation is valid, then any proof-tree of it has only T-leaves. If the proof-tree of a proof-situation has only T-leaves, then the proof-situation is valid.

Furthermore one can add the resolution rule (in order to make the calculus more efficient), and one can enrich the syntax by introducing more logical connectives and their corresponding rules.