i read that First-Order Logic is strong enough to formalise all of Set Theory and thereby virtually all of Mathematics. How would you express in First-Order Logic the theorem: 3SAT is NP-complete?

  • 1
    $\begingroup$ Welcome to Computer Science! What have you tried? Where did you get stuck? We do not want to just hand you the solution; we want you to gain understanding. However, as it is we do not know what your underlying problem is, so we can not begin to help. See here for tips on asking questions about exercise problems. If you are uncertain how to improve your question, why not ask around in Computer Science Chat? $\endgroup$ – Raphael Oct 22 '16 at 8:14
  • $\begingroup$ Where did you read that? Statements like $\forall A, B : A \subseteq B \implies |A| \leq |B|$ are not FOL; are they part of your notion of set theory? And to quote Wikipedia: "No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line." So no infinite sets? $\endgroup$ – Raphael Oct 22 '16 at 8:14
  • 3
    $\begingroup$ I don't think this question is really answerable in the Stack Exchange format. Even trying to express the theorem "3SAT is NP-complete" from first principles in English takes pages and pages: you have to explain Boolean logic, Turing machines, nondeterminism, polynomials, ... To explain that in FO, or even to explain how to explain it seems far too much to ask for in an answer. $\endgroup$ – David Richerby Oct 22 '16 at 9:32
  • $\begingroup$ Why the negativity? You don't have to actually write up the statement in $FOL$ so it can be processed by some proof assistant, we only need to convince ourselves that every part in the sentence can be written as a first order expression. It's similar to saying that in order to show $L\in NP$ you have to draw the nondeterministic machine (I probably only did this once or twice). Suppose we work in the language of set theory, with $ZFC$, then we can talk about natural numbers and arithmetic, so Turing machines are in. Existence of reductions can also be written in first order. $\endgroup$ – Ariel Oct 22 '16 at 11:01
  • 3
    $\begingroup$ It's not unreasonable to expect the person asking the question to make an attempt on their own before asking and show us in the question how far they've gotten and where they got stuck. If they can't make any progress at all, then this is probably asking too much for a single Stack Exchange question (you could write a concise answer that would be understandable by experts and convincing to experts, but to make it understandable and convincing to someone who can't make any progress on their own probably requires much greater length). $\endgroup$ – D.W. Oct 22 '16 at 11:20

There has been a lot of work on formalizing mathematics, and in all of this work one needs to express definitions, theorems and proofs within the logic that one is using for formalization.

This is always quite involved.

To describe the statement that 3SAT is NP-complete, we will need a version of first-order logic with a term language that will allow us to express notions of languages, time complexity, Turing machines, polynomial-time reducibility, propositional logic and conjunctive normal forms.

Once we have an appropriate term language, we will need to describe 3SAT and NP-completeness in it. This requires us to be able to express the definitions of these notions, and this in turn involves the definition of first-order predicates that correspond to these notions and the notions that were used to define them.

Let us take a brief look at a part of this construction - this should convince you that this is indeed fairly involved. A language $L$ is NP-complete if

  1. $L \in \mathrm{NP}$
  2. For every $L' \in \mathrm{NP}$ we have that $L'$ polynomial-time reduces to $L$

We define a predicate $NPC(x)$ which holds if the following conjunction holds for $x$

  1. $x$ is a language in $\mathrm{NP}$
  2. for every $y$, if $y$ is a language in $\mathrm{NP}$, then $y$ polynomial-time reduces to $x$

We therefore need a predicate $NP(x)$ that captures that $x$ is a language in $\mathrm{NP}$, and we need a predicate $PTR(x,y)$ that captures that $y$ polynomial-time reduces to $x$. If we have these, then we can define

$$ NPC(x) = NP(x) \wedge \forall y. NP(y) \Rightarrow PTR(x,y) $$

The definition $NP(x)$ must capture the following

  1. $x$ is a language.
  2. There exists a nondeterministic Turing machine $M$ with polynomial-time complexity such that for all $w$, $M$ will accept $w$ if and only if $w$ is an element of $x$.

And this in turn requires us to define predicates $L(x)$, which must describe that $x$ is a language, $TM(y)$ which must describe that $y$ is a nondeterministic Turing machine, $ACC(m,w)$ which must describe that $m$ is a Turing machine that accepts string $w$, $TC(x,c)$ which describes that $x$ is a Turing machine within $c$ steps and $POL(c,p,n)$ which describes that $c$ is bounded by the polynomial $p(n)$.

Once we have defined these, we may have needed to introduce and define further predicates. And once this has been done, we need to define $PTR(x,y)$. Here, we can make use of some of the predicates that we already have, but we also need to introduce some new ones as well.

I hope that this outlines that this process of formalization is a involved and not entirely trivial task, and I hope this also explains why I do not present the entire construction of the first-order formula here.

  • 1
    $\begingroup$ 1) Your "need"s and "require"s are to be taken with a grain of salt. One may choose to follow other approaches. 2) Why do you expect FOL is enough to express the statement at all? $\endgroup$ – Raphael Oct 22 '16 at 8:16
  • 1
    $\begingroup$ I have only used the word "requires" to indicate that when we introduce a predicate, then we need to define it also. $\endgroup$ – Hans Hüttel Oct 22 '16 at 8:20
  • $\begingroup$ @Raphael I thought everything was expressible in first order logic because of settheory.net/second-order-theory but that injecting higher logics in it made some statement unprovable. $\endgroup$ – xavierm02 Oct 22 '16 at 8:38
  • 1
    $\begingroup$ @xavierm02 It says there, very clearly: " The problem is, first-order logic cannot fully express (determine) the concept of which is the true powerset of a given set." $\endgroup$ – Raphael Oct 22 '16 at 8:53
  • 1
    $\begingroup$ @xavierm02 I can't say I have thought a lot about which logic system is used to express which part of mathematics. I guess people mostly use whichever syntax and semantics they want to express what they want. Only relatively few people try to formalize what everybody else has been doing haphazardly. While an important effort (imho) it has probably little import on the workings of most practitioners and users of mathematics. (Note that we leave the mandate of Computer Science at some point and should go to Mathematics or MathOverflow, and/or Computer Science Chat.) $\endgroup$ – Raphael Oct 22 '16 at 13:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.