Logic - 2021-10-15

3:46 AM

Besides ZFC2, are there any other interesting examples of non-categorical but quasi-categorical theories?

4:37 AM

@Amr Elementary function arithmetic (EFA) contains Robinson arithmetic (Q), which can already represent all computable functions (see here).

user76284

4:49 AM

@Amr You might be interested in these:
https://en.wikipedia.org/wiki/Hereditarily_finite_set#Theories_of_finite_sets
https://en.wikipedia.org/wiki/Finitist_set_theory

user21820

6:22 AM

@Amr You need to click the "reply" button or have the ":" in front of the message id otherwise it won't link to the message you're replying to.

@Amr Strict finitism wouldn't even like EFA, because although EFA doesn't have induction it has exponentiation, which might be argued to go beyond the means of finitist representation. You see, if we use binary, addition and multiplication are polynomial-time algorithms (with polynomial-size outputs), so they can be carried out 'within reasonable physical means'. Exponentiation goes beyond that.

user21820

6:37 AM

Since exponentiation is definable over PA, strict finitism necessarily must be formalized by a system weaker than PA.

There are multiple possible options. The most obvious safe option is PA−. PA− is strong enough to prove simple stuff, enough that it can reason about finite program execution (which is called "can reason about programs" in this post). PA− can even prove facts of number theory up to any explicit bound such that the ∃-witnesses are polynomially bounded.

user21820

6:56 AM

But PA− cannot prove many generalized (unbounded) simple facts of number theory. That is why people look for fragments of PA that are in-between PA− and full PA. The natural hierarchy is of course the induction hierarchy, where Σ[n]-induction means induction for (universal closures of) Σ[n]-formulae. Σ1-induction almost always suffices for practical applications of mathematics. Relevant are these comments:

in Discussion on answer by Noah Schweber: If the universe is finite does that nullify Godel's incompleteness, halting problem, and Church-Turing thesis?, Oct 4 at 15:59, by user21820

@JKusin: A huge amount of technology is built on science and mathematics that could be said to rely on the correctness of PA at least at human scales. I mentioned HTTPS in the linked post. The very fact that you can read this website right now relies on RSA encryption (as stated in the certificate), which relies on Fermat's little theorem, which can be cleanly stated and proven in a weak system called ACA0 that is essentially no stronger than PA. PA is PA− plus induction. So PA/ACA0 is very useful for applied mathematics.

in Discussion on answer by Noah Schweber: If the universe is finite does that nullify Godel's incompleteness, halting problem, and Church-Turing thesis?, Oct 4 at 15:59, by Noah Schweber

@user21820 To be fair, PA is galactic overkill there. I'm not aware of any even superficial need to go beyond, say, ISigma2 (or even ISigma1 for that matter).

user21820

7:36 AM

IΣ[n] means PA− plus Σ[n]-induction. In reverse mathematics, IΣ1 proves exactly the same arithmetical theorems as RCA0. So it can essentially handle all primitive recursive constructions as well as most applied mathematics. But this means that IΣ1 goes way beyond totality of exponentiation, and hence way beyond EFA. So strict finitists would definitely reject IΣ1.

@Amr But let me repeat what I said above; PA− already can reason about finite program execution. There is an arithmetical property R such that ( PA− ⊢ R(p,i,o) ) if p halts on input i and outputs o, and ( PA− ⊢ ¬R(p,i,o) ) if p halts on input i but does not output o. Define H(p,i) ≡ ∃o ( R(p,i,o) ). Then ( PA− ⊢ H(p,i) ) if p halts on input i. PA− may be unable to prove non-halting, but it can prove truly halting behaviour. So both PRA and EFA also can.

user21820

7:54 AM

This fact that I just stated is called Σ1-completeness of PA−, meaning that PA− proves every true Σ1-sentence. Obviously, one cannot prove this fact without using induction... So to even believe this fact you have to believe Σ1-induction. Heheheh...

user21820

8:26 AM

@Amr As for proof-theoretic ordinal of a theory T that interprets PA−, roughly speaking it is the supremum of all ordinals k such that there is some computable well-ordering W (given by a program) that T proves transfinite induction along W. This is a bit beyond me, as I never got around to learning the technical details, and there are tons of details and differing definitions floating around the internet.

One supposedly excellent reference is Michael Rathjen's "Proof Theory", but it strangely only asks for transfinite induction along W for quantifier-free predicates, and I have no idea why.

user21820

8:58 AM

This post mentions some possible choices for the complexity of the predicate, but I have no idea why the author of the PDF I mentioned didn't just go with "elementary computable predicate", since he did in another PDF. Maybe it's so that weak fragments of PA won't be given an artificial penalty in being unable to prove TI(k) for small ordinal k.

@Lereau I've left a comment there, but I do think your explanations were a bit unclear. That said, I do not understand the downvotes, unless they are related to the fact that the question is too unclear as to be opinion-based. I also do not understand why the vast majority of logic-untrained people do not get that proof by contrapositive ( ¬B⇒¬A ⊢ A⇒B ) is just as bad as genuine proof by contradiction ( ¬B⇒⊥ ⊢ B ). They appear to believe they understand proofs by contrapositive, but no...

user21820

9:30 AM

@user76284 Hmm what in the first place is the generalization for "quasi-categorical"? Also, this talk has some interesting bits, such as the admission at the very end that categoricity is actually philosophically contrary to reflection.

It's like with categoricity of PA2, which fails to pin down ℕ because it only guarantees categoricity with respect to the intended model of the meta-system. Similarly, categoricity of the second-order axiomatization of ℝ fails to pin down ℝ except with respect to the 'intended model' of the meta-system (e.g. Z set theory). This is actually worse (hence the scare-quotes), since there is no non-circular description of an intended model of Z.

Lereau

9:58 AM

@user21820 @user21820 Thanks for leaving a comment! At some point I was really confused about the downvotes. Do you think my last edit has clarified it enough or should I add more?

user21820

@Lereau I saw it after your edit, but I think it's still unclear. You've to remember that the vast majority of people on Math SE, including the professors, don't actually know basic logic. Most of them get by via unconscious logical reasoning; they are in the 1% of the population who manage to unconsciously grasp enough to not make obvious mathematical errors, but probe a bit and you will find lots of problems (e.g. uncertainty whether they used AC or not, ...).

Lereau

@user21820 @user21820 Yeah I guess that's right. Guess I should just use some De Morgan equivalences to show that $\neg B \to \neg A$ is equivalent to $\neg (A \land \neg B)$.

user21820

Anyway, I had already upvoted your answer because technically there is nothing wrong! Probably unrelated, but I have also gotten quite a number of recent downvotes on my posts related to logic, such as here and here and here and here. The last two were even downvoted together, so likely a troll.

Joe

10:15 AM

@user21820: Could you please explain why proof by contrapositive is as bad as genuine proof by contradiction?

user21820

@Joe In that same message where I said they are just as bad, I gave the precise form of those two rules. They are equivalent over intuitionistic logic IL (whether propositional or first-order).

Joe

@user21820: Sorry, I don't see where you wrote that.

user21820

1 hour ago, by user21820

@Lereau I've left a comment there, but I do think your explanations were a bit unclear. That said, I do not understand the downvotes, unless they are related to the fact that the question is too unclear as to be opinion-based. I also do not understand why the vast majority of logic-untrained people do not get that proof by contrapositive ( ¬B⇒¬A ⊢ A⇒B ) is just as bad as genuine proof by contradiction ( ¬B⇒⊥ ⊢ B ). They appear to believe they understand proofs by contrapositive, but no...

The two rules are right there. You can easily derive one from the other over IL.

@Joe: By the way, I don't fault your question for being unclear, precisely because I think you don't know enough to make a clear question out of it. However, it might explain the downvotes on both your question and Lereau's answer, as well as the close-votes. I did not vote at all on question or answer.

Lereau

@user21820 It is not that unrelated I guess. They seem like another case of downvoting with no real feedback / pointing to actual mistakes that could be discussed.

user21820

@Lereau Well, there are some users on Math SE who are actively against logic. I don't want to mention who, but there are at least two.

Sorry I meant to say I didn't vote at all at first, until after Lereau got two inexplicable downvotes, then I upvoted that answer. =)

Lereau

10:31 AM

@user21820 @user21820 Welp, then there is literally no way to reason with them 🤷🏻‍♂️

user21820

@Lereau Exactly. It's a futile endeavour. And I've actually tried a number of times. Most of the time it backfired and wasted my time.

@Joe: Anyway, the misunderstanding you have probably stems from the confusing quoted paragraph:

> If in a proof by contradiction you establish a number of intermediate results A[1..n], then those results are not guaranteed to be valid outside of the contradictory framework you are working in [...]. However, if you give a direct proof of ¬Q→¬P, then any intermediate results you establish along the way are valid. By phrasing the proof by contrapositive as a proof by contradiction, you are at risk of misleading the reader.

This is confusing at best and wrong at worst.

A good proof by contradiction of (P⇒Q) would be of the form:

If P:
  ...
  If ¬Q:
    ...
    ⊥.
  Q.

Anything you do in the first "..." may very well be constructive/intuitionistic/whatever, and remain valid outside the "proof by contradiction". Furthermore, it would be quite wrong to presume that what you do in the second "..." is 'poorer', because each statement A under "¬Q" directly yields "¬Q⇒A" at the same level as the first "..."!

So what's the difference between this and a proof of (¬Q⇒¬P)? None, really. Any real-life example is likely to be so deeply intertwined with classical logic (including most of classical real analysis) that it would be silly to ask whether some proof of some standard real analysis theorem is better expressed using proof by contrapositive or proof by contradiction.

The very construction of a subset of ℝ to which we apply the completeness axiom already presupposes classical FOL quite severely.

user21820

10:54 AM

@Joe: To put it in other words, the so-called "risk of misleading the reader" in the quoted paragraph is actually a strawman. Obviously, if the reader is incapable of doing basic FOL, they can be misled by a proof by contradiction. But so what? They can be misled by many other things too, such as invalid quantifier swap, which show up even in the absence of negation.

user21820

4:28 PM

@Amr: One fun fact that I forgot to mention. The Ackermann function cannot be proven total in IΣ1. The Union-Find algorithm (using both path-compression and height-balancing) is proven to be optimal and has time complexity proportional to the inverse ackermann function... So if you consider this algorithmic problem and its optimal solution to be a practical application, then you would have to accept more than IΣ1!

user21820

4:50 PM

room mode changed to Gallery: anyone may enter, but only approved users can talk

@SimonHenry Actually one should be careful in order to get to $\omega^\omega$ as the ordinal of $\mathsf{PRA}$; I list the ways that I know. 1. The least $\alpha$ (from a canonical ordinal notation system) s.t. $\mathsf{EA}+\Delta_0\text{-}\mathsf{TI}(\alpha)\vdash \mathsf{Con}(\mathsf{PRA})$. 2. The suprema of $\alpha$ s.t. $\mathsf{PRA}$ proves the totality of function $H_\alpha$ from Hardy's hierarchy. 3. The suprema of order types of primitive recursive well-orderings $\prec$ such that $\mathsf{PRA}(f)$ proves that free unary functional symbol $f$ isn't a descending sequence in $\prec$. — Fedor Pakhomov Dec 7 '19 at 9:21

@Amr: The above comment is one of many scattered examples showing the variety of definitions of proof-theoretic ordinals that disagree below ε0. You might want to ask at MO if you want to know more, as I certainly cannot help there. =)

Joe

@user21820: But isn't it the case that in many proofs by contradiction, we need to use both $P$ and $\neg Q$ to reach a contradiction. If we prove $P\land\neg Q\to A_1\to A_2\to\dots\to A_n\to\bot$, then it might well be the case that the statements $A_1,A_2,\dots A_n$ are all false. If instead we prove $\neg Q \to A_1 \to A_2\to\dots\to A_n\to\neg P$, then the statements $A_1,A_2,\dots A_n$ will all hold when $\neg Q$ is true. These results might be useful for proving other theorems.

user21820

@Joe I already answered that in my above explanation here:

6 hours ago, by user21820

Anything you do in the first "..." may very well be constructive/intuitionistic/whatever, and remain valid outside the "proof by contradiction". Furthermore, it would be quite wrong to presume that what you do in the second "..." is 'poorer', because each statement A under "¬Q" directly yields "¬Q⇒A" at the same level as the first "..."!

There is no reason to even claim that we cannot extract exactly the same "useful" stuff from a proof by contradiction that we can from any other proof.

Any illusion that they differ in this respect is actually due to a faulty understanding of FOL reasoning.

Joe

5:06 PM

@user21820: Really? In this answer, Joel David Hamkins argues that proof by contrapositive often yields more information than proof by contradiction does. He's a professor of logic—not someone who would have a faulty understanding of FOL.

user21820

@Joe Did you really believe that I had not read that answer? Nothing in what I said contradicts any of the logic experts, including JDH and Noah Schweber. You are just heavily misunderstanding both me and them.

Amr

Hello everyone, hello user21820 I 'll read your responses in detail soon

user21820

@Amr No problem, take your time.

@Joe: The key lies in the precise structure of the proof outline I gave above.

If you stuff everything in the first "..." into the second "...", then yes you are asking for less information, and that is entirely 'your' fault (generic "you"). But this issue has nothing really to do with the actual logical rules of proof by contrapositive/contradiction!

What many logically untrained people believe to be proof by contradiction/contrapositive can result in what JDH observed. But that is a matter of the execution, not the principle.

user21820

5:44 PM

@Joe: Do you get the point or not? The same issue of less information can arise with a bad proof by contrapositive. A good proof by contrapositive would go:

If ¬Q:
  ...
  If P:
    ...
    ⊥.
  ¬P.

Again, if you stuff everything from the first "..." into the second "...", you would lose information. And again, that would be the fault of the execution, not the principle.

Joe

5:58 PM

@user21820: Yes, I think I understand now. Thanks.

user21820

@Joe You're welcome. Note that even the two possible stuffings I describe above aren't the worst.

The worst is something like:

If ¬(A⇒B):
  ...
  ⊥.

The end result is equivalent to both stuffings, but it's worse this way because doing this literally forces oneself to have no choice but to end up with the least possible information for this subproof.

Joe

@user21820: Yes, I suppose the objection JDH was raising was that it is easy to poorly structure the proof, and put everything under the "If $\neg(A\to B)$" clause when it doesn't need to be. But I now see that you can make that mistake regardless of whether you are proving by contrapositive or contradiction.

user21820

Correct. In fact this issue is well-known in programming, where we want to factor out code where possibly useful for other use.

And it is extremely natural to do the same in a Fitch-style proof in mathematics.

Why then do JDH and other mathematicians observe 'poor proof structure'? Because students don't realize the context-structure in proofs and hence have poor execution of a proof, and can't even easily factor out things.

In a paragraph-style proof, even I would often have some trouble factoring things without mentally rearranging it into the hidden context structure.

Joe

@user21820: So, as a rule of thumb, when trying to prove an implication $P\to Q$, it is best to minimise the amount of working done using the contradictory assumptions $P\land\neg Q$. This applies to both proof by contradiction and proof by contrapositive.

user21820

6:13 PM

@Joe Yes. More generally, move everything to the outermost context possible, unless it is only to be used inside the inner context.

So if you use some cute little lemma that is so ad-hoc that it is useless elsewhere, there is no point putting it in the global context. This in programming (especially defining something as a global when it's only needed inside some procedure) is known as "polluting the global namespace".

But if you want to see what makes a proof really tick, pull everything out as far as it can go.

user76284

11:10 PM

Yes. Coincidentally, I read that right before asking. Hamkins describes categoricity as anti-large cardinal (and anti-reflection) notion. I can intuit why that is.

Regarding the correct generalization for quasi-categorical, I guess something along the lines of: For any two models of the theory, one is isomorphic to an initial segment (?) of the other. (Which means they can only be extended in a "unique direction"?) Or one contains the other in some defined sense. Or perhaps something more general: Any two models have a "join"? Thinking out loud here.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic