Skip to content

The Proof Theory Blog

!A ⊢ ?!?A

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

Essential incompleteness in propositional logic

Posted on May 21, 2020July 23, 2020 by Andrei Sipoș

Consider the following formulation of Gödel’s first incompleteness theorem.

Theorem. Any complete, consistent theory that extends PA is not recursive. In other words, PA is essentially incomplete.

Five years ago, I wondered whether such a recursively enumerable and essentially incomplete theory could be easily found in classical propositional logic, where formulas are built up from a countable set of variables V=\{v_0,v_1,\ldots\} using negation and implication. It turns out that this is an almost immediate consequence of the following classical result, which asserts the existence of recursively inseparable sets.

Theorem. There exist disjoint sets A, B\subseteq \mathbb{N} which are recursively enumerable such that there is no recursive C \subseteq \mathbb{N} with A \subseteq C and B \cap C = \emptyset.

Proof. Let \varphi be a partial binary computable function which is universal, in the sense that for every partial unary computable function g there is an n such that g=\varphi(n,\cdot). Let A to be the set of all n such that \varphi(n,n)=0 and B the set of all n such that \varphi(n,n)=1. Suppose that there is a C as in the statement, and let e be such that \chi_C=\varphi(e,\cdot). Assume that e\in C. Then 1=\chi_C(e)=\varphi(e,e), so e\in B, which contradicts B \cap C = \emptyset. Thus e \notin C, i.e. 0=\chi_C(e)=\varphi(e,e), so e\in A, which contradicts A \subseteq C.

Now take A and B as above and \Gamma to be the set \{v_n \mid n \in A\} \cup \{\neg v_n \mid n \in B\}. We show that this consistent theory is essentially incomplete. Assume that there is a complete recursive extension T of \Gamma. Then the set of all n \in \mathbb{N} such that T \models v_n is also recursive and separates A and B, a contradiction.

4 thoughts on “Essential incompleteness in propositional logic”

  1. Anupam Das says:
    May 21, 2020 at 4:27 pm

    Hi Andrei,

    This is a nice example of recursive inseparability! But something is a little unsatisfying here: usually theories are closed under substitution, whereas your \Gamma is not. Is there a way to use the same/similar trick to devise a theory that is closed under substitution and essentially incomplete?

    Reply
  2. Andrei Sipoș says:
    May 21, 2020 at 4:39 pm

    Theories are not closed under substitution, they are usually closed under deduction, so one can just take the deductive closure – that is why I usually don’t bother with pointing this explicitly (even in the definition of a theory).

    Reply
    1. Anupam Das says:
      June 1, 2020 at 11:16 am

      I would say that it depends whether we treat ‘propositional variables’ as actual variables or constant symbols…. but for the avoidance of ambiguity, let us henceforth call a set of propositional formulas closed under deduction and substitution a ‘logic’.

      I think the answer to my question above is negative, since classical propositional logic is maximally consistent; if we add any non-tautologous formula as an axiom, then it becomes inconsistent. However, the question does seem to make sense for Intuitionistic Propositional Logic. Can we use the same idea to find an essentially incomplete intermediate logic?

      Reply
      1. Benedict Konhäuser says:
        April 25, 2025 at 11:28 am

        Hello Anupam,

        I think completeness makes sense for theories but not really for logics. Completeness essentially “fixes” the truth-value of atomic statements, whereas they’re used as placeholders for arbitrary propositions in logics.

        So if your theory T is complete then either p or ~p is provable in T. If it’s additionally closed under substituion, then either A or ~A is provable for all formulas A. Therefore all complete superintuitionistic logics must be inconsistent.

        Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2026 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT