All the computer languages I'm familiar with, be they imperative or declarative have the same core mechanics (arithmetic and logic).They have the same loops, conditionals etc. Whatever the language it seems to have the same logical power as the others despite the differences in syntax and attractiveness. A bash script can, with effort, be written to do the same thing a Prolog program.

Question: can the commonly uses computer languages be said to instantiate predicate logic only?

  • 2
    What exactly do you mean by "instantiate"? A syntactical correct expression/statement in a programming language usually isn't said to be true. – Jishin Noben Jun 13 at 19:54
  • 4
    They all "do the same thing" because all computers are, basically, glorified universal Turing machines, with the same types of programming instructions (loops, conditionals, memory recalls, etc.). This has nothing to do with the predicate calculus in particular, and can "instantiate" any formal "logic" whatsoever, or rather any computation whatsoever (since computation is not deduction we are not really dealing with logic). In essence, this is what the Church-Turing thesis says. – Conifold Jun 13 at 20:16
  • There is a precise relation between programs and proofs, and programming languages and proof systems, known as the Curry–Howard correspondence. For example, (intuitionistic) natural deduction systems "can be directly interpreted... as a typed variant of the model of computation known as lambda calculus". But the correspondence is not tied to any particular proof system (like predicate calculus) or to any particular model of computation. – Conifold Jun 14 at 9:23

As the comments have noted, this is a rather unclear question. However, there's an important sense in which the answer is yes.

I'll write "N" for the set of natural numbers and N for the structure of the natural numbers with zero, successor, addition, and multiplication.

Specifically, looking at a function F from N to N for simplicity, the following are equivalent:

  • F is computable by a Turing machine (or equivalently, per the comments above, any Turing-complete programming language - which is all of the ones you'd actually use).

  • F is representable in first-order Peano arithmetic PA (or indeed even less): there is a formula p(x,y) such that for each natural number n, there is exactly one natural number m such that PA proves p(n,m), and moreover that natural number is exactly f(n). Here for simplicity I'm conflating a number with the corresponding numeral - e.g. 2 versus S(S(0)).

  • F is Sigma^0_1-definable in N.

(Similar results hold for higher-arity functions, partial functions, and relations.)

So we have both provability and definability criteria, tied to first-order theories and structures respectively, which exactly capture computability. And indeed this is only a tiny fragment of first-order logic: there are non-computable sets of natural numbers (e.g. the Halting Problem) which are nonetheless first-order definable in N. Really, I would say that models of computation correspond to a very tiny fragment of first-order logic specifically in the context of N or similar structures.

That said, this isn't really the whole picture. Logics stronger than first-order logic are still "computable on finite structures" - e.g. we can brute-force determine whether a second-order sentence with k second-order quantifiers holds in a structure of size n in time more-or-less 2^(kn) - and this plays an important role in descriptive complexity theory - the point being that we can often view individual inputs to algorithms as finite structures. By contrast, the above section is looking at how the whole "input space" is construed.

  • 1
    I think this would be a (qualified) yes to "instantiate a fragment of formal systems" rather than of predicate calculus. There are plenty of alternatives to the predicate calculus and Peano arithmetic, diagrammatic systems, for example, that have the same representational strength. Some look very differently, just as artificial neuronets look very differently from Turing machines, while having the same computational strength. The Curry-Howard isomorphism suggests a more immediate "instantiation" of the intuitionistic calculus. – Conifold Jun 14 at 9:16
  • 1
    @Conifold That's definitely a fair interpretation - the question isn't very specific on this point! – Noah Schweber Jun 14 at 9:29

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.