1) Note that the existential qualifier ∃ ("there exists") can be constructed from the universal qualifier ∀ ("for all"). If we say that there exists object x that satisfies condition <foo>, it's the same as saying "it's not true that for all x, <foo> is false".
There's a bunch of other redundancies in formal logic, but we allow them because they make our life simpler. For example, equivalence (p ⇔ q) can be also written as (p ⇒ q) ∧ (q ⇒ p), p ∨ q is the same as ¬(¬p ∧ ¬q), and so forth.
2) In the closing section, I noted that first-order logic, axiom systems that talk about infinite mathematical structures can't control the size of their models. The upward part ("model larger than intended") is easy to swallow; more confusingly, ZFC and similar axiom systems can also have infinite models that are "smaller" than intuitively expected. In particular, ZFC can have a model that has "only" a countable infinity of elements -- that's the "size" of the set of natural numbers -- even though ZFC can seemingly prove the existence of sets of higher cardinality, such as the set of real numbers, and operate on them (see https://lcamtuf.substack.com/p/how-has-mathematics-gotten-so-abstract).
This is known as Skolem's paradox. It's not a paradox in a formal sense - all we're saying that there's some countably infinite collection of statements / functions / predicates which produces the same outwardly observable reasoning outcomes with "fewer" parts than what ZFC can internally talk about. That said, it makes philosophers cranky, for obvious reasons.
3) In first-order logic, you have quantifiers ("generalizations") over objects; in second-order logic, you add quantifiers over object properties / predicates. As an example, second-order logic allows you to symbolically express the axiom of induction for natural numbers:
∀A ( ( A(0) ∧ ∀x (A(x) ⇒ A(x+1)) ) ⇒ ∀x A(x) )
Or, in plain language: for any property A, if the property is true for object zero and we can show that that the truth of A(x+1) follows from the truth of A(x), then A(x) must be true for all x.
Second-order logic is powerful enough to avoid the size control problem outlined in the article. Nevertheless, we don't routinely use it because, as noted earlier, strengthening the system's expressive power actually makes it harder to prove many things. Some of the proof techniques rely on the ability to add new terms to a theory without degrading it, and that's not a given in SOL.
4) There are non-standard logic systems that try to address some of the gotchas outlined in the article. For example, they might require p and q in "if p then q" to be "relevantly related" (no "if grass is green then kittens are cute"). Or, they may ditch some reasoning rules - most commonly, the law of the excluded middle (p ∨ ¬p) and double negation (¬¬p ⇔ p) - to prevent explosions on contradiction, at the expense of making more things unprovable. Or, they may have logic values other than "true" and "false". None of that is widely used today.
5) If you want to have some idle fun with first-order logic on a computer, I recommend exploring Prolog. You will never use this for anything practical, but it's a cool language to have some exposure to.
Some postscripts:
1) Note that the existential qualifier ∃ ("there exists") can be constructed from the universal qualifier ∀ ("for all"). If we say that there exists object x that satisfies condition <foo>, it's the same as saying "it's not true that for all x, <foo> is false".
There's a bunch of other redundancies in formal logic, but we allow them because they make our life simpler. For example, equivalence (p ⇔ q) can be also written as (p ⇒ q) ∧ (q ⇒ p), p ∨ q is the same as ¬(¬p ∧ ¬q), and so forth.
2) In the closing section, I noted that first-order logic, axiom systems that talk about infinite mathematical structures can't control the size of their models. The upward part ("model larger than intended") is easy to swallow; more confusingly, ZFC and similar axiom systems can also have infinite models that are "smaller" than intuitively expected. In particular, ZFC can have a model that has "only" a countable infinity of elements -- that's the "size" of the set of natural numbers -- even though ZFC can seemingly prove the existence of sets of higher cardinality, such as the set of real numbers, and operate on them (see https://lcamtuf.substack.com/p/how-has-mathematics-gotten-so-abstract).
This is known as Skolem's paradox. It's not a paradox in a formal sense - all we're saying that there's some countably infinite collection of statements / functions / predicates which produces the same outwardly observable reasoning outcomes with "fewer" parts than what ZFC can internally talk about. That said, it makes philosophers cranky, for obvious reasons.
3) In first-order logic, you have quantifiers ("generalizations") over objects; in second-order logic, you add quantifiers over object properties / predicates. As an example, second-order logic allows you to symbolically express the axiom of induction for natural numbers:
∀A ( ( A(0) ∧ ∀x (A(x) ⇒ A(x+1)) ) ⇒ ∀x A(x) )
Or, in plain language: for any property A, if the property is true for object zero and we can show that that the truth of A(x+1) follows from the truth of A(x), then A(x) must be true for all x.
Second-order logic is powerful enough to avoid the size control problem outlined in the article. Nevertheless, we don't routinely use it because, as noted earlier, strengthening the system's expressive power actually makes it harder to prove many things. Some of the proof techniques rely on the ability to add new terms to a theory without degrading it, and that's not a given in SOL.
4) There are non-standard logic systems that try to address some of the gotchas outlined in the article. For example, they might require p and q in "if p then q" to be "relevantly related" (no "if grass is green then kittens are cute"). Or, they may ditch some reasoning rules - most commonly, the law of the excluded middle (p ∨ ¬p) and double negation (¬¬p ⇔ p) - to prevent explosions on contradiction, at the expense of making more things unprovable. Or, they may have logic values other than "true" and "false". None of that is widely used today.
5) If you want to have some idle fun with first-order logic on a computer, I recommend exploring Prolog. You will never use this for anything practical, but it's a cool language to have some exposure to.
Half-way in, stalled. Semiring-want to puzzle on that.
Great brain stretch for me. Thank you.
Good article, as usual, but my brain hurts now!