On the Relationship Between Intuitionistic Propositional Logic and Intuitionistic Protothetics

A.D. Yashin

This work was partially supported by RFBR grant No 98–06–80205 ”Logical theory of informalizability”.

Let Int be the intuitionistic propositional logic, V ar be a set of propositional variables and T be a theory formulated in some rich language L. One may conceive either the 1-st or 2-nd order language, or the propositional language with propositional quantification, etc.

The language L is assumed to contain the standard intuitionistic connectives →, ∨, ∧, ¬. Also we suppose that the class of all L-formulas includes the subclass Sent(L) of sentences.

A function t : V ar → Sent(L) is said to be an interpretation. An arbitrary interpretation is expanded on the class of all propositional formulas by means of induction:

t(A ∘ B) = t(A) ∘ t(B) for binary connective ∘, and t(¬A) = ¬t(A).

Let the inference system of T supports the standard axiom schemata and rules of Int. Then the following statement is undoubtful:

”If Int ⊢ A, then for every interpretation t, T ⊢ t(A)”. (the soundness theorem). The inverse statement

”If Int ⊬ A, then for some interpretation t, T ⊬ t(A)” one may treate as the completeness theorem for Int w.r.t. T.

The completeness of Int w.r.t. the intuitionistic arithmetic HA (Heyting arithmetic) is known as de-Jongh–Smorynski theorem.

We present a similar result for quite intuitionistic prototetics Int2_{i}, i.e. for intuitionistic propositional logic with propositional quantification, with an additional axiom ¬∀p (p ∨ ¬p) (the negation of tertium non datur).

Theorem. Let A(p_{1}, …, p_{n}) be a propositional formula, such that Int ⊬ A(p_{1}, …, p_{n}). Then there are sentences E_{1}, …, E_{n} of the language of protothetics, such that Int2_{i} ⊬ A(p_{1}|E_{1}, …, p_{n}|E_{n}).

Address: Izhevsk, Russia

E-mail: yashin@wing.uni.udm.ru