1
$\begingroup$

I'm confused as to why we can't write formulas of infinite length in FO. For example, to express reachability, I understand the proof that there cannot be a single formula for it, but it is expressible with a set of formulas?

Since any formula has an equivalent formula in CNF, if we transform a formula of infinite length to some CNF, and then break the conjunct up into clauses and put them in a set, is it then expressed with an infinite set of finite formulas?

On the other hand, can an infinite set of finite formulas be joined by conjunctions to obtain an equivalent formula of infinite length?

$\endgroup$
  • $\begingroup$ What do "FO formula" mean? Is it first-order logic? $\endgroup$ – D.W. Jun 10 '18 at 19:41
3
$\begingroup$

You are getting at infinitary (first-order) logic. While a well-defined (and natural, and extensively studied) concept, it is quite different from ordinary first-order logic. Before diving into more detail, let me point out the main issue with your suggestion:

There are "infinitely long" expressions which aren't just infinite conjunctions of finite expressions.

That is to say, your idea

Since any formula has an equivalent formula in CNF, if we transform a formula of infinite length to some CNF, and then break the conjunct up into clauses and put them in a set, is it then expressed with an infinite set of finite formulas?

is incorrect. One way to see this is with the compactness theorem. For example, suppose I had a set $\Gamma$ of (finitary) first-order sentences which expressed connectedness. Then consider the expansion of $\Gamma$ to include sentences saying "$c$ is at distance at least $n$ from $d$," for each natural number $n$, where $c$ and $d$ are new constant symbols. By the usual compactness argument, this has a model, but (the reduct of) this model isn't a connected graph; contradiction.

The usual manipulations we perform with finitary formulas don't behave intuitively in general when we look at "infinitary" formulas, and in fact infinitary logic (see below) is a very different beast from its finite counterpart.


Having said what infinitary logic isn't, let me end by saying a couple sentences about what infinitary logic is.

For a start, let's look at the simplest nontrivial example: $\mathcal{L}_{\omega_1,\omega}$. This is smallest class containing all first-order formulas, closed under (a) quantifiers and (b) countably infinite conjunctions and disjunctions. This logic is much stronger than first-order logic - for example, connectedness (in the language of graphs) is definable by an $\mathcal{L}_{\omega_1,\omega}$-formula, namely

$$\forall x,y[\bigvee_{n\in\mathbb{N}}\exists z_1,...,z_n(z_1=x,z_n=y, z_1Ez_2E...Ez_n)].$$ This is a relatively simple infinitary formula, and there are much more complicated ones we can consider; there is a rich (and non-collapsing) hierarchy of infinitary formulas, and in fact many fragments of $\mathcal{L}_{\omega_1,\omega}$ of mathematical interest (see e.g. this paper for a good starting point).

We can go beyond $\mathcal{L}_{\omega_1,\omega}$ by either allowing longer Boolean combinations, or infinitely long blocks of quantifiers, but as we go further up the hierarchy of infinitary logics things get progressively much nastier. $\mathcal{L}_{\omega_1,\omega}$ is quite abstract, but still "concrete" enough to be relevant outside of infinitary logic - see e.g. the notion of a Scott sentence, which is useful in computability theory, classical model theory, and set theory.

There are several texts on infinitary logic; I recommend Marker's recent book as a good starting point, and Barwise's old book for a more in-depth treatment of the "local" flavor.

$\endgroup$
  • $\begingroup$ Thank you. Incredibly helpful! Opened up a whole new world for me! $\endgroup$ – RexYuan Jun 12 '18 at 1:23
1
$\begingroup$

Assuming "FO formula" means a formula in first-order logic (aka a well-formed formula), it's part of the definition that a formula has to be finite. The set of well-formed formulas is defined by induction, and induction can only give you a finite formula. See https://en.wikipedia.org/wiki/First-order_logic#Formulas.


Also: If you had an 'infinite formula' in first-order logic (whatever that means; let's assume it is somehow meaningful) that contained infinitely many variables, as Derek Elkin explains, there might not be a way to translate it to an infinite CNF formula that is equivalent (it's not obvious whether that should be possible, and it would presumably depend on how you defined "infinite formula").

$\endgroup$
  • 1
    $\begingroup$ Presumably it would be translated to an "infinite CNF formula", but again, as you say, the proof that every formula has a CNF equivalent is typically done by induction on the original formula and there's no reason that proof would generalize to "infiinite formulas". As an analogy, while we can use associativity of addition and induction on the number terms in a summation to show that any finite summation can be arbitrarily reassociated, this result does not extend to infinite summations. $\endgroup$ – Derek Elkins Jun 10 '18 at 19:53

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.